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