let S be set ; PRVECT_2:def 3 ( not S in proj2 <*E,F,G*> or S is RLSStruct )
assume
S in rng <*E,F,G*>
; S is RLSStruct
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 RealLinearSpace
by A1, FINSEQ_1:45; verum