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, FINSEQ_1:45; :: thesis: verum

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, FINSEQ_1:45; :: thesis: verum