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 4;
hence ( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX ) by Def2, Def3; :: thesis: verum