theorem Th34:
for
S,
S9 being non
empty non
void ManySortedSign for
A1,
A2 being
MSAlgebra over
S st 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
for
f being
Function of the
carrier of
S9, the
carrier of
S for
g being
Function st
f,
g form_morphism_between S9,
S holds
ex
h9 being
ManySortedFunction of
(A1 | (S9,f,g)),
(A2 | (S9,f,g)) st
(
h9 = h * f &
h9 is_homomorphism A1 | (
S9,
f,
g),
A2 | (
S9,
f,
g) )