theorem :: RFUNCT_1:58

for C being non empty set
for c being Element of C
for f being PartFunc of C,REAL st f is total holds
( (- f) . c = - (f . c) & (abs f) . c = |.(f . c).| ) by VALUED_1:8, VALUED_1:18;