deffunc H₁( Element of Funcs ( the carrier of M, the carrier of M), Element of Funcs ( the carrier of M, the carrier of M)) -> Element of Funcs ( the carrier of M, the carrier of M) = $1 * $2;
consider F being BinOp of (Funcs ( the carrier of M, the carrier of M)) such that
A1: for x, y being Element of Funcs ( the carrier of M, the carrier of M) holds F . (x,y) = H₁(x,y) from BINOP_1:sch 4();
take F ; :: thesis: for f, g being Element of Funcs ( the carrier of M, the carrier of M) holds F . (f,g) = f * g
let f, g be Element of Funcs ( the carrier of M, the carrier of M); :: thesis: F . (f,g) = f * g
thus F . (f,g) = f * g by A1; :: thesis: verum