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