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

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