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