let D be non empty set ; :: thesis: for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for k, m being Nat st m in dom (s . k) holds
ex n being Nat st
( n = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 & (joined_seq s) . n = (s . k) . m )
let Y be with_non-empty_element FinSequenceSet of D; :: thesis: for s being non-empty sequence of Y
for k, m being Nat st m in dom (s . k) holds
ex n being Nat st
( n = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 & (joined_seq s) . n = (s . k) . m )
let s be non-empty sequence of Y; :: thesis: for k, m being Nat st m in dom (s . k) holds
ex n being Nat st
( n = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 & (joined_seq s) . n = (s . k) . m )
let k, m be Nat; :: thesis: ( m in dom (s . k) implies ex n being Nat st
( n = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 & (joined_seq s) . n = (s . k) . m ) )
assume A0: m in dom (s . k) ; :: thesis: ex n being Nat st
( n = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 & (joined_seq s) . n = (s . k) . m )
then A1: ( 1 <= m & m <= len (s . k) ) by FINSEQ_3:25;
now :: thesis: ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 is Nat
per cases ( k = 0 or k <> 0 ) ;
suppose A2: k = 0 ; :: thesis: ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 is Nat
then (Partial_Sums (Length s)) . k = (Length s) . 0 by SERIES_1:def 1
.= len (s . 0) by Def3 ;
hence ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 is Nat by A1, A2, NAT_1:21; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 is Nat
then reconsider k1 = k - 1 as Element of NAT by NAT_1:14, NAT_1:21;
k = k1 + 1 ;
then (Partial_Sums (Length s)) . k = ((Partial_Sums (Length s)) . k1) + ((Length s) . k) by SERIES_1:def 1
.= ((Partial_Sums (Length s)) . k1) + (len (s . k)) by Def3 ;
then reconsider n1 = ((Partial_Sums (Length s)) . k) - (len (s . k)) as Nat ;
n1 + m >= m by NAT_1:11;
hence ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 is Nat by A1, XXREAL_0:2, NAT_1:21; :: thesis: verum
end;
end;
end;
then reconsider n = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 as Nat ;
take n ; :: thesis: ( n = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 & (joined_seq s) . n = (s . k) . m )
thus n = ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 ; :: thesis: (joined_seq s) . n = (s . k) . m
consider k2, m2 being Nat such that
A4: ( m2 in dom (s . k2) & ((((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2) - 1 = n & (joined_seq s) . n = (s . k2) . m2 ) by Def4;
( m = m2 & k = k2 ) by A0, A4, Th10;
hence (joined_seq s) . n = (s . k) . m by A4; :: thesis: verum