let b1, b2 be BinOp of (MSAAut U1); ( ( for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAAut U1 holds b2 . (x,y) = y ** x ) implies b1 = b2 )
assume that
A2:
for x, y being Element of MSAAut U1 holds b1 . (x,y) = y ** x
and
A3:
for x, y being Element of MSAAut U1 holds b2 . (x,y) = y ** x
; b1 = b2
for x, y being Element of MSAAut U1 holds b1 . (x,y) = b2 . (x,y)
hence
b1 = b2
by BINOP_1:2; verum