for X being RealNormSpace
for Y, Z being Subset of X st Z = the carrier of (Lin Y) holds
the carrier of (Lin Z) = Z by RLVECT_3:18;