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 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of ,B1 st
( h' = h & h' 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 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of ,B1 st
( h' = h & h' 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 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of ,B1 st
( h' = h & h' is_homomorphism B1,B2 )
let h be ManySortedFunction of ,A1; :: thesis: ( h is_homomorphism A1,A2 implies ex h' being ManySortedFunction of ,B1 st
( h' = h & h' is_homomorphism B1,B2 ) )
assume A4: h is_homomorphism A1,A2 ; :: thesis: ex h' being ManySortedFunction of ,B1 st
( h' = h & h' is_homomorphism B1,B2 )
reconsider h' = h as ManySortedFunction of ,B1 by A1, A2;
take h' ; :: thesis: ( h' = h & h' is_homomorphism B1,B2 )
thus h' = h ; :: thesis: h' is_homomorphism B1,B2
let o be OperSymbol of ; :: according to MSUALG_3:def 9 :: thesis: ( Args o,B1 = {} or for b₁ being Element of Args o,B1 holds (h' . (the_result_sort_of o)) . ((Den o,B1) . b₁) = (Den o,B2) . (h' # b₁) )
assume A5: Args o,B1 <> {} ; :: thesis: for b₁ being Element of Args o,B1 holds (h' . (the_result_sort_of o)) . ((Den o,B1) . b₁) = (Den o,B2) . (h' # b₁)
then A6: Args o,B2 <> {} by A1, A2, A3, Th3;
let x be Element of Args o,B1; :: thesis: (h' . (the_result_sort_of o)) . ((Den o,B1) . x) = (Den o,B2) . (h' # x)
reconsider y = x as Element of Args o,A1 by A1;
thus (h' . (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) . (h' # x) by A1, A2, A5, A6, Th6 ; :: thesis: verum