for V being RealLinearSpace
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
the carrier of (Lin V1) = V1