for k being Nat
for p, q being XFinSequence of NAT st p is dominated_by_0 & 2 * (Sum (p | k)) = k & p = (p | k) ^ q holds
q is dominated_by_0