let F1, F2 be BinOp of (carr (x,o)); :: thesis: ( ( for a, b being Element of carr (x,o) holds F1 . (a,b) = addR (a,b) ) & ( for a, b being Element of carr (x,o) holds F2 . (a,b) = addR (a,b) ) implies F1 = F2 )
assume that
A2: for a, b being Element of carr (x,o) holds F1 . (a,b) = addR (a,b) and
A3: for a, b being Element of carr (x,o) holds F2 . (a,b) = addR (a,b) ; :: thesis: F1 = F2

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

let a, b be Element of carr (x,o); :: thesis: F1 . (a,b) = F2 . (a,b)
thus F1 . (a,b) = addR (a,b) by A2
.= F2 . (a,b) by A3 ; :: thesis: verum

end;

hence F1 = F2 by BINOP_1:2; :: thesis: verum