deffunc H₁( Element of PFuncs (D,REAL), Element of PFuncs (D,REAL)) -> Element of PFuncs (D,REAL) = $1 + $2;
ex o being BinOp of (PFuncs (D,REAL)) st
for a, b being Element of PFuncs (D,REAL) holds o . (a,b) = H₁(a,b) from BINOP_1:sch 4();
hence ex b₁ being BinOp of (PFuncs (D,REAL)) st
for F1, F2 being Element of PFuncs (D,REAL) holds b₁ . (F1,F2) = F1 + F2 ; :: thesis: verum