:: deftheorem defp defines '+' VECTSP13:def 11 :
for X being non empty set
for L being non empty addLoopStr
for f, g, b₅ being Function of X,L holds
( b₅ = f '+' g iff for x being Element of X holds b₅ . x = (f . x) + (g . x) );