theorem Th58: :: CFUNCT_1:59

for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Complex holds
( f is total iff r (#) f is total ) by Th4;