:: deftheorem Def1 defines FuncAdd LOPBAN_1:def 1 :
for X being non empty set
for Y being non empty addLoopStr
for b₃ being BinOp of (Funcs (X, the carrier of Y)) holds
( b₃ = FuncAdd (X,Y) iff for f, g being Element of Funcs (X, the carrier of Y) holds b₃ . (f,g) = the addF of Y .: (f,g) );