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