deffunc H₁( Element of Funcs (X, the carrier of Y), Element of Funcs (X, the carrier of Y)) -> Element of Funcs (X, the carrier of Y) = the addF of Y .: ($1,$2);
thus ex ADD being BinOp of (Funcs (X, the carrier of Y)) st
for f, g being Element of Funcs (X, the carrier of Y) holds ADD . (f,g) = H₁(f,g) from BINOP_1:sch 4(); :: thesis: verum