for n being Nat
for p being XFinSequence of NAT st p is dominated_by_0 holds
p | n is dominated_by_0