set V = RLSp2RVSp X;
set W = RLSp2RVSp Y;
A1: the carrier of (RLSp2RVSp Y) c= the carrier of (RLSp2RVSp X) by RLSUB_1:def 2;
A2: 0. (RLSp2RVSp Y) = 0. Y
.= 0. X by RLSUB_1:def 2
.= 0. (RLSp2RVSp X) ;
A3: the addF of (RLSp2RVSp Y) = the addF of (RLSp2RVSp X) || the carrier of (RLSp2RVSp Y) by RLSUB_1:def 2;
the lmult of (RLSp2RVSp Y) = the lmult of (RLSp2RVSp X) | [:REAL, the carrier of (RLSp2RVSp Y):] by RLSUB_1:def 2;
hence RLSp2RVSp Y is Subspace of RLSp2RVSp X by A1, A2, A3, VECTSP_4:def 2; :: thesis: verum