let X be non empty set ; :: thesis: for Y being non empty addLoopStr 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) = the addF of Y .: (f,g)
let Y be non empty addLoopStr ; :: thesis: 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) = the addF of Y .: (f,g)
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);
consider ADD being BinOp of (Funcs (X, the carrier of Y)) such that
A1: for f, g being Element of Funcs (X, the carrier of Y) holds ADD . (f,g) = H₁(f,g) from BINOP_1:sch 4();
take ADD ; :: thesis: for f, g being Element of Funcs (X, the carrier of Y) holds ADD . (f,g) = the addF of Y .: (f,g)
thus for f, g being Element of Funcs (X, the carrier of Y) holds ADD . (f,g) = the addF of Y .: (f,g) by A1; :: thesis: verum