:: deftheorem defines isgn COMPLEX3:def 6 :
for a being Complex holds isgn a = Im (director a);