defpred S₁[ set , set ] means $2 in S . $1;
A1: for k being Nat st k in Seg (len S) holds
ex x being Element of GA-Space S st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len S) implies ex x being Element of GA-Space S st S₁[k,x] )
assume A2: k in Seg (len S) ; :: thesis: ex x being Element of GA-Space S st S₁[k,x]
then reconsider k9 = k as Element of dom S by FINSEQ_1:def 3;
S . k9 <> {} ;
then consider x being Element of S . k such that
A3: x in [#] (S . k) by SUBSET_1:4;
k in dom S by A2, FINSEQ_1:def 3;
then S . k in rng S by FUNCT_1:def 3;
then [#] (S . k) c= union (rng S) by ZFMISC_1:74;
then reconsider x = x as Element of GA-Space S by A3, CARD_3:def 4;
take x ; :: thesis: S₁[k,x]
thus S₁[k,x] by A3; :: thesis: verum

end;

consider IT being FinSequence of GA-Space S such that
A4: ( dom IT = Seg (len S) & ( for k being Nat st k in Seg (len S) holds
S₁[k,IT . k] ) ) from FINSEQ_1:sch 5(A1);
take IT ; :: thesis: ( len IT = len S & ( for i being Element of NAT st i in dom IT holds
IT . i in S . i ) )
thus ( len IT = len S & ( for i being Element of NAT st i in dom IT holds
IT . i in S . i ) ) by A4, FINSEQ_1:def 3; :: thesis: verum