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 holds Partial_Sums (Length s) is increasing