theorem :: DUALSP01:6

for V being RealLinearSpace
for f, g, h being VECTOR of (V *') holds
( h = f + g iff for x being VECTOR of V holds h . x = (f . x) + (g . x) )