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