let r be Real; :: 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:
set C2 = R^1 (right_closed_halfline (r / 3));
set C1 = R^1 (left_closed_halfline (- (r / 3)));
set A2 = right_closed_halfline (r / 3);
set A1 = left_closed_halfline (- (r / 3));
let f be continuous Function of (T | A),R^1; :: thesis:
assume A3: for x being set st x in A /\ (dom f) holds
|.(f . x).| <= r ; :: according to TIETZE:def 1 :: thesis:
reconsider r1 = r as Real ;
set e = (2 * r1) / 3;
0 < 2 * r by A1, XREAL_1:129;
then (2 * r1) / 3 > 0 by XREAL_1:139;
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
A4: h is being_homeomorphism and
A5: for w being Real st w in [.0,1.] holds
h . w = (((2 * r1) / 3) * w) + (- (r1 / 3)) by JGRAPH_5:36;
A6: h is continuous by A4, TOPS_2:def 5;
A7: the carrier of (Closed-Interval-TSpace (0,1)) = [.0,1.] by TOPMETR:18;
( f " (R^1 (left_closed_halfline (- (r / 3)))) is closed & f " (R^1 (right_closed_halfline (r / 3))) is closed ) by PRE_TOPC:def 6;
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:11, TSEP_1:12;
A8: left_closed_halfline (- (r / 3)) = R^1 (left_closed_halfline (- (r / 3))) by TOPREALB:def 3;
A9: right_closed_halfline (r / 3) = R^1 (right_closed_halfline (r / 3)) by TOPREALB:def 3;
A10: - (- (r / 3)) > 0 by A1, XREAL_1:139;
then f " (left_closed_halfline (- (r / 3))) misses f " (right_closed_halfline (r / 3)) by FUNCT_1:71, XXREAL_1:279;
then consider F being Function of T,R^1 such that
A11: F is continuous and
A12: 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, A8, A9, URYSOHN3:20;
A13: rng F c= [.0,1.]

proof

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

end;

then reconsider F1 = F as Function of T,(Closed-Interval-TSpace (0,1)) by A7, FUNCT_2:6;
A16: the carrier of (Closed-Interval-TSpace ((- (r / 3)),(r / 3))) = [.(- (r / 3)),(r / 3).] by A1, TOPMETR:18;
set g1 = h * F;
A17: rng (h * F) c= the carrier of (Closed-Interval-TSpace ((- (r / 3)),(r / 3))) ;
( dom F = the carrier of T & dom h = the carrier of (Closed-Interval-TSpace (0,1)) ) by FUNCT_2:def 1;
then A18: dom (h * F) = the carrier of T by A7, A13, RELAT_1:27;
then reconsider g1 = h * F as Function of T,(Closed-Interval-TSpace ((- (r / 3)),(r / 3))) by A17, FUNCT_2:2;
reconsider g = g1 as Function of T,R^1 by TOPREALA:7;
F1 is continuous by A11, PRE_TOPC:27;
then reconsider g = g as continuous Function of T,R^1 by A6, PRE_TOPC:26;
take g ; :: thesis:
A19: rng g1 c= the carrier of (Closed-Interval-TSpace ((- (r / 3)),(r / 3))) ;
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 3;
then ( - (r / 3) <= g . x & g . x <= r / 3 ) by A16, A19, XXREAL_1:1;
hence |.(g . x).| <= r / 3 by ABSVALUE:5; :: thesis:

end;

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

proof

A20: 1 in [.0,1.] by XXREAL_1:1;
A21: 0 in [.0,1.] by XXREAL_1:1;
let x be set ; :: according to TIETZE:def 1 :: thesis:
assume A22: x in A /\ (dom (f - g)) ; :: thesis:
A23: x in dom (f - g) by A22, XBOOLE_0:def 4;
then A24: (f - g) . x = (f . x) - (g . x) by VALUED_1:13;
dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12;
then A25: x in dom f by A23, XBOOLE_0:def 4;
x in A by A22, XBOOLE_0:def 4;
then x in A /\ (dom f) by A25, XBOOLE_0:def 4;
then A26: |.(f . x).| <= r by A3;
then A27: - r <= f . x by ABSVALUE:5;

per cases ;

suppose A28: 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 A25, FUNCT_1:def 7;
then F . x = 0 by A8, A12;
then A29: g . x = h . 0 by A18, A22, FUNCT_1:12
.= - (r1 / 3) by A5, A21 ;
- r = (- ((2 * r) / 3)) - (r / 3) ;
then A30: - ((2 * r) / 3) <= (f . x) + (r / 3) by A27, XREAL_1:20;
(f . x) + (r / 3) <= (- (r / 3)) + (r / 3) by A28, XREAL_1:6;
hence |.((f - g) . x).| <= (2 * r) / 3 by A1, A24, A29, A30, ABSVALUE:5; :: thesis:

end;

suppose A31: 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 A25, FUNCT_1:def 7;
then F . x = 1 by A9, A12;
then A32: g . x = h . 1 by A18, A22, FUNCT_1:12
.= r1 / 3 by A5, A20 ;
f . x <= (r / 3) + ((2 * r) / 3) by A26, ABSVALUE:5;
then A33: (f . x) - (r / 3) <= (2 * r) / 3 by XREAL_1:20;
(- ((2 * r) / 3)) + (r / 3) <= f . x by A10, A31;
then - ((2 * r) / 3) <= (f . x) - (r / 3) by XREAL_1:19;
hence |.((f - g) . x).| <= (2 * r) / 3 by A24, A32, A33, ABSVALUE:5; :: thesis:

end;

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

A35: g . x in rng g by A18, A22, FUNCT_1:def 3;
then ( - ((2 * r) / 3) = (- (r / 3)) - (r / 3) & g . x <= r / 3 ) by A16, A17, XXREAL_1:1;
then A36: - ((2 * r) / 3) <= (f . x) - (g . x) by A34, XREAL_1:13;
- (r / 3) <= g . x by A16, A17, A35, XXREAL_1:1;
then (f . x) - (g . x) <= (r / 3) - (- (r / 3)) by A34, XREAL_1:14;
hence |.((f - g) . x).| <= (2 * r) / 3 by A24, A36, ABSVALUE:5; :: thesis:

end;