let S be non empty non void ManySortedSign ; :: thesis: for A being feasible MSAlgebra over S
for s1, s2 being SortSymbol of S
for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( 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 ) holds
( 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 <> {} ) ) )
let A be feasible MSAlgebra over S; :: thesis: for s1, s2 being SortSymbol of S
for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( 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 ) holds
( 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 <> {} ) ) )
let s1, s2 be SortSymbol of S; :: thesis: for q being RedSequence of TranslationRel S
for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( 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 ) holds
( 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 <> {} ) ) )
let q be RedSequence of TranslationRel S; :: thesis: for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( 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 ) holds
( 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 <> {} ) ) )
let p be Function-yielding FinSequence; :: thesis: ( len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( 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 ) implies ( 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 <> {} ) ) ) )
assume that
A1: len q = (len p) + 1 and
A2: s1 = q . 1 and
A3: s2 = q . (len q) and
A4: 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: ( 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 <> {} ) ) )

per cases ( p = {} or p <> {} ) ;

suppose A5: p = {} ; :: thesis: ( 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 <> {} ) ) )

then A6: len p = 0 ;
compose (p,( the Sorts of A . s1)) = id ( the Sorts of A . s1) by A5, FUNCT_7:39;
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, A2, A3, A6; :: thesis: verum

end;

suppose p <> {} ; :: thesis: ( 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 <> {} ) ) )

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

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
( i in dom pp implies not pp . i is empty ) and
A16: i + 1 in dom pp ; :: thesis: not pp . (i + 1) is empty
A17: i <= i + 1 by NAT_1:11;
i + 1 <= len pp by A16, FINSEQ_3:25;
then A18: i <= len pp by A17, XXREAL_0:2;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: not pp . (i + 1) is empty

hence not pp . (i + 1) is empty by A14, A12, A16; :: thesis: verum

end;

suppose i > 0 ; :: thesis: not pp . (i + 1) is empty

then i >= 0 + 1 by NAT_1:13;
then A19: i in dom pp by A18, FINSEQ_3:25;
then [(q . i),(q . (i + 1))] in TranslationRel S by A10, A13, A16, REWRITE1:def 2;
then reconsider s1 = q . i, s2 = q . (i + 1) as SortSymbol of S by ZFMISC_1:87;
reconsider f = p . i as Function ;
i in dom p by A1, A11, A16, A19, FUNCT_7:22;
then A20: f is_e.translation_of A,s1,s2 by A4;
pp . (i + 1) = the Sorts of A . s2 by A12, A16;
hence not pp . (i + 1) is empty by A20, Th11; :: thesis: verum

end;

end;

end;

A21: S₁[ 0 ] by FINSEQ_3:25;
A22: for i being Nat holds S₁[i] from NAT_1:sch 2(A21, A15);
A23: pp is non-empty by A22;
A24: dom pp = Seg (len q) by A11, FINSEQ_1:def 3;
reconsider pp = pp as non-empty non empty FinSequence by A11, A23;
A25: dom p = Seg (len p) by FINSEQ_1:def 3;
p is FuncSequence of pp

proof

thus (len p) + 1 = len pp by A1, A11; :: according to FUNCT_7:def 10 :: thesis: for b₁ being set holds
( not b₁ in dom p or p . b₁ in K93((pp . b₁),(pp . (b₁ + 1))) )
let j be Nat; :: thesis: ( not j in dom p or p . j in K93((pp . j),(pp . (j + 1))) )
reconsider f = p . j as Function ;
assume A26: j in dom p ; :: thesis: p . j in K93((pp . j),(pp . (j + 1)))
then A27: j >= 1 by A25, FINSEQ_1:1;
then A28: j + 1 >= 1 by NAT_1:13;
A29: j <= len p by A25, A26, FINSEQ_1:1;
then j <= len q by A1, NAT_1:13;
then A30: j in Seg (len q) by A27, FINSEQ_1:1;
j + 1 <= len q by A1, A29, XREAL_1:6;
then A31: j + 1 in Seg (len q) by A28, FINSEQ_1:1;
then [(q . j),(q . (j + 1))] in TranslationRel S by A10, A30, REWRITE1:def 2;
then reconsider s1 = q . j, s2 = q . (j + 1) as SortSymbol of S by ZFMISC_1:87;
A32: pp . (j + 1) = the Sorts of A . s2 by A12, A24, A31;
A33: f is_e.translation_of A,s1,s2 by A4, A26;
then A34: p . j is Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11;
A35: the Sorts of A . s2 <> {} by A33, Th11;
pp . j = the Sorts of A . s1 by A12, A24, A30;
hence p . j in K93((pp . j),(pp . (j + 1))) by A34, A35, A32, FUNCT_2:8; :: thesis: verum

end;

then reconsider p9 = p as FuncSequence of pp ;
A36: 1 in dom q by FINSEQ_5:6;
then A37: pp . 1 = the Sorts of A . s1 by A2, A10, A12, A13;
then A38: dom (compose (p9,( the Sorts of A . s1))) = the Sorts of A . s1 by FUNCT_7:67;
A39: len q in dom q by FINSEQ_5:6;
then A40: pp . (len pp) = the Sorts of A . s2 by A3, A10, A11, A12, A13;
then rng (compose (p9,( the Sorts of A . s1))) c= the Sorts of A . s2 by A37, FUNCT_7:67;
hence compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) by A10, A11, A13, A39, A40, A38, FUNCT_2:def 1, RELSET_1:4; :: thesis: ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) )
thus ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) by A10, A11, A13, A36, A39, A37, A40; :: thesis: verum

end;

end;