theorem :: DUALSP01:3

for X being RealLinearSpace
for v, w being Element of X
for v1, w1 being Element of (RLSp2RVSp X) st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )