:: deftheorem dA defines mapAdd VECTSP13:def 14 :
for X being non empty set
for L being non empty addLoopStr
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 );