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