theorem Th1: :: CFDIFF_2:1

for f being PartFunc of COMPLEX,COMPLEX st f is total holds
( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX )