consider r1 being Real such that
A1: for c being object st c in dom f holds
|.(f . c).| <= r1 by Th72;

now :: thesis: ex r1 being Real st
for c being object st c in dom (abs f) holds
|.((abs f) . c).| <= r1

take r1 = r1; :: thesis: for c being object st c in dom (abs f) holds
|.((abs f) . c).| <= r1
let c be object ; :: thesis: ( c in dom (abs f) implies |.((abs f) . c).| <= r1 )
assume c in dom (abs f) ; :: thesis: |.((abs f) . c).| <= r1
then c in dom f by VALUED_1:def 11;
then |.|.(f . c).|.| <= r1 by A1;
hence |.((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 Th72; :: thesis: verum