:: deftheorem defines cfrac COMPLEX3:def 7 :
for a being Complex holds cfrac a = (director a) * (frac |.a.|);