for U1, U2, U3 being Universal_Algebra st U1,U2 are_similar & U2,U3 are_similar holds
for h1 being Function of U1,U2
for h2 being Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1)