consider r being Element of REAL such that
A2: for c being Element of C st c in dom f holds
f . c = r by PARTFUN2:def 1;

now :: thesis: ex p being Element of REAL st
for c being Element of C st c in dom (abs f) holds
(abs f) . c = p

reconsider p = |.r.| as Element of REAL by XREAL_0:def 1;
take p = p; :: thesis: for c being Element of C st c in dom (abs f) holds
(abs f) . c = p
let c be Element of C; :: thesis: ( c in dom (abs f) implies (abs f) . c = p )
assume c in dom (abs f) ; :: thesis: (abs f) . c = p
then c in dom f by VALUED_1:def 11;
then |.(f . c).| = p by A2;
hence (abs f) . c = p by VALUED_1:18; :: thesis: verum

end;

hence abs f is constant by PARTFUN2:def 1; :: thesis: verum