for n being Nat
for p being XFinSequence of NAT st p is dominated_by_0 holds
2 * (Sum (p | ((2 * n) + 1))) < (2 * n) + 1