let r be real number ; :: thesis:
let T be non empty TopSpace; :: thesis:
let A be closed Subset of T; :: thesis:
assume that
A1: r > 0 and
A2: T is normal ; :: thesis:
let f be continuous Function of (T | A),R^1 ; :: thesis:
assume A3: for x being set st x in A /\ (dom f) holds
abs (f . x) <= r ; :: according to TIETZE:def 1 :: thesis:
set A1 = left_closed_halfline (- (r / 3));
set A2 = right_closed_halfline (r / 3);
set C1 = R^1 (left_closed_halfline (- (r / 3)));
set C2 = R^1 (right_closed_halfline (r / 3));
A4: ( left_closed_halfline (- (r / 3)) = R^1 (left_closed_halfline (- (r / 3))) & right_closed_halfline (r / 3) = R^1 (right_closed_halfline (r / 3)) ) by TOPREALB:def 3;
A5: - (- (r / 3)) > 0 by A1, XREAL_1:141;
then A6: - (r / 3) < r / 3 ;
then A7: f " (left_closed_halfline (- (r / 3))) misses f " (right_closed_halfline (r / 3)) by FUNCT_1:141, XXREAL_1:279;
( f " (R^1 (left_closed_halfline (- (r / 3)))) is closed & f " (R^1 (right_closed_halfline (r / 3))) is closed ) by PRE_TOPC:def 12;
then reconsider D1 = f " (R^1 (left_closed_halfline (- (r / 3)))), D2 = f " (R^1 (right_closed_halfline (r / 3))) as closed Subset of T by PRE_TOPC:39, TSEP_1:12;
consider F being Function of T,R^1 such that
A8: F is continuous and
A9: for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in D1 implies F . x = 0 ) & ( x in D2 implies F . x = 1 ) ) by A2, A4, A7, URYSOHN3:23;
reconsider r1 = r as Real by XREAL_0:def 1;
set e = (2 * r1) / 3;
0 < 2 * r by A1, XREAL_1:131;
then A10: (2 * r1) / 3 > 0 by XREAL_1:141;
then consider h being Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace ((((2 * r1) / 3) * 0 ) + (- (r1 / 3))),((((2 * r1) / 3) * 1) + (- (r1 / 3)))) such that
A11: h is being_homeomorphism and
A12: for w being Real st w in [.0 ,1.] holds
h . w = (((2 * r1) / 3) * w) + (- (r1 / 3)) by JGRAPH_5:39;
A13: the carrier of (Closed-Interval-TSpace (- (r / 3)),(r / 3)) = [.(- (r / 3)),(r / 3).] by A6, TOPMETR:25;
A14: the carrier of (Closed-Interval-TSpace 0 ,1) = [.0 ,1.] by TOPMETR:25;
set g1 = h * F;
A15: dom F = the carrier of T by FUNCT_2:def 1;
A16: dom h = the carrier of (Closed-Interval-TSpace 0 ,1) by FUNCT_2:def 1;
A17: rng F c= [.0 ,1.]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng F ; :: thesis:
then consider x being set such that
A18: x in dom F and
A19: F . x = y by FUNCT_1:def 5;
( 0 <= F . x & F . x <= 1 ) by A9, A18;
hence y in [.0 ,1.] by A19, XXREAL_1:1; :: thesis:

end;

then A20: dom (h * F) = the carrier of T by A14, A15, A16, RELAT_1:46;
A21: rng (h * F) c= the carrier of (Closed-Interval-TSpace (- (r / 3)),(r / 3)) ;
then reconsider g1 = h * F as Function of T,(Closed-Interval-TSpace (- (r / 3)),(r / 3)) by A20, FUNCT_2:4;
A22: rng g1 c= the carrier of (Closed-Interval-TSpace (- (r / 3)),(r / 3)) ;
A23: h is continuous by A11, TOPS_2:def 5;
reconsider g = g1 as Function of T,R^1 by TOPREALA:28;
reconsider F1 = F as Function of T,(Closed-Interval-TSpace 0 ,1) by A14, A17, FUNCT_2:8;
F1 is continuous by A8, PRE_TOPC:57;
then h * F1 is continuous by A23;
then reconsider g = g as continuous Function of T,R^1 by PRE_TOPC:56;
take g ; :: thesis:
thus g, dom g is_absolutely_bounded_by r / 3 :: thesis:

proof

let x be set ; :: according to TIETZE:def 1 :: thesis:
assume x in (dom g) /\ (dom g) ; :: thesis:
then g . x in rng g by FUNCT_1:def 5;
then ( - (r / 3) <= g . x & g . x <= r / 3 ) by A13, A22, XXREAL_1:1;
hence abs (g . x) <= r / 3 by ABSVALUE:12; :: thesis:

end;

thus f - g,A is_absolutely_bounded_by (2 * r) / 3 :: thesis:

proof

let x be set ; :: according to TIETZE:def 1 :: thesis:
assume A24: x in A /\ (dom (f - g)) ; :: thesis:
A25: dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12;
A26: x in dom (f - g) by A24, XBOOLE_0:def 4;
then A27: x in dom f by A25, XBOOLE_0:def 4;
x in A by A24, XBOOLE_0:def 4;
then x in A /\ (dom f) by A27, XBOOLE_0:def 4;
then A28: abs (f . x) <= r by A3;
then A29: - r <= f . x by ABSVALUE:12;
A30: 0 in [.0 ,1.] by XXREAL_1:1;
A31: 1 in [.0 ,1.] by XXREAL_1:1;
A32: (f - g) . x = (f . x) - (g . x) by A26, VALUED_1:13;

per cases ;

suppose A33: f . x <= - (r / 3) ; :: thesis:

then f . x in left_closed_halfline (- (r / 3)) by XXREAL_1:234;
then x in f " (left_closed_halfline (- (r / 3))) by A27, FUNCT_1:def 13;
then F . x = 0 by A4, A9;
then A34: g . x = h . 0 by A20, A24, FUNCT_1:22
.= - (r1 / 3) by A12, A30 ;
- r = (- ((2 * r) / 3)) - (r / 3) ;
then A35: - ((2 * r) / 3) <= (f . x) + (r / 3) by A29, XREAL_1:22;
(f . x) + (r / 3) <= (- (r / 3)) + (r / 3) by A33, XREAL_1:8;
hence abs ((f - g) . x) <= (2 * r) / 3 by A10, A32, A34, A35, ABSVALUE:12; :: thesis:

end;

suppose A36: r / 3 <= f . x ; :: thesis:

then f . x in right_closed_halfline (r / 3) by XXREAL_1:236;
then x in f " (right_closed_halfline (r / 3)) by A27, FUNCT_1:def 13;
then F . x = 1 by A4, A9;
then A37: g . x = h . 1 by A20, A24, FUNCT_1:22
.= r1 / 3 by A12, A31 ;
(- ((2 * r) / 3)) + (r / 3) <= f . x by A5, A36;
then A38: - ((2 * r) / 3) <= (f . x) - (r / 3) by XREAL_1:21;
f . x <= (r / 3) + ((2 * r) / 3) by A28, ABSVALUE:12;
then (f . x) - (r / 3) <= (2 * r) / 3 by XREAL_1:22;
hence abs ((f - g) . x) <= (2 * r) / 3 by A32, A37, A38, ABSVALUE:12; :: thesis:

end;

suppose A39: ( - (r / 3) < f . x & f . x < r / 3 ) ; :: thesis:

A40: - ((2 * r) / 3) = (- (r / 3)) - (r / 3) ;
g . x in rng g by A20, A24, FUNCT_1:def 5;
then A41: ( - (r / 3) <= g . x & g . x <= r / 3 ) by A13, A21, XXREAL_1:1;
then A42: - ((2 * r) / 3) <= (f . x) - (g . x) by A39, A40, XREAL_1:15;
(f . x) - (g . x) <= (r / 3) - (- (r / 3)) by A39, A41, XREAL_1:16;
hence abs ((f - g) . x) <= (2 * r) / 3 by A32, A42, ABSVALUE:12; :: thesis:

end;