let S be non empty non void ManySortedSign ; :: thesis:
let A be feasible MSAlgebra of S; :: thesis:
let s1, s2 be SortSymbol of S; :: thesis:
assume TranslationRel S reduces s1,s2 ; :: thesis:
let q be RedSequence of TranslationRel S; :: thesis:
let p be Function-yielding FinSequence; :: thesis:
assume that
A1: ( len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) ) and
A2: for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds
f is_e.translation_of A,s1,s2 ; :: thesis:

per cases ;

suppose p = {} ; :: thesis:

then ( compose p,(the Sorts of A . s1) = id (the Sorts of A . s1) & len p = 0 ) by FUNCT_7:41;
hence ( compose p,(the Sorts of A . s1) is Function of (the Sorts of A . s1),(the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) by A1; :: thesis:

end;

suppose p <> {} ; :: thesis:

then A4: rng p <> {} ;
then A5: 1 in dom p by FINSEQ_3:34;
reconsider f = p . 1 as Function ;
( 1 in dom q & 1 + 1 in dom q ) by A1, A5, FUNCT_7:24;
then [(q . 1),(q . (1 + 1))] in TranslationRel S by REWRITE1:def 2;
then reconsider q1 = q . 1, q2 = q . (1 + 1) as SortSymbol of S by ZFMISC_1:106;
f is_e.translation_of A,q1,q2 by A2, A4, FINSEQ_3:34;
then A6: ( the Sorts of A . q1 <> {} & the Sorts of A . q2 <> {} ) by Th11;
A7: ( dom q = Seg (len q) & dom p = Seg (len p) ) by FINSEQ_1:def 3;
deffunc H₁( set ) -> set = the Sorts of A . (q . $1);
consider pp being FinSequence such that
A8: len pp = len q and
A9: for i being Nat st i in dom pp holds
pp . i = H₁(i) from FINSEQ_1:sch 2();
A10: dom pp = Seg (len q) by A8, FINSEQ_1:def 3;
A11: ( 1 in dom q & dom pp = Seg (len q) ) by A8, FINSEQ_1:def 3, FINSEQ_5:6;
defpred S₁[ Element of NAT ] means ( $1 in dom pp implies not pp . $1 is empty );
A12: S₁[ 0 ] by FINSEQ_3:27;
A13: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

let i be Element of NAT ; :: thesis:
assume that
( i in dom pp implies not pp . i is empty ) and
A14: i + 1 in dom pp ; :: thesis:
( i <= i + 1 & i + 1 <= len pp ) by A14, FINSEQ_3:27, NAT_1:11;
then A15: i <= len pp by XXREAL_0:2;

per cases ;

suppose i = 0 ; :: thesis:

hence not pp . (i + 1) is empty by A6, A9, A14; :: thesis:

end;

suppose i > 0 ; :: thesis:

then i >= 0 + 1 by NAT_1:13;
then A16: i in dom pp by A15, FINSEQ_3:27;
then A17: i in dom p by A1, A8, A14, FUNCT_7:24;
reconsider f = p . i as Function ;
[(q . i),(q . (i + 1))] in TranslationRel S by A7, A11, A14, A16, REWRITE1:def 2;
then reconsider s1 = q . i, s2 = q . (i + 1) as SortSymbol of S by ZFMISC_1:106;
( f is_e.translation_of A,s1,s2 & pp . (i + 1) = the Sorts of A . s2 ) by A2, A9, A14, A17;
hence not pp . (i + 1) is empty by Th11; :: thesis:

end;

A18: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A12, A13);
A19: pp is non-empty

let x be set ; :: according to FUNCT_1:def 15 :: thesis:
assume x in dom pp ; :: thesis:
hence not pp . x is empty by A18; :: thesis:

end;

[1,(pp . 1)] in pp by A7, A11, FUNCT_1:def 4;
then reconsider pp = pp as non-empty non empty FinSequence by A19;
p is FuncSequence of pp

thus (len p) + 1 = len pp by A1, A8; :: according to FUNCT_7:def 10 :: thesis:
let j be Element of NAT ; :: thesis:
assume A20: j in dom p ; :: thesis:
reconsider f = p . j as Function ;
A21: ( j >= 1 & j <= len p ) by A7, A20, FINSEQ_1:3;
then ( j <= len q & j + 1 <= len q & j + 1 >= 1 ) by A1, NAT_1:13, XREAL_1:8;
then A22: ( j in Seg (len q) & j + 1 in Seg (len q) ) by A21, FINSEQ_1:3;
then [(q . j),(q . (j + 1))] in TranslationRel S by A7, REWRITE1:def 2;
then reconsider s1 = q . j, s2 = q . (j + 1) as SortSymbol of S by ZFMISC_1:106;
set i = j;
( p . j = f & j = j & s1 = q . j & s2 = q . (j + 1) & f is_e.translation_of A,s1,s2 ) by A2, A20;
then A23: ( p . j is Function of (the Sorts of A . s1),(the Sorts of A . s2) & the Sorts of A . s2 <> {} ) by Th11;
( pp . j = the Sorts of A . s1 & pp . (j + 1) = the Sorts of A . s2 ) by A9, A22, A10;
hence p . j in K83((pp . j),(pp . (j + 1))) by A23, FUNCT_2:11; :: thesis:

end;

then reconsider p' = p as FuncSequence of pp ;
( 1 in dom q & len q in dom q ) by FINSEQ_5:6;
then A24: ( pp . 1 = the Sorts of A . s1 & pp . (len pp) = the Sorts of A . s2 & pp . 1 <> {} & pp . (len pp) <> {} ) by A1, A7, A8, A9, A11;
then ( dom (compose p',(the Sorts of A . s1)) = the Sorts of A . s1 & rng (compose p',(the Sorts of A . s1)) c= the Sorts of A . s2 ) by FUNCT_7:69;
hence compose p,(the Sorts of A . s1) is Function of (the Sorts of A . s1),(the Sorts of A . s2) by A24, FUNCT_2:def 1, RELSET_1:11; :: thesis:
thus ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) by A24; :: thesis:

end;