let b1, b2 be BinOp of (UAAut UA); :: thesis: ( ( for x, y being Element of UAAut UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ) implies b1 = b2 )

assume that

A2: for x, y being Element of UAAut UA holds b1 . (x,y) = y * x and

A3: for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ; :: thesis: b1 = b2

for x, y being Element of UAAut UA holds b1 . (x,y) = b2 . (x,y)

assume that

A2: for x, y being Element of UAAut UA holds b1 . (x,y) = y * x and

A3: for x, y being Element of UAAut UA holds b2 . (x,y) = y * x ; :: thesis: b1 = b2

for x, y being Element of UAAut UA holds b1 . (x,y) = b2 . (x,y)

proof

hence
b1 = b2
by BINOP_1:2; :: thesis: verum
let x, y be Element of UAAut UA; :: thesis: b1 . (x,y) = b2 . (x,y)

thus b1 . (x,y) = y * x by A2

.= b2 . (x,y) by A3 ; :: thesis: verum

end;thus b1 . (x,y) = y * x by A2

.= b2 . (x,y) by A3 ; :: thesis: verum