let S be non empty non void ManySortedSign ; :: thesis: for A1, A2, B1, B2 being MSAlgebra of S st MSAlgebra(# the Sorts of A1,the Charact of A1 #) = MSAlgebra(# the Sorts of B1,the Charact of B1 #) & MSAlgebra(# the Sorts of A2,the Charact of A2 #) = MSAlgebra(# the Sorts of B2,the Charact of B2 #) & the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 )
let A1, A2, B1, B2 be MSAlgebra of S; :: thesis: ( MSAlgebra(# the Sorts of A1,the Charact of A1 #) = MSAlgebra(# the Sorts of B1,the Charact of B1 #) & MSAlgebra(# the Sorts of A2,the Charact of A2 #) = MSAlgebra(# the Sorts of B2,the Charact of B2 #) & the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 ) )
assume that
A1: MSAlgebra(# the Sorts of A1,the Charact of A1 #) = MSAlgebra(# the Sorts of B1,the Charact of B1 #) and
A2: MSAlgebra(# the Sorts of A2,the Charact of A2 #) = MSAlgebra(# the Sorts of B2,the Charact of B2 #) and
A3: the Sorts of A1 is_transformable_to the Sorts of A2 ; :: thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 )
let h be ManySortedFunction of A1,A2; :: thesis: ( h is_homomorphism A1,A2 implies ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 ) )
assume A4: h is_homomorphism A1,A2 ; :: thesis: ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 )
reconsider h9 = h as ManySortedFunction of B1,B2 by A1, A2;
take h9 ; :: thesis: ( h9 = h & h9 is_homomorphism B1,B2 )
thus h9 = h ; :: thesis: h9 is_homomorphism B1,B2
let o be OperSymbol of S; :: according to MSUALG_3:def 9 :: thesis: ( Args o,B1 = {} or for b₁ being Element of Args o,B1 holds (h9 . (the_result_sort_of o)) . ((Den o,B1) . b₁) = (Den o,B2) . (h9 # b₁) )
assume A5: Args o,B1 <> {} ; :: thesis: for b₁ being Element of Args o,B1 holds (h9 . (the_result_sort_of o)) . ((Den o,B1) . b₁) = (Den o,B2) . (h9 # b₁)
then A6: Args o,B2 <> {} by A1, A2, A3, Th3;
let x be Element of Args o,B1; :: thesis: (h9 . (the_result_sort_of o)) . ((Den o,B1) . x) = (Den o,B2) . (h9 # x)
reconsider y = x as Element of Args o,A1 by A1;
thus (h9 . (the_result_sort_of o)) . ((Den o,B1) . x) = (h . (the_result_sort_of o)) . ((Den o,A1) . y) by A1
.= (Den o,A2) . (h # y) by A1, A4, A5, MSUALG_3:def 9
.= (Den o,B2) . (h9 # x) by A1, A2, A5, A6, Th6 ; :: thesis: verum