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