let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 & TranslationRel S reduces s2,s3 holds
for t1 being Translation of A,s1,s2
for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3
let A be non-empty MSAlgebra over S; :: thesis: for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 & TranslationRel S reduces s2,s3 holds
for t1 being Translation of A,s1,s2
for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3
let s1, s2, s3 be SortSymbol of S; :: thesis: ( TranslationRel S reduces s1,s2 & TranslationRel S reduces s2,s3 implies for t1 being Translation of A,s1,s2
for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3 )
assume that
A1: TranslationRel S reduces s1,s2 and
A2: TranslationRel S reduces s2,s3 ; :: thesis: for t1 being Translation of A,s1,s2
for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3
let t1 be Translation of A,s1,s2; :: thesis: for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3
let t2 be Translation of A,s2,s3; :: thesis: t2 * t1 is Translation of A,s1,s3
thus TranslationRel S reduces s1,s3 by A1, A2, REWRITE1:16; :: according to MSUALG_6:def 6 :: thesis: ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st
( t2 * t1 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s3 = 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 ) )
consider q1 being RedSequence of TranslationRel S, p1 being Function-yielding FinSequence such that
A3: t1 = compose (p1,( the Sorts of A . s1)) and
A4: len q1 = (len p1) + 1 and
A5: s1 = q1 . 1 and
A6: s2 = q1 . (len q1) and
A7: for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p1 & f = p1 . i & s1 = q1 . i & s2 = q1 . (i + 1) holds
f is_e.translation_of A,s1,s2 by A1, Def6;
consider q2 being RedSequence of TranslationRel S, p2 being Function-yielding FinSequence such that
A8: t2 = compose (p2,( the Sorts of A . s2)) and
A9: len q2 = (len p2) + 1 and
A10: s2 = q2 . 1 and
A11: s3 = q2 . (len q2) and
A12: for i being Element of NAT
for f being Function
for s1, s2 being SortSymbol of S st i in dom p2 & f = p2 . i & s1 = q2 . i & s2 = q2 . (i + 1) holds
f is_e.translation_of A,s1,s2 by A2, Def6;
reconsider q = q1 $^ q2 as RedSequence of TranslationRel S by A6, A10, REWRITE1:8;
take q ; :: thesis: ex p being Function-yielding FinSequence st
( t2 * t1 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s3 = 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 ) )
take p = p1 ^ p2; :: thesis: ( t2 * t1 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s3 = 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 ) )
rng t1 c= the Sorts of A . s2 by RELAT_1:def 19;
hence t2 * t1 = compose (p,( the Sorts of A . s1)) by A3, A8, FUNCT_7:48; :: thesis: ( len q = (len p) + 1 & s1 = q . 1 & s3 = 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 ) )
A13: len p = (len p1) + (len p2) by FINSEQ_1:22;
consider x2 being object , r2 being FinSequence such that
A14: q2 = <*x2*> ^ r2 and
len q2 = (len r2) + 1 by REWRITE1:5;
A15: x2 = s2 by A10, A14, FINSEQ_1:41;
consider r1 being FinSequence, x1 being object such that
A16: q1 = r1 ^ <*x1*> by FINSEQ_1:46;
A17: q = r1 ^ q2 by A16, REWRITE1:2;
len <*x1*> = 1 by FINSEQ_1:40;
then A18: len q1 = (len r1) + 1 by A16, FINSEQ_1:22;
then A19: len q = (len p1) + (len q2) by A4, A17, FINSEQ_1:22;
hence len q = (len p) + 1 by A9, A13; :: thesis: ( s1 = q . 1 & s3 = 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 ) )
x1 = s2 by A6, A16, A18, FINSEQ_1:42;
then A20: q = q1 ^ r2 by A16, A14, A17, A15, FINSEQ_1:32;
( 1 <= len r1 or 0 + 1 > len r1 ) ;
then ( ( 1 in Seg (len r1) & Seg (len r1) = dom r1 ) or ( 0 <= len r1 & 0 >= len r1 ) ) by FINSEQ_1:1, FINSEQ_1:def 3, NAT_1:13;
then A21: ( ( q . 1 = r1 . 1 & r1 . 1 = q1 . 1 ) or ( r1 = {} & {} ^ q2 = q2 ) ) by A16, A17, FINSEQ_1:34, FINSEQ_1:def 7;
thus s1 = q . 1 by A5, A6, A10, A16, A18, A21, REWRITE1:2; :: thesis: ( s3 = 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 ) )
len q2 in dom q2 by FINSEQ_5:6;
hence s3 = q . (len q) by A4, A11, A18, A17, A19, FINSEQ_1:def 7; :: thesis: 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
let i be Element of NAT ; :: thesis: 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
let f be Function; :: thesis: 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
let s1, s2 be SortSymbol of S; :: thesis: ( i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 )
assume that
A22: i in dom p and
A23: f = p . i and
A24: s1 = q . i and
A25: s2 = q . (i + 1) ; :: thesis: f is_e.translation_of A,s1,s2

per cases ( i in dom p1 or not i in dom p1 ) ;

suppose A26: i in dom p1 ; :: thesis: f is_e.translation_of A,s1,s2

then i + 1 in dom q1 by A4, FUNCT_7:22;
then A27: s2 = q1 . (i + 1) by A20, A25, FINSEQ_1:def 7;
i in dom q1 by A4, A26, FUNCT_7:22;
then A28: s1 = q1 . i by A20, A24, FINSEQ_1:def 7;
f = p1 . i by A23, A26, FINSEQ_1:def 7;
hence f is_e.translation_of A,s1,s2 by A7, A26, A28, A27; :: thesis: verum

end;

suppose not i in dom p1 ; :: thesis: f is_e.translation_of A,s1,s2

then ( not i <= len p1 or not i >= 1 ) by FINSEQ_3:25;
then i >= (len p1) + 1 by A22, FINSEQ_3:25, NAT_1:13;
then consider k being Nat such that
A29: i = ((len p1) + 1) + k by NAT_1:10;
A30: (len p1) + ((k + 1) + 1) = i + 1 by A29;
A31: k + 1 >= 1 by NAT_1:11;
A32: i = (len p1) + (1 + k) by A29;
i <= len p by A22, FINSEQ_3:25;
then k + 1 <= len p2 by A13, A32, XREAL_1:6;
then A33: k + 1 in dom p2 by A31, FINSEQ_3:25;
then k + 1 in dom q2 by A9, FUNCT_7:22;
then A34: s1 = q2 . (k + 1) by A4, A18, A17, A24, A32, FINSEQ_1:def 7;
(k + 1) + 1 in dom q2 by A9, A33, FUNCT_7:22;
then A35: s2 = q2 . ((k + 1) + 1) by A4, A18, A17, A25, A30, FINSEQ_1:def 7;
f = p2 . (k + 1) by A23, A32, A33, FINSEQ_1:def 7;
hence f is_e.translation_of A,s1,s2 by A12, A33, A34, A35; :: thesis: verum

end;

end;