deffunc H_{1}( Element of BoundedLinearOperators (X,X), Element of BoundedLinearOperators (X,X)) -> Element of BoundedLinearOperators (X,X) = $1 * $2;

consider F being BinOp of (BoundedLinearOperators (X,X)) such that

A1: for x, y being Element of BoundedLinearOperators (X,X) holds F . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

take F ; :: thesis: for f, g being Element of BoundedLinearOperators (X,X) holds F . (f,g) = f * g

let f, g be Element of BoundedLinearOperators (X,X); :: thesis: F . (f,g) = f * g

thus F . (f,g) = f * g by A1; :: thesis: verum

consider F being BinOp of (BoundedLinearOperators (X,X)) such that

A1: for x, y being Element of BoundedLinearOperators (X,X) holds F . (x,y) = H

take F ; :: thesis: for f, g being Element of BoundedLinearOperators (X,X) holds F . (f,g) = f * g

let f, g be Element of BoundedLinearOperators (X,X); :: thesis: F . (f,g) = f * g

thus F . (f,g) = f * g by A1; :: thesis: verum