let V be RealLinearSpace; :: thesis: for W being strict Subspace of V holds W is strict Subspace of (Omega). V
let W be strict Subspace of V; :: thesis: W is strict Subspace of (Omega). V
set V0 = (Omega). V;
A1: (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLSUB_1:def 4;
A2: ( the carrier of W c= the carrier of V & 0. W = 0. V & the addF of W = the addF of V || the carrier of W & the Mult of W = the Mult of V | [:REAL, the carrier of W:] ) by RLSUB_1:def 2;
( the carrier of V = the carrier of ((Omega). V) & 0. V = 0. ((Omega). V) & the addF of V = the addF of ((Omega). V) & the Mult of V = the Mult of ((Omega). V) ) by A1;
hence W is strict Subspace of (Omega). V by A2, RLSUB_1:def 2; :: thesis: verum