let S be set ; :: according to PRVECT_2:def 3 :: thesis: ( not S in proj2 (G ^ F) or S is RLSStruct )
assume S in rng (G ^ F) ; :: thesis: S is RLSStruct
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;

per cases ( i in dom G or ex n being Nat st
( n in dom F & i = (len G) + n ) ) by FINSEQ_1:38, A1;

suppose A3: i in dom G ; :: thesis: S is RLSStruct

then X1: (G ^ F) . i = G . i by FINSEQ_1:def 7;
G . i in rng G by A3, FUNCT_1:12;
hence S is RealLinearSpace by X1, A1, PRVECT_2:def 3; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom F & i = (len G) + n ) ; :: thesis: S is RLSStruct

then consider n being Nat such that
A41: ( n in dom F & i = (len G) + n ) ;
X1: (G ^ F) . i = F . n by A41, FINSEQ_1:def 7;
F . n in rng F by A41, FUNCT_1:12;
hence S is RealLinearSpace by X1, A1, PRVECT_2:def 3; :: thesis: verum

end;

end;