let F1, F2 be BinOp of X; :: thesis: ( ( for a, b being Element of X holds F1 . (a,b) = addemb (f,a,b) ) & ( for a, b being Element of X holds F2 . (a,b) = addemb (f,a,b) ) implies F1 = F2 )
assume that
A2: for a, b being Element of X holds F1 . (a,b) = addemb (f,a,b) and
A3: for a, b being Element of X holds F2 . (a,b) = addemb (f,a,b) ; :: thesis: F1 = F2

now :: thesis: for a, b being Element of X holds F1 . (a,b) = F2 . (a,b)

let a, b be Element of X; :: thesis: F1 . (a,b) = F2 . (a,b)
thus F1 . (a,b) = addemb (f,a,b) by A2
.= F2 . (a,b) by A3 ; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum