tietze.miz

    begin

    reserve r for Real,

X for set,

f,g,h for real-valued Function;

    theorem :: TIETZE:1



     Th1: for a,b,c be Real st |.(a - b).| <= c holds (b - c) <= a & a <= (b + c)

    proof

      let a,b,c be Real;

      assume

       A1: |.(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;

      per cases ;

        suppose (a - b) >= 0 ;

        then |.(a - b).| = (a - b) & a >= ( 0 qua Nat + b) by ABSVALUE:def 1, XREAL_1: 19;

        hence thesis by A1, A4, XREAL_1: 20, XXREAL_0: 2;

      end;

        suppose (a - b) < 0 ;



        then

         A5: |.(a - b).| = ( - (a - b)) by ABSVALUE:def 1

        .= (b - a);

        then ( 0 qua Nat + a) <= b by A2, XREAL_1: 19;

        hence thesis by A1, A3, A5, XREAL_1: 12, XXREAL_0: 2;

      end;

    end;

    theorem :: TIETZE:2



     Th2: f c= g implies (h - f) c= (h - g)

    proof



       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;

      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

        let x be object;

        assume

         A5: x in ( dom (h - f));

        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;

      end;

      hence thesis by A4, GRFUNC_1: 2;

    end;

    theorem :: TIETZE:3

    f c= g implies (f - h) c= (g - h)

    proof



       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;

      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

        let x be object;

        assume

         A5: x in ( dom (f - h));

        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;

      end;

      hence thesis by A4, GRFUNC_1: 2;

    end;

    definition

      let f be real-valued Function, r be Real, X be set;

      :: TIETZE:def1

      pred f,X is_absolutely_bounded_by r means for x be set st x in (X /\ ( dom f)) holds |.(f . x).| <= r;

    end

    registration

      cluster summable constant convergent for Real_Sequence;

      existence

      proof

        take f = ( seq_const 0 );

        for n be Nat holds (f . n) = 0 ;

        hence f is summable by RSSPACE: 16;

        thus f is constant;

        thus thesis;

      end;

    end

    theorem :: TIETZE:4

    for T1 be empty TopSpace, T2 be TopSpace holds for f be Function of T1, T2 holds f is continuous

    proof

      let T1 be empty TopSpace, T2 be TopSpace;

      let f be Function of T1, T2;

      let A be Subset of T2;

      thus thesis;

    end;

    theorem :: TIETZE:5

    for f,g be summable Real_Sequence st for n be Nat holds (f . n) <= (g . n) holds ( Sum f) <= ( Sum g)

    proof

      let f,g be summable Real_Sequence;



       A1: ( Sum f) = ( lim ( Partial_Sums f)) & ( Sum g) = ( lim ( Partial_Sums g)) by SERIES_1:def 3;

      assume for n be Nat holds (f . n) <= (g . n);

      then

       A2: for n be 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 thesis by A1, A2, SEQ_2: 18;

    end;

    theorem :: TIETZE:6



     Th6: for f be Real_Sequence st f is absolutely_summable holds |.( Sum f).| <= ( Sum ( abs f))

    proof

      let f be Real_Sequence;

      defpred P[ Nat] means (( abs ( Partial_Sums f)) . $1) <= (( Partial_Sums ( abs f)) . $1);

       A1:

      now

        let n be Nat;

        assume P[n];

        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 P[(n + 1)] by SERIES_1:def 1;

      end;

      (( abs ( Partial_Sums f)) . 0 ) = |.(( Partial_Sums f) . 0 ).| by SEQ_1: 12

      .= |.(f . 0 ).| by SERIES_1:def 1

      .= (( abs f) . 0 ) by SEQ_1: 12;

      then

       A2: P[ 0 ] by SERIES_1:def 1;



       A3: for n be Nat holds P[n] from NAT_1:sch 2( A2, A1);

      assume

       A4: f is absolutely_summable;

      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 |.( lim ( Partial_Sums f)).| <= ( lim ( Partial_Sums ( abs f))) by A6, SEQ_4: 14;

      then |.( lim ( Partial_Sums f)).| <= ( Sum ( abs f)) by SERIES_1:def 3;

      hence thesis by SERIES_1:def 3;

    end;

    theorem :: TIETZE:7



     Th7: for f be Real_Sequence holds for a,r be positive Real st r < 1 & for n be Nat holds |.((f . n) - (f . (n + 1))).| <= (a * (r to_power n)) holds f is convergent & for n be Nat holds |.(( lim f) - (f . n)).| <= ((a * (r to_power n)) / (1 - r))

    proof

      let f be Real_Sequence;

      let a,r be positive Real;

      deffunc S( Nat, Real) = ( In (((f . ($1 + 1)) - (f . $1)), REAL ));

      consider g be sequence of REAL such that

       A1: (g . 0 ) = (f . 0 ) & for n be Nat holds (g . (n + 1)) = S(n,.) from NAT_1:sch 12;

      now

        let n be Nat;



         A2: (g . (n + 1)) = S(n,.) by A1;



        thus (f . (n + 1)) = (((f . (n + 1)) - (f . n)) + (f . n))

        .= ((f . n) + (g . (n + 1))) by A2;

      end;

      then

       A3: f = ( Partial_Sums g) by A1, SERIES_1:def 1;

       A4:

      now

        let n be Nat;

        (( abs g) . n) = |.(g . n).| by SEQ_1: 12;

        hence 0 <= (( abs g) . n) by COMPLEX1: 46;

      end;



       A5: |.r.| = r by COMPLEX1: 43;

      assume

       A6: r < 1;

      then

       A7: (r GeoSeq ) is summable by A5, SERIES_1: 24;

      assume

       A8: for n be Nat holds |.((f . n) - (f . (n + 1))).| <= (a * (r to_power n));

       A9:

      now

        let n be Nat;

        set m = 1;

        assume m <= n;

        then

        consider k be Nat such that

         A10: n = (1 + k) by NAT_1: 10;

        (g . n) = S(k,.) by A1, A10;



        then (( abs g) . n) = |.((f . n) - (f . k)).| by A10, SEQ_1: 12

        .= |.((f . k) - (f . n)).| by COMPLEX1: 60;

        then

         A11: (( abs g) . n) <= (a * (r to_power k)) by A8, A10;

        ((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 A10, 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 A11, SEQ_1: 9;

      end;

      ((a * (r " )) (#) (r GeoSeq )) is summable by A7, SERIES_1: 10;

      then ( abs g) is summable by A4, A9, SERIES_1: 19;

      then

       A12: g is absolutely_summable by SERIES_1:def 4;

      then g is summable;

      hence f is convergent by A3, SERIES_1:def 2;

      let n be Nat;

      reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

       A13:

      now

        let k be Nat;

        reconsider kk = k as Element of NAT by ORDINAL1:def 12;

        (( abs (g ^\ (n9 + 1))) . k) = |.((g ^\ (n9 + 1)) . k).| by SEQ_1: 12;

        hence 0 <= (( abs (g ^\ (n9 + 1))) . k) by COMPLEX1: 46;

        (( abs (g ^\ (n9 + 1))) . k) = |.((g ^\ (n9 + 1)) . k).| by SEQ_1: 12

        .= |.(g . ((n9 + 1) + k)).| by NAT_1:def 3

        .= |. S(+,.).| by A1

        .= |.((f . ((n9 + k) + 1)) - (f . (n9 + k))).|

        .= |.((f . (n9 + k)) - (f . ((n9 + k) + 1))).| by UNIFORM1: 11;

        then (( abs (g ^\ (n9 + 1))) . k) <= (a * (r to_power (n9 + kk))) by A8;

        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;

      end;



       A14: ((a * (r to_power n)) (#) (r GeoSeq )) is summable by A7, SERIES_1: 10;

      then ( abs (g ^\ (n9 + 1))) is summable by A13, SERIES_1: 20;

      then

       A15: (g ^\ (n9 + 1)) is absolutely_summable by SERIES_1:def 4;

      ( lim f) = ( Sum g) by A3, SERIES_1:def 3;

      then ( lim f) = ((f . n) + ( Sum (g ^\ (n9 + 1)))) by A3, A12, SERIES_1: 15;

      then

       A16: |.(( lim f) - (f . n)).| <= ( Sum ( abs (g ^\ (n9 + 1)))) by A15, Th6;



       A17: ( Sum ( abs (g ^\ (n9 + 1)))) <= ( Sum ((a * (r to_power n)) (#) (r GeoSeq ))) by A14, A13, SERIES_1: 20;

      ( Sum ((a * (r to_power n)) (#) (r GeoSeq ))) = ((a * (r to_power n)) * ( Sum (r GeoSeq ))) by A7, SERIES_1: 10

      .= ((a * (r to_power n)) * (1 / (1 - r))) by A6, A5, SERIES_1: 24

      .= ((a * (r to_power n)) / (1 - r)) by XCMPLX_1: 99;

      hence thesis by A17, A16, XXREAL_0: 2;

    end;

    theorem :: TIETZE:8

    for f be Real_Sequence holds for a,r be positive Real st r < 1 & for n be 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;

      let a,r be positive Real;

      assume

       A1: r < 1;



       A2: (r to_power 0 ) = 1 by POWER: 24;

      assume for n be Nat holds |.((f . n) - (f . (n + 1))).| <= (a * (r to_power n));

      then |.(( lim f) - (f . 0 )).| <= ((a * 1) / (1 - r)) by A1, A2, Th7;

      hence thesis by Th1;

    end;

    theorem :: TIETZE:9



     Th9: for X,Z be non empty set holds for F be Functional_Sequence of X, REAL st Z common_on_dom F holds for a,r be positive Real st r < 1 & for n be 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 be 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;

      let F be Functional_Sequence of X, REAL such that

       A1: Z common_on_dom F;

      Z c= ( dom (F . 0 )) by A1;

      then

      reconsider Z9 = Z as non empty Subset of X by XBOOLE_1: 1;

      deffunc ff( Element of Z9) = ( In (( lim (F # $1)), REAL ));

      let a,r be positive Real such that

       A2: r < 1;

      consider f be Function of Z9, REAL such that

       A3: for x be Element of Z9 holds (f . x) = ff(x) from FUNCT_2:sch 4;

      reconsider f as PartFunc of X, REAL by RELSET_1: 7;

      assume

       A4: for n be Nat holds (((F . n) - (F . (n + 1))),Z) is_absolutely_bounded_by (a * (r to_power n));

      thus F is_unif_conv_on Z

      proof

        thus Z common_on_dom F by A1;

        take f;

        thus Z = ( dom f) by FUNCT_2:def 1;



         A5: (1 - r) > 0 by A2, XREAL_1: 50;

        let p be Real;

        assume p > 0 ;

        then (p * (1 - r)) > 0 by A5, XREAL_1: 129;

        then

         A6: ((p * (1 - r)) / a) > 0 by XREAL_1: 139;

        consider k be 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;

        let n be Nat, x be Element of X;

        assume that

         A10: n >= k and

         A11: x in Z;



         A12: ((F . n) . x) = ((F # x) . n) & |.(((F . n) . x) - (f . x)).| = |.((f . x) - ((F . n) . x)).| by COMPLEX1: 60, SEQFUNC:def 10;

        now

          let n be Nat;



           A13: ((F # x) . n) = ((F . n) . x) by SEQFUNC:def 10;



           A14: Z c= ( dom (F . (n + 1))) by A1;

          Z c= ( dom (F . n)) by A1;

          then x in (( dom (F . n)) /\ ( dom (F . (n + 1)))) by A11, A14, XBOOLE_0:def 4;

          then x in ( dom ((F . n) - (F . (n + 1)))) by VALUED_1: 12;

          then

           A15: (((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 A15;

          hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= (a * (r to_power n)) by A13, SEQFUNC:def 10;

        end;

        then

         A16: |.(( 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

         A17: (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 A17, XREAL_1: 72;

        then

         A18: |.(( lim (F # x)) - ((F # x) . n)).| <= ((a * (r to_power k)) / (1 - r)) by A16, XXREAL_0: 2;

        reconsider xx = x as Element of Z9 by A11;

        (f . x) = ff(xx) by A3;

        hence |.(((F . n) . x) - (f . x)).| < p by A9, A18, A12, XXREAL_0: 2;

      end;

      then

       A19: F is_point_conv_on Z by SEQFUNC: 22;

      let n9 be Nat, z be set;

      reconsider n = n9 as Element of NAT by ORDINAL1:def 12;

      assume

       A20: z in (Z /\ ( dom (( lim (F,Z)) - (F . n9))));

      then

      reconsider x = z as Element of X;



       A21: z in Z9 by A20, XBOOLE_0:def 4;

      now

        let n be Nat;



         A22: ((F # x) . (n + 1)) = ((F . (n + 1)) . x) by SEQFUNC:def 10;



         A23: Z c= ( dom (F . (n + 1))) by A1;

        Z c= ( dom (F . n)) by A1;

        then z in (( dom (F . n)) /\ ( dom (F . (n + 1)))) by A21, A23, XBOOLE_0:def 4;

        then

         A24: x in ( dom ((F . n) - (F . (n + 1)))) by VALUED_1: 12;

        then

         A25: x in (Z /\ ( dom ((F . n) - (F . (n + 1))))) by A21, XBOOLE_0:def 4;



         A26: (((F . n) - (F . (n + 1))),Z) is_absolutely_bounded_by (a * (r to_power n)) by A4;

        ((F # x) . n) = ((F . n) . x) by SEQFUNC:def 10;

        then (((F . n) - (F . (n + 1))) . x) = (((F # x) . n) - ((F # x) . (n + 1))) by A24, A22, VALUED_1: 13;

        hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= (a * (r to_power n)) by A25, A26;

      end;

      then

       A27: |.(( lim (F # x)) - ((F # x) . n)).| <= ((a * (r to_power n)) / (1 - r)) by A2, Th7;

      Z = ( dom ( lim (F,Z))) by A19, SEQFUNC:def 13;

      then |.((( lim (F,Z)) . x) - ((F # x) . n)).| <= ((a * (r to_power n)) / (1 - r)) by A19, A21, A27, SEQFUNC:def 13;

      then

       A28: |.((( 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 A20, XBOOLE_0:def 4;

      hence thesis by A28, VALUED_1: 13;

    end;

    theorem :: TIETZE:10



     Th10: for X,Z be non empty set holds for F be Functional_Sequence of X, REAL st Z common_on_dom F holds for a,r be positive Real st r < 1 & for n be Nat holds (((F . n) - (F . (n + 1))),Z) is_absolutely_bounded_by (a * (r to_power n)) holds for z be 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;

      let F be Functional_Sequence of X, REAL ;

      assume

       A1: Z common_on_dom F;

      let a,r be positive Real;

      assume

       A2: r < 1;

      assume

       A3: for n be Nat holds (((F . n) - (F . (n + 1))),Z) is_absolutely_bounded_by (a * (r to_power n));

      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;

      z in Z & Z c= ( dom (F . 0 )) by A1;

      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;

      then |.((( lim (F,Z)) . z) - ((F . 0 ) . z)).| <= ((a * 1) / (1 - r)) by A6, VALUED_1: 13;

      hence thesis by Th1;

    end;

    theorem :: TIETZE:11



     Th11: for X,Z be non empty set holds for F be Functional_Sequence of X, REAL st Z common_on_dom F holds for a,r be positive Real holds for f be Function of Z, REAL st r < 1 & for n be 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;

      let F be Functional_Sequence of X, REAL ;

      assume

       A1: Z common_on_dom F;

      let a,r be positive Real;

      let f be Function of Z, REAL ;



       A2: ( dom f) = Z by FUNCT_2:def 1;

      Z c= ( dom (F . 0 )) by A1;

      then

      reconsider g = f as PartFunc of X, REAL by A2, RELSET_1: 5, XBOOLE_1: 1;

      assume

       A3: r < 1;

      assume

       A4: for n be Nat holds (((F . n) - f),Z) is_absolutely_bounded_by (a * (r to_power n));

       A5:

      now

        let x be Element of X such that

         A6: x in Z;

        let p be Real such that

         A7: p > 0 ;

        consider k be 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;

        reconsider k as Nat;

        take k;

        let n be Nat;

        Z c= ( dom (F . n)) by A1;

        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;

        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;

        then |.(((F . n) . x) - (g . x)).| <= ((a * (r to_power k)) / (1 - r)) by A18, XXREAL_0: 2;

        hence |.(((F . n) . x) - (g . x)).| < p by A12, XXREAL_0: 2;

      end;

      thus

       A19: F is_point_conv_on Z

      proof

        thus Z common_on_dom F by A1;

        take g;

        thus Z = ( dom g) by FUNCT_2:def 1;

        thus thesis by A5;

      end;

      now

        let x be Element of X;

        assume

         A20: x in ( dom g);



         A21: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.(((F # x) . m) - (g . x)).| < p

        proof

          let p be Real;

          reconsider p9 = p as Real;

          assume 0 < p;

          then

          consider n be Nat such that

           A22: for m be Nat st n <= m holds |.(((F . m) . x) - (g . x)).| < p9 by A2, A5, A20;

          reconsider n as Nat;

          take n;

          let m be Nat;

          ((F . m) . x) = ((F # x) . m) by SEQFUNC:def 10;

          hence thesis by A22;

        end;

        (F # x) is convergent by A2, A19, A20, SEQFUNC: 20;

        hence (g . x) = ( lim (F # x)) by A21, SEQ_2:def 7;

      end;

      hence thesis by A2, A19, SEQFUNC:def 13;

    end;

    registration

      let T be TopSpace, A be closed Subset of T;

      cluster (T | A) -> closed;

      coherence by PRE_TOPC: 8;

    end

    theorem :: TIETZE:12



     Th12: for X,Y be non empty TopSpace, X1,X2 be non empty SubSpace of X holds for f1 be Function of X1, Y, f2 be Function of X2, Y st X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2)) holds for x be 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, X1,X2 be non empty SubSpace of X;

      let f1 be Function of X1, Y, f2 be Function of X2, Y;

      assume

       A1: X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2));

      let x be Point of X;

      set F = (f1 union f2);



       A2: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      hereby

        assume x in the carrier of X1;



        hence (F . x) = ((F | the carrier of X1) . x) by FUNCT_1: 49

        .= ((F | X1) . x) by A2, TMAP_1:def 5

        .= (f1 . x) by A1, TMAP_1:def 12;

      end;



       A3: X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

      assume x in the carrier of X2;



      hence (F . x) = ((F | the carrier of X2) . x) by FUNCT_1: 49

      .= ((F | X2) . x) by A3, TMAP_1:def 5

      .= (f2 . x) by A1, TMAP_1:def 12;

    end;

    theorem :: TIETZE:13



     Th13: for X,Y be non empty TopSpace, X1,X2 be non empty SubSpace of X holds for f1 be Function of X1, Y, f2 be 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, X1,X2 be non empty SubSpace of X;

      let f1 be Function of X1, Y, f2 be Function of X2, Y;

      set F = (f1 union f2);

      assume

       A1: X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2));

      thus ( rng F) c= (( rng f1) \/ ( rng f2))

      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 object;



         A4: the carrier of X1 = ( dom f1) by FUNCT_2:def 1;

        assume y in ( rng F);

        then

        consider x be object such that

         A5: x in ( dom F) and

         A6: (F . x) = y by FUNCT_1:def 3;



         A7: x is Point of X by A5, PRE_TOPC: 25;

        per cases by A5, A2, XBOOLE_0:def 3;

          suppose x in the carrier of X1;

          then (f1 . x) in ( rng f1) & (F . x) = (f1 . x) by A1, A4, A7, Th12, FUNCT_1:def 3;

          hence thesis by A6, XBOOLE_0:def 3;

        end;

          suppose x in the carrier of X2;

          then (f2 . x) in ( rng f2) & (F . x) = (f2 . x) by A1, A3, A7, Th12, FUNCT_1:def 3;

          hence thesis by A6, XBOOLE_0:def 3;

        end;

      end;

    end;

    theorem :: TIETZE:14



     Th14: for X,Y be non empty TopSpace, X1,X2 be non empty SubSpace of X holds for f1 be Function of X1, Y, f2 be Function of X2, Y st X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2)) holds (for A be Subset of X1 holds ((f1 union f2) .: A) = (f1 .: A)) & for A be Subset of X2 holds ((f1 union f2) .: A) = (f2 .: A)

    proof

      let X,Y be non empty TopSpace, X1,X2 be non empty SubSpace of X;

      let f1 be Function of X1, Y, f2 be Function of X2, Y;

      assume

       A1: X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2));

      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

        let A be Subset of X1;

        thus ((f1 union f2) .: A) = (f1 .: A)

        proof

          hereby

            let y be object;

            assume y in ((f1 union f2) .: A);

            then

            consider x be Element of (X1 union X2) such that

             A3: x in A and

             A4: y = (F . x) by FUNCT_2: 65;

            x is Point of X by PRE_TOPC: 25;

            then (F . x) = (f1 . x) by A1, A3, Th12;

            hence y in (f1 .: A) by A3, A4, FUNCT_2: 35;

          end;

          let y be object;

          assume y in (f1 .: A);

          then

          consider x be 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: (F . x) = (f1 . x) by A1, Th12;

          x in the carrier of (X1 union X2) by A2, XBOOLE_0:def 3;

          hence thesis by A5, A6, FUNCT_2: 35;

        end;

      end;

      let A be Subset of X2;

      hereby

        let y be object;

        assume y in ((f1 union f2) .: A);

        then

        consider x be Element of (X1 union X2) such that

         A7: x in A and

         A8: y = (F . x) by FUNCT_2: 65;

        x is Point of X by PRE_TOPC: 25;

        then (F . x) = (f2 . x) by A1, A7, Th12;

        hence y in (f2 .: A) by A7, A8, FUNCT_2: 35;

      end;

      let y be object;

      assume y in (f2 .: A);

      then

      consider x be 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: (F . x) = (f2 . x) by A1, Th12;

      x in the carrier of (X1 union X2) by A2, XBOOLE_0:def 3;

      hence thesis by A9, A10, FUNCT_2: 35;

    end;

    theorem :: TIETZE:15



     Th15: f c= g & (g,X) is_absolutely_bounded_by r implies (f,X) is_absolutely_bounded_by r

    proof

      assume that

       A1: f c= g and

       A2: (g,X) is_absolutely_bounded_by r;

      let x be set;

      assume

       A3: x in (X /\ ( dom f));

      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 |.(g . x).| <= r by A2;

      hence thesis by A1, A4, GRFUNC_1: 2;

    end;

    theorem :: TIETZE:16



     Th16: (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

    proof

      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;

      let x be set;

      assume

       A4: x in (X /\ ( dom g));

      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 thesis by A3, A6;

    end;

    reserve T for non empty TopSpace,

A for closed Subset of T;

    theorem :: TIETZE:17



     Th17: r > 0 & T is normal implies for f be continuous Function of (T | A), R^1 st (f,A) is_absolutely_bounded_by r holds ex g be 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

      assume that

       A1: r > 0 and

       A2: T is normal;

      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 such that

       A3: for x be set st x in (A /\ ( dom f)) holds |.(f . x).| <= r;

      reconsider r1 = r as Real;

      set e = ((2 * r1) / 3);

       0 < (2 * r) by A1, XREAL_1: 129;

      then e > 0 by XREAL_1: 139;

      then

      consider h be Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace (((e * 0 ) + ( - (r1 / 3))),((e * 1) + ( - (r1 / 3))))) such that

       A4: h is being_homeomorphism and

       A5: for w be Real st w in [. 0 , 1.] holds (h . w) = ((e * 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 " C1) is closed & (f " C2) is closed by PRE_TOPC:def 6;

      then

      reconsider D1 = (f " C1), D2 = (f " C2) as closed Subset of T by PRE_TOPC: 11, TSEP_1: 12;



       A8: A1 = C1 by TOPREALB:def 3;



       A9: A2 = C2 by TOPREALB:def 3;



       A10: ( - ( - (r / 3))) > 0 by A1, XREAL_1: 139;

      then (f " A1) misses (f " A2) by FUNCT_1: 71, XXREAL_1: 279;

      then

      consider F be Function of T, R^1 such that

       A11: F is continuous and

       A12: for x be Point of T holds 0 <= (F . x) & (F . x) <= 1 & (x in D1 implies (F . x) = 0 ) & (x in D2 implies (F . x) = 1) by A2, A8, A9, URYSOHN3: 20;



       A13: ( rng F) c= [. 0 , 1.]

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A14: x in ( dom F) and

         A15: (F . x) = y by FUNCT_1:def 3;

         0 <= (F . x) & (F . x) <= 1 by A12, A14;

        hence thesis by A15, XXREAL_1: 1;

      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 g1) 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 g1) = the carrier of T by A7, A13, RELAT_1: 27;

      then

      reconsider g1 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 as continuous Function of T, R^1 by A6, PRE_TOPC: 26;

      take g;



       A19: ( rng g1) c= the carrier of ( Closed-Interval-TSpace (( - (r / 3)),(r / 3)));

      thus (g,( dom g)) is_absolutely_bounded_by (r / 3)

      proof

        let x be set;

        assume x in (( dom g) /\ ( dom g));

        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 thesis by ABSVALUE: 5;

      end;

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

      proof



         A20: 1 in [. 0 , 1.] by XXREAL_1: 1;



         A21: 0 in [. 0 , 1.] by XXREAL_1: 1;

        let x be set such that

         A22: x in (A /\ ( dom (f - g)));



         A23: x in ( dom (f - g)) by A22, XBOOLE_0:def 4;

        then

         A24: ((f - g) . x) = ((f . x) - (g . x)) by VALUED_1: 13;

        ( dom (f - g)) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        then

         A25: x in ( dom f) by A23, XBOOLE_0:def 4;

        x in A by A22, XBOOLE_0:def 4;

        then x in (A /\ ( dom f)) by A25, XBOOLE_0:def 4;

        then

         A26: |.(f . x).| <= r by A3;

        then

         A27: ( - r) <= (f . x) by ABSVALUE: 5;

        per cases ;

          suppose

           A28: (f . x) <= ( - (r / 3));

          then (f . x) in A1 by XXREAL_1: 234;

          then x in (f " A1) 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 thesis by A1, A24, A29, A30, ABSVALUE: 5;

        end;

          suppose

           A31: (r / 3) <= (f . x);

          then (f . x) in A2 by XXREAL_1: 236;

          then x in (f " A2) 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 thesis by A24, A32, A33, ABSVALUE: 5;

        end;

          suppose

           A34: ( - (r / 3)) < (f . x) & (f . x) < (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 thesis by A24, A36, ABSVALUE: 5;

        end;

      end;

    end;

    theorem :: TIETZE:18



     Th18: (for A,B be non empty closed Subset of T st A misses B holds ex f be continuous Function of T, R^1 st (f .: A) = { 0 } & (f .: B) = {1}) implies T is normal

    proof

      assume

       A1: for A,B be non empty closed Subset of T st A misses B holds ex f be continuous Function of T, R^1 st (f .: A) = { 0 } & (f .: B) = {1};

      let W,V be Subset of T;

      assume W <> {} & V <> {} & W is closed & V is closed & W misses V;

      then

      consider f be 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 P, Q;

      ( [#] R^1 ) <> {} ;

      hence P is open & Q is open by TOPS_2: 43;



       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= P

      proof

        let a be object;



         A6: 0 in ( left_open_halfline (1 / 2)) by XXREAL_1: 233;

        assume

         A7: a in W;

        then (f . a) in (f .: W) by FUNCT_2: 35;

        then (f . a) = 0 by A2, TARSKI:def 1;

        hence thesis by A4, A5, A7, A6, FUNCT_1:def 7;

      end;



       A8: ( R^1 ( right_open_halfline (1 / 2))) = ( right_open_halfline (1 / 2)) by TOPREALB:def 3;

      thus V c= Q

      proof

        let a be object;



         A9: 1 in ( right_open_halfline (1 / 2)) by XXREAL_1: 235;

        assume

         A10: a in V;

        then (f . a) in (f .: V) by FUNCT_2: 35;

        then (f . a) = 1 by A3, TARSKI:def 1;

        hence thesis by A8, A5, A10, A9, FUNCT_1:def 7;

      end;

      thus thesis by A4, A8, FUNCT_1: 71, XXREAL_1: 275;

    end;

    theorem :: TIETZE:19



     Th19: for f be Function of T, R^1 , x be Point of T holds f is_continuous_at x iff for e be Real st e > 0 holds ex H be Subset of T st H is open & x in H & for y be Point of T st y in H holds |.((f . y) - (f . x)).| < e

    proof

      let f be Function of T, R^1 , x be Point of T;

      thus f is_continuous_at x implies for e be Real st e > 0 holds ex H be Subset of T st H is open & x in H & for y be Point of T st y in H holds |.((f . y) - (f . x)).| < e

      proof

        reconsider fx = (f . x) as Point of RealSpace by TOPMETR: 12, TOPMETR:def 6;

        assume

         A1: f is_continuous_at x;

        let e be Real such that

         A2: e > 0 ;

        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 be 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;

        thus H is open & x in H by A3;



         A5: ( dom f) = the carrier of T by FUNCT_2:def 1;

        let y be Point of T;

        assume y in H;

        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 thesis by TOPMETR: 11;

      end;

      assume

       A7: for e be Real st e > 0 holds ex H be Subset of T st H is open & x in H & for y be Point of T st y in H holds |.((f . y) - (f . x)).| < e;

      now

        reconsider fx = (f . x) as Point of RealSpace by TOPMETR: 12, TOPMETR:def 6;

        let G be Subset of R^1 ;

        assume G is open & (f . x) in G;

        then

        consider r be Real such that

         A8: r > 0 and

         A9: ( Ball (fx,r)) c= G by TOPMETR: 15, TOPMETR:def 6;

        consider H be Subset of T such that

         A10: H is open & x in H and

         A11: for y be Point of T st y in H holds |.((f . y) - (f . x)).| < r by A7, A8;

        take H;

        thus H is open & x in H by A10;

        thus (f .: H) c= G

        proof

          let a be object;

          assume a in (f .: H);

          then

          consider y be object such that

           A12: y in ( dom f) and

           A13: y in H and

           A14: a = (f . y) by FUNCT_1:def 6;

          reconsider y as Point of T by A12;

          reconsider fy = (f . y) as Point of RealSpace by TOPMETR: 12, TOPMETR:def 6;

           |.((f . y) - (f . x)).| < r by A11, A13;

          then |.( - ((f . y) - (f . x))).| < r by COMPLEX1: 52;

          then |.((f . x) - (f . y)).| < r;

          then ( dist (fx,fy)) < r by TOPMETR: 11;

          then fy in ( Ball (fx,r)) by METRIC_1: 11;

          hence thesis by A9, A14;

        end;

      end;

      hence thesis by TMAP_1: 43;

    end;

    theorem :: TIETZE:20



     Th20: for F be Functional_Sequence of the carrier of T, REAL st F is_unif_conv_on the carrier of T & for i be 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 F be Functional_Sequence of the carrier of T, REAL such that

       A1: F is_unif_conv_on the carrier of T and

       A2: for i be Nat holds (F . i) 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

        let p be Point of T;

        now

          let e be Real such that

           A3: e > 0 ;

          reconsider e3 = (e / 3) as Real;



           A4: e3 > 0 by A3, XREAL_1: 139;

          then

          consider k be Nat such that

           A5: for n be Nat holds for x be Point of T st n >= k & x in the carrier of T holds |.(((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: |.((Fk . p) - (l . p)).| < e3 by A5;

          Fk is_continuous_at p by TMAP_1: 44;

          then

          consider H be Subset of T such that

           A7: H is open & p in H and

           A8: for y be Point of T st y in H holds |.((Fk . y) - (Fk . p)).| < e3 by A4, Th19;

          take H;

          thus H is open & p in H by A7;

          let y be Point of T such that

           A9: y in H;

           |.((Fk . y) - (l . y)).| < e3 by A5;

          then |.( - ((Fk . y) - (l . y))).| < e3 by COMPLEX1: 52;

          then |.(((Fk . p) - (l . p)) + (( - (Fk . y)) + (l . y))).| <= ( |.((Fk . p) - (l . p)).| + |.( - ((Fk . y) - (l . y))).|) & ( |.((Fk . p) - (l . p)).| + |.( - ((Fk . y) - (l . y))).|) < (e3 + e3) by A6, COMPLEX1: 56, XREAL_1: 8;

          then |.(((Fk . p) - (l . p)) + (( - (Fk . y)) + (l . y))).| < (2 * e3) by XXREAL_0: 2;

          then |.(((Fk . y) - (Fk . p)) + (((Fk . p) - (l . p)) + (( - (Fk . y)) + (l . y)))).| <= ( |.((Fk . y) - (Fk . p)).| + |.(((Fk . p) - (l . p)) + (( - (Fk . y)) + (l . y))).|) & ( |.((Fk . y) - (Fk . p)).| + |.(((Fk . p) - (l . p)) + (( - (Fk . y)) + (l . y))).|) < (e3 + (2 * e3)) by A8, A9, COMPLEX1: 56, XREAL_1: 8;

          hence |.((l . y) - (l . p)).| < e by XXREAL_0: 2;

        end;

        hence l is_continuous_at p by Th19;

      end;

      hence thesis by TMAP_1: 44;

    end;

    theorem :: TIETZE:21



     Th21: for T be non empty TopSpace holds for f be Function of T, R^1 holds for r be positive Real 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;

      let f be Function of T, R^1 ;

      let r be positive Real;



       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))

      proof

        assume

         A2: (f,the carrier of T) is_absolutely_bounded_by r;

        now

          let x be object;

          assume x in the carrier of T;

          then x in (the carrier of T /\ ( dom f)) by A1;

          then |.(f . x).| <= r by A2;

          then (2 * |.(f . x).|) <= (2 * r) by XREAL_1: 64;

          then ( |.2.| * |.(f . x).|) <= (2 * r) by ABSVALUE:def 1;

          then ( |.( - 2).| * |.(f . x).|) <= (2 * r) by COMPLEX1: 52;

          then |.(( - 2) * (f . x)).| <= (r - ( - r)) by COMPLEX1: 65;

          then |.((( - 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;

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

      assume

       A3: f is Function of T, ( Closed-Interval-TSpace (( - r),r));

      let x be set;

      assume x in (the carrier of T /\ ( dom f));

      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 |.((( - r) + r) - (2 * (f . x))).| <= (r - ( - r)) by RCOMP_1: 2;

      then |.(( - 2) * (f . x)).| <= (r - ( - r));

      then ( |.( - 2).| * |.(f . x).|) <= (2 * r) by COMPLEX1: 65;

      then ( |.2.| * |.(f . x).|) <= (2 * r) by COMPLEX1: 52;

      then (2 * |.(f . x).|) <= (2 * r) by ABSVALUE:def 1;

      then ((2 * |.(f . x).|) / 2) <= ((2 * r) / 2) by XREAL_1: 72;

      hence thesis;

    end;

    theorem :: TIETZE:22



     Th22: ((f - g),X) is_absolutely_bounded_by r implies ((g - f),X) is_absolutely_bounded_by r

    proof

      assume

       A1: ((f - g),X) is_absolutely_bounded_by r;

      let x be set;

      assume

       A2: x in (X /\ ( dom (g - f)));

      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 |.((f - g) . x).| <= r by A1, A2;

      then |.((f . x) - (g . x)).| <= r by A4, A3, VALUED_1: 13;

      then |.( - ((f . x) - (g . x))).| <= r by COMPLEX1: 52;

      then |.((g . x) - (f . x)).| <= r;

      hence thesis by A3, VALUED_1: 13;

    end;

    ::$Notion-Name

    theorem :: TIETZE:23

    T is normal implies for A holds for f be Function of (T | A), ( Closed-Interval-TSpace (( - 1),1)) st f is continuous holds ex g be continuous Function of T, ( Closed-Interval-TSpace (( - 1),1)) st (g | A) = f

    proof

      assume

       A1: T is normal;

      let A;

      let f be Function of (T | A), ( Closed-Interval-TSpace (( - 1),1)) such that

       A2: f is continuous;



       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;

      per cases ;

        suppose A is empty;

        then

        reconsider A1 = A as empty Subset of T;

        set g = (T --> ( R^1 0 ));

        g = (the carrier of T --> 0 ) by TOPREALB:def 2;

        then

         A5: ( rng g) = { 0 } by FUNCOP_1: 8;

        ( rng g) c= the carrier of ( Closed-Interval-TSpace (( - 1),1))

        proof

          let y be object;

          assume y in ( rng g);

          then y = 0 by A5, TARSKI:def 1;

          hence thesis by A4, XXREAL_1: 1;

        end;

        then

        reconsider g as Function of T, ( Closed-Interval-TSpace (( - 1),1)) by FUNCT_2: 6;

        reconsider g as continuous Function of T, ( Closed-Interval-TSpace (( - 1),1)) by PRE_TOPC: 27;

        take g;

        (g | A1) is empty;

        hence thesis;

      end;

        suppose A is non empty;

        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 be Element of DF : q is continuous Function of T, R^1 };

        reconsider f1 = f as Function of (T | A1), R^1 by TOPREALA: 7;

        defpred Z[ Nat, set, set] means ex E2 be continuous Function of T, R^1 st E2 = $2 & (((f - E2),A) is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ $1)) implies ex g be 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 DF by FUNCT_2: 8;

        then (T --> ( R^1 0 )) in D;

        then

        reconsider D as non empty set;

        (f1,A) is_absolutely_bounded_by 1

        proof

          let x be set;

          assume x in (A /\ ( dom f1));

          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 thesis by ABSVALUE: 5;

        end;

        then

        consider g0 be 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 DF by FUNCT_2: 8;

        then g0 in D;

        then

        reconsider g0d = g0 as Element of D;



         A10: for n be Nat holds for x be Element of D holds ex y be Element of D st Z[n, x, y]

        proof

          let n be Nat, x be Element of D;

          x in D;

          then

          consider E2 be Element of DF such that

           A11: E2 = x and

           A12: E2 is continuous Function of T, R^1 ;

          reconsider E2 as continuous Function of T, R^1 by A12;

          per cases ;

            suppose

             A13: not ((f - E2),A) is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ n));

            take x, E2;

            thus thesis by A11, A13;

          end;

            suppose

             A14: ((f - E2),A) is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ n));

            reconsider E2b = (E2 | A) as Function of (T | A1), R^1 by PRE_TOPC: 9;

            reconsider 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 as continuous RealMap of T by JORDAN5A: 27;

            (f1c - E2c) is continuous RealMap of (T | A1);

            then

            reconsider k as continuous Function of (T | A1), R^1 by JORDAN5A: 27, TOPMETR: 17;

            reconsider f1c, 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 r > ((2 / 3) * 0 ) by XREAL_1: 68;

            then r > 0 ;

            then

            consider g be continuous Function of T, R^1 such that

             A17: (g,( dom g)) is_absolutely_bounded_by (r / 3) and

             A18: ((k - g),A) is_absolutely_bounded_by ((2 * r) / 3) by A1, A15, Th17;

            reconsider ga = g as RealMap of T by TOPMETR: 17;

            reconsider ga as continuous RealMap of T by JORDAN5A: 27;

            set y = (E2a + ga);

            reconsider y1 = y as continuous Function of T, R^1 by JORDAN5A: 27, TOPMETR: 17;

            y1 in DF & y1 is continuous Function of T, R^1 by FUNCT_2: 8;

            then y in D;

            then

            reconsider y as Element of D;

            take y, E2;

            thus E2 = x by A11;

            assume ((f - E2),A) is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ n));

            take g;

            thus y = (E2 + g);



             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;



             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)

            .= ((f - (E2 | A)) - g)

            .= (((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 thesis by A18, A19, A21, Th16;

          end;

        end;

        consider F be sequence of D such that

         A22: (F . 0 ) = g0d and

         A23: for n be Nat holds Z[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A10);

         A24:

        now

          let n be Nat;

           Z[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;

        end;

        ( dom F) = NAT by FUNCT_2:def 1;

        then

        reconsider F as Functional_Sequence of the carrier of T, REAL by A24, SEQFUNC: 1;

        consider E2 be 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 be continuous Function of T, R^1 st (F . ( 0 qua Nat + 1)) = (E2 + g) & (g,the carrier of T) is_absolutely_bounded_by ((1 / 3) * ((2 / 3) |^ ( 0 qua Nat + 1))) & (((f - E2) - g),A) is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ ( 0 qua Nat + 1))) by A23;

        ((2 / 3) |^ 0 ) = 1 by NEWTON: 4;

        then

        consider g1 be continuous Function of T, R^1 such that

         A27: (F . ( 0 qua Nat + 1)) = (E2 + g1) and

         A28: (g1,the carrier of T) is_absolutely_bounded_by ((1 / 3) * ((2 / 3) |^ ( 0 qua Nat + 1))) and (((f - E2) - g1),A) is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ ( 0 qua Nat + 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 P[ 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

          let n be Nat;



           A31: ( dom f) = ( [#] (T | A1)) by FUNCT_2:def 1

          .= A by PRE_TOPC:def 5;

          consider E2 be 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 be 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 P[n];

          then (((F . n) - f),A1) is_absolutely_bounded_by ((2 / 3) * ((2 / 3) |^ n)) by POWER: 41;

          then

          consider g be 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 be 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 be 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

            let a be object;

            assume

             A41: a in 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;

          end;

          then

          consider gx be 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

            let a be object;

            assume

             A47: a in ( dom gx);



            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);

          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 P[(n + 1)] by A33, A43, A45, A48, Th22, JORDAN5A: 27, METRIC_1:def 13, TOPMETR: 12, TOPMETR:def 6;

        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

          let a be object;

          assume

           A50: a in ( dom g1);



          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);

        end;

        then

         A51: ((F . ( 0 qua Nat + 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 POWER: 24;

        then

         A52: P[ 0 ] by A9, A22, A28, A51, Th22;



         A53: for n be Nat holds P[n] from NAT_1:sch 2( A52, A30);



         A54: for n be Nat holds (((F . n) - (F . (n + 1))),the carrier of T) is_absolutely_bounded_by ((2 / 9) * ((2 / 3) to_power n)) by A53;

        ( 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

          let n be Nat;

           Z[n, (F . n), (F . (n + 1))] by A23;

          hence the carrier of T c= ( dom (F . n)) by FUNCT_2:def 1;

        end;

        then

         A56: the carrier of T common_on_dom F;

        then

         A57: A1 common_on_dom F by SEQFUNC: 23;



         A58: for n be Nat holds (((F . n) - f),A1) is_absolutely_bounded_by ((2 / 3) * ((2 / 3) to_power n)) by A53;



         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;

          assume x in (the carrier of T /\ ( dom h));

          then

          reconsider z = x as Element of T;



           A61: ( dom (F . 0 )) = the carrier of T by A22, FUNCT_2:def 1;



           A62: |.((F . 0 ) . z).| <= (1 / 3) by A8, A22, A61;

          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 thesis by A65, ABSVALUE: 5;

        end;

        then

        reconsider 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 thesis by A60;

      end;

    end;

    theorem :: TIETZE:24

    (for A be non empty closed Subset of T holds for f be continuous Function of (T | A), ( Closed-Interval-TSpace (( - 1),1)) holds ex g be continuous Function of T, ( Closed-Interval-TSpace (( - 1),1)) st (g | A) = f) implies T is normal

    proof

      assume

       A1: for A be non empty closed Subset of T holds for f be continuous Function of (T | A), ( Closed-Interval-TSpace (( - 1),1)) holds ex g be continuous Function of T, ( Closed-Interval-TSpace (( - 1),1)) st (g | A) = f;

      for C,D be non empty closed Subset of T st C misses D holds ex f be 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 such that

         A2: C misses D;

        set g1 = (f1 | (T | C)), g2 = (f2 | (T | D));

        set f = (g1 union g2);



         A3: the carrier of (T | D) = D by PRE_TOPC: 8;

        g2 = (f2 | the carrier of (T | D)) by TMAP_1:def 4;

        then

         A4: ( rng g2) c= ( rng f2) by RELAT_1: 70;

        g1 = (f1 | the carrier of (T | C)) by TMAP_1:def 4;

        then ( rng g1) c= ( rng f1) by RELAT_1: 70;

        then

         A5: (( rng g1) \/ ( rng g2)) c= (( rng f1) \/ ( rng f2)) by A4, XBOOLE_1: 13;



         A6: f1 = (the carrier of T --> 0 ) by TOPREALB:def 2;

        then

         A7: ( rng f1) = { 0 } by FUNCOP_1: 8;



         A8: f2 = (the carrier of T --> 1) by TOPREALB:def 2;

        then

         A9: ( rng f2) = {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 f) c= (( rng g1) \/ ( rng g2)) by Th13;

        then

         A12: ( rng f) c= (( rng f1) \/ ( rng f2)) by A5;



         A13: ( rng f) c= [.( - 1), 1.]

        proof

          let x be object;

          assume x in ( rng f);

          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 thesis by XXREAL_1: 1;

        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: (f2 .: D) = {1}

        proof

          thus (f2 .: D) c= {1} by A8, FUNCOP_1: 81;

          let y be object;

          consider c be object such that

           A16: c in D by XBOOLE_0:def 1;

          assume y in {1};

          then

           A17: y = 1 by TARSKI:def 1;

          ( dom f2) = the carrier of T & (f2 . c) = 1 by A8, A16, FUNCOP_1: 7, FUNCOP_1: 13;

          hence thesis by A17, A16, FUNCT_1:def 6;

        end;



         A18: (f1 .: C) = { 0 }

        proof

          thus (f1 .: C) c= { 0 } by A6, FUNCOP_1: 81;

          let y be object;

          consider c be object such that

           A19: c in C by XBOOLE_0:def 1;

          assume y in { 0 };

          then

           A20: y = 0 by TARSKI:def 1;

          ( dom f1) = the carrier of T & (f1 . c) = 0 by A6, A19, FUNCOP_1: 7, FUNCOP_1: 13;

          hence thesis by A20, A19, FUNCT_1:def 6;

        end;



         A21: (C \/ D) is closed by TOPS_1: 9;

        the carrier of ( Closed-Interval-TSpace (( - 1),1)) = [.( - 1), 1.] by TOPMETR: 18;

        then

        reconsider h = f as Function of (T | (C \/ D)), ( Closed-Interval-TSpace (( - 1),1)) by A14, A13, FUNCT_2: 6;

        f 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 be continuous Function of T, ( Closed-Interval-TSpace (( - 1),1)) such that

         A22: (g | (C \/ D)) = f by A1, A21;

        reconsider F = g as continuous Function of T, R^1 by PRE_TOPC: 26, TOPREALA: 7;

        take F;



        thus (F .: C) = (f .: C) by A22, FUNCT_2: 97, XBOOLE_1: 7

        .= (g1 .: C) by A10, A11, Th14

        .= ((f1 | C) .: C) by A10, TMAP_1:def 3

        .= { 0 } by A18, RELAT_1: 129;



        thus (F .: D) = (f .: D) by A22, FUNCT_2: 97, XBOOLE_1: 7

        .= (g2 .: D) by A3, A11, Th14

        .= ((f2 | D) .: D) by A3, TMAP_1:def 3

        .= {1} by A15, RELAT_1: 129;

      end;

      hence thesis by Th18;

    end;