theorem
for
S1,
S2 being non
empty ManySortedSign for
A,
B being
MSAlgebra over
S2 st
MSAlgebra(# the
Sorts of
A, the
Charact of
A #)
= MSAlgebra(# the
Sorts of
B, the
Charact of
B #) holds
for
f,
g being
Function st
f,
g form_morphism_between S1,
S2 holds
A | (
S1,
f,
g)
= B | (
S1,
f,
g)