the addF of (RLSp2RVSp Y) = the addF of (RLSp2RVSp Y) || the carrier of (RLSp2RVSp Y) ;
hence RLSp2RVSp Y is Subspace of RLSp2RVSp X ; :: thesis: verum