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