:: deftheorem dA defines mapAdd VECTSP13:def 19 :
for X being non empty set
for R being non empty addLoopStr
for L being non empty ModuleStr over R
for b₄ being BinOp of (Funcs (X, the carrier of L)) holds
( b₄ = mapAdd (X,L) iff for f, g being Function of X,L holds b₄ . (f,g) = f '+' g );