let D be set ; :: thesis: for Y being FinSequenceSet of D
for F being FinSequence of Y
for n being Nat st 1 <= n & n <= Sum (Length F) 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))) )
let Y be FinSequenceSet of D; :: thesis: for F being FinSequence of Y
for n being Nat st 1 <= n & n <= Sum (Length F) 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))) )
let F be FinSequence of Y; :: thesis: for n being Nat st 1 <= n & n <= Sum (Length F) 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))) )
let n be Nat; :: thesis: ( 1 <= n & n <= Sum (Length F) implies 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))) ) )
assume A1: ( 1 <= n & n <= Sum (Length F) ) ; :: thesis: 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))) )

now :: thesis: ex k being Nat st
( not n <= Sum (Length (F | k)) & not n > Sum (Length (F | (k + 1))) )

assume A2: for k being Nat holds
( n <= Sum (Length (F | k)) or n > Sum (Length (F | (k + 1))) ) ; :: thesis: contradiction
defpred S₁[ Nat] means n > Sum (Length (F | ($1 + 1)));
dom (Length (F | 0)) = dom {} by Def1;
then Length (F | 0) = {} ;
then A3: S₁[ 0 ] by A2, A1, RVSUM_1:72;
A4: for k being Nat st S₁[k] holds
S₁[k + 1] by A2;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
then n > Sum (Length (F | ((len F) + 1))) ;
hence contradiction by A1, FINSEQ_1:58, NAT_1:11; :: thesis: verum

end;

then consider k being Nat such that
A6: ( Sum (Length (F | k)) < n & n <= Sum (Length (F | (k + 1))) ) ;
consider m being Nat such that
A7: n = (Sum (Length (F | k))) + m by A6, NAT_1:10;
take k ; :: thesis: ex 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))) )
take m ; :: thesis: ( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) )

A8: now :: thesis: not len F <= k

assume A9: len F <= k ; :: thesis: contradiction
k <= k + 1 by NAT_1:11;
then ( F | (k + 1) = F & F | k = F ) by A9, XXREAL_0:2, FINSEQ_1:58;
hence contradiction by A6; :: thesis: verum

end;

then Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*> by Th2;
then m + (Sum (Length (F | k))) <= (Sum (Length (F | k))) + (len (F . (k + 1))) by A6, A7, RVSUM_1:74;
hence ( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) ) by A6, A7, NAT_1:19, A8, XREAL_1:6; :: thesis: verum