theorem Th2: :: PDIFF_7:2

for i, j being Nat st i <= j holds
(0* j) | (i -' 1) = 0* (i -' 1)