theorem :: RLSUB_1:6
for V being RealLinearSpace
for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is VECTOR of V : ( v in V1 & u in V2 ) } holds
V3 is linearly-closed