let X be RealLinearSpace; :: thesis: 0. (X *') = the carrier of X --> 0

A1: X *' is Subspace of RealVectSpace the carrier of X by Th17, RSSPACE:11;

0. (RealVectSpace the carrier of X) = the carrier of X --> 0 ;

hence 0. (X *') = the carrier of X --> 0 by A1, RLSUB_1:11; :: thesis: verum

A1: X *' is Subspace of RealVectSpace the carrier of X by Th17, RSSPACE:11;

0. (RealVectSpace the carrier of X) = the carrier of X --> 0 ;

hence 0. (X *') = the carrier of X --> 0 by A1, RLSUB_1:11; :: thesis: verum