let D be non empty set ; :: thesis: for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )
let Y be non empty with_non-empty_element FinSequenceSet of D; :: thesis: for s being non-empty sequence of Y
for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )
let s be non-empty sequence of Y; :: thesis: for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )
let n be Nat; :: thesis: ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )
per cases ( n < len (s . 0) or len (s . 0) <= n ) ;
suppose A1: n < len (s . 0) ; :: thesis: ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )
set k = 0 ;
set m = n + 1;
take 0 ; :: thesis: ex m being Nat st
( m in dom (s . 0) & ((((Partial_Sums (Length s)) . 0) - (len (s . 0))) + m) - 1 = n )
take n + 1 ; :: thesis: ( n + 1 in dom (s . 0) & ((((Partial_Sums (Length s)) . 0) - (len (s . 0))) + (n + 1)) - 1 = n )
A4: n + 1 <= len (s . 0) by A1, NAT_1:13;
(Partial_Sums (Length s)) . 0 = (Length s) . 0 by SERIES_1:def 1
.= len (s . 0) by Def3 ;
hence ( n + 1 in dom (s . 0) & ((((Partial_Sums (Length s)) . 0) - (len (s . 0))) + (n + 1)) - 1 = n ) by NAT_1:11, A4, FINSEQ_3:25; :: thesis: verum
end;
suppose A5: len (s . 0) <= n ; :: thesis: ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )
then (Length s) . 0 <= n by Def3;
then A6: (Partial_Sums (Length s)) . 0 <= n by SERIES_1:def 1;
now :: thesis: ex k being Nat st
( k < n & not n < (Partial_Sums (Length s)) . k & not (Partial_Sums (Length s)) . (k + 1) <= n )
assume A8: for k being Nat holds
( not k < n or n < (Partial_Sums (Length s)) . k or (Partial_Sums (Length s)) . (k + 1) <= n ) ; :: thesis: contradiction
defpred S1[ Nat] means ( $1 < n implies (Partial_Sums (Length s)) . ($1 + 1) <= n );
A9: S1[ 0 ] by A6, A8;
A12: for k being Nat st S1[k] holds
S1[k + 1] by A8, NAT_1:13;
A13: for k being Nat holds S1[k] from NAT_1:sch 2(A9, A12);
reconsider n1 = n - 1 as Nat by A5, NAT_1:20;
(Partial_Sums (Length s)) . (n1 + 1) <= n by A13, NAT_1:19;
hence contradiction by Th7; :: thesis: verum
end;
then consider k1 being Nat such that
A14: ( k1 < n & (Partial_Sums (Length s)) . k1 <= n & n < (Partial_Sums (Length s)) . (k1 + 1) ) ;
take k = k1 + 1; :: thesis: ex m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )
reconsider m1 = ((Partial_Sums (Length s)) . k) - n as Nat by A14, NAT_1:21;
(Partial_Sums (Length s)) . k = ((Partial_Sums (Length s)) . k1) + ((Length s) . k) by SERIES_1:def 1;
then A15: m1 = (((Partial_Sums (Length s)) . k1) + (len (s . k))) - n by Def3;
((Partial_Sums (Length s)) . k1) - n <= 0 by A14, XREAL_1:47;
then A17: (((Partial_Sums (Length s)) . k1) - n) + (len (s . k)) <= len (s . k) by XREAL_1:32;
then ( m1 <= len (s . k) & len (s . k) <= (len (s . k)) + 1 ) by A15, NAT_1:11;
then reconsider m = ((len (s . k)) + 1) - m1 as Nat by NAT_1:21, XXREAL_0:2;
take m ; :: thesis: ( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n )
m1 > 0 by A14, XREAL_1:50;
then ( (len (s . k)) - m1 >= 0 & 1 - m1 <= 0 ) by A15, A17, NAT_1:14, XREAL_1:47, XREAL_1:48;
then ( ((len (s . k)) - m1) + 1 >= 0 + 1 & (len (s . k)) + (1 - m1) <= (len (s . k)) + 0 ) by XREAL_1:6;
hence ( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n ) by FINSEQ_3:25; :: thesis: verum
end;
end;