theorem :: DUALSP01:4

for X being VectSp of F_Real
for v, w being Element of X
for v1, w1 being Element of (RVSp2RLSp X) st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )