for U1, U2 being Universal_Algebra
for h being Function of U1,U2 st U1,U2 are_similar holds
MSAlg h is ManySortedSet of {0}