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