let V be RealLinearSpace; :: thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

the carrier of (Lin V1) = V1

let V1 be Subset of V; :: thesis: ( V1 <> {} & V1 is linearly-closed implies the carrier of (Lin V1) = V1 )

assume ( V1 <> {} & V1 is linearly-closed ) ; :: thesis: the carrier of (Lin V1) = V1

then ex W0 being strict Subspace of V st V1 = the carrier of W0 by RLSUB_1:35;

hence the carrier of (Lin V1) = V1 by RLVECT_3:18; :: thesis: verum

the carrier of (Lin V1) = V1

let V1 be Subset of V; :: thesis: ( V1 <> {} & V1 is linearly-closed implies the carrier of (Lin V1) = V1 )

assume ( V1 <> {} & V1 is linearly-closed ) ; :: thesis: the carrier of (Lin V1) = V1

then ex W0 being strict Subspace of V st V1 = the carrier of W0 by RLSUB_1:35;

hence the carrier of (Lin V1) = V1 by RLVECT_3:18; :: thesis: verum