theorem Th4: :: EUCLID:7

for n being Nat holds |.(0* n).| = 0