let S, S9 be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S

for f being Function of the carrier of S9, the carrier of S

for g being Function st f,g form_morphism_between S9,S holds

for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

let A be non-empty MSAlgebra over S; :: thesis: for f being Function of the carrier of S9, the carrier of S

for g being Function st f,g form_morphism_between S9,S holds

for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

let f be Function of the carrier of S9, the carrier of S; :: thesis: for g being Function st f,g form_morphism_between S9,S holds

for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

let g be Function; :: thesis: ( f,g form_morphism_between S9,S implies for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2 )

assume A1: f,g form_morphism_between S9,S ; :: thesis: for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

A2: ( dom g = the carrier' of S9 & rng g c= the carrier' of S ) by A1;

let B be non-empty MSAlgebra over S9; :: thesis: ( B = A | (S9,f,g) implies for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2 )

assume A3: B = A | (S9,f,g) ; :: thesis: for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

reconsider g = g as Function of the carrier' of S9, the carrier' of S by A2, FUNCT_2:def 1, RELSET_1:4;

let s1, s2 be SortSymbol of S9; :: thesis: for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

let t be Function; :: thesis: ( t is_e.translation_of B,s1,s2 implies t is_e.translation_of A,f . s1,f . s2 )

given o being OperSymbol of S9 such that A4: the_result_sort_of o = s2 and

A5: ex i being Element of NAT st

( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st

( a in Args (o,B) & t = transl (o,i,a,B) ) ) ; :: according to MSUALG_6:def 5 :: thesis: t is_e.translation_of A,f . s1,f . s2

A6: f * (the_arity_of o) = the_arity_of (g . o) by A1;

take g . o ; :: according to MSUALG_6:def 5 :: thesis: ( the_result_sort_of (g . o) = f . s2 & ex b_{1} being Element of NAT st

( b_{1} in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b_{1} = f . s1 & ex b_{2} being set st

( b_{2} in Args ((g . o),A) & t = transl ((g . o),b_{1},b_{2},A) ) ) )

f * the ResultSort of S9 = the ResultSort of S * g by A1;

hence the_result_sort_of (g . o) = (f * the ResultSort of S9) . o by FUNCT_2:15

.= f . s2 by A4, FUNCT_2:15 ;

:: thesis: ex b_{1} being Element of NAT st

( b_{1} in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b_{1} = f . s1 & ex b_{2} being set st

( b_{2} in Args ((g . o),A) & t = transl ((g . o),b_{1},b_{2},A) ) )

consider i being Element of NAT , a being Function such that

A7: i in dom (the_arity_of o) and

A8: (the_arity_of o) /. i = s1 and

A9: a in Args (o,B) and

A10: t = transl (o,i,a,B) by A5;

take i ; :: thesis: ( i in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. i = f . s1 & ex b_{1} being set st

( b_{1} in Args ((g . o),A) & t = transl ((g . o),i,b_{1},A) ) )

( rng (the_arity_of o) c= the carrier of S9 & dom f = the carrier of S9 ) by FINSEQ_1:def 4, FUNCT_2:def 1;

hence i in dom (the_arity_of (g . o)) by A7, A6, RELAT_1:27; :: thesis: ( (the_arity_of (g . o)) /. i = f . s1 & ex b_{1} being set st

( b_{1} in Args ((g . o),A) & t = transl ((g . o),i,b_{1},A) ) )

hence A11: (the_arity_of (g . o)) /. i = (the_arity_of (g . o)) . i by PARTFUN1:def 6

.= f . ((the_arity_of o) . i) by A7, A6, FUNCT_1:13

.= f . s1 by A7, A8, PARTFUN1:def 6 ;

:: thesis: ex b_{1} being set st

( b_{1} in Args ((g . o),A) & t = transl ((g . o),i,b_{1},A) )

then A12: dom (transl ((g . o),i,a,A)) = the Sorts of A . (f . s1) by MSUALG_6:def 4;

A13: the Sorts of B = the Sorts of A * f by A1, A3, Def3;

then A14: the Sorts of B . s1 = the Sorts of A . (f . s1) by FUNCT_2:15;

thus a in Args ((g . o),A) by A1, A3, A9, Th24; :: thesis: t = transl ((g . o),i,a,A)

dom t = the Sorts of B . s1 by A8, A10, MSUALG_6:def 4;

hence t = transl ((g . o),i,a,A) by A12, A13, A15, FUNCT_2:15; :: thesis: verum

for f being Function of the carrier of S9, the carrier of S

for g being Function st f,g form_morphism_between S9,S holds

for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

let A be non-empty MSAlgebra over S; :: thesis: for f being Function of the carrier of S9, the carrier of S

for g being Function st f,g form_morphism_between S9,S holds

for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

let f be Function of the carrier of S9, the carrier of S; :: thesis: for g being Function st f,g form_morphism_between S9,S holds

for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

let g be Function; :: thesis: ( f,g form_morphism_between S9,S implies for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2 )

assume A1: f,g form_morphism_between S9,S ; :: thesis: for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds

for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

A2: ( dom g = the carrier' of S9 & rng g c= the carrier' of S ) by A1;

let B be non-empty MSAlgebra over S9; :: thesis: ( B = A | (S9,f,g) implies for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2 )

assume A3: B = A | (S9,f,g) ; :: thesis: for s1, s2 being SortSymbol of S9

for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

reconsider g = g as Function of the carrier' of S9, the carrier' of S by A2, FUNCT_2:def 1, RELSET_1:4;

let s1, s2 be SortSymbol of S9; :: thesis: for t being Function st t is_e.translation_of B,s1,s2 holds

t is_e.translation_of A,f . s1,f . s2

let t be Function; :: thesis: ( t is_e.translation_of B,s1,s2 implies t is_e.translation_of A,f . s1,f . s2 )

given o being OperSymbol of S9 such that A4: the_result_sort_of o = s2 and

A5: ex i being Element of NAT st

( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st

( a in Args (o,B) & t = transl (o,i,a,B) ) ) ; :: according to MSUALG_6:def 5 :: thesis: t is_e.translation_of A,f . s1,f . s2

A6: f * (the_arity_of o) = the_arity_of (g . o) by A1;

take g . o ; :: according to MSUALG_6:def 5 :: thesis: ( the_result_sort_of (g . o) = f . s2 & ex b

( b

( b

f * the ResultSort of S9 = the ResultSort of S * g by A1;

hence the_result_sort_of (g . o) = (f * the ResultSort of S9) . o by FUNCT_2:15

.= f . s2 by A4, FUNCT_2:15 ;

:: thesis: ex b

( b

( b

consider i being Element of NAT , a being Function such that

A7: i in dom (the_arity_of o) and

A8: (the_arity_of o) /. i = s1 and

A9: a in Args (o,B) and

A10: t = transl (o,i,a,B) by A5;

take i ; :: thesis: ( i in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. i = f . s1 & ex b

( b

( rng (the_arity_of o) c= the carrier of S9 & dom f = the carrier of S9 ) by FINSEQ_1:def 4, FUNCT_2:def 1;

hence i in dom (the_arity_of (g . o)) by A7, A6, RELAT_1:27; :: thesis: ( (the_arity_of (g . o)) /. i = f . s1 & ex b

( b

hence A11: (the_arity_of (g . o)) /. i = (the_arity_of (g . o)) . i by PARTFUN1:def 6

.= f . ((the_arity_of o) . i) by A7, A6, FUNCT_1:13

.= f . s1 by A7, A8, PARTFUN1:def 6 ;

:: thesis: ex b

( b

then A12: dom (transl ((g . o),i,a,A)) = the Sorts of A . (f . s1) by MSUALG_6:def 4;

A13: the Sorts of B = the Sorts of A * f by A1, A3, Def3;

then A14: the Sorts of B . s1 = the Sorts of A . (f . s1) by FUNCT_2:15;

A15: now :: thesis: for x being object st x in the Sorts of B . s1 holds

t . x = (transl ((g . o),i,a,A)) . x

take
a
; :: thesis: ( a in Args ((g . o),A) & t = transl ((g . o),i,a,A) )t . x = (transl ((g . o),i,a,A)) . x

let x be object ; :: thesis: ( x in the Sorts of B . s1 implies t . x = (transl ((g . o),i,a,A)) . x )

assume x in the Sorts of B . s1 ; :: thesis: t . x = (transl ((g . o),i,a,A)) . x

then ( t . x = (Den (o,B)) . (a +* (i,x)) & (transl ((g . o),i,a,A)) . x = (Den ((g . o),A)) . (a +* (i,x)) ) by A8, A10, A11, A14, MSUALG_6:def 4;

hence t . x = (transl ((g . o),i,a,A)) . x by A1, A3, Th23; :: thesis: verum

end;assume x in the Sorts of B . s1 ; :: thesis: t . x = (transl ((g . o),i,a,A)) . x

then ( t . x = (Den (o,B)) . (a +* (i,x)) & (transl ((g . o),i,a,A)) . x = (Den ((g . o),A)) . (a +* (i,x)) ) by A8, A10, A11, A14, MSUALG_6:def 4;

hence t . x = (transl ((g . o),i,a,A)) . x by A1, A3, Th23; :: thesis: verum

thus a in Args ((g . o),A) by A1, A3, A9, Th24; :: thesis: t = transl ((g . o),i,a,A)

dom t = the Sorts of B . s1 by A8, A10, MSUALG_6:def 4;

hence t = transl ((g . o),i,a,A) by A12, A13, A15, FUNCT_2:15; :: thesis: verum