let S be non empty non void ManySortedSign ; 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; 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; ( 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
; 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; 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; t2 * t1 is Translation of A,s1,s3
thus
TranslationRel S reduces s1,s3
by A1, A2, REWRITE1:16; MSUALG_6:def 6 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
; 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; ( 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; ( 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; ( 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; ( 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; 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 ; 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; 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; ( 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)
; 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
;
f is_e.translation_of A,s1,s2then
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;
verum end; suppose
not
i in dom p1
;
f is_e.translation_of A,s1,s2then
( 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;
verum end;