theorem :: RLVECT_X:14

for V being RealLinearSpace
for A, B being Subset of V holds Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B)