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 b1 being real-valued Function st b1 = abs f holds
b1 is bounded by Th72; :: thesis: verum