set S = F1();
set A = F2();
let s1, s2 be SortSymbol of F1(); ( TranslationRel F1() reduces s1,s2 implies for t being Translation of F2(),s1,s2 holds P1[t,s1,s2] )
assume A3:
TranslationRel F1() reduces s1,s2
; for t being Translation of F2(),s1,s2 holds P1[t,s1,s2]
let t be Translation of F2(),s1,s2; P1[t,s1,s2]
consider q being RedSequence of TranslationRel F1(), p being Function-yielding FinSequence such that
A4:
t = compose (p,( the Sorts of F2() . s1))
and
A5:
len q = (len p) + 1
and
A6:
s1 = q . 1
and
A7:
s2 = q . (len q)
and
A8:
for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of F1() st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of F2(),s1,s2
by A3, Def6;
defpred S1[ Nat] means ( $1 in dom p implies ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg $1) & s = q . ($1 + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] ) );
A9:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume that A10:
(
i in dom p implies ex
s being
SortSymbol of
F1() ex
t being
Translation of
F2(),
s1,
s ex
p9 being
Function-yielding FinSequence st
(
p9 = p | (Seg i) &
s = q . (i + 1) &
TranslationRel F1()
reduces s1,
s &
t = compose (
p9,
( the Sorts of F2() . s1)) &
P1[
t,
s1,
s] ) )
and A11:
i + 1
in dom p
;
ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg (i + 1)) & s = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] )
A12:
(i + 1) + 1
in dom q
by A5, A11, FUNCT_7:22;
i + 1
in dom q
by A5, A11, FUNCT_7:22;
then
[(q . (i + 1)),(q . ((i + 1) + 1))] in TranslationRel F1()
by A12, REWRITE1:def 2;
then reconsider v1 =
q . (i + 1),
v2 =
q . ((i + 1) + 1) as
SortSymbol of
F1()
by ZFMISC_1:87;
reconsider f =
p . (i + 1) as
Function ;
A13:
f is_e.translation_of F2(),
v1,
v2
by A8, A11;
then reconsider t =
f as
Translation of
F2(),
v1,
v2 by Th17;
per cases
( i = 0 or i > 0 )
;
suppose A14:
i = 0
;
ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg (i + 1)) & s = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] )then reconsider t =
t as
Translation of
F2(),
s1,
v2 by A6;
reconsider p9 =
p | (Seg 1) as
Function-yielding FinSequence by FINSEQ_1:15;
A15:
t * (id ( the Sorts of F2() . s1)) = t
by FUNCT_2:17;
take
v2
;
ex t being Translation of F2(),s1,v2 ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] )take
t
;
ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] )take
p9
;
( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] )thus
(
p9 = p | (Seg (i + 1)) &
v2 = q . ((i + 1) + 1) )
by A14;
( TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] )thus
TranslationRel F1()
reduces s1,
v2
by A6, A13, A14, Th17;
( t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] )A16:
dom t = the
Sorts of
F2()
. s1
by FUNCT_2:def 1;
1
in Seg 1
by FINSEQ_1:2, TARSKI:def 1;
then A17:
p9 . 1
= t
by A14, FUNCT_1:49;
0 + 1
<= len p
by A11, A14, FINSEQ_3:25;
then
len p9 = 1
by FINSEQ_1:17;
then
p9 = <*t*>
by A17, FINSEQ_1:40;
hence
t = compose (
p9,
( the Sorts of F2() . s1))
by A16, FUNCT_7:46;
P1[t,s1,v2]A18:
TranslationRel F1()
reduces s1,
s1
by REWRITE1:12;
A19:
P1[
id ( the Sorts of F2() . s1),
s1,
s1]
by A1;
id ( the Sorts of F2() . s1) is
Translation of
F2(),
s1,
s1
by Th16;
hence
P1[
t,
s1,
v2]
by A2, A6, A8, A11, A14, A18, A15, A19;
verum end; suppose A20:
i > 0
;
ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg (i + 1)) & s = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] )reconsider pp =
p | (Seg (i + 1)) as
FinSequence by FINSEQ_1:15;
take
v2
;
ex t being Translation of F2(),s1,v2 ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] )A21:
i + 1
<= len p
by A11, FINSEQ_3:25;
then A22:
i <= len p
by NAT_1:13;
i >= 0 + 1
by A20, NAT_1:13;
then consider s being
SortSymbol of
F1(),
t9 being
Translation of
F2(),
s1,
s,
p9 being
Function-yielding FinSequence such that A23:
p9 = p | (Seg i)
and A24:
s = q . (i + 1)
and A25:
TranslationRel F1()
reduces s1,
s
and A26:
t9 = compose (
p9,
( the Sorts of F2() . s1))
and A27:
P1[
t9,
s1,
s]
by A10, A22, FINSEQ_3:25;
reconsider T =
t * t9 as
Translation of
F2(),
s1,
v2 by A8, A11, A24, A25, Th19;
take
T
;
ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & T = compose (p9,( the Sorts of F2() . s1)) & P1[T,s1,v2] )take y =
p9 ^ <*f*>;
( y = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & T = compose (y,( the Sorts of F2() . s1)) & P1[T,s1,v2] )
i <= len p
by A21, NAT_1:13;
then A28:
len p9 = i
by A23, FINSEQ_1:17;
i + 1
<= len p
by A11, FINSEQ_3:25;
then A29:
dom pp = Seg (i + 1)
by FINSEQ_1:17;
len <*f*> = 1
by FINSEQ_1:40;
then
len y = (len p9) + 1
by FINSEQ_1:22;
then
dom y = Seg (i + 1)
by A28, FINSEQ_1:def 3;
hence
y = p | (Seg (i + 1))
by A29, A30;
( v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & T = compose (y,( the Sorts of F2() . s1)) & P1[T,s1,v2] )thus
v2 = q . ((i + 1) + 1)
;
( TranslationRel F1() reduces s1,v2 & T = compose (y,( the Sorts of F2() . s1)) & P1[T,s1,v2] )
TranslationRel F1()
reduces v1,
v2
by A13, Th17;
hence
TranslationRel F1()
reduces s1,
v2
by A24, A25, REWRITE1:16;
( T = compose (y,( the Sorts of F2() . s1)) & P1[T,s1,v2] )thus
T = compose (
y,
( the Sorts of F2() . s1))
by A26, FUNCT_7:41;
P1[T,s1,v2]thus
P1[
T,
s1,
v2]
by A2, A8, A11, A24, A25, A27;
verum end; end;
end;
A32:
S1[ 0 ]
by FINSEQ_3:25;
A33:
for i being Nat holds S1[i]
from NAT_1:sch 2(A32, A9);
per cases
( p = {} or p <> {} )
;
suppose
p <> {}
;
P1[t,s1,s2]then
len p >= 0 + 1
by NAT_1:13;
then A36:
len p in dom p
by FINSEQ_3:25;
A37:
p | (dom p) = p
;
dom p = Seg (len p)
by FINSEQ_1:def 3;
then
ex
s being
SortSymbol of
F1() ex
t being
Translation of
F2(),
s1,
s ex
p9 being
Function-yielding FinSequence st
(
p9 = p &
s = q . ((len p) + 1) &
TranslationRel F1()
reduces s1,
s &
t = compose (
p9,
( the Sorts of F2() . s1)) &
P1[
t,
s1,
s] )
by A33, A36, A37;
hence
P1[
t,
s1,
s2]
by A4, A5, A7;
verum end; end;