:: TIETZE semantic presentation begin theorem Th1: :: TIETZE:1 for a, b, c being real number st |.(a - b).| <= c holds ( b - c <= a & a <= b + c ) proof let a, b, c be real number ; ::_thesis: ( |.(a - b).| <= c implies ( b - c <= a & a <= b + c ) ) assume A1: |.(a - b).| <= c ; ::_thesis: ( b - c <= a & a <= b + c ) A2: |.(a - b).| >= 0 by COMPLEX1:46; then A3: b <= b + c by A1, XREAL_1:31; A4: b >= b - c by A1, A2, XREAL_1:43; percases ( a - b >= 0 or a - b < 0 ) ; suppose a - b >= 0 ; ::_thesis: ( b - c <= a & a <= b + c ) then ( |.(a - b).| = a - b & a >= 0 + b ) by ABSVALUE:def_1, XREAL_1:19; hence ( b - c <= a & a <= b + c ) by A1, A4, XREAL_1:20, XXREAL_0:2; ::_thesis: verum end; suppose a - b < 0 ; ::_thesis: ( b - c <= a & a <= b + c ) then A5: |.(a - b).| = - (a - b) by ABSVALUE:def_1 .= b - a ; then 0 + a <= b by A2, XREAL_1:19; hence ( b - c <= a & a <= b + c ) by A1, A3, A5, XREAL_1:12, XXREAL_0:2; ::_thesis: verum end; end; end; theorem Th2: :: TIETZE:2 for f, g, h being real-valued Function st f c= g holds h - f c= h - g proof let f, g, h be real-valued Function; ::_thesis: ( f c= g implies h - f c= h - g ) A1: dom (h - g) = (dom h) /\ (dom g) by VALUED_1:12; A2: dom (h - f) = (dom h) /\ (dom f) by VALUED_1:12; assume A3: f c= g ; ::_thesis: h - f c= h - g then dom f c= dom g by GRFUNC_1:2; then A4: dom (h - f) c= dom (h - g) by A1, A2, XBOOLE_1:27; now__::_thesis:_for_x_being_set_st_x_in_dom_(h_-_f)_holds_ (h_-_f)_._x_=_(h_-_g)_._x let x be set ; ::_thesis: ( x in dom (h - f) implies (h - f) . x = (h - g) . x ) assume A5: x in dom (h - f) ; ::_thesis: (h - f) . x = (h - g) . x then A6: x in dom f by A2, XBOOLE_0:def_4; thus (h - f) . x = (h . x) - (f . x) by A5, VALUED_1:13 .= (h . x) - (g . x) by A3, A6, GRFUNC_1:2 .= (h - g) . x by A4, A5, VALUED_1:13 ; ::_thesis: verum end; hence h - f c= h - g by A4, GRFUNC_1:2; ::_thesis: verum end; theorem :: TIETZE:3 for f, g, h being real-valued Function st f c= g holds f - h c= g - h proof let f, g, h be real-valued Function; ::_thesis: ( f c= g implies f - h c= g - h ) A1: dom (f - h) = (dom f) /\ (dom h) by VALUED_1:12; A2: dom (g - h) = (dom g) /\ (dom h) by VALUED_1:12; assume A3: f c= g ; ::_thesis: f - h c= g - h then dom f c= dom g by GRFUNC_1:2; then A4: dom (f - h) c= dom (g - h) by A1, A2, XBOOLE_1:27; now__::_thesis:_for_x_being_set_st_x_in_dom_(f_-_h)_holds_ (f_-_h)_._x_=_(g_-_h)_._x let x be set ; ::_thesis: ( x in dom (f - h) implies (f - h) . x = (g - h) . x ) assume A5: x in dom (f - h) ; ::_thesis: (f - h) . x = (g - h) . x then A6: x in dom f by A1, XBOOLE_0:def_4; thus (f - h) . x = (f . x) - (h . x) by A5, VALUED_1:13 .= (g . x) - (h . x) by A3, A6, GRFUNC_1:2 .= (g - h) . x by A4, A5, VALUED_1:13 ; ::_thesis: verum end; hence f - h c= g - h by A4, GRFUNC_1:2; ::_thesis: verum end; definition let f be real-valued Function; let r be real number ; let X be set ; predf,X is_absolutely_bounded_by r means :Def1: :: TIETZE:def 1 for x being set st x in X /\ (dom f) holds abs (f . x) <= r; end; :: deftheorem Def1 defines is_absolutely_bounded_by TIETZE:def_1_:_ for f being real-valued Function for r being real number for X being set holds ( f,X is_absolutely_bounded_by r iff for x being set st x in X /\ (dom f) holds abs (f . x) <= r ); registration cluster non empty Relation-like NAT -defined REAL -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued summable convergent for Element of K10(K11(NAT,REAL)); existence ex b1 being Real_Sequence st ( b1 is summable & b1 is constant & b1 is convergent ) proof set f = NAT --> 0; reconsider f = NAT --> 0 as Real_Sequence by FUNCOP_1:45; take f ; ::_thesis: ( f is summable & f is constant & f is convergent ) for n being Element of NAT holds f . n = 0 by FUNCOP_1:7; hence f is summable by RSSPACE:16; ::_thesis: ( f is constant & f is convergent ) thus f is constant ; ::_thesis: f is convergent thus f is convergent ; ::_thesis: verum end; end; theorem :: TIETZE:4 for T1 being empty TopSpace for T2 being TopSpace for f being Function of T1,T2 holds f is continuous proof let T1 be empty TopSpace; ::_thesis: for T2 being TopSpace for f being Function of T1,T2 holds f is continuous let T2 be TopSpace; ::_thesis: for f being Function of T1,T2 holds f is continuous let f be Function of T1,T2; ::_thesis: f is continuous let A be Subset of T2; :: according to PRE_TOPC:def_6 ::_thesis: ( not A is closed or f " A is closed ) thus ( not A is closed or f " A is closed ) ; ::_thesis: verum end; theorem :: TIETZE:5 for f, g being summable Real_Sequence st ( for n being Element of NAT holds f . n <= g . n ) holds Sum f <= Sum g proof let f, g be summable Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds f . n <= g . n ) implies Sum f <= Sum g ) A1: ( Sum f = lim (Partial_Sums f) & Sum g = lim (Partial_Sums g) ) by SERIES_1:def_3; assume for n being Element of NAT holds f . n <= g . n ; ::_thesis: Sum f <= Sum g then A2: for n being Element of NAT holds (Partial_Sums f) . n <= (Partial_Sums g) . n by SERIES_1:14; ( Partial_Sums f is convergent & Partial_Sums g is convergent ) by SERIES_1:def_2; hence Sum f <= Sum g by A1, A2, SEQ_2:18; ::_thesis: verum end; theorem Th6: :: TIETZE:6 for f being Real_Sequence st f is absolutely_summable holds abs (Sum f) <= Sum (abs f) proof let f be Real_Sequence; ::_thesis: ( f is absolutely_summable implies abs (Sum f) <= Sum (abs f) ) defpred S1[ Element of NAT ] means (abs (Partial_Sums f)) . \$1 <= (Partial_Sums (abs f)) . \$1; A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then |.((Partial_Sums f) . n).| <= (Partial_Sums (abs f)) . n by SEQ_1:12; then ( |.(((Partial_Sums f) . n) + (f . (n + 1))).| <= |.((Partial_Sums f) . n).| + |.(f . (n + 1)).| & |.((Partial_Sums f) . n).| + |.(f . (n + 1)).| <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| ) by COMPLEX1:56, XREAL_1:6; then |.(((Partial_Sums f) . n) + (f . (n + 1))).| <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| by XXREAL_0:2; then |.((Partial_Sums f) . (n + 1)).| <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| by SERIES_1:def_1; then (abs (Partial_Sums f)) . (n + 1) <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| by SEQ_1:12; then (abs (Partial_Sums f)) . (n + 1) <= ((Partial_Sums (abs f)) . n) + ((abs f) . (n + 1)) by SEQ_1:12; hence S1[n + 1] by SERIES_1:def_1; ::_thesis: verum end; (abs (Partial_Sums f)) . 0 = abs ((Partial_Sums f) . 0) by SEQ_1:12 .= abs (f . 0) by SERIES_1:def_1 .= (abs f) . 0 by SEQ_1:12 ; then A2: S1[ 0 ] by SERIES_1:def_1; A3: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); assume A4: f is absolutely_summable ; ::_thesis: abs (Sum f) <= Sum (abs f) then abs f is summable by SERIES_1:def_4; then A5: Partial_Sums (abs f) is convergent by SERIES_1:def_2; f is summable by A4; then A6: Partial_Sums f is convergent by SERIES_1:def_2; then lim (abs (Partial_Sums f)) <= lim (Partial_Sums (abs f)) by A5, A3, SEQ_2:18; then abs (lim (Partial_Sums f)) <= lim (Partial_Sums (abs f)) by A6, SEQ_4:14; then abs (lim (Partial_Sums f)) <= Sum (abs f) by SERIES_1:def_3; hence abs (Sum f) <= Sum (abs f) by SERIES_1:def_3; ::_thesis: verum end; theorem Th7: :: TIETZE:7 for f being Real_Sequence for a, r being positive real number st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) proof let f be Real_Sequence; ::_thesis: for a, r being positive real number st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) let a, r be positive real number ; ::_thesis: ( r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) implies ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) ) deffunc H1( Nat, Real) -> Element of REAL = (f . (\$1 + 1)) - (f . \$1); consider g being Function of NAT,REAL such that A1: ( g . 0 = f . 0 & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) ) from NAT_1:sch_12(); now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._(n_+_1)_=_(f_._n)_+_(g_._(n_+_1)) let n be Element of NAT ; ::_thesis: f . (n + 1) = (f . n) + (g . (n + 1)) thus f . (n + 1) = ((f . (n + 1)) - (f . n)) + (f . n) .= (f . n) + (g . (n + 1)) by A1 ; ::_thesis: verum end; then A2: f = Partial_Sums g by A1, SERIES_1:def_1; A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(abs_g)_._n let n be Element of NAT ; ::_thesis: 0 <= (abs g) . n (abs g) . n = abs (g . n) by SEQ_1:12; hence 0 <= (abs g) . n by COMPLEX1:46; ::_thesis: verum end; A4: |.r.| = r by COMPLEX1:43; assume A5: r < 1 ; ::_thesis: ( ex n being Nat st not |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) or ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) ) then A6: r GeoSeq is summable by A4, SERIES_1:24; assume A7: for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ; ::_thesis: ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) A8: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_holds_ (abs_g)_._n_<=_((a_*_(r_"))_(#)_(r_GeoSeq))_._n let n be Element of NAT ; ::_thesis: ( 1 <= n implies (abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n ) set m = 1; assume 1 <= n ; ::_thesis: (abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n then consider k being Nat such that A9: n = 1 + k by NAT_1:10; g . n = H1(k,g . k) by A1, A9; then (abs g) . n = |.((f . n) - (f . k)).| by A9, SEQ_1:12 .= |.((f . k) - (f . n)).| by COMPLEX1:60 ; then A10: (abs g) . n <= a * (r to_power k) by A7, A9; (a * 1) * (r to_power k) = (a * ((r ") * r)) * (r to_power k) by XCMPLX_0:def_7 .= (a * (r ")) * (r * (r to_power k)) .= (a * (r ")) * ((r to_power 1) * (r to_power k)) by POWER:25 .= (a * (r ")) * (r to_power n) by A9, POWER:27 .= (a * (r ")) * (r |^ n) by POWER:41 .= (a * (r ")) * ((r GeoSeq) . n) by PREPOWER:def_1 ; hence (abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n by A10, SEQ_1:9; ::_thesis: verum end; (a * (r ")) (#) (r GeoSeq) is summable by A6, SERIES_1:10; then abs g is summable by A3, A8, SERIES_1:19; then A11: g is absolutely_summable by SERIES_1:def_4; then g is summable ; hence f is convergent by A2, SERIES_1:def_2; ::_thesis: for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) let n be Nat; ::_thesis: |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; A12: now__::_thesis:_for_k_being_Element_of_NAT_holds_ (_0_<=_(abs_(g_^\_(n9_+_1)))_._k_&_(abs_(g_^\_(n9_+_1)))_._k_<=_((a_*_(r_to_power_n))_(#)_(r_GeoSeq))_._k_) let k be Element of NAT ; ::_thesis: ( 0 <= (abs (g ^\ (n9 + 1))) . k & (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k ) (abs (g ^\ (n9 + 1))) . k = |.((g ^\ (n9 + 1)) . k).| by SEQ_1:12; hence 0 <= (abs (g ^\ (n9 + 1))) . k by COMPLEX1:46; ::_thesis: (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k (abs (g ^\ (n9 + 1))) . k = |.((g ^\ (n9 + 1)) . k).| by SEQ_1:12 .= |.(g . ((n9 + 1) + k)).| by NAT_1:def_3 .= |.((f . ((n9 + k) + 1)) - (f . (n9 + k))).| by A1 .= |.((f . (n9 + k)) - (f . ((n9 + k) + 1))).| by UNIFORM1:11 ; then (abs (g ^\ (n9 + 1))) . k <= a * (r to_power (n9 + k)) by A7; then (abs (g ^\ (n9 + 1))) . k <= a * ((r to_power n9) * (r to_power k)) by POWER:27; then (abs (g ^\ (n9 + 1))) . k <= (a * (r to_power n9)) * (r to_power k) ; then (abs (g ^\ (n9 + 1))) . k <= (a * (r to_power n9)) * (r |^ k) by POWER:41; then (abs (g ^\ (n9 + 1))) . k <= (a * (r to_power n9)) * ((r GeoSeq) . k) by PREPOWER:def_1; hence (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k by SEQ_1:9; ::_thesis: verum end; A13: (a * (r to_power n)) (#) (r GeoSeq) is summable by A6, SERIES_1:10; then abs (g ^\ (n9 + 1)) is summable by A12, SERIES_1:20; then A14: g ^\ (n9 + 1) is absolutely_summable by SERIES_1:def_4; lim f = Sum g by A2, SERIES_1:def_3; then lim f = (f . n) + (Sum (g ^\ (n9 + 1))) by A2, A11, SERIES_1:15; then A15: |.((lim f) - (f . n)).| <= Sum (abs (g ^\ (n9 + 1))) by A14, Th6; A16: Sum (abs (g ^\ (n9 + 1))) <= Sum ((a * (r to_power n)) (#) (r GeoSeq)) by A13, A12, SERIES_1:20; Sum ((a * (r to_power n)) (#) (r GeoSeq)) = (a * (r to_power n)) * (Sum (r GeoSeq)) by A6, SERIES_1:10 .= (a * (r to_power n)) * (1 / (1 - r)) by A5, A4, SERIES_1:24 .= (a * (r to_power n)) / (1 - r) by XCMPLX_1:99 ; hence |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) by A16, A15, XXREAL_0:2; ::_thesis: verum end; theorem :: TIETZE:8 for f being Real_Sequence for a, r being positive real number st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) proof let f be Real_Sequence; ::_thesis: for a, r being positive real number st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) let a, r be positive real number ; ::_thesis: ( r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) implies ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) ) assume A1: r < 1 ; ::_thesis: ( ex n being Nat st not |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) or ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) ) A2: r to_power 0 = 1 by POWER:24; assume for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ; ::_thesis: ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) then |.((lim f) - (f . 0)).| <= (a * 1) / (1 - r) by A1, A2, Th7; hence ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) by Th1; ::_thesis: verum end; theorem Th9: :: TIETZE:9 for X, Z being non empty set for F being Functional_Sequence of X,REAL st Z common_on_dom F holds for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) proof let X, Z be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL st Z common_on_dom F holds for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) let F be Functional_Sequence of X,REAL; ::_thesis: ( Z common_on_dom F implies for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) ) assume A1: Z common_on_dom F ; ::_thesis: for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) Z c= dom (F . 0) by A1, SEQFUNC:def_9; then reconsider Z9 = Z as non empty Subset of X by XBOOLE_1:1; deffunc H1( Element of Z9) -> Element of REAL = lim (F # \$1); let a, r be positive real number ; ::_thesis: ( r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) implies ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) ) assume A2: r < 1 ; ::_thesis: ( ex n being Nat st not (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) or ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) ) consider f being Function of Z9,REAL such that A3: for x being Element of Z9 holds f . x = H1(x) from FUNCT_2:sch_4(); reconsider f = f as PartFunc of X,REAL by RELSET_1:7; assume A4: for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ; ::_thesis: ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) thus F is_unif_conv_on Z ::_thesis: for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) proof thus Z common_on_dom F by A1; :: according to SEQFUNC:def_12 ::_thesis: ex b1 being Element of K10(K11(X,REAL)) st ( Z = dom b1 & ( for b2 being Element of REAL holds ( b2 <= 0 or ex b3 being Element of NAT st for b4 being Element of NAT for b5 being Element of X holds ( not b3 <= b4 or not b5 in Z or not b2 <= abs (((F . b4) . b5) - (b1 . b5)) ) ) ) ) take f ; ::_thesis: ( Z = dom f & ( for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT for b4 being Element of X holds ( not b2 <= b3 or not b4 in Z or not b1 <= abs (((F . b3) . b4) - (f . b4)) ) ) ) ) thus Z = dom f by FUNCT_2:def_1; ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT for b4 being Element of X holds ( not b2 <= b3 or not b4 in Z or not b1 <= abs (((F . b3) . b4) - (f . b4)) ) ) A5: 1 - r > 0 by A2, XREAL_1:50; let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT for b3 being Element of X holds ( not b1 <= b2 or not b3 in Z or not p <= abs (((F . b2) . b3) - (f . b3)) ) ) assume p > 0 ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT for b3 being Element of X holds ( not b1 <= b2 or not b3 in Z or not p <= abs (((F . b2) . b3) - (f . b3)) ) then p * (1 - r) > 0 by A5, XREAL_1:129; then A6: (p * (1 - r)) / a > 0 by XREAL_1:139; consider k being Element of NAT such that A7: k >= 1 + (log (r,((p * (1 - r)) / a))) by MESFUNC1:8; A8: ( a * ((p * (1 - r)) / a) = (p * (1 - r)) * (a / a) & a / a = 1 ) by XCMPLX_1:60, XCMPLX_1:75; k > log (r,((p * (1 - r)) / a)) by A7, XREAL_1:39; then r to_power k < r to_power (log (r,((p * (1 - r)) / a))) by A2, POWER:40; then r to_power k < (p * (1 - r)) / a by A2, A6, POWER:def_3; then a * (r to_power k) < a * ((p * (1 - r)) / a) by XREAL_1:68; then (a * (r to_power k)) / (1 - r) < (p * (1 - r)) / (1 - r) by A5, A8, XREAL_1:74; then A9: (a * (r to_power k)) / (1 - r) < p by A5, XCMPLX_1:89; take k ; ::_thesis: for b1 being Element of NAT for b2 being Element of X holds ( not k <= b1 or not b2 in Z or not p <= abs (((F . b1) . b2) - (f . b2)) ) let n be Element of NAT ; ::_thesis: for b1 being Element of X holds ( not k <= n or not b1 in Z or not p <= abs (((F . n) . b1) - (f . b1)) ) let x be Element of X; ::_thesis: ( not k <= n or not x in Z or not p <= abs (((F . n) . x) - (f . x)) ) assume that A10: n >= k and A11: x in Z ; ::_thesis: not p <= abs (((F . n) . x) - (f . x)) A12: ( (F . n) . x = (F # x) . n & |.(((F . n) . x) - (f . x)).| = |.((f . x) - ((F . n) . x)).| ) by COMPLEX1:60, SEQFUNC:def_10; now__::_thesis:_for_n_being_Nat_holds_|.(((F_#_x)_._n)_-_((F_#_x)_._(n_+_1))).|_<=_a_*_(r_to_power_n) let n be Nat; ::_thesis: |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) A13: n in NAT by ORDINAL1:def_12; then A14: (F # x) . n = (F . n) . x by SEQFUNC:def_10; A15: Z c= dom (F . (n + 1)) by A1, SEQFUNC:def_9; Z c= dom (F . n) by A1, A13, SEQFUNC:def_9; then x in (dom (F . n)) /\ (dom (F . (n + 1))) by A11, A15, XBOOLE_0:def_4; then x in dom ((F . n) - (F . (n + 1))) by VALUED_1:12; then A16: ( ((F . n) - (F . (n + 1))) . x = ((F . n) . x) - ((F . (n + 1)) . x) & x in Z /\ (dom ((F . n) - (F . (n + 1)))) ) by A11, VALUED_1:13, XBOOLE_0:def_4; (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) by A4; then |.(((F . n) . x) - ((F . (n + 1)) . x)).| <= a * (r to_power n) by A16, Def1; hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) by A14, SEQFUNC:def_10; ::_thesis: verum end; then A17: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A2, Th7; ( n = k or n > k ) by A10, XXREAL_0:1; then r to_power n <= r to_power k by A2, POWER:40; then A18: a * (r to_power n) <= a * (r to_power k) by XREAL_1:64; 1 - r > 1 - 1 by A2, XREAL_1:10; then (a * (r to_power n)) / (1 - r) <= (a * (r to_power k)) / (1 - r) by A18, XREAL_1:72; then A19: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power k)) / (1 - r) by A17, XXREAL_0:2; f . x = lim (F # x) by A3, A11; hence |.(((F . n) . x) - (f . x)).| < p by A9, A19, A12, XXREAL_0:2; ::_thesis: verum end; then A20: F is_point_conv_on Z by SEQFUNC:22; let n9 be Nat; ::_thesis: (lim (F,Z)) - (F . n9),Z is_absolutely_bounded_by (a * (r to_power n9)) / (1 - r) let z be set ; :: according to TIETZE:def_1 ::_thesis: ( z in Z /\ (dom ((lim (F,Z)) - (F . n9))) implies abs (((lim (F,Z)) - (F . n9)) . z) <= (a * (r to_power n9)) / (1 - r) ) reconsider n = n9 as Element of NAT by ORDINAL1:def_12; assume A21: z in Z /\ (dom ((lim (F,Z)) - (F . n9))) ; ::_thesis: abs (((lim (F,Z)) - (F . n9)) . z) <= (a * (r to_power n9)) / (1 - r) then reconsider x = z as Element of X ; A22: z in Z9 by A21, XBOOLE_0:def_4; now__::_thesis:_for_n_being_Nat_holds_|.(((F_#_x)_._n)_-_((F_#_x)_._(n_+_1))).|_<=_a_*_(r_to_power_n) let n be Nat; ::_thesis: |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) A23: (F # x) . (n + 1) = (F . (n + 1)) . x by SEQFUNC:def_10; A24: Z c= dom (F . (n + 1)) by A1, SEQFUNC:def_9; A25: n in NAT by ORDINAL1:def_12; then Z c= dom (F . n) by A1, SEQFUNC:def_9; then z in (dom (F . n)) /\ (dom (F . (n + 1))) by A22, A24, XBOOLE_0:def_4; then A26: x in dom ((F . n) - (F . (n + 1))) by VALUED_1:12; then A27: x in Z /\ (dom ((F . n) - (F . (n + 1)))) by A22, XBOOLE_0:def_4; A28: (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) by A4; (F # x) . n = (F . n) . x by A25, SEQFUNC:def_10; then ((F . n) - (F . (n + 1))) . x = ((F # x) . n) - ((F # x) . (n + 1)) by A26, A23, VALUED_1:13; hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) by A27, A28, Def1; ::_thesis: verum end; then A29: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A2, Th7; Z = dom (lim (F,Z)) by A20, SEQFUNC:def_13; then |.(((lim (F,Z)) . x) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A20, A22, A29, SEQFUNC:def_13; then A30: |.(((lim (F,Z)) . x) - ((F . n) . x)).| <= (a * (r to_power n)) / (1 - r) by SEQFUNC:def_10; z in dom ((lim (F,Z)) - (F . n9)) by A21, XBOOLE_0:def_4; hence abs (((lim (F,Z)) - (F . n9)) . z) <= (a * (r to_power n9)) / (1 - r) by A30, VALUED_1:13; ::_thesis: verum end; theorem Th10: :: TIETZE:10 for X, Z being non empty set for F being Functional_Sequence of X,REAL st Z common_on_dom F holds for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds for z being Element of Z holds ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) proof let X, Z be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL st Z common_on_dom F holds for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds for z being Element of Z holds ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) let F be Functional_Sequence of X,REAL; ::_thesis: ( Z common_on_dom F implies for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds for z being Element of Z holds ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) ) assume A1: Z common_on_dom F ; ::_thesis: for a, r being positive real number st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds for z being Element of Z holds ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) let a, r be positive real number ; ::_thesis: ( r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) implies for z being Element of Z holds ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) ) assume A2: r < 1 ; ::_thesis: ( ex n being Nat st not (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) or for z being Element of Z holds ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) ) assume A3: for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ; ::_thesis: for z being Element of Z holds ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) then F is_point_conv_on Z by A1, A2, Th9, SEQFUNC:22; then A4: dom (lim (F,Z)) = Z by SEQFUNC:def_13; r to_power 0 = 1 by POWER:24; then A5: (lim (F,Z)) - (F . 0),Z is_absolutely_bounded_by (a * 1) / (1 - r) by A1, A2, A3, Th9; let z be Element of Z; ::_thesis: ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) ( z in Z & Z c= dom (F . 0) ) by A1, SEQFUNC:def_9; then z in (dom (lim (F,Z))) /\ (dom (F . 0)) by A4, XBOOLE_0:def_4; then A6: z in dom ((lim (F,Z)) - (F . 0)) by VALUED_1:12; then z in Z /\ (dom ((lim (F,Z)) - (F . 0))) by XBOOLE_0:def_4; then |.(((lim (F,Z)) - (F . 0)) . z).| <= (a * 1) / (1 - r) by A5, Def1; then |.(((lim (F,Z)) . z) - ((F . 0) . z)).| <= (a * 1) / (1 - r) by A6, VALUED_1:13; hence ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) ) by Th1; ::_thesis: verum end; theorem Th11: :: TIETZE:11 for X, Z being non empty set for F being Functional_Sequence of X,REAL st Z common_on_dom F holds for a, r being positive real number for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds ( F is_point_conv_on Z & lim (F,Z) = f ) proof let X, Z be non empty set ; ::_thesis: for F being Functional_Sequence of X,REAL st Z common_on_dom F holds for a, r being positive real number for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds ( F is_point_conv_on Z & lim (F,Z) = f ) let F be Functional_Sequence of X,REAL; ::_thesis: ( Z common_on_dom F implies for a, r being positive real number for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds ( F is_point_conv_on Z & lim (F,Z) = f ) ) assume A1: Z common_on_dom F ; ::_thesis: for a, r being positive real number for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds ( F is_point_conv_on Z & lim (F,Z) = f ) let a, r be positive real number ; ::_thesis: for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds ( F is_point_conv_on Z & lim (F,Z) = f ) let f be Function of Z,REAL; ::_thesis: ( r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) implies ( F is_point_conv_on Z & lim (F,Z) = f ) ) A2: dom f = Z by FUNCT_2:def_1; Z c= dom (F . 0) by A1, SEQFUNC:def_9; then reconsider g = f as PartFunc of X,REAL by A2, RELSET_1:5, XBOOLE_1:1; assume A3: r < 1 ; ::_thesis: ( ex n being Nat st not (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) or ( F is_point_conv_on Z & lim (F,Z) = f ) ) assume A4: for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ; ::_thesis: ( F is_point_conv_on Z & lim (F,Z) = f ) A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_Z_holds_ for_p_being_Real_st_p_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_k_holds_ abs_(((F_._n)_._x)_-_(g_._x))_<_p let x be Element of X; ::_thesis: ( x in Z implies for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((F . n) . x) - (g . x)) < p ) assume A6: x in Z ; ::_thesis: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((F . n) . x) - (g . x)) < p let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((F . n) . x) - (g . x)) < p ) assume A7: p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((F . n) . x) - (g . x)) < p consider k being Element of NAT such that A8: k >= 1 + (log (r,((p * (1 - r)) / a))) by MESFUNC1:8; k > log (r,((p * (1 - r)) / a)) by A8, XREAL_1:39; then A9: r to_power k < r to_power (log (r,((p * (1 - r)) / a))) by A3, POWER:40; A10: ( a * ((p * (1 - r)) / a) = (p * (1 - r)) * (a / a) & a / a = 1 ) by XCMPLX_1:60, XCMPLX_1:75; A11: 1 - r > 0 by A3, XREAL_1:50; then p * (1 - r) > 0 by A7, XREAL_1:129; then (p * (1 - r)) / a > 0 by XREAL_1:139; then r to_power k < (p * (1 - r)) / a by A3, A9, POWER:def_3; then a * (r to_power k) < a * ((p * (1 - r)) / a) by XREAL_1:68; then (a * (r to_power k)) / (1 - r) < (p * (1 - r)) / (1 - r) by A11, A10, XREAL_1:74; then A12: (a * (r to_power k)) / (1 - r) < p by A11, XCMPLX_1:89; take k = k; ::_thesis: for n being Element of NAT st n >= k holds abs (((F . n) . x) - (g . x)) < p let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((F . n) . x) - (g . x)) < p ) Z c= dom (F . n) by A1, SEQFUNC:def_9; then x in (dom (F . n)) /\ (dom f) by A2, A6, XBOOLE_0:def_4; then A13: x in dom ((F . n) - f) by VALUED_1:12; then A14: ((F . n) - f) . x = ((F . n) . x) - (f . x) by VALUED_1:13; assume n >= k ; ::_thesis: abs (((F . n) . x) - (g . x)) < p then ( n = k or n > k ) by XXREAL_0:1; then r to_power n <= r to_power k by A3, POWER:40; then A15: a * (r to_power n) <= a * (r to_power k) by XREAL_1:64; A16: (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) by A4; r to_power n >= 0 by POWER:34; then (a * (r to_power n)) * (1 - r) <= (a * (r to_power n)) * 1 by XREAL_1:43, XREAL_1:64; then A17: (a * (r to_power n)) / 1 <= (a * (r to_power n)) / (1 - r) by A11, XREAL_1:102; 1 - r > 1 - 1 by A3, XREAL_1:10; then (a * (r to_power n)) / (1 - r) <= (a * (r to_power k)) / (1 - r) by A15, XREAL_1:72; then A18: a * (r to_power n) <= (a * (r to_power k)) / (1 - r) by A17, XXREAL_0:2; x in Z /\ (dom ((F . n) - f)) by A13, XBOOLE_0:def_4; then |.(((F . n) . x) - (f . x)).| <= a * (r to_power n) by A14, A16, Def1; then abs (((F . n) . x) - (g . x)) <= (a * (r to_power k)) / (1 - r) by A18, XXREAL_0:2; hence abs (((F . n) . x) - (g . x)) < p by A12, XXREAL_0:2; ::_thesis: verum end; thus A19: F is_point_conv_on Z ::_thesis: lim (F,Z) = f proof thus Z common_on_dom F by A1; :: according to SEQFUNC:def_11 ::_thesis: ex b1 being Element of K10(K11(X,REAL)) st ( Z = dom b1 & ( for b2 being Element of X holds ( not b2 in Z or for b3 being Element of REAL holds ( b3 <= 0 or ex b4 being Element of NAT st for b5 being Element of NAT holds ( not b4 <= b5 or not b3 <= abs (((F . b5) . b2) - (b1 . b2)) ) ) ) ) ) take g ; ::_thesis: ( Z = dom g & ( for b1 being Element of X holds ( not b1 in Z or for b2 being Element of REAL holds ( b2 <= 0 or ex b3 being Element of NAT st for b4 being Element of NAT holds ( not b3 <= b4 or not b2 <= abs (((F . b4) . b1) - (g . b1)) ) ) ) ) ) thus Z = dom g by FUNCT_2:def_1; ::_thesis: for b1 being Element of X holds ( not b1 in Z or for b2 being Element of REAL holds ( b2 <= 0 or ex b3 being Element of NAT st for b4 being Element of NAT holds ( not b3 <= b4 or not b2 <= abs (((F . b4) . b1) - (g . b1)) ) ) ) thus for b1 being Element of X holds ( not b1 in Z or for b2 being Element of REAL holds ( b2 <= 0 or ex b3 being Element of NAT st for b4 being Element of NAT holds ( not b3 <= b4 or not b2 <= abs (((F . b4) . b1) - (g . b1)) ) ) ) by A5; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_lim_(F_#_x) let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim (F # x) ) assume A20: x in dom g ; ::_thesis: g . x = lim (F # x) A21: for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((F # x) . m) - (g . x)) < p proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((F # x) . m) - (g . x)) < p ) reconsider p9 = p as Real by XREAL_0:def_1; assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((F # x) . m) - (g . x)) < p then consider n being Element of NAT such that A22: for m being Element of NAT st n <= m holds abs (((F . m) . x) - (g . x)) < p9 by A2, A5, A20; take n ; ::_thesis: for m being Element of NAT st n <= m holds abs (((F # x) . m) - (g . x)) < p let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((F # x) . m) - (g . x)) < p ) (F . m) . x = (F # x) . m by SEQFUNC:def_10; hence ( n <= m implies abs (((F # x) . m) - (g . x)) < p ) by A22; ::_thesis: verum end; F # x is convergent by A2, A19, A20, SEQFUNC:20; hence g . x = lim (F # x) by A21, SEQ_2:def_7; ::_thesis: verum end; hence lim (F,Z) = f by A2, A19, SEQFUNC:def_13; ::_thesis: verum end; registration let T be TopSpace; let A be closed Subset of T; clusterT | A -> closed ; coherence T | A is closed proof let X be Subset of T; :: according to BORSUK_1:def_11 ::_thesis: ( not X = the carrier of (T | A) or X is closed ) thus ( not X = the carrier of (T | A) or X is closed ) by PRE_TOPC:8; ::_thesis: verum end; end; theorem Th12: :: TIETZE:12 for X, Y being non empty TopSpace for X1, X2 being non empty SubSpace of X for f1 being Function of X1,Y for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds for x being Point of X holds ( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) ) proof let X, Y be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X for f1 being Function of X1,Y for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds for x being Point of X holds ( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) ) let X1, X2 be non empty SubSpace of X; ::_thesis: for f1 being Function of X1,Y for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds for x being Point of X holds ( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) ) let f1 be Function of X1,Y; ::_thesis: for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds for x being Point of X holds ( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) ) let f2 be Function of X2,Y; ::_thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) implies for x being Point of X holds ( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) ) ) assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; ::_thesis: for x being Point of X holds ( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) ) let x be Point of X; ::_thesis: ( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) ) set F = f1 union f2; A2: X1 is SubSpace of X1 union X2 by TSEP_1:22; hereby ::_thesis: ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) assume x in the carrier of X1 ; ::_thesis: (f1 union f2) . x = f1 . x hence (f1 union f2) . x = ((f1 union f2) | the carrier of X1) . x by FUNCT_1:49 .= ((f1 union f2) | X1) . x by A2, TMAP_1:def_5 .= f1 . x by A1, TMAP_1:def_12 ; ::_thesis: verum end; A3: X2 is SubSpace of X1 union X2 by TSEP_1:22; assume x in the carrier of X2 ; ::_thesis: (f1 union f2) . x = f2 . x hence (f1 union f2) . x = ((f1 union f2) | the carrier of X2) . x by FUNCT_1:49 .= ((f1 union f2) | X2) . x by A3, TMAP_1:def_5 .= f2 . x by A1, TMAP_1:def_12 ; ::_thesis: verum end; theorem Th13: :: TIETZE:13 for X, Y being non empty TopSpace for X1, X2 being non empty SubSpace of X for f1 being Function of X1,Y for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds rng (f1 union f2) c= (rng f1) \/ (rng f2) proof let X, Y be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X for f1 being Function of X1,Y for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds rng (f1 union f2) c= (rng f1) \/ (rng f2) let X1, X2 be non empty SubSpace of X; ::_thesis: for f1 being Function of X1,Y for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds rng (f1 union f2) c= (rng f1) \/ (rng f2) let f1 be Function of X1,Y; ::_thesis: for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds rng (f1 union f2) c= (rng f1) \/ (rng f2) let f2 be Function of X2,Y; ::_thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) implies rng (f1 union f2) c= (rng f1) \/ (rng f2) ) set F = f1 union f2; assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; ::_thesis: rng (f1 union f2) c= (rng f1) \/ (rng f2) thus rng (f1 union f2) c= (rng f1) \/ (rng f2) ::_thesis: verum proof A2: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def_2; A3: the carrier of X2 = dom f2 by FUNCT_2:def_1; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f1 union f2) or y in (rng f1) \/ (rng f2) ) A4: the carrier of X1 = dom f1 by FUNCT_2:def_1; assume y in rng (f1 union f2) ; ::_thesis: y in (rng f1) \/ (rng f2) then consider x being set such that A5: x in dom (f1 union f2) and A6: (f1 union f2) . x = y by FUNCT_1:def_3; A7: x is Point of X by A5, PRE_TOPC:25; percases ( x in the carrier of X1 or x in the carrier of X2 ) by A5, A2, XBOOLE_0:def_3; suppose x in the carrier of X1 ; ::_thesis: y in (rng f1) \/ (rng f2) then ( f1 . x in rng f1 & (f1 union f2) . x = f1 . x ) by A1, A4, A7, Th12, FUNCT_1:def_3; hence y in (rng f1) \/ (rng f2) by A6, XBOOLE_0:def_3; ::_thesis: verum end; suppose x in the carrier of X2 ; ::_thesis: y in (rng f1) \/ (rng f2) then ( f2 . x in rng f2 & (f1 union f2) . x = f2 . x ) by A1, A3, A7, Th12, FUNCT_1:def_3; hence y in (rng f1) \/ (rng f2) by A6, XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; theorem Th14: :: TIETZE:14 for X, Y being non empty TopSpace for X1, X2 being non empty SubSpace of X for f1 being Function of X1,Y for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) ) proof let X, Y be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X for f1 being Function of X1,Y for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) ) let X1, X2 be non empty SubSpace of X; ::_thesis: for f1 being Function of X1,Y for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) ) let f1 be Function of X1,Y; ::_thesis: for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) ) let f2 be Function of X2,Y; ::_thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) implies ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) ) ) assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; ::_thesis: ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) ) set F = f1 union f2; A2: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def_2; hereby ::_thesis: for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A let A be Subset of X1; ::_thesis: (f1 union f2) .: A = f1 .: A thus (f1 union f2) .: A = f1 .: A ::_thesis: verum proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: f1 .: A c= (f1 union f2) .: A let y be set ; ::_thesis: ( y in (f1 union f2) .: A implies y in f1 .: A ) assume y in (f1 union f2) .: A ; ::_thesis: y in f1 .: A then consider x being Element of (X1 union X2) such that A3: x in A and A4: y = (f1 union f2) . x by FUNCT_2:65; x is Point of X by PRE_TOPC:25; then (f1 union f2) . x = f1 . x by A1, A3, Th12; hence y in f1 .: A by A3, A4, FUNCT_2:35; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f1 .: A or y in (f1 union f2) .: A ) assume y in f1 .: A ; ::_thesis: y in (f1 union f2) .: A then consider x being Element of X1 such that A5: ( x in A & y = f1 . x ) by FUNCT_2:65; x is Point of X by PRE_TOPC:25; then A6: (f1 union f2) . x = f1 . x by A1, Th12; x in the carrier of (X1 union X2) by A2, XBOOLE_0:def_3; hence y in (f1 union f2) .: A by A5, A6, FUNCT_2:35; ::_thesis: verum end; end; let A be Subset of X2; ::_thesis: (f1 union f2) .: A = f2 .: A hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: f2 .: A c= (f1 union f2) .: A let y be set ; ::_thesis: ( y in (f1 union f2) .: A implies y in f2 .: A ) assume y in (f1 union f2) .: A ; ::_thesis: y in f2 .: A then consider x being Element of (X1 union X2) such that A7: x in A and A8: y = (f1 union f2) . x by FUNCT_2:65; x is Point of X by PRE_TOPC:25; then (f1 union f2) . x = f2 . x by A1, A7, Th12; hence y in f2 .: A by A7, A8, FUNCT_2:35; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f2 .: A or y in (f1 union f2) .: A ) assume y in f2 .: A ; ::_thesis: y in (f1 union f2) .: A then consider x being Element of X2 such that A9: ( x in A & y = f2 . x ) by FUNCT_2:65; x is Point of X by PRE_TOPC:25; then A10: (f1 union f2) . x = f2 . x by A1, Th12; x in the carrier of (X1 union X2) by A2, XBOOLE_0:def_3; hence y in (f1 union f2) .: A by A9, A10, FUNCT_2:35; ::_thesis: verum end; theorem Th15: :: TIETZE:15 for r being real number for X being set for f, g being real-valued Function st f c= g & g,X is_absolutely_bounded_by r holds f,X is_absolutely_bounded_by r proof let r be real number ; ::_thesis: for X being set for f, g being real-valued Function st f c= g & g,X is_absolutely_bounded_by r holds f,X is_absolutely_bounded_by r let X be set ; ::_thesis: for f, g being real-valued Function st f c= g & g,X is_absolutely_bounded_by r holds f,X is_absolutely_bounded_by r let f, g be real-valued Function; ::_thesis: ( f c= g & g,X is_absolutely_bounded_by r implies f,X is_absolutely_bounded_by r ) assume that A1: f c= g and A2: g,X is_absolutely_bounded_by r ; ::_thesis: f,X is_absolutely_bounded_by r let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in X /\ (dom f) implies abs (f . x) <= r ) assume A3: x in X /\ (dom f) ; ::_thesis: abs (f . x) <= r then A4: x in dom f by XBOOLE_0:def_4; A5: x in X by A3, XBOOLE_0:def_4; dom f c= dom g by A1, GRFUNC_1:2; then x in X /\ (dom g) by A4, A5, XBOOLE_0:def_4; then abs (g . x) <= r by A2, Def1; hence abs (f . x) <= r by A1, A4, GRFUNC_1:2; ::_thesis: verum end; theorem Th16: :: TIETZE:16 for r being real number for X being set for f, g being real-valued Function st ( X c= dom f or dom g c= dom f ) & f | X = g | X & f,X is_absolutely_bounded_by r holds g,X is_absolutely_bounded_by r proof let r be real number ; ::_thesis: for X being set for f, g being real-valued Function st ( X c= dom f or dom g c= dom f ) & f | X = g | X & f,X is_absolutely_bounded_by r holds g,X is_absolutely_bounded_by r let X be set ; ::_thesis: for f, g being real-valued Function st ( X c= dom f or dom g c= dom f ) & f | X = g | X & f,X is_absolutely_bounded_by r holds g,X is_absolutely_bounded_by r let f, g be real-valued Function; ::_thesis: ( ( X c= dom f or dom g c= dom f ) & f | X = g | X & f,X is_absolutely_bounded_by r implies g,X is_absolutely_bounded_by r ) assume that A1: ( X c= dom f or dom g c= dom f ) and A2: f | X = g | X and A3: f,X is_absolutely_bounded_by r ; ::_thesis: g,X is_absolutely_bounded_by r let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in X /\ (dom g) implies abs (g . x) <= r ) assume A4: x in X /\ (dom g) ; ::_thesis: abs (g . x) <= r then A5: x in X by XBOOLE_0:def_4; then A6: f . x = (f | X) . x by FUNCT_1:49 .= g . x by A2, A5, FUNCT_1:49 ; x in dom g by A4, XBOOLE_0:def_4; then x in X /\ (dom f) by A1, A5, XBOOLE_0:def_4; hence abs (g . x) <= r by A3, A6, Def1; ::_thesis: verum end; theorem Th17: :: TIETZE:17 for r being real number 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 ) proof let r be real number ; ::_thesis: 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 ) let T be non empty TopSpace; ::_thesis: 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 ) let A be closed Subset of T; ::_thesis: ( r > 0 & T is normal implies 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 ) ) assume that A1: r > 0 and A2: T is normal ; ::_thesis: 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 ) 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: ( f,A is_absolutely_bounded_by r implies 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 ) ) assume A3: for x being set st x in A /\ (dom f) holds abs (f . x) <= r ; :: according to TIETZE:def_1 ::_thesis: 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 ) reconsider r1 = r as Real by XREAL_0:def_1; 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in [.0,1.] ) assume y in rng F ; ::_thesis: y in [.0,1.] then consider x being set 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: verum 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: ( g, dom g is_absolutely_bounded_by r / 3 & f - g,A is_absolutely_bounded_by (2 * r) / 3 ) 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: f - g,A is_absolutely_bounded_by (2 * r) / 3 proof let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in (dom g) /\ (dom g) implies abs (g . x) <= r / 3 ) assume x in (dom g) /\ (dom g) ; ::_thesis: abs (g . x) <= r / 3 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 abs (g . x) <= r / 3 by ABSVALUE:5; ::_thesis: verum end; thus f - g,A is_absolutely_bounded_by (2 * r) / 3 ::_thesis: verum 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: ( x in A /\ (dom (f - g)) implies abs ((f - g) . x) <= (2 * r) / 3 ) assume A22: x in A /\ (dom (f - g)) ; ::_thesis: abs ((f - g) . x) <= (2 * r) / 3 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: abs (f . x) <= r by A3; then A27: - r <= f . x by ABSVALUE:5; percases ( f . x <= - (r / 3) or r / 3 <= f . x or ( - (r / 3) < f . x & f . x < r / 3 ) ) ; supposeA28: f . x <= - (r / 3) ; ::_thesis: abs ((f - g) . x) <= (2 * r) / 3 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 abs ((f - g) . x) <= (2 * r) / 3 by A1, A24, A29, A30, ABSVALUE:5; ::_thesis: verum end; supposeA31: r / 3 <= f . x ; ::_thesis: abs ((f - g) . x) <= (2 * r) / 3 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 abs ((f - g) . x) <= (2 * r) / 3 by A24, A32, A33, ABSVALUE:5; ::_thesis: verum end; supposeA34: ( - (r / 3) < f . x & f . x < r / 3 ) ; ::_thesis: abs ((f - g) . x) <= (2 * r) / 3 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 abs ((f - g) . x) <= (2 * r) / 3 by A24, A36, ABSVALUE:5; ::_thesis: verum end; end; end; end; theorem Th18: :: TIETZE:18 for T being non empty TopSpace st ( for A, B being non empty closed Subset of T st A misses B holds ex f being continuous Function of T,R^1 st ( f .: A = {0} & f .: B = {1} ) ) holds T is normal proof let T be non empty TopSpace; ::_thesis: ( ( for A, B being non empty closed Subset of T st A misses B holds ex f being continuous Function of T,R^1 st ( f .: A = {0} & f .: B = {1} ) ) implies T is normal ) assume A1: for A, B being non empty closed Subset of T st A misses B holds ex f being continuous Function of T,R^1 st ( f .: A = {0} & f .: B = {1} ) ; ::_thesis: T is normal let W, V be Subset of T; :: according to COMPTS_1:def_3 ::_thesis: ( W = {} or V = {} or not W is closed or not V is closed or not W misses V or ex b1, b2 being Element of K10( the carrier of T) st ( b1 is open & b2 is open & W c= b1 & V c= b2 & b1 misses b2 ) ) assume ( W <> {} & V <> {} & W is closed & V is closed & W misses V ) ; ::_thesis: ex b1, b2 being Element of K10( the carrier of T) st ( b1 is open & b2 is open & W c= b1 & V c= b2 & b1 misses b2 ) then consider f being continuous Function of T,R^1 such that A2: f .: W = {0} and A3: f .: V = {1} by A1; set Q = f " (R^1 (right_open_halfline (1 / 2))); set P = f " (R^1 (left_open_halfline (1 / 2))); take f " (R^1 (left_open_halfline (1 / 2))) ; ::_thesis: ex b1 being Element of K10( the carrier of T) st ( f " (R^1 (left_open_halfline (1 / 2))) is open & b1 is open & W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= b1 & f " (R^1 (left_open_halfline (1 / 2))) misses b1 ) take f " (R^1 (right_open_halfline (1 / 2))) ; ::_thesis: ( f " (R^1 (left_open_halfline (1 / 2))) is open & f " (R^1 (right_open_halfline (1 / 2))) is open & W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= f " (R^1 (right_open_halfline (1 / 2))) & f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) ) [#] R^1 <> {} ; hence ( f " (R^1 (left_open_halfline (1 / 2))) is open & f " (R^1 (right_open_halfline (1 / 2))) is open ) by TOPS_2:43; ::_thesis: ( W c= f " (R^1 (left_open_halfline (1 / 2))) & V c= f " (R^1 (right_open_halfline (1 / 2))) & f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) ) A4: R^1 (left_open_halfline (1 / 2)) = left_open_halfline (1 / 2) by TOPREALB:def_3; A5: dom f = the carrier of T by FUNCT_2:def_1; thus W c= f " (R^1 (left_open_halfline (1 / 2))) ::_thesis: ( V c= f " (R^1 (right_open_halfline (1 / 2))) & f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) ) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in W or a in f " (R^1 (left_open_halfline (1 / 2))) ) A6: 0 in left_open_halfline (1 / 2) by XXREAL_1:233; assume A7: a in W ; ::_thesis: a in f " (R^1 (left_open_halfline (1 / 2))) then f . a in f .: W by FUNCT_2:35; then f . a = 0 by A2, TARSKI:def_1; hence a in f " (R^1 (left_open_halfline (1 / 2))) by A4, A5, A7, A6, FUNCT_1:def_7; ::_thesis: verum end; A8: R^1 (right_open_halfline (1 / 2)) = right_open_halfline (1 / 2) by TOPREALB:def_3; thus V c= f " (R^1 (right_open_halfline (1 / 2))) ::_thesis: f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in V or a in f " (R^1 (right_open_halfline (1 / 2))) ) A9: 1 in right_open_halfline (1 / 2) by XXREAL_1:235; assume A10: a in V ; ::_thesis: a in f " (R^1 (right_open_halfline (1 / 2))) then f . a in f .: V by FUNCT_2:35; then f . a = 1 by A3, TARSKI:def_1; hence a in f " (R^1 (right_open_halfline (1 / 2))) by A8, A5, A10, A9, FUNCT_1:def_7; ::_thesis: verum end; thus f " (R^1 (left_open_halfline (1 / 2))) misses f " (R^1 (right_open_halfline (1 / 2))) by A4, A8, FUNCT_1:71, XXREAL_1:275; ::_thesis: verum end; theorem Th19: :: TIETZE:19 for T being non empty TopSpace for f being Function of T,R^1 for x being Point of T holds ( f is_continuous_at x iff for e being real number st e > 0 holds ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) ) proof let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1 for x being Point of T holds ( f is_continuous_at x iff for e being real number st e > 0 holds ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) ) let f be Function of T,R^1; ::_thesis: for x being Point of T holds ( f is_continuous_at x iff for e being real number st e > 0 holds ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) ) let x be Point of T; ::_thesis: ( f is_continuous_at x iff for e being real number st e > 0 holds ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) ) thus ( f is_continuous_at x implies for e being real number st e > 0 holds ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) ) ::_thesis: ( ( for e being real number st e > 0 holds ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) ) implies f is_continuous_at x ) proof reconsider fx = f . x as Point of RealSpace by TOPMETR:12, TOPMETR:def_6; assume A1: f is_continuous_at x ; ::_thesis: for e being real number st e > 0 holds ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) let e be real number ; ::_thesis: ( e > 0 implies ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) ) assume A2: e > 0 ; ::_thesis: ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) reconsider G = Ball (fx,e) as Subset of R^1 by TOPMETR:12, TOPMETR:def_6; ( G is open & fx in G ) by A2, GOBOARD6:1, TOPMETR:14, TOPMETR:def_6; then consider H being Subset of T such that A3: ( H is open & x in H ) and A4: f .: H c= G by A1, TMAP_1:43; take H ; ::_thesis: ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) thus ( H is open & x in H ) by A3; ::_thesis: for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e A5: dom f = the carrier of T by FUNCT_2:def_1; let y be Point of T; ::_thesis: ( y in H implies abs ((f . y) - (f . x)) < e ) assume y in H ; ::_thesis: abs ((f . y) - (f . x)) < e then A6: f . y in f .: H by A5, FUNCT_1:def_6; then f . y in G by A4; then reconsider fy = f . y as Point of RealSpace ; dist (fy,fx) < e by A4, A6, METRIC_1:11; hence abs ((f . y) - (f . x)) < e by TOPMETR:11; ::_thesis: verum end; assume A7: for e being real number st e > 0 holds ex H being Subset of T st ( H is open & x in H & ( for y being Point of T st y in H holds abs ((f . y) - (f . x)) < e ) ) ; ::_thesis: f is_continuous_at x now__::_thesis:_for_G_being_Subset_of_R^1_st_G_is_open_&_f_._x_in_G_holds_ ex_H_being_Subset_of_T_st_ (_H_is_open_&_x_in_H_&_f_.:_H_c=_G_) reconsider fx = f . x as Point of RealSpace by TOPMETR:12, TOPMETR:def_6; let G be Subset of R^1; ::_thesis: ( G is open & f . x in G implies ex H being Subset of T st ( H is open & x in H & f .: H c= G ) ) assume ( G is open & f . x in G ) ; ::_thesis: ex H being Subset of T st ( H is open & x in H & f .: H c= G ) then consider r being real number such that A8: r > 0 and A9: Ball (fx,r) c= G by TOPMETR:15, TOPMETR:def_6; consider H being Subset of T such that A10: ( H is open & x in H ) and A11: for y being Point of T st y in H holds abs ((f . y) - (f . x)) < r by A7, A8; take H = H; ::_thesis: ( H is open & x in H & f .: H c= G ) thus ( H is open & x in H ) by A10; ::_thesis: f .: H c= G thus f .: H c= G ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: H or a in G ) assume a in f .: H ; ::_thesis: a in G then consider y being set such that A12: y in dom f and A13: y in H and A14: a = f . y by FUNCT_1:def_6; reconsider y = y as Point of T by A12; reconsider fy = f . y as Point of RealSpace by TOPMETR:12, TOPMETR:def_6; abs ((f . y) - (f . x)) < r by A11, A13; then abs (- ((f . y) - (f . x))) < r by COMPLEX1:52; then abs ((f . x) - (f . y)) < r ; then dist (fx,fy) < r by TOPMETR:11; then fy in Ball (fx,r) by METRIC_1:11; hence a in G by A9, A14; ::_thesis: verum end; end; hence f is_continuous_at x by TMAP_1:43; ::_thesis: verum end; theorem Th20: :: TIETZE:20 for T being non empty TopSpace for F being Functional_Sequence of the carrier of T,REAL st F is_unif_conv_on the carrier of T & ( for i being Element of NAT holds F . i is continuous Function of T,R^1 ) holds lim (F, the carrier of T) is continuous Function of T,R^1 proof let T be non empty TopSpace; ::_thesis: for F being Functional_Sequence of the carrier of T,REAL st F is_unif_conv_on the carrier of T & ( for i being Element of NAT holds F . i is continuous Function of T,R^1 ) holds lim (F, the carrier of T) is continuous Function of T,R^1 let F be Functional_Sequence of the carrier of T,REAL; ::_thesis: ( F is_unif_conv_on the carrier of T & ( for i being Element of NAT holds F . i is continuous Function of T,R^1 ) implies lim (F, the carrier of T) is continuous Function of T,R^1 ) assume that A1: F is_unif_conv_on the carrier of T and A2: for i being Element of NAT holds F . i is continuous Function of T,R^1 ; ::_thesis: lim (F, the carrier of T) is continuous Function of T,R^1 F is_point_conv_on the carrier of T by A1, SEQFUNC:43; then dom (lim (F, the carrier of T)) = the carrier of T by SEQFUNC:def_13; then reconsider l = lim (F, the carrier of T) as Function of T,R^1 by FUNCT_2:def_1, TOPMETR:17; now__::_thesis:_for_p_being_Point_of_T_holds_l_is_continuous_at_p let p be Point of T; ::_thesis: l is_continuous_at p now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_ ex_H_being_Subset_of_T_st_ (_H_is_open_&_p_in_H_&_(_for_y_being_Point_of_T_st_y_in_H_holds_ abs_((l_._y)_-_(l_._p))_<_e_)_) let e be real number ; ::_thesis: ( e > 0 implies ex H being Subset of T st ( H is open & p in H & ( for y being Point of T st y in H holds abs ((l . y) - (l . p)) < e ) ) ) assume A3: e > 0 ; ::_thesis: ex H being Subset of T st ( H is open & p in H & ( for y being Point of T st y in H holds abs ((l . y) - (l . p)) < e ) ) reconsider e3 = e / 3 as Real ; A4: e3 > 0 by A3, XREAL_1:139; then consider k being Element of NAT such that A5: for n being Element of NAT for x being Point of T st n >= k & x in the carrier of T holds abs (((F . n) . x) - ((lim (F, the carrier of T)) . x)) < e3 by A1, SEQFUNC:43; reconsider Fk = F . k as continuous Function of T,R^1 by A2; A6: abs ((Fk . p) - (l . p)) < e3 by A5; Fk is_continuous_at p by TMAP_1:44; then consider H being Subset of T such that A7: ( H is open & p in H ) and A8: for y being Point of T st y in H holds abs ((Fk . y) - (Fk . p)) < e3 by A4, Th19; take H = H; ::_thesis: ( H is open & p in H & ( for y being Point of T st y in H holds abs ((l . y) - (l . p)) < e ) ) thus ( H is open & p in H ) by A7; ::_thesis: for y being Point of T st y in H holds abs ((l . y) - (l . p)) < e let y be Point of T; ::_thesis: ( y in H implies abs ((l . y) - (l . p)) < e ) assume A9: y in H ; ::_thesis: abs ((l . y) - (l . p)) < e abs ((Fk . y) - (l . y)) < e3 by A5; then abs (- ((Fk . y) - (l . y))) < e3 by COMPLEX1:52; then ( abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))) <= (abs ((Fk . p) - (l . p))) + (abs (- ((Fk . y) - (l . y)))) & (abs ((Fk . p) - (l . p))) + (abs (- ((Fk . y) - (l . y)))) < e3 + e3 ) by A6, COMPLEX1:56, XREAL_1:8; then abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))) < 2 * e3 by XXREAL_0:2; then ( abs (((Fk . y) - (Fk . p)) + (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))) <= (abs ((Fk . y) - (Fk . p))) + (abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))) & (abs ((Fk . y) - (Fk . p))) + (abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))) < e3 + (2 * e3) ) by A8, A9, COMPLEX1:56, XREAL_1:8; hence abs ((l . y) - (l . p)) < e by XXREAL_0:2; ::_thesis: verum end; hence l is_continuous_at p by Th19; ::_thesis: verum end; hence lim (F, the carrier of T) is continuous Function of T,R^1 by TMAP_1:44; ::_thesis: verum end; theorem Th21: :: TIETZE:21 for T being non empty TopSpace for f being Function of T,R^1 for r being positive real number holds ( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) ) proof let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1 for r being positive real number holds ( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) ) let f be Function of T,R^1; ::_thesis: for r being positive real number holds ( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) ) let r be positive real number ; ::_thesis: ( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) ) A1: dom f = the carrier of T by FUNCT_2:def_1; thus ( f, the carrier of T is_absolutely_bounded_by r implies f is Function of T,(Closed-Interval-TSpace ((- r),r)) ) ::_thesis: ( f is Function of T,(Closed-Interval-TSpace ((- r),r)) implies f, the carrier of T is_absolutely_bounded_by r ) proof assume A2: f, the carrier of T is_absolutely_bounded_by r ; ::_thesis: f is Function of T,(Closed-Interval-TSpace ((- r),r)) now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_T_holds_ f_._x_in_the_carrier_of_(Closed-Interval-TSpace_((-_r),r)) let x be set ; ::_thesis: ( x in the carrier of T implies f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) ) assume x in the carrier of T ; ::_thesis: f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) then x in the carrier of T /\ (dom f) by A1; then abs (f . x) <= r by A2, Def1; then 2 * (abs (f . x)) <= 2 * r by XREAL_1:64; then (abs 2) * (abs (f . x)) <= 2 * r by ABSVALUE:def_1; then (abs (- 2)) * (abs (f . x)) <= 2 * r by COMPLEX1:52; then abs ((- 2) * (f . x)) <= r - (- r) by COMPLEX1:65; then abs (((- r) + r) - (2 * (f . x))) <= r - (- r) ; then f . x in [.(- r),r.] by RCOMP_1:2; hence f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) by TOPMETR:18; ::_thesis: verum end; hence f is Function of T,(Closed-Interval-TSpace ((- r),r)) by A1, FUNCT_2:3; ::_thesis: verum end; assume A3: f is Function of T,(Closed-Interval-TSpace ((- r),r)) ; ::_thesis: f, the carrier of T is_absolutely_bounded_by r let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in the carrier of T /\ (dom f) implies abs (f . x) <= r ) assume x in the carrier of T /\ (dom f) ; ::_thesis: abs (f . x) <= r then f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) by A3, FUNCT_2:5; then f . x in [.(- r),r.] by TOPMETR:18; then abs (((- r) + r) - (2 * (f . x))) <= r - (- r) by RCOMP_1:2; then abs ((- 2) * (f . x)) <= r - (- r) ; then (abs (- 2)) * (abs (f . x)) <= 2 * r by COMPLEX1:65; then (abs 2) * (abs (f . x)) <= 2 * r by COMPLEX1:52; then 2 * (abs (f . x)) <= 2 * r by ABSVALUE:def_1; then (2 * (abs (f . x))) / 2 <= (2 * r) / 2 by XREAL_1:72; hence abs (f . x) <= r ; ::_thesis: verum end; theorem Th22: :: TIETZE:22 for r being real number for X being set for f, g being real-valued Function st f - g,X is_absolutely_bounded_by r holds g - f,X is_absolutely_bounded_by r proof let r be real number ; ::_thesis: for X being set for f, g being real-valued Function st f - g,X is_absolutely_bounded_by r holds g - f,X is_absolutely_bounded_by r let X be set ; ::_thesis: for f, g being real-valued Function st f - g,X is_absolutely_bounded_by r holds g - f,X is_absolutely_bounded_by r let f, g be real-valued Function; ::_thesis: ( f - g,X is_absolutely_bounded_by r implies g - f,X is_absolutely_bounded_by r ) assume A1: f - g,X is_absolutely_bounded_by r ; ::_thesis: g - f,X is_absolutely_bounded_by r let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in X /\ (dom (g - f)) implies abs ((g - f) . x) <= r ) assume A2: x in X /\ (dom (g - f)) ; ::_thesis: abs ((g - f) . x) <= r then A3: x in dom (g - f) by XBOOLE_0:def_4; A4: dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12 .= dom (g - f) by VALUED_1:12 ; then abs ((f - g) . x) <= r by A1, A2, Def1; then abs ((f . x) - (g . x)) <= r by A4, A3, VALUED_1:13; then abs (- ((f . x) - (g . x))) <= r by COMPLEX1:52; then abs ((g . x) - (f . x)) <= r ; hence abs ((g - f) . x) <= r by A3, VALUED_1:13; ::_thesis: verum end; theorem :: TIETZE:23 for T being non empty TopSpace st T is normal holds for A being closed Subset of T for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f proof let T be non empty TopSpace; ::_thesis: ( T is normal implies for A being closed Subset of T for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f ) assume A1: T is normal ; ::_thesis: for A being closed Subset of T for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f let A be closed Subset of T; ::_thesis: for f being Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) st f is continuous holds ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f let f be Function of (T | A),(Closed-Interval-TSpace ((- 1),1)); ::_thesis: ( f is continuous implies ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f ) assume A2: f is continuous ; ::_thesis: ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f A3: the carrier of (T | A) = A by PRE_TOPC:8; A4: the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:18; percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f then reconsider A1 = A as empty Subset of T ; set g = T --> (R^1 0); T --> (R^1 0) = the carrier of T --> 0 by TOPREALB:def_2; then A5: rng (T --> (R^1 0)) = {0} by FUNCOP_1:8; rng (T --> (R^1 0)) c= the carrier of (Closed-Interval-TSpace ((- 1),1)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (T --> (R^1 0)) or y in the carrier of (Closed-Interval-TSpace ((- 1),1)) ) assume y in rng (T --> (R^1 0)) ; ::_thesis: y in the carrier of (Closed-Interval-TSpace ((- 1),1)) then y = 0 by A5, TARSKI:def_1; hence y in the carrier of (Closed-Interval-TSpace ((- 1),1)) by A4, XXREAL_1:1; ::_thesis: verum end; then reconsider g = T --> (R^1 0) as Function of T,(Closed-Interval-TSpace ((- 1),1)) by FUNCT_2:6; reconsider g = g as continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) by PRE_TOPC:27; take g ; ::_thesis: g | A = f g | A1 is empty ; hence g | A = f ; ::_thesis: verum end; suppose not A is empty ; ::_thesis: ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f then reconsider A1 = A as non empty Subset of T ; set DF = Funcs ( the carrier of T, the carrier of R^1); set D = { q where q is Element of Funcs ( the carrier of T, the carrier of R^1) : q is continuous Function of T,R^1 } ; reconsider f1 = f as Function of (T | A1),R^1 by TOPREALA:7; defpred S1[ Element of NAT , set , set ] means ex E2 being continuous Function of T,R^1 st ( E2 = \$2 & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ \$1) implies ex g being continuous Function of T,R^1 st ( \$3 = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (\$1 + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (\$1 + 1)) ) ) ); A6: 2 / 3 > 0 ; f1 is continuous by A2, PRE_TOPC:26; then reconsider f1 = f as continuous Function of (T | A1),R^1 ; T --> (R^1 0) is Element of Funcs ( the carrier of T, the carrier of R^1) by FUNCT_2:8; then T --> (R^1 0) in { q where q is Element of Funcs ( the carrier of T, the carrier of R^1) : q is continuous Function of T,R^1 } ; then reconsider D = { q where q is Element of Funcs ( the carrier of T, the carrier of R^1) : q is continuous Function of T,R^1 } as non empty set ; f1,A is_absolutely_bounded_by 1 proof let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in A /\ (dom f1) implies abs (f1 . x) <= 1 ) assume x in A /\ (dom f1) ; ::_thesis: abs (f1 . x) <= 1 then x in dom f1 by XBOOLE_0:def_4; then A7: f1 . x in rng f1 by FUNCT_1:def_3; rng f1 c= the carrier of (Closed-Interval-TSpace ((- 1),1)) by RELAT_1:def_19; then ( - 1 <= f1 . x & f1 . x <= 1 ) by A4, A7, XXREAL_1:1; hence abs (f1 . x) <= 1 by ABSVALUE:5; ::_thesis: verum end; then consider g0 being continuous Function of T,R^1 such that A8: g0, dom g0 is_absolutely_bounded_by 1 / 3 and A9: f1 - g0,A is_absolutely_bounded_by (2 * 1) / 3 by A1, Th17; g0 in Funcs ( the carrier of T, the carrier of R^1) by FUNCT_2:8; then g0 in D ; then reconsider g0d = g0 as Element of D ; A10: for n being Element of NAT for x being Element of D ex y being Element of D st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of D ex y being Element of D st S1[n,x,y] let x be Element of D; ::_thesis: ex y being Element of D st S1[n,x,y] x in D ; then consider E2 being Element of Funcs ( the carrier of T, the carrier of R^1) such that A11: E2 = x and A12: E2 is continuous Function of T,R^1 ; reconsider E2 = E2 as continuous Function of T,R^1 by A12; percases ( not f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) or f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ) ; supposeA13: not f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; ::_thesis: ex y being Element of D st S1[n,x,y] take x ; ::_thesis: S1[n,x,x] take E2 ; ::_thesis: ( E2 = x & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st ( x = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) ) thus ( E2 = x & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st ( x = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) ) by A11, A13; ::_thesis: verum end; supposeA14: f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; ::_thesis: ex y being Element of D st S1[n,x,y] reconsider E2b = E2 | A as Function of (T | A1),R^1 by PRE_TOPC:9; reconsider E2b = E2b as continuous Function of (T | A1),R^1 by TOPMETR:7; E2b c= E2 by RELAT_1:59; then A15: f - E2b,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) by A14, Th2, Th15; set r = (2 / 3) * ((2 / 3) |^ n); reconsider f1c = f1, E2c = E2b as continuous RealMap of (T | A1) by JORDAN5A:27, TOPMETR:17; set k = f1 - E2b; reconsider E2a = E2 as RealMap of T by TOPMETR:17; reconsider E2a = E2a as continuous RealMap of T by JORDAN5A:27; f1c - E2c is continuous RealMap of (T | A1) ; then reconsider k = f1 - E2b as continuous Function of (T | A1),R^1 by JORDAN5A:27, TOPMETR:17; reconsider f1c = f1c, E2c = E2c as continuous RealMap of (T | A1) ; A16: ( dom f = the carrier of (T | A) & dom E2b = the carrier of (T | A) ) by FUNCT_2:def_1; (2 / 3) |^ n > 0 by NEWTON:83; then (2 / 3) * ((2 / 3) |^ n) > (2 / 3) * 0 by XREAL_1:68; then (2 / 3) * ((2 / 3) |^ n) > 0 ; then consider g being continuous Function of T,R^1 such that A17: g, dom g is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ n)) / 3 and A18: k - g,A is_absolutely_bounded_by (2 * ((2 / 3) * ((2 / 3) |^ n))) / 3 by A1, A15, Th17; reconsider ga = g as RealMap of T by TOPMETR:17; reconsider ga = ga as continuous RealMap of T by JORDAN5A:27; set y = E2a + ga; reconsider y1 = E2a + ga as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17; ( y1 in Funcs ( the carrier of T, the carrier of R^1) & y1 is continuous Function of T,R^1 ) by FUNCT_2:8; then E2a + ga in D ; then reconsider y = E2a + ga as Element of D ; take y ; ::_thesis: S1[n,x,y] take E2 ; ::_thesis: ( E2 = x & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st ( y = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) ) thus E2 = x by A11; ::_thesis: ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st ( y = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) assume f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) ; ::_thesis: ex g being continuous Function of T,R^1 st ( y = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) take g ; ::_thesis: ( y = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) thus y = E2 + g ; ::_thesis: ( g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) A19: (2 / 3) * ((2 / 3) |^ n) = (2 / 3) |^ (n + 1) by NEWTON:6; hence g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) by A17, FUNCT_2:def_1; ::_thesis: (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) A20: dom g = the carrier of T by FUNCT_2:def_1; A21: ((f - E2b) - g) | A = ((f - E2b) | A) - g by RFUNCT_1:47 .= (f - (E2b | A)) - g by RFUNCT_1:47 .= (f - (E2 | A)) - g by RELAT_1:72 .= ((f - E2) | A) - g by RFUNCT_1:47 .= ((f - E2) - g) | A by RFUNCT_1:47 ; dom ((f - E2b) - g) = (dom (f - E2b)) /\ (dom g) by VALUED_1:12 .= ((dom f) /\ (dom E2b)) /\ (dom g) by VALUED_1:12 .= A by A3, A16, A20, XBOOLE_1:28 ; hence (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) by A18, A19, A21, Th16; ::_thesis: verum end; end; end; consider F being Function of NAT,D such that A22: F . 0 = g0d and A23: for n being Element of NAT holds S1[n,F . n,F . (n + 1)] from RECDEF_1:sch_2(A10); A24: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_PartFunc_of_the_carrier_of_T,REAL let n be Element of NAT ; ::_thesis: F . n is PartFunc of the carrier of T,REAL S1[n,F . n,F . (n + 1)] by A23; hence F . n is PartFunc of the carrier of T,REAL by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6; ::_thesis: verum end; dom F = NAT by FUNCT_2:def_1; then reconsider F = F as Functional_Sequence of the carrier of T,REAL by A24, SEQFUNC:1; consider E2 being continuous Function of T,R^1 such that A25: E2 = F . 0 and A26: ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ 0) implies ex g being continuous Function of T,R^1 st ( F . (0 + 1) = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (0 + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (0 + 1)) ) ) by A23; (2 / 3) |^ 0 = 1 by NEWTON:4; then consider g1 being continuous Function of T,R^1 such that A27: F . (0 + 1) = E2 + g1 and A28: g1, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (0 + 1)) and (f - E2) - g1,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (0 + 1)) by A9, A22, A25, A26; A29: dom g1 = the carrier of T by FUNCT_2:def_1 .= dom E2 by FUNCT_2:def_1 ; defpred S2[ Nat] means ( F . \$1 is continuous Function of T,R^1 & (F . \$1) - (F . (\$1 + 1)), the carrier of T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power \$1) & (F . \$1) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power \$1) ); A30: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_ S2[n_+_1] let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) A31: dom f = [#] (T | A1) by FUNCT_2:def_1 .= A by PRE_TOPC:def_5 ; consider E2 being continuous Function of T,R^1 such that A32: ( E2 = F . n & ( f - E2,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) implies ex g being continuous Function of T,R^1 st ( F . (n + 1) = E2 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) & (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) ) ) ) by A23; assume S2[n] ; ::_thesis: S2[n + 1] then (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ n) by POWER:41; then consider g being continuous Function of T,R^1 such that A33: F . (n + 1) = E2 + g and g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ (n + 1)) and A34: (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) by A32, Th22; A35: dom ((f - E2) - g) = (dom (f - E2)) /\ (dom g) by VALUED_1:12 .= ((dom f) /\ (dom E2)) /\ (dom g) by VALUED_1:12 .= ((dom f) /\ the carrier of T) /\ (dom g) by FUNCT_2:def_1 .= (dom f) /\ (dom g) by A31, XBOOLE_1:28 .= (dom f) /\ the carrier of T by FUNCT_2:def_1 .= A by A31, XBOOLE_1:28 ; reconsider g9 = g as continuous RealMap of T by JORDAN5A:27, METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6; consider E3 being continuous Function of T,R^1 such that A36: E3 = F . (n + 1) and A37: ( f - E3,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ (n + 1)) implies ex g being continuous Function of T,R^1 st ( F . ((n + 1) + 1) = E3 + g & g, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ ((n + 1) + 1)) & (f - E3) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ ((n + 1) + 1)) ) ) by A23; A38: dom (f - (E2 + g)) = (dom f) /\ (dom (E2 + g)) by VALUED_1:12 .= A /\ ((dom E2) /\ (dom g)) by A31, VALUED_1:def_1 .= A /\ ((dom E2) /\ the carrier of T) by FUNCT_2:def_1 .= A /\ ( the carrier of T /\ the carrier of T) by FUNCT_2:def_1 .= A by XBOOLE_1:28 ; A39: dom (f - E2) = A /\ (dom E2) by A31, VALUED_1:12 .= A /\ the carrier of T by FUNCT_2:def_1 .= A by XBOOLE_1:28 ; A40: now__::_thesis:_for_a_being_set_st_a_in_A_holds_ ((f_-_E2)_-_g)_._a_=_(f_-_(E2_+_g))_._a let a be set ; ::_thesis: ( a in A implies ((f - E2) - g) . a = (f - (E2 + g)) . a ) assume A41: a in A ; ::_thesis: ((f - E2) - g) . a = (f - (E2 + g)) . a hence ((f - E2) - g) . a = ((f - E2) . a) - (g . a) by A35, VALUED_1:13 .= ((f . a) - (E2 . a)) - (g . a) by A39, A41, VALUED_1:13 .= (f . a) - ((E2 . a) + (g . a)) .= (f . a) - ((E2 + g) . a) by A41, VALUED_1:1 .= (f - (E2 + g)) . a by A38, A41, VALUED_1:13 ; ::_thesis: verum end; then consider gx being continuous Function of T,R^1 such that A42: F . ((n + 1) + 1) = E3 + gx and A43: gx, the carrier of T is_absolutely_bounded_by (1 / 3) * ((2 / 3) |^ ((n + 1) + 1)) and (f - E3) - gx,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) |^ ((n + 1) + 1)) by A33, A34, A36, A37, A35, A38, FUNCT_1:2; A44: dom gx = the carrier of T by FUNCT_2:def_1 .= dom E3 by FUNCT_2:def_1 ; reconsider E29 = E2 as continuous RealMap of T by JORDAN5A:27, METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6; A45: (2 / 9) * ((2 / 3) to_power (n + 1)) = ((1 / 3) * (2 / 3)) * ((2 / 3) |^ (n + 1)) by POWER:41 .= (1 / 3) * ((2 / 3) * ((2 / 3) |^ (n + 1))) .= (1 / 3) * ((2 / 3) |^ ((n + 1) + 1)) by NEWTON:6 ; A46: dom ((gx + E3) - E3) = (dom (gx + E3)) /\ (dom E3) by VALUED_1:12 .= ((dom gx) /\ (dom E3)) /\ (dom E3) by VALUED_1:def_1 .= dom gx by A44 ; now__::_thesis:_for_a_being_set_st_a_in_dom_gx_holds_ ((gx_+_E3)_-_E3)_._a_=_gx_._a let a be set ; ::_thesis: ( a in dom gx implies ((gx + E3) - E3) . a = gx . a ) assume A47: a in dom gx ; ::_thesis: ((gx + E3) - E3) . a = gx . a hence ((gx + E3) - E3) . a = ((gx + E3) . a) - (E3 . a) by A46, VALUED_1:13 .= ((gx . a) + (E3 . a)) - (E3 . a) by A47, VALUED_1:1 .= gx . a ; ::_thesis: verum end; then A48: (F . ((n + 1) + 1)) - (F . (n + 1)) = gx by A36, A42, A46, FUNCT_1:2; (f - E2) - g,A is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1)) by A34, POWER:41; then ( E29 + g9 is continuous RealMap of T & f - (F . (n + 1)),A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power (n + 1)) ) by A33, A35, A38, A40, FUNCT_1:2; hence S2[n + 1] by A33, A43, A45, A48, Th22, JORDAN5A:27, METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6; ::_thesis: verum end; A49: dom ((g1 + E2) - E2) = (dom (g1 + E2)) /\ (dom E2) by VALUED_1:12 .= ((dom g1) /\ (dom E2)) /\ (dom E2) by VALUED_1:def_1 .= dom g1 by A29 ; now__::_thesis:_for_a_being_set_st_a_in_dom_g1_holds_ ((g1_+_E2)_-_E2)_._a_=_g1_._a let a be set ; ::_thesis: ( a in dom g1 implies ((g1 + E2) - E2) . a = g1 . a ) assume A50: a in dom g1 ; ::_thesis: ((g1 + E2) - E2) . a = g1 . a hence ((g1 + E2) - E2) . a = ((g1 + E2) . a) - (E2 . a) by A49, VALUED_1:13 .= ((g1 . a) + (E2 . a)) - (E2 . a) by A50, VALUED_1:1 .= g1 . a ; ::_thesis: verum end; then A51: (F . (0 + 1)) - (F . 0) = g1 by A25, A27, A49, FUNCT_1:2; ( (2 / 3) to_power 0 = 1 & (1 / 3) * ((2 / 3) |^ 1) = (1 / 3) * (2 / 3) ) by NEWTON:5, POWER:24; then A52: S2[ 0 ] by A9, A22, A28, A51, Th22; A53: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A52, A30); A54: now__::_thesis:_for_n_being_Nat_holds_(F_._n)_-_(F_._(n_+_1)),_the_carrier_of_T_is_absolutely_bounded_by_(2_/_9)_*_((2_/_3)_to_power_n) let n be Nat; ::_thesis: (F . n) - (F . (n + 1)), the carrier of T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power n) n in NAT by ORDINAL1:def_12; hence (F . n) - (F . (n + 1)), the carrier of T is_absolutely_bounded_by (2 / 9) * ((2 / 3) to_power n) by A53; ::_thesis: verum end; ( dom f = the carrier of (T | A1) & rng f c= REAL ) by FUNCT_2:def_1, VALUED_0:def_3; then A55: f is Function of A1,REAL by A3, FUNCT_2:2; now__::_thesis:_for_n_being_Element_of_NAT_holds_the_carrier_of_T_c=_dom_(F_._n) let n be Element of NAT ; ::_thesis: the carrier of T c= dom (F . n) S1[n,F . n,F . (n + 1)] by A23; hence the carrier of T c= dom (F . n) by FUNCT_2:def_1; ::_thesis: verum end; then A56: the carrier of T common_on_dom F by SEQFUNC:def_9; then A57: A1 common_on_dom F by SEQFUNC:23; A58: now__::_thesis:_for_n_being_Nat_holds_(F_._n)_-_f,A1_is_absolutely_bounded_by_(2_/_3)_*_((2_/_3)_to_power_n) let n be Nat; ::_thesis: (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power n) n in NAT by ORDINAL1:def_12; hence (F . n) - f,A1 is_absolutely_bounded_by (2 / 3) * ((2 / 3) to_power n) by A53; ::_thesis: verum end; A59: 2 / 9 > 0 ; then F is_unif_conv_on the carrier of T by A56, A6, A54, Th9; then reconsider h = lim (F, the carrier of T) as continuous Function of T,R^1 by A53, Th20; F is_point_conv_on the carrier of T by A56, A59, A6, A54, Th9, SEQFUNC:22; then A60: h | A1 = lim (F,A1) by SEQFUNC:24 .= f by A6, A58, A57, A55, Th11 ; h, the carrier of T is_absolutely_bounded_by 1 proof let x be set ; :: according to TIETZE:def_1 ::_thesis: ( x in the carrier of T /\ (dom h) implies abs (h . x) <= 1 ) assume x in the carrier of T /\ (dom h) ; ::_thesis: abs (h . x) <= 1 then reconsider z = x as Element of T ; A61: dom (F . 0) = the carrier of T by A22, FUNCT_2:def_1; then z in the carrier of T /\ (dom (F . 0)) ; then A62: |.((F . 0) . z).| <= 1 / 3 by A8, A22, A61, Def1; then (F . 0) . z >= - (1 / 3) by ABSVALUE:5; then A63: ((F . 0) . z) - ((2 / 9) / (1 - (2 / 3))) >= (- (1 / 3)) - ((2 / 9) / (1 - (2 / 3))) by XREAL_1:9; (F . 0) . z <= 1 / 3 by A62, ABSVALUE:5; then A64: ((F . 0) . z) + ((2 / 9) / (1 - (2 / 3))) <= (1 / 3) + ((2 / 9) / (1 - (2 / 3))) by XREAL_1:7; h . z <= ((F . 0) . z) + ((2 / 9) / (1 - (2 / 3))) by A56, A59, A6, A54, Th10; then A65: h . z <= 1 by A64, XXREAL_0:2; h . z >= ((F . 0) . z) - ((2 / 9) / (1 - (2 / 3))) by A56, A59, A6, A54, Th10; then h . z >= - 1 by A63, XXREAL_0:2; hence abs (h . x) <= 1 by A65, ABSVALUE:5; ::_thesis: verum end; then reconsider h = h as Function of T,(Closed-Interval-TSpace ((- 1),1)) by Th21; R^1 [.(- 1),1.] = [#] (Closed-Interval-TSpace ((- 1),1)) by A4, TOPREALB:def_3; then Closed-Interval-TSpace ((- 1),1) = R^1 | (R^1 [.(- 1),1.]) by PRE_TOPC:def_5; then h is continuous by TOPMETR:6; hence ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f by A60; ::_thesis: verum end; end; end; theorem :: TIETZE:24 for T being non empty TopSpace st ( for A being non empty closed Subset of T for f being continuous Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f ) holds T is normal proof let T be non empty TopSpace; ::_thesis: ( ( for A being non empty closed Subset of T for f being continuous Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f ) implies T is normal ) assume A1: for A being non empty closed Subset of T for f being continuous Function of (T | A),(Closed-Interval-TSpace ((- 1),1)) ex g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) st g | A = f ; ::_thesis: T is normal for C, D being non empty closed Subset of T st C misses D holds ex f being continuous Function of T,R^1 st ( f .: C = {0} & f .: D = {1} ) proof set f2 = T --> (R^1 1); set f1 = T --> (R^1 0); let C, D be non empty closed Subset of T; ::_thesis: ( C misses D implies ex f being continuous Function of T,R^1 st ( f .: C = {0} & f .: D = {1} ) ) assume A2: C misses D ; ::_thesis: ex f being continuous Function of T,R^1 st ( f .: C = {0} & f .: D = {1} ) set g1 = (T --> (R^1 0)) | (T | C); set g2 = (T --> (R^1 1)) | (T | D); set f = ((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)); A3: the carrier of (T | D) = D by PRE_TOPC:8; (T --> (R^1 1)) | (T | D) = (T --> (R^1 1)) | the carrier of (T | D) by TMAP_1:def_4; then A4: rng ((T --> (R^1 1)) | (T | D)) c= rng (T --> (R^1 1)) by RELAT_1:70; (T --> (R^1 0)) | (T | C) = (T --> (R^1 0)) | the carrier of (T | C) by TMAP_1:def_4; then rng ((T --> (R^1 0)) | (T | C)) c= rng (T --> (R^1 0)) by RELAT_1:70; then A5: (rng ((T --> (R^1 0)) | (T | C))) \/ (rng ((T --> (R^1 1)) | (T | D))) c= (rng (T --> (R^1 0))) \/ (rng (T --> (R^1 1))) by A4, XBOOLE_1:13; A6: T --> (R^1 0) = the carrier of T --> 0 by TOPREALB:def_2; then A7: rng (T --> (R^1 0)) = {0} by FUNCOP_1:8; A8: T --> (R^1 1) = the carrier of T --> 1 by TOPREALB:def_2; then A9: rng (T --> (R^1 1)) = {1} by FUNCOP_1:8; A10: the carrier of (T | C) = C by PRE_TOPC:8; then A11: T | C misses T | D by A2, A3, TSEP_1:def_3; then rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= (rng ((T --> (R^1 0)) | (T | C))) \/ (rng ((T --> (R^1 1)) | (T | D))) by Th13; then A12: rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= (rng (T --> (R^1 0))) \/ (rng (T --> (R^1 1))) by A5, XBOOLE_1:1; A13: rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) c= [.(- 1),1.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) or x in [.(- 1),1.] ) assume x in rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) ; ::_thesis: x in [.(- 1),1.] then ( x in {0} or x in {1} ) by A12, A7, A9, XBOOLE_0:def_3; then ( x = 0 or x = 1 ) by TARSKI:def_1; hence x in [.(- 1),1.] by XXREAL_1:1; ::_thesis: verum end; the carrier of (T | (C \/ D)) = C \/ D by PRE_TOPC:8; then A14: T | (C \/ D) = (T | C) union (T | D) by A10, A3, TSEP_1:def_2; A15: (T --> (R^1 1)) .: D = {1} proof thus (T --> (R^1 1)) .: D c= {1} by A8, FUNCOP_1:81; :: according to XBOOLE_0:def_10 ::_thesis: {1} c= (T --> (R^1 1)) .: D let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {1} or y in (T --> (R^1 1)) .: D ) consider c being set such that A16: c in D by XBOOLE_0:def_1; assume y in {1} ; ::_thesis: y in (T --> (R^1 1)) .: D then A17: y = 1 by TARSKI:def_1; ( dom (T --> (R^1 1)) = the carrier of T & (T --> (R^1 1)) . c = 1 ) by A8, A16, FUNCOP_1:7, FUNCOP_1:13; hence y in (T --> (R^1 1)) .: D by A17, A16, FUNCT_1:def_6; ::_thesis: verum end; A18: D c= D ; A19: (T --> (R^1 0)) .: C = {0} proof thus (T --> (R^1 0)) .: C c= {0} by A6, FUNCOP_1:81; :: according to XBOOLE_0:def_10 ::_thesis: {0} c= (T --> (R^1 0)) .: C let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {0} or y in (T --> (R^1 0)) .: C ) consider c being set such that A20: c in C by XBOOLE_0:def_1; assume y in {0} ; ::_thesis: y in (T --> (R^1 0)) .: C then A21: y = 0 by TARSKI:def_1; ( dom (T --> (R^1 0)) = the carrier of T & (T --> (R^1 0)) . c = 0 ) by A6, A20, FUNCOP_1:7, FUNCOP_1:13; hence y in (T --> (R^1 0)) .: C by A21, A20, FUNCT_1:def_6; ::_thesis: verum end; A22: C \/ D is closed by TOPS_1:9; the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.] by TOPMETR:18; then reconsider h = ((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)) as Function of (T | (C \/ D)),(Closed-Interval-TSpace ((- 1),1)) by A14, A13, FUNCT_2:6; ((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)) is continuous Function of ((T | C) union (T | D)),R^1 by A11, TMAP_1:136; then h is continuous by A14, PRE_TOPC:27; then consider g being continuous Function of T,(Closed-Interval-TSpace ((- 1),1)) such that A23: g | (C \/ D) = ((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)) by A1, A22; reconsider F = g as continuous Function of T,R^1 by PRE_TOPC:26, TOPREALA:7; take F ; ::_thesis: ( F .: C = {0} & F .: D = {1} ) A24: C c= C ; thus F .: C = (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: C by A23, FUNCT_2:97, XBOOLE_1:7 .= ((T --> (R^1 0)) | (T | C)) .: C by A10, A11, A24, Th14 .= ((T --> (R^1 0)) | C) .: C by A10, TMAP_1:def_3 .= {0} by A19, RELAT_1:129 ; ::_thesis: F .: D = {1} thus F .: D = (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: D by A23, FUNCT_2:97, XBOOLE_1:7 .= ((T --> (R^1 1)) | (T | D)) .: D by A3, A11, A18, Th14 .= ((T --> (R^1 1)) | D) .: D by A3, TMAP_1:def_3 .= {1} by A15, RELAT_1:129 ; ::_thesis: verum end; hence T is normal by Th18; ::_thesis: verum end;