let S be non empty non void ManySortedSign ; :: thesis: for A1, A2, B1 being MSAlgebra over S
for B2 being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) & MSAlgebra(# the Sorts of B1, the Charact of B1 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds
for h1 being ManySortedFunction of A1,B1
for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_homomorphism A1,B1 holds
h2 is_homomorphism A2,B2
let A1, A2, B1 be MSAlgebra over S; :: thesis: for B2 being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) & MSAlgebra(# the Sorts of B1, the Charact of B1 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds
for h1 being ManySortedFunction of A1,B1
for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_homomorphism A1,B1 holds
h2 is_homomorphism A2,B2
let B2 be non-empty MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) & MSAlgebra(# the Sorts of B1, the Charact of B1 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) implies for h1 being ManySortedFunction of A1,B1
for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_homomorphism A1,B1 holds
h2 is_homomorphism A2,B2 )
assume A1: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) & MSAlgebra(# the Sorts of B1, the Charact of B1 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) ) ; :: thesis: for h1 being ManySortedFunction of A1,B1
for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_homomorphism A1,B1 holds
h2 is_homomorphism A2,B2
let h1 be ManySortedFunction of A1,B1; :: thesis: for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_homomorphism A1,B1 holds
h2 is_homomorphism A2,B2
let h2 be ManySortedFunction of A2,B2; :: thesis: ( h1 = h2 & h1 is_homomorphism A1,B1 implies h2 is_homomorphism A2,B2 )
assume A2: ( h1 = h2 & h1 is_homomorphism A1,B1 ) ; :: thesis: h2 is_homomorphism A2,B2
let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,A2) = {} or for b₁ being Element of Args (o,A2) holds (h2 . (the_result_sort_of o)) . ((Den (o,A2)) . b₁) = (Den (o,B2)) . (h2 # b₁) )
assume A3: Args (o,A2) <> {} ; :: thesis: for b₁ being Element of Args (o,A2) holds (h2 . (the_result_sort_of o)) . ((Den (o,A2)) . b₁) = (Den (o,B2)) . (h2 # b₁)
let x be Element of Args (o,A2); :: thesis: (h2 . (the_result_sort_of o)) . ((Den (o,A2)) . x) = (Den (o,B2)) . (h2 # x)
reconsider x1 = x as Element of Args (o,A1) by A1;
thus (h2 . (the_result_sort_of o)) . ((Den (o,A2)) . x) = (h1 . (the_result_sort_of o)) . ((Den (o,A1)) . x1) by A1, A2
.= (Den (o,B1)) . (h1 # x1) by A2, A1, A3
.= (Den (o,B2)) . (h2 # x) by A1, A2, A3, INSTALG1:5 ; :: thesis: verum