consider r1 being real number such that
A1: for c being set st c in dom f holds
abs (f . c) <= r1 by Th89;

now

take r1 = r1; :: thesis: for c being set st c in dom (abs f) holds
abs ((abs f) . c) <= r1
let c be set ; :: thesis: ( c in dom (abs f) implies abs ((abs f) . c) <= r1 )
assume c in dom (abs f) ; :: thesis: abs ((abs f) . c) <= r1
then c in dom f by VALUED_1:def 11;
then abs (abs (f . c)) <= r1 by A1;
hence abs ((abs f) . c) <= r1 by VALUED_1:18; :: thesis: verum

end;

hence for b₁ being real-valued Function st b₁ = abs f holds
b₁ is bounded by Th89; :: thesis: verum