let S, S' be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for f being Function of the carrier of S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S'
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 of S; :: thesis: for f being Function of the carrier of S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S'
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 S',the carrier of S; :: thesis: for g being Function st f,g form_morphism_between S',S holds
for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S'
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 S',S implies for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S'
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 S',S ; :: thesis: for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S'
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 B be non-empty MSAlgebra of S'; :: thesis: ( B = A | S',f,g implies for s1, s2 being SortSymbol of S'
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 A2: B = A | S',f,g ; :: thesis: for s1, s2 being SortSymbol of S'
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
( dom g = the carrier' of S' & rng g c= the carrier' of S ) by A1, PUA2MSS1:def 13;
then reconsider g = g as Function of the carrier' of S',the carrier' of S by FUNCT_2:def 1, RELSET_1:11;
let s1, s2 be SortSymbol of S'; :: 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 S' such that A3: the_result_sort_of o = s2 and
A4: 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
consider i being Element of NAT , a being Function such that
A5: ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & a in Args o,B & t = transl o,i,a,B ) by A4;
take g . o ; :: according to MSUALG_6:def 5 :: thesis: ( the_result_sort_of (g . o) = f . s2 & ex b₁ being Element of NAT st
( b₁ in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b₁ = f . s1 & ex b₂ being set st
( b₂ in Args (g . o),A & t = transl (g . o),b₁,b₂,A ) ) )
( f * the ResultSort of S' = the ResultSort of S * g & the_result_sort_of (g . o) = the ResultSort of S . (g . o) ) by A1, PUA2MSS1:def 13;
hence the_result_sort_of (g . o) = (f * the ResultSort of S') . o by FUNCT_2:21
.= f . s2 by A3, FUNCT_2:21 ;
:: thesis: ex b₁ being Element of NAT st
( b₁ in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b₁ = f . s1 & ex b₂ being set st
( b₂ in Args (g . o),A & t = transl (g . o),b₁,b₂,A ) )
take i ; :: thesis: ( i in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. i = f . s1 & ex b₁ being set st
( b₁ in Args (g . o),A & t = transl (g . o),i,b₁,A ) )
A6: f * (the_arity_of o) = the_arity_of (g . o) by A1, PUA2MSS1:def 13;
( rng (the_arity_of o) c= the carrier of S' & dom f = the carrier of S' ) by FINSEQ_1:def 4, FUNCT_2:def 1;
hence i in dom (the_arity_of (g . o)) by A5, A6, RELAT_1:46; :: thesis: ( (the_arity_of (g . o)) /. i = f . s1 & ex b₁ being set st
( b₁ in Args (g . o),A & t = transl (g . o),i,b₁,A ) )
hence A7: (the_arity_of (g . o)) /. i = (the_arity_of (g . o)) . i by PARTFUN1:def 8
.= f . ((the_arity_of o) . i) by A5, A6, FUNCT_1:23
.= f . s1 by A5, PARTFUN1:def 8 ;
:: thesis: ex b₁ being set st
( b₁ in Args (g . o),A & t = transl (g . o),i,b₁,A )
take a ; :: thesis: ( a in Args (g . o),A & t = transl (g . o),i,a,A )
thus a in Args (g . o),A by A1, A2, A5, Th25; :: thesis: t = transl (g . o),i,a,A
A8: ( dom (transl (g . o),i,a,A) = the Sorts of A . (f . s1) & dom t = the Sorts of B . s1 ) by A5, A7, MSUALG_6:def 4;
the Sorts of B = the Sorts of A * f by A1, A2, Def3;
then A9: the Sorts of B . s1 = the Sorts of A . (f . s1) by FUNCT_2:21;

now

let x be set ; :: 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 A5, A7, A9, MSUALG_6:def 4;
hence t . x = (transl (g . o),i,a,A) . x by A1, A2, Th24; :: thesis: verum

end;

hence t = transl (g . o),i,a,A by A8, A9, FUNCT_1:9; :: thesis: verum