let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f is total implies ( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX ) )
assume f is total ; :: thesis: ( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX )
then dom f = COMPLEX by PARTFUN1:def 2;
hence ( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX ) by COMSEQ_3:def 3, COMSEQ_3:def 4; :: thesis: verum