theorem Th13: :: RLSUB_1:13

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u