theorem :: EUCLID:72

for n being Nat holds abs (1* n) = n |-> 1