theorem LMQ03: :: NORMSP_3:52

for X being RealLinearSpace
for Y being Subspace of X
for v being Element of X
for v1 being Element of (RLSp2RVSp X) st v = v1 holds
v + Y = v1 + (RLSp2RVSp Y)