let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being non-empty MSAlgebra of S
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A1,s1,s2 holds
ex T being Function of the Sorts of A2 . s1,the Sorts of A2 . s2 st
( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t )
let A1, A2 be non-empty MSAlgebra of S; :: thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A1,s1,s2 holds
ex T being Function of the Sorts of A2 . s1,the Sorts of A2 . s2 st
( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t )
let h be ManySortedFunction of A1,A2; :: thesis: ( h is_homomorphism A1,A2 implies for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A1,s1,s2 holds
ex T being Function of the Sorts of A2 . s1,the Sorts of A2 . s2 st
( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) )
assume A1: h is_homomorphism A1,A2 ; :: thesis: for s1, s2 being SortSymbol of S
for t being Function st t is_e.translation_of A1,s1,s2 holds
ex T being Function of the Sorts of A2 . s1,the Sorts of A2 . s2 st
( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t )
let s1, s2 be SortSymbol of S; :: thesis: for t being Function st t is_e.translation_of A1,s1,s2 holds
ex T being Function of the Sorts of A2 . s1,the Sorts of A2 . s2 st
( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t )
let t be Function; :: thesis: ( t is_e.translation_of A1,s1,s2 implies ex T being Function of the Sorts of A2 . s1,the Sorts of A2 . s2 st
( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) )
assume t is_e.translation_of A1,s1,s2 ; :: thesis: ex T being Function of the Sorts of A2 . s1,the Sorts of A2 . s2 st
( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t )
then consider o being OperSymbol of S such that
A2: the_result_sort_of o = s2 and
A3: 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,A1 & t = transl o,i,a,A1 ) ) by Def5;
consider i being Element of NAT , a being Function such that
A4: ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) and
A5: ( a in Args o,A1 & t = transl o,i,a,A1 ) by A3;
reconsider a = a as Element of Args o,A1 by A5;
reconsider T = transl o,i,(h # a),A2 as Function of the Sorts of A2 . s1,the Sorts of A2 . s2 by A2, A4, Th10;
take T ; :: thesis: ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t )
thus T is_e.translation_of A2,s1,s2 by A2, A4, Def5; :: thesis: T * (h . s1) = (h . s2) * t
thus T * (h . s1) = (h . s2) * t by A1, A2, A4, A5, Th21; :: thesis: verum