consider r1 being Real such that

A1: for c being object st c in dom f holds

|.(f . c).| <= r1 by Th72;

_{1} being real-valued Function st b_{1} = abs f holds

b_{1} is bounded
by Th72; :: thesis: verum

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

hence
for bfor 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;|.((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

b