for m being Nat holds m = |.m.| ;