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

assume S in rng <*G*> ; :: thesis: S is VectSp of K

then consider i being object such that

A1: ( i in dom <*G*> & <*G*> . i = S ) by FUNCT_1:def 3;

reconsider i = i as Element of NAT by A1;

dom <*G*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

then i = 1 by A1, TARSKI:def 1;

hence S is VectSp of K by A1, FINSEQ_1:40; :: thesis: verum

assume S in rng <*G*> ; :: thesis: S is VectSp of K

then consider i being object such that

A1: ( i in dom <*G*> & <*G*> . i = S ) by FUNCT_1:def 3;

reconsider i = i as Element of NAT by A1;

dom <*G*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

then i = 1 by A1, TARSKI:def 1;

hence S is VectSp of K by A1, FINSEQ_1:40; :: thesis: verum