let n be Nat; :: thesis: abs (0* n) = n |-> 0
reconsider m = n as Element of NAT by ORDINAL1:def 12;
thus abs (0* n) = m |-> (absreal . 0) by FINSEQOP:16
.= n |-> (abs 0) by Def2
.= n |-> 0 by ABSVALUE:2 ; :: thesis: verum