:: deftheorem Def4 defines FuncComp LMOD_XX1:def 4 :
for M being AbGroup
for b₂ being BinOp of (Funcs ( the carrier of M, the carrier of M)) holds
( b₂ = FuncComp M iff for f, g being Element of Funcs ( the carrier of M, the carrier of M) holds b₂ . (f,g) = f * g );