set S = F₁();
set A = F₂();
let s1, s2 be SortSymbol of F₁(); :: thesis:
assume A3: TranslationRel F₁() reduces s1,s2 ; :: thesis:
let t be Translation of F₂(),s1,s2; :: thesis:
consider q being RedSequence of TranslationRel F₁(), p being Function-yielding FinSequence such that
A4: t = compose (p,( the Sorts of F₂() . 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 F₁() st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of F₂(),s1,s2 by A3, Def6;
defpred S₁[ Nat] means ( $1 in dom p implies ex s being SortSymbol of F₁() ex t being Translation of F₂(),s1,s ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg $1) & s = q . ($1 + 1) & TranslationRel F₁() reduces s1,s & t = compose (p9,( the Sorts of F₂() . s1)) & P₁[t,s1,s] ) );
A9: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume that
A10: ( i in dom p implies ex s being SortSymbol of F₁() ex t being Translation of F₂(),s1,s ex p9 being Function-yielding FinSequence st
( p9 = p | (Seg i) & s = q . (i + 1) & TranslationRel F₁() reduces s1,s & t = compose (p9,( the Sorts of F₂() . s1)) & P₁[t,s1,s] ) ) and
A11: i + 1 in dom p ; :: thesis:
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 F₁() by A12, REWRITE1:def 2;
then reconsider v1 = q . (i + 1), v2 = q . ((i + 1) + 1) as SortSymbol of F₁() by ZFMISC_1:87;
reconsider f = p . (i + 1) as Function ;
A13: f is_e.translation_of F₂(),v1,v2 by A8, A11;
then reconsider t = f as Translation of F₂(),v1,v2 by Th17;

per cases ;

suppose A14: i = 0 ; :: thesis:

then reconsider t = t as Translation of F₂(),s1,v2 by A6;
reconsider p9 = p | (Seg 1) as Function-yielding FinSequence by FINSEQ_1:15;
A15: t * (id ( the Sorts of F₂() . s1)) = t by FUNCT_2:17;
take v2 ; :: thesis:
take t ; :: thesis:
take p9 ; :: thesis:
thus ( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) ) by A14; :: thesis:
thus TranslationRel F₁() reduces s1,v2 by A6, A13, A14, Th17; :: thesis:
A16: dom t = the Sorts of F₂() . 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 F₂() . s1)) by A16, FUNCT_7:46; :: thesis:
A18: TranslationRel F₁() reduces s1,s1 by REWRITE1:12;
A19: P₁[ id ( the Sorts of F₂() . s1),s1,s1] by A1;
id ( the Sorts of F₂() . s1) is Translation of F₂(),s1,s1 by Th16;
hence P₁[t,s1,v2] by A2, A6, A8, A11, A14, A18, A15, A19; :: thesis:

end;

suppose A20: i > 0 ; :: thesis:

reconsider pp = p | (Seg (i + 1)) as FinSequence by FINSEQ_1:15;
take v2 ; :: thesis:
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 F₁(), t9 being Translation of F₂(),s1,s, p9 being Function-yielding FinSequence such that
A23: p9 = p | (Seg i) and
A24: s = q . (i + 1) and
A25: TranslationRel F₁() reduces s1,s and
A26: t9 = compose (p9,( the Sorts of F₂() . s1)) and
A27: P₁[t9,s1,s] by A10, A22, FINSEQ_3:25;
reconsider T = t * t9 as Translation of F₂(),s1,v2 by A8, A11, A24, A25, Th19;
take T ; :: thesis:
take y = p9 ^ <*f*>; :: thesis:
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;

A30: now :: thesis:

let k be Nat; :: thesis:
assume A31: k in Seg (i + 1) ; :: thesis:
then k <= i + 1 by FINSEQ_1:1;
then ( ( k <= i & k >= 1 ) or k = i + 1 ) by A31, FINSEQ_1:1, NAT_1:8;
then ( k in dom p9 or k = i + 1 ) by A28, FINSEQ_3:25;
then ( ( y . k = p9 . k & p9 . k = p . k ) or y . k = p . k ) by A23, A28, FINSEQ_1:42, FINSEQ_1:def 7, FUNCT_1:47;
hence y . k = pp . k by A29, A31, FUNCT_1:47; :: thesis:

end;

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; :: thesis:
thus v2 = q . ((i + 1) + 1) ; :: thesis:
TranslationRel F₁() reduces v1,v2 by A13, Th17;
hence TranslationRel F₁() reduces s1,v2 by A24, A25, REWRITE1:16; :: thesis:
thus T = compose (y,( the Sorts of F₂() . s1)) by A26, FUNCT_7:41; :: thesis:
thus P₁[T,s1,v2] by A2, A8, A11, A24, A25, A27; :: thesis:

end;

end;

end;

A32: S₁[ 0 ] by FINSEQ_3:25;
A33: for i being Nat holds S₁[i] from NAT_1:sch 2(A32, A9);

per cases ;

suppose A34: p = {} ; :: thesis:

then A35: len p = 0 ;
t = id ( the Sorts of F₂() . s1) by A4, A34, FUNCT_7:39;
hence P₁[t,s1,s2] by A1, A5, A6, A7, A35; :: thesis:

end;

suppose p <> {} ; :: thesis:

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 F₁() ex t being Translation of F₂(),s1,s ex p9 being Function-yielding FinSequence st
( p9 = p & s = q . ((len p) + 1) & TranslationRel F₁() reduces s1,s & t = compose (p9,( the Sorts of F₂() . s1)) & P₁[t,s1,s] ) by A33, A36, A37;
hence P₁[t,s1,s2] by A4, A5, A7; :: thesis:

end;

end;