let o1, o2 be BinOp of (PFuncs (D,REAL)); :: thesis: ( ( 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 ; :: thesis: o1 = o2

now :: thesis: for f1, f2 being Element of PFuncs (D,REAL) holds o1 . (f1,f2) = o2 . (f1,f2)

let f1, f2 be Element of PFuncs (D,REAL); :: thesis: o1 . (f1,f2) = o2 . (f1,f2)
o1 . (f1,f2) = f1 + f2 by A1;
hence o1 . (f1,f2) = o2 . (f1,f2) by A2; :: thesis: verum

end;

hence o1 = o2 ; :: thesis: verum