let S be set ; :: according to VECTSP12:def 3 :: thesis: ( S in rng (G ^ F) implies S is VectSp of K )

assume S in rng (G ^ F) ; :: thesis: S is VectSp of K

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;

assume S in rng (G ^ F) ; :: thesis: S is VectSp of K

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;

end;

( n in dom F & i = (len G) + n ) ) by A1, FINSEQ_1:25;

suppose A2:
i in dom G
; :: thesis: S is VectSp of K

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 VectSp of K by A3, A1, Def3; :: thesis: verum

end;G . i in rng G by A2, FUNCT_1:3;

hence S is VectSp of K by A3, A1, Def3; :: thesis: verum

suppose
ex n being Nat st

( n in dom F & i = (len G) + n ) ; :: thesis: S is VectSp of K

( n in dom F & i = (len G) + n ) ; :: thesis: S is VectSp of K

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 VectSp of K by A5, A1, Def3; :: thesis: verum

end;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 VectSp of K by A5, A1, Def3; :: thesis: verum