defpred S_{1}[ 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_{1}[k,x]

A4: ( dom IT = Seg (len S) & ( for k being Nat st k in Seg (len S) holds

S_{1}[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

A1: for k being Nat st k in Seg (len S) holds

ex x being Element of GA-Space S st S

proof

consider IT being FinSequence of GA-Space S such that
let k be Nat; :: thesis: ( k in Seg (len S) implies ex x being Element of GA-Space S st S_{1}[k,x] )

assume A2: k in Seg (len S) ; :: thesis: ex x being Element of GA-Space S st S_{1}[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_{1}[k,x]

thus S_{1}[k,x]
by A3; :: thesis: verum

end;assume A2: k in Seg (len S) ; :: thesis: ex x being Element of GA-Space S st S

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

thus S

A4: ( dom IT = Seg (len S) & ( for k being Nat st k in Seg (len S) holds

S

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