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