theorem :: CFUNCT_1:61

for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f is total iff |.f.| is total ) by VALUED_1:def 11;