for i, j being Nat holds
( ( i <= j implies (0* j) | (i -' 1) = 0* (i -' 1) ) & (0* j) /^ i = 0* (j -' i) ) by Th2, Th3;