theorem Th3: :: PDIFF_7:3

for i, j being Nat holds (0* j) /^ i = 0* (j -' i)