theorem Th17: :: TIETZE:17

for r being Real
for T being non empty TopSpace
for A being closed Subset of T st r > 0 & T is normal holds
for f being continuous Function of (T | A),R^1 st f,A is_absolutely_bounded_by r holds
ex g being continuous Function of T,R^1 st
( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 )