let S be set ; :: according to PRVECT_2:def 3 :: thesis: ( not S in rng (G ^ F) or S is RLSStruct )
assume S in rng (G ^ F) ; :: thesis: S is RLSStruct
then consider i being object such that
A1: ( i in dom (G ^ F) & (G ^ F) . i = S ) by FUNCT_1:def 3;
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 A1, FINSEQ_1:25;

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

then A3: (G ^ F) . i = G . i by FINSEQ_1:def 7;
G . i in rng G by A2, FUNCT_1:3;
hence S is RealLinearSpace by A3, 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
A4: ( n in dom F & i = (len G) + n ) ;
A5: (G ^ F) . i = F . n by A4, FINSEQ_1:def 7;
F . n in rng F by A4, FUNCT_1:3;
hence S is RealLinearSpace by A5, A1, PRVECT_2:def 3; :: thesis: verum

end;

end;