A1: dom (abs f) = dom f by VALUED_1:def 11;
for x being object st x in dom (abs f) holds
(abs f) . x = f . x

proof

let x be object ; :: thesis: ( x in dom (abs f) implies (abs f) . x = f . x )
assume A1: x in dom (abs f) ; :: thesis: (abs f) . x = f . x
(abs f) . x = |.(f . x).| by A1, VALUED_1:def 11
.= f . x ;
hence (abs f) . x = f . x ; :: thesis: verum

end;

hence abs f = f by A1, FUNCT_1:2; :: thesis: verum