for n, i being Element of NAT st i <= n holds
(0* n) | i = 0* i