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