theorem Th9: :: RLVECT_X:9

for V being RealLinearSpace
for v, u being VECTOR of V
for A being Subset of V st v in Z_Lin A & u in Z_Lin A holds
v + u in Z_Lin A