theorem Th89: :: SEQ_4:90

for n being Nat holds abs (0c n) = n |-> 0