let F1, F2 be BinOp of (Funcs (A,REAL)); ( ( for f, g being Element of Funcs (A,REAL) holds F1 . (f,g) = minreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds F2 . (f,g) = minreal .: (f,g) ) implies F1 = F2 )
assume that
A3:
for f, g being Element of Funcs (A,REAL) holds F1 . (f,g) = minreal .: (f,g)
and
A4:
for f, g being Element of Funcs (A,REAL) holds F2 . (f,g) = minreal .: (f,g)
; F1 = F2
hence
F1 = F2
by BINOP_1:2; verum