theorem
for
S being non
empty non
void ManySortedSign 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 )