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

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

end;

hence o1 = o2 by BINOP_1:2; :: thesis: verum