let S be non empty non void ManySortedSign ; :: thesis: for A1, A2, B1, B2 being MSAlgebra over 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 over 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 7 :: 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, Th2;
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
.= (Den (o,B2)) . (h9 # x) by A1, A2, A5, A6, Th5 ; :: thesis: verum