deffunc H1( Element of Funcs (A,COMPLEX), Element of Funcs (A,COMPLEX)) -> Element of Funcs (A,COMPLEX) = multcomplex .: ($1,$2);
consider F being BinOp of (Funcs (A,COMPLEX)) such that
A1:
for x, y being Element of Funcs (A,COMPLEX) holds F . (x,y) = H1(x,y)
from BINOP_1:sch 4();
take
F
; for f, g being Element of Funcs (A,COMPLEX) holds F . (f,g) = multcomplex .: (f,g)
let f, g be Element of Funcs (A,COMPLEX); F . (f,g) = multcomplex .: (f,g)
thus
F . (f,g) = multcomplex .: (f,g)
by A1; verum