defpred S₁[ Nat, object ] means ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = $1 & $1 <= Sum (Length (F | (k + 1))) & $2 = (F . (k + 1)) . m );
A1: for n being Nat st n in Seg (Sum (Length F)) holds
ex x being Element of D st S₁[n,x]

proof

let n be Nat; :: thesis: ( n in Seg (Sum (Length F)) implies ex x being Element of D st S₁[n,x] )
assume n in Seg (Sum (Length F)) ; :: thesis: ex x being Element of D st S₁[n,x]
then ( 1 <= n & n <= Sum (Length F) ) by FINSEQ_1:1;
then consider k, m being Nat such that
A2: ( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) ) by Th3;
m in dom (F . (k + 1)) by A2, FINSEQ_3:25;
then (F . (k + 1)) . m in rng (F . (k + 1)) by FUNCT_1:3;
then reconsider x = (F . (k + 1)) . m as Element of D ;
take x ; :: thesis: S₁[n,x]
thus S₁[n,x] by A2; :: thesis: verum

end;

consider IT being FinSequence of D such that
A3: ( dom IT = Seg (Sum (Length F)) & ( for n being Nat st n in Seg (Sum (Length F)) holds
S₁[n,IT . n] ) ) from FINSEQ_1:sch 5(A1);
take IT ; :: thesis: ( len IT = Sum (Length F) & ( for n being Nat st n in dom IT holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & IT . n = (F . (k + 1)) . m ) ) )
thus len IT = Sum (Length F) by A3, FINSEQ_1:def 3; :: thesis: for n being Nat st n in dom IT holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & IT . n = (F . (k + 1)) . m )
thus for n being Nat st n in dom IT holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & IT . n = (F . (k + 1)) . m ) by A3; :: thesis: verum