let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being non-empty MSAlgebra over 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 over 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) ) ) ;
consider i being Element of NAT , a being Function such that
A4: i in dom (the_arity_of o) and
A5: (the_arity_of o) /. i = s1 and
A6: a in Args (o,A1) and
A7: t = transl (o,i,a,A1) by A3;
reconsider a = a as Element of Args (o,A1) by A6;
reconsider T = transl (o,i,(h # a),A2) as Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) by A2, A5, 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, A5; :: thesis: T * (h . s1) = (h . s2) * t
thus T * (h . s1) = (h . s2) * t by A1, A2, A4, A5, A7, Th21; :: thesis: verum