begin
Lm1:
for U1 being Universal_Algebra holds dom (signature U1) = dom the charact of U1
Lm2:
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for o being OperSymbol of (MSSign U1) holds Den (o,((MSAlg U2) Over (MSSign U1))) is operation of U2
Lm3:
for U1 being Universal_Algebra
for n being Nat st n in dom the charact of U1 holds
n is OperSymbol of (MSSign U1)