theorem :: VECTSP10:32

for K being non empty addLoopStr
for V being non empty ModuleStr over K
for f, g being Functional of V
for v being Vector of V holds (f - g) . v = (f . v) - (g . v)