theorem Th72: :: RFUNCT_1:72

for f being real-valued Function holds
( f is bounded iff ex r being Real st
for c being object st c in dom f holds
|.(f . c).| <= r )