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

proof

let x, y be Element of Aut G; :: thesis: b1 . (x,y) = b2 . (x,y)
thus b1 . (x,y) = x * y by A2
.= b2 . (x,y) by A3 ; :: thesis: verum

end;

hence b1 = b2 ; :: thesis: verum