theorem RSSPACE11: :: NORMSP_3:68

for X being RealNormSpace
for V1, CL being Subset of X st CL = the carrier of (ClNLin V1) holds
RLSStruct(# CL,(Zero_ (CL,X)),(Add_ (CL,X)),(Mult_ (CL,X)) #) is Subspace of X