deffunc H_{1}( 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_{1}(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

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

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