let o1, o2 be BinOp of (PFuncs (D,REAL)); ( ( for F1, F2 being Element of PFuncs (D,REAL) holds o1 . (F1,F2) = F1 + F2 ) & ( for F1, F2 being Element of PFuncs (D,REAL) holds o2 . (F1,F2) = F1 + F2 ) implies o1 = o2 )
assume that
A1:
for f1, f2 being Element of PFuncs (D,REAL) holds o1 . (f1,f2) = f1 + f2
and
A2:
for f1, f2 being Element of PFuncs (D,REAL) holds o2 . (f1,f2) = f1 + f2
; o1 = o2
hence
o1 = o2
; verum