let a be Complex; :: thesis: cfrac (- a) = - (cfrac a)
cfrac (- a) = (- (director a)) * (frac |.(- a).|) by DIR
.= (- (director a)) * (frac |.a.|) by COMPLEX1:52 ;
hence cfrac (- a) = - (cfrac a) ; :: thesis: verum