let b1, b2 be BinOp of (MSAEnd U1); :: thesis: ( ( for x, y being Element of MSAEnd U1 holds b1 . x,y = y ** x ) & ( for x, y being Element of MSAEnd U1 holds b2 . x,y = y ** x ) implies b1 = b2 )
assume that
A2: for x, y being Element of MSAEnd U1 holds b1 . x,y = y ** x and
A3: for x, y being Element of MSAEnd U1 holds b2 . x,y = y ** x ; :: thesis: b1 = b2
for x, y being Element of MSAEnd U1 holds b1 . x,y = b2 . x,y

proof

let x, y be Element of MSAEnd U1; :: thesis: b1 . x,y = b2 . x,y
thus b1 . x,y = y ** x by A2
.= b2 . x,y by A3 ; :: thesis: verum

end;

hence b1 = b2 by BINOP_1:2; :: thesis: verum