let f1, f2 be BinOp of REAL; ( ( for x, y being Real holds f1 . (x,y) = max (x,y) ) & ( for x, y being Real holds f2 . (x,y) = max (x,y) ) implies f1 = f2 )
assume that
A5:
for x, y being Real holds f1 . (x,y) = max (x,y)
and
A6:
for x, y being Real holds f2 . (x,y) = max (x,y)
; f1 = f2
for x, y being Element of REAL holds f1 . (x,y) = f2 . (x,y)
hence
f1 = f2
by BINOP_1:2; verum