let o1, o2 be BinOp of REAL; ( ( for a, b being Real holds o1 . (a,b) = F1(a,b) ) & ( for a, b being Real holds o2 . (a,b) = F1(a,b) ) implies o1 = o2 )
assume that
A1:
for a, b being Real holds o1 . (a,b) = F1(a,b)
and
A2:
for a, b being Real holds o2 . (a,b) = F1(a,b)
; o1 = o2
hence
o1 = o2
; verum