deffunc H₁( 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 = H₁(x,y) from BINOP_1:sch 4();
take F ; :: thesis: 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 ; :: thesis: F . f,g = multcomplex .: f,g
thus F . f,g = multcomplex .: f,g by A1; :: thesis: verum