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 |-> |.0.| by Def2
.= n |-> 0 by ABSVALUE:2 ; :: thesis: verum