let n be Element of NAT ; :: thesis: abs (0c n) = n |-> 0
thus abs (0c n) = n |-> (abscomplex . 0c) by FINSEQOP:17
.= n |-> 0 by Def6, COMPLEX1:130 ; :: thesis: verum