theorem Th51: :: RFUNCT_1:51

for C being non empty set
for r being Real
for f being PartFunc of C,REAL holds
( f is total iff r (#) f is total ) by VALUED_1:def 5;