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;

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

hence
abs f is constant
by PARTFUN2:def 1; :: thesis: verumfor 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;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