consider S being RealLinearSpace;
take <*S*> ; :: thesis: ( not <*S*> is empty & <*S*> is RealLinearSpace-yielding )
thus not <*S*> is empty ; :: thesis: <*S*> is RealLinearSpace-yielding
let x be set ; :: according to PRVECT_2:def 3 :: thesis: ( x in rng <*S*> implies x is RealLinearSpace )
assume A1: ( x in rng <*S*> & x is not RealLinearSpace ) ; :: thesis: contradiction
then x in {S} by FINSEQ_1:55;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum