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;