let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty MSAlgebra of S; :: thesis:
let s1, s2, s3 be SortSymbol of S; :: thesis:
assume A1: ( TranslationRel S reduces s1,s2 & TranslationRel S reduces s2,s3 ) ; :: thesis:
let t1 be Translation of A,s1,s2; :: thesis:
let t2 be Translation of A,s2,s3; :: thesis:
consider q1 being RedSequence of TranslationRel S, p1 being Function-yielding FinSequence such that
A2: t1 = compose p1,(the Sorts of A . s1) and
A3: ( len q1 = (len p1) + 1 & s1 = q1 . 1 & s2 = q1 . (len q1) ) and
A4: 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
A5: t2 = compose p2,(the Sorts of A . s2) and
A6: ( len q2 = (len p2) + 1 & s2 = q2 . 1 & s3 = q2 . (len q2) ) and
A7: 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 A1, Def6;
thus TranslationRel S reduces s1,s3 by A1, REWRITE1:17; :: according to MSUALG_6:def 6 :: thesis:
consider r1 being FinSequence, x1 being set such that
A8: q1 = r1 ^ <*x1*> by FINSEQ_1:63;
consider x2 being set , r2 being FinSequence such that
A9: ( q2 = <*x2*> ^ r2 & len q2 = (len r2) + 1 ) by REWRITE1:5;
reconsider q = q1 $^ q2 as RedSequence of TranslationRel S by A3, A6, REWRITE1:9;
take q ; :: thesis:
take p = p1 ^ p2; :: thesis:
rng t1 c= the Sorts of A . s2 by RELAT_1:def 19;
hence t2 * t1 = compose p,(the Sorts of A . s1) by A2, A5, FUNCT_7:50; :: thesis:
len <*x1*> = 1 by FINSEQ_1:57;
then A10: len q1 = (len r1) + 1 by A8, FINSEQ_1:35;
then A11: ( q = r1 ^ q2 & len r1 = len p1 ) by A3, A8, REWRITE1:2;
then A12: ( len q = (len p1) + (len q2) & len p = (len p1) + (len p2) ) by FINSEQ_1:35;
hence len q = (len p) + 1 by A6; :: thesis:
( x1 = s2 & x2 = s2 ) by A3, A6, A8, A9, A10, FINSEQ_1:58, FINSEQ_1:59;
then A13: q = q1 ^ r2 by A8, A9, A11, FINSEQ_1:45;
( 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:3, FINSEQ_1:def 3, NAT_1:13;
then X: ( ( q . 1 = r1 . 1 & r1 . 1 = q1 . 1 ) or ( len r1 = 0 & {} ^ q2 = q2 ) ) by A8, A11, FINSEQ_1:47, FINSEQ_1:def 7;
then ( ( q . 1 = r1 . 1 & r1 . 1 = q1 . 1 ) or ( r1 = {} & {} ^ q2 = q2 ) ) ;
hence s1 = q . 1 by A3, A6, A11, X; :: thesis:
len q2 in dom q2 by FINSEQ_5:6;
hence s3 = q . (len q) by A6, A11, A12, FINSEQ_1:def 7; :: thesis:
let i be Element of NAT ; :: thesis:
let f be Function; :: thesis:
let s1, s2 be SortSymbol of S; :: thesis:
assume A14: ( i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) ) ; :: thesis:

per cases ;

suppose A15: i in dom p1 ; :: thesis:

then ( i in dom q1 & i + 1 in dom q1 ) by A3, FUNCT_7:24;
then ( s1 = q1 . i & s2 = q1 . (i + 1) & f = p1 . i ) by A13, A14, A15, FINSEQ_1:def 7;
hence f is_e.translation_of A,s1,s2 by A4, A15; :: thesis:

end;

suppose not i in dom p1 ; :: thesis:

then ( ( not i <= len p1 or not i >= 1 ) & i >= 1 ) by A14, FINSEQ_3:27;
then i >= (len p1) + 1 by NAT_1:13;
then consider k being Nat such that
A16: i = ((len p1) + 1) + k by NAT_1:10;
A17: ( i <= len p & i = (len p1) + (1 + k) ) by A14, A16, FINSEQ_3:27;
then ( k + 1 >= 1 & k + 1 <= len p2 ) by A12, NAT_1:11, XREAL_1:8;
then A18: k + 1 in dom p2 by FINSEQ_3:27;
then ( k + 1 in dom q2 & (k + 1) + 1 in dom q2 & (len p1) + ((k + 1) + 1) = i + 1 ) by A6, A16, FUNCT_7:24;
then ( s1 = q2 . (k + 1) & s2 = q2 . ((k + 1) + 1) & f = p2 . (k + 1) ) by A11, A14, A17, A18, FINSEQ_1:def 7;
hence f is_e.translation_of A,s1,s2 by A7, A18; :: thesis:

end;