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 m1, m2, k1, k2 being Nat st m1 in dom (s . k1) & m2 in dom (s . k2) & (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 = (((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2 holds
( m1 = m2 & k1 = k2 )
let Y be non empty with_non-empty_element FinSequenceSet of D; :: thesis: for s being non-empty sequence of Y
for m1, m2, k1, k2 being Nat st m1 in dom (s . k1) & m2 in dom (s . k2) & (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 = (((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2 holds
( m1 = m2 & k1 = k2 )
let s be non-empty sequence of Y; :: thesis: for m1, m2, k1, k2 being Nat st m1 in dom (s . k1) & m2 in dom (s . k2) & (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 = (((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2 holds
( m1 = m2 & k1 = k2 )
let m1, m2, k1, k2 be Nat; :: thesis: ( m1 in dom (s . k1) & m2 in dom (s . k2) & (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 = (((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2 implies ( m1 = m2 & k1 = k2 ) )
assume that
A1: ( m1 in dom (s . k1) & m2 in dom (s . k2) ) and
A2: (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 = (((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2 ; :: thesis: ( m1 = m2 & k1 = k2 )
set n = (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1;
A3: ( 1 <= m1 & m1 <= len (s . k1) & 1 <= m2 & m2 <= len (s . k2) ) by A1, FINSEQ_3:25;
then ( (len (s . k1)) - m1 >= 0 & (len (s . k2)) - m2 >= 0 ) by XREAL_1:48;
then A4: ( ((Partial_Sums (Length s)) . k1) - ((len (s . k1)) - m1) <= (Partial_Sums (Length s)) . k1 & ((Partial_Sums (Length s)) . k2) - ((len (s . k2)) - m2) <= (Partial_Sums (Length s)) . k2 ) by XREAL_1:43;
A5: dom (Partial_Sums (Length s)) = NAT by FUNCT_2:def 1;
then A6: ( k1 in dom (Partial_Sums (Length s)) & k2 in dom (Partial_Sums (Length s)) ) by ORDINAL1:def 12;
A7: Partial_Sums (Length s) is increasing by Th9;
A14: now :: thesis: not k1 <> k2
assume A8: k1 <> k2 ; :: thesis: contradiction
per cases ( k1 < k2 or k2 < k1 ) by A8, XXREAL_0:1;
suppose k1 < k2 ; :: thesis: contradiction
then A10: k1 + 1 <= k2 by NAT_1:13;
1 <= k1 + 1 by NAT_1:11;
then reconsider j = k2 - 1 as Element of NAT by NAT_1:21, A10, XXREAL_0:2;
A11: k1 <= j by A10, XREAL_1:19;
A12: (Partial_Sums (Length s)) . k1 <= (Partial_Sums (Length s)) . j
proof
( k1 = j or k1 < j ) by A11, XXREAL_0:1;
hence (Partial_Sums (Length s)) . k1 <= (Partial_Sums (Length s)) . j by A5, A6, A7, SEQM_3:def 1; :: thesis: verum
end;
(Partial_Sums (Length s)) . (j + 1) = ((Partial_Sums (Length s)) . j) + ((Length s) . (j + 1)) by SERIES_1:def 1
.= ((Partial_Sums (Length s)) . j) + (len (s . k2)) by Def3 ;
then (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 > (Partial_Sums (Length s)) . j by A3, A2, XREAL_1:29;
hence contradiction by A4, A12, XXREAL_0:2; :: thesis: verum
end;
suppose k2 < k1 ; :: thesis: contradiction
then A10: k2 + 1 <= k1 by NAT_1:13;
1 <= k2 + 1 by NAT_1:11;
then reconsider j = k1 - 1 as Element of NAT by NAT_1:21, A10, XXREAL_0:2;
A11: k2 <= j by A10, XREAL_1:19;
A12: (Partial_Sums (Length s)) . k2 <= (Partial_Sums (Length s)) . j
proof
( k2 = j or k2 < j ) by A11, XXREAL_0:1;
hence (Partial_Sums (Length s)) . k2 <= (Partial_Sums (Length s)) . j by A5, A6, A7, SEQM_3:def 1; :: thesis: verum
end;
(Partial_Sums (Length s)) . (j + 1) = ((Partial_Sums (Length s)) . j) + ((Length s) . (j + 1)) by SERIES_1:def 1
.= ((Partial_Sums (Length s)) . j) + (len (s . k1)) by Def3 ;
then (((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1 > (Partial_Sums (Length s)) . j by A3, XREAL_1:29;
hence contradiction by A2, A4, A12, XXREAL_0:2; :: thesis: verum
end;
end;
end;
then ((Partial_Sums (Length s)) . k1) - (len (s . k1)) = ((Partial_Sums (Length s)) . k2) - (len (s . k2)) ;
hence ( m1 = m2 & k1 = k2 ) by A2, A14; :: thesis: verum