deffunc H₁( 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₁(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