for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for x, y being Element of (MSAEndMonoid U1)
for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f