:: deftheorem Def1 defines ADD LMOD_XX1:def 1 :
for M, N being AbGroup
for b₃ being BinOp of (Funcs ( the carrier of M, the carrier of N)) holds
( b₃ = ADD (M,N) iff for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds b₃ . (f,g) = the addF of N .: (f,g) );