let S be set ; :: according to PRVECT_2:def 10 :: thesis: ( not S in rng <*G*> or S is NORMSTR )
assume S in rng <*G*> ; :: thesis: S is NORMSTR
then consider i being object such that
A1: ( i in dom <*G*> & <*G*> . i = S ) by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A1;
len <*G*> = 1 by FINSEQ_1:40;
then dom <*G*> = {1} by FINSEQ_1:2, FINSEQ_1:def 3;
then i = 1 by A1, TARSKI:def 1;
hence S is RealNormSpace by A1, FINSEQ_1:40; :: thesis: verum