defpred S1[ 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 S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len S) implies ex x being Element of GA-Space S st S1[k,x] )
assume A2: k in Seg (len S) ; :: thesis: ex x being Element of GA-Space S st S1[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 ;
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 ;
take x ; :: thesis: S1[k,x]
thus S1[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
S1[k,IT . k] ) ) from 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 ; :: thesis: verum