theorem :: RFUNCT_1:53

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