for D being non empty set
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 )