heine.miz



    begin

    reserve a,b,x,y for Real,

i,k,n,m for Nat;

    reserve p,w for Real;

    theorem :: HEINE:1

    

     Th1: for A be SubSpace of RealSpace , p,q be Point of A st x = p & y = q holds ( dist (p,q)) = |.(x - y).|

    proof

      let A be SubSpace of RealSpace , p,q be Point of A;

      assume

       A1: x = p & y = q;

      

      thus ( dist (p,q)) = (the distance of A . (p,q)) by METRIC_1:def 1

      .= ( real_dist . (x,y)) by A1, METRIC_1:def 13, TOPMETR:def 1

      .= |.(x - y).| by METRIC_1:def 12;

    end;

    reserve seq for Real_Sequence;

    theorem :: HEINE:2

    

     Th2: seq is increasing & ( rng seq) c= NAT implies n <= (seq . n)

    proof

      defpred P[ Nat] means $1 <= (seq . $1);

      assume that

       A1: seq is increasing and

       A2: ( rng seq) c= NAT ;

      

       A3: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A4: k <= (seq . k);

        (k + 1) in NAT ;

        then (k + 1) in ( dom seq) by FUNCT_2:def 1;

        then (seq . (k + 1)) in ( rng seq) by FUNCT_1:def 3;

        then

        reconsider k9 = (seq . (k + 1)) as Element of NAT by A2;

        (seq . k) < (seq . (k + 1)) by A1, SEQM_3:def 6;

        then k < k9 by A4, XXREAL_0: 2;

        hence thesis by NAT_1: 13;

      end;

       0 in NAT ;

      then 0 in ( dom seq) by FUNCT_2:def 1;

      then (seq . 0 ) in ( rng seq) by FUNCT_1:def 3;

      then

       A5: P[ 0 ] by A2;

      for n holds P[n] from NAT_1:sch 2( A5, A3);

      hence thesis;

    end;

    definition

      let seq, k;

      :: HEINE:def1

      func k to_power seq -> Real_Sequence means

      : Def1: for n holds (it . n) = (k to_power (seq . n));

      existence

      proof

        deffunc F( Nat) = (k to_power (seq . $1));

        thus ex s be Real_Sequence st for n holds (s . n) = F(n) from SEQ_1:sch 1;

      end;

      uniqueness

      proof

        let s1,s2 be Real_Sequence;

        assume that

         A1: for n holds (s1 . n) = (k to_power (seq . n)) and

         A2: for n holds (s2 . n) = (k to_power (seq . n));

        let n be Element of NAT ;

        

        thus (s1 . n) = (k to_power (seq . n)) by A1

        .= (s2 . n) by A2;

      end;

    end

    theorem :: HEINE:3

    

     Th3: seq is divergent_to+infty implies (2 to_power seq) is divergent_to+infty

    proof

      assume

       A1: seq is divergent_to+infty;

      let r be Real;

      consider p be Nat such that

       A2: p > r by SEQ_4: 3;

      consider n such that

       A3: for m st n <= m holds p < (seq . m) by A1;

      take n;

      let m;

      assume m >= n;

      then p < (seq . m) by A3;

      then

       A4: (2 to_power p) < (2 to_power (seq . m)) by POWER: 39;

      p < (2 to_power p) by NEWTON: 86;

      then p < (2 to_power (seq . m)) by A4, XXREAL_0: 2;

      then r < (2 to_power (seq . m)) by A2, XXREAL_0: 2;

      hence thesis by Def1;

    end;

    ::$Notion-Name

    theorem :: HEINE:4

    a <= b implies ( Closed-Interval-TSpace (a,b)) is compact

    proof

      set M = ( Closed-Interval-MSpace (a,b));

      assume

       A1: a <= b;

      reconsider a, b as Real;

      set r = (b - a) qua Real;

      now

        per cases by A1, XREAL_1: 48;

          suppose r = 0 ;

          then [.a, b.] = {a} & the carrier of ( Closed-Interval-TSpace (a,b)) = [.a, b.] by TOPMETR: 18, XXREAL_1: 17;

          hence ( Closed-Interval-TSpace (a,b)) is compact by COMPTS_1: 18;

        end;

          suppose

           A2: r > 0 ;

          

           A3: ( TopSpaceMetr M) = ( Closed-Interval-TSpace (a,b)) by TOPMETR:def 7;

          assume not ( Closed-Interval-TSpace (a,b)) is compact;

          then not M is compact by A3, TOPMETR:def 5;

          then

          consider F be Subset-Family of M such that

           A4: F is being_ball-family and

           A5: F is Cover of M and

           A6: not ex G be Subset-Family of M st (G c= F & G is Cover of M & G is finite) by TOPMETR: 16;

          defpred P[ Nat, Element of REAL , Element of REAL ] means (( not ex G be Subset-Family of M st G c= F & [.($2 - (r / (2 |^ ($1 + 1)))), $2.] c= ( union G) & G is finite) implies $3 = ($2 - (r / (2 |^ ($1 + 2))))) & ( not ( not ex G be Subset-Family of M st G c= F & [.($2 - (r / (2 |^ ($1 + 1)))), $2.] c= ( union G) & G is finite) implies $3 = ($2 + (r / (2 |^ ($1 + 2)))));

          

           A7: for n be Nat holds for p be Element of REAL holds ex w be Element of REAL st P[n, p, w]

          proof

            let n be Nat;

            let p be Element of REAL ;

            now

              per cases ;

                suppose

                 A8: not ex G be Subset-Family of M st G c= F & [.(p - (r / (2 |^ (n + 1)))), p.] c= ( union G) & G is finite;

                reconsider y = (p - (r / (2 |^ (n + 2)))) as Element of REAL by XREAL_0:def 1;

                take y;

                thus P[n, p, y] by A8;

              end;

                suppose

                 A9: ex G be Subset-Family of M st G c= F & [.(p - (r / (2 |^ (n + 1)))), p.] c= ( union G) & G is finite;

                reconsider y = (p + (r / (2 |^ (n + 2)))) as Element of REAL by XREAL_0:def 1;

                take y;

                thus P[n, p, y] by A9;

              end;

            end;

            hence thesis;

          end;

          consider f be sequence of REAL such that

           A10: (f . 0 ) = ( In (((a + b) / 2), REAL )) and

           A11: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A7);

          defpred R[ Nat] means not ex G be Subset-Family of M st (G c= F & [.((f . $1) - (r / (2 |^ ($1 + 1)))), ((f . $1) + (r / (2 |^ ($1 + 1)))).] c= ( union G) & G is finite);

          

           A12: ((f . 0 ) + (r / (2 |^ ( 0 + 1)))) = (((a + b) / 2) + (r / 2)) by A10

          .= b;

          defpred Q[ Nat] means a <= ((f . $1) - (r / (2 |^ ($1 + 1)))) & ((f . $1) + (r / (2 |^ ($1 + 1)))) <= b;

          

           A13: for n holds (f . (n + 1)) = ((f . n) + (r / (2 |^ (n + 2)))) or (f . (n + 1)) = ((f . n) - (r / (2 |^ (n + 2))))

          proof

            let n;

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

             P[n, (f . n), (f . (n + 1))] by A11;

            hence thesis;

          end;

          

           A14: for k st Q[k] holds Q[(k + 1)]

          proof

            let k;

            

             A15: ((r / (2 * (2 |^ (k + 1)))) + (r / (2 * (2 |^ (k + 1))))) = (r / (2 |^ (k + 1))) by XCMPLX_1: 118;

            

             A16: ((r / (2 |^ (k + 1))) - (r / (2 |^ (k + (1 + 1))))) = ((r / (2 |^ (k + 1))) - (r / (2 |^ ((k + 1) + 1))))

            .= ((r / (2 |^ (k + 1))) - (r / (2 * (2 |^ (k + 1))))) by NEWTON: 6

            .= (r / (2 |^ ((k + 1) + 1))) by A15, NEWTON: 6

            .= (r / (2 |^ (k + (1 + 1))));

            assume

             A17: Q[k];

            then

             A18: (b - (f . k)) >= (r / (2 |^ (k + 1))) by XREAL_1: 19;

            

             A19: ((f . k) - a) >= (r / (2 |^ (k + 1))) by A17, XREAL_1: 11;

            now

              per cases by A13;

                suppose

                 A20: (f . (k + 1)) = ((f . k) + (r / (2 |^ (k + 2))));

                (2 |^ (k + 1)) > 0 & r >= 0 by A1, NEWTON: 83, XREAL_1: 48;

                then

                 A21: (r / (2 |^ (k + 1))) >= 0 ;

                ((f . (k + 1)) - a) = (((f . k) - a) + (r / (2 |^ (k + 2)))) by A20;

                then ((f . (k + 1)) - a) >= (r / (2 |^ (k + 2))) by A19, A21, XREAL_1: 31;

                hence a <= ((f . (k + 1)) - (r / (2 |^ ((k + 1) + 1)))) by XREAL_1: 11;

                (b - (f . (k + 1))) = ((b - (f . k)) - (r / (2 |^ (k + 2)))) by A20;

                then (b - (f . (k + 1))) >= (r / (2 |^ (k + 2))) by A18, A16, XREAL_1: 9;

                hence ((f . (k + 1)) + (r / (2 |^ ((k + 1) + 1)))) <= b by XREAL_1: 19;

              end;

                suppose

                 A22: (f . (k + 1)) = ((f . k) - (r / (2 |^ (k + 2))));

                then ((f . (k + 1)) - a) = (((f . k) - a) - (r / (2 |^ (k + 2))));

                then ((f . (k + 1)) - a) >= (r / (2 |^ (k + 2))) by A19, A16, XREAL_1: 9;

                hence a <= ((f . (k + 1)) - (r / (2 |^ ((k + 1) + 1)))) by XREAL_1: 11;

                (2 |^ (k + 1)) > 0 & r >= 0 by A1, NEWTON: 83, XREAL_1: 48;

                then

                 A23: (r / (2 |^ (k + 1))) >= 0 ;

                (b - (f . (k + 1))) = ((b - (f . k)) + (r / (2 |^ (k + 2)))) by A22;

                then (b - (f . (k + 1))) >= (r / (2 |^ (k + 2))) by A18, A23, XREAL_1: 31;

                hence ((f . (k + 1)) + (r / (2 |^ ((k + 1) + 1)))) <= b by XREAL_1: 19;

              end;

            end;

            hence thesis;

          end;

          

           A24: ((f . 0 ) - (r / (2 |^ ( 0 + 1)))) = (((a + b) / 2) - (r / 2)) by A10

          .= a;

          then

           A25: Q[ 0 ] by A12;

          

           A26: for k holds Q[k] from NAT_1:sch 2( A25, A14);

          

           A27: ( rng f) c= [.a, b.]

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider x be object such that

             A28: x in ( dom f) and

             A29: y = (f . x) by FUNCT_1:def 3;

            reconsider n = x as Element of NAT by A28, FUNCT_2:def 1;

            

             A30: (2 |^ (n + 1)) > 0 & r >= 0 by A1, NEWTON: 83, XREAL_1: 48;

            ((f . n) + (r / (2 |^ (n + 1)))) <= b by A26;

            then

             A31: (f . n) <= b by A30, XREAL_1: 40;

            a <= ((f . n) - (r / (2 |^ (n + 1)))) by A26;

            then a <= (f . n) by A30, XREAL_1: 51;

            then y in { y1 where y1 be Real : a <= y1 <= b } by A29, A31;

            hence thesis by RCOMP_1:def 1;

          end;

          

           A32: for k st R[k] holds R[(k + 1)]

          proof

            let k such that

             A33: R[k];

            given G be Subset-Family of M such that

             A34: G c= F and

             A35: [.((f . (k + 1)) - (r / (2 |^ ((k + 1) + 1)))), ((f . (k + 1)) + (r / (2 |^ ((k + 1) + 1)))).] c= ( union G) and

             A36: G is finite;

            

             A37: (r / (2 |^ (k + (1 + 1)))) = (r / (2 |^ ((k + 1) + 1)))

            .= (r / ((2 |^ (k + 1)) * 2)) by NEWTON: 6

            .= ((r / (2 |^ (k + 1))) / 2) by XCMPLX_1: 78;

            now

              per cases ;

                suppose

                 A38: ex G be Subset-Family of M st G c= F & [.((f . k) - (r / (2 |^ (k + 1)))), (f . k).] c= ( union G) & G is finite;

                (2 |^ (k + 1)) > 0 & r >= 0 by A1, NEWTON: 83, XREAL_1: 48;

                then ((f . k) - (r / (2 |^ (k + 1)))) <= (f . k) & (f . k) <= ((f . k) + (r / (2 |^ (k + 1)))) by XREAL_1: 31, XREAL_1: 43;

                then

                 A39: [.((f . k) - (r / (2 |^ (k + 1)))), ((f . k) + (r / (2 |^ (k + 1)))).] = ( [.((f . k) - (r / (2 |^ (k + 1)))), (f . k).] \/ [.(f . k), ((f . k) + (r / (2 |^ (k + 1)))).]) by XXREAL_1: 165;

                

                 A40: ((f . (k + 1)) - (r / (2 |^ ((k + 1) + 1)))) = (((f . k) + (r / (2 |^ (k + 2)))) - (r / (2 |^ (k + (1 + 1))))) by A11, A38

                .= (f . k);

                consider G1 be Subset-Family of M such that

                 A41: G1 c= F and

                 A42: [.((f . k) - (r / (2 |^ (k + 1)))), (f . k).] c= ( union G1) and

                 A43: G1 is finite by A38;

                reconsider G3 = (G1 \/ G) as Subset-Family of M;

                ((f . (k + 1)) + (r / (2 |^ ((k + 1) + 1)))) = (((f . k) + (r / (2 |^ (k + 2)))) + (r / (2 |^ (k + (1 + 1))))) by A11, A38

                .= (((f . k) + ((r / (2 |^ (k + 1))) / 2)) + ((r / (2 |^ (k + 1))) / 2)) by A37

                .= ((f . k) + (r / (2 |^ (k + 1))));

                then [.((f . k) - (r / (2 |^ (k + 1)))), ((f . k) + (r / (2 |^ (k + 1)))).] c= (( union G1) \/ ( union G)) by A35, A42, A40, A39, XBOOLE_1: 13;

                then [.((f . k) - (r / (2 |^ (k + 1)))), ((f . k) + (r / (2 |^ (k + 1)))).] c= ( union G3) by ZFMISC_1: 78;

                hence contradiction by A33, A34, A36, A41, A43, XBOOLE_1: 8;

              end;

                suppose

                 A44: not (ex G be Subset-Family of M st G c= F & [.((f . k) - (r / (2 |^ (k + 1)))), (f . k).] c= ( union G) & G is finite);

                

                then

                 A45: ((f . (k + 1)) + (r / (2 |^ ((k + 1) + 1)))) = (((f . k) - (r / (2 |^ (k + 2)))) + (r / (2 |^ (k + (1 + 1))))) by A11

                .= (f . k);

                ((f . (k + 1)) - (r / (2 |^ ((k + 1) + 1)))) = (((f . k) - (r / (2 |^ (k + 2)))) - (r / (2 |^ (k + (1 + 1))))) by A11, A44

                .= (((f . k) - ((r / (2 |^ (k + 1))) / 2)) - ((r / (2 |^ (k + 1))) / 2)) by A37

                .= ((f . k) - (r / (2 |^ (k + 1))));

                hence contradiction by A34, A35, A36, A44, A45;

              end;

            end;

            hence thesis;

          end;

          

           A46: the carrier of M = [.a, b.] by A1, TOPMETR: 10;

          

           A47: R[ 0 ]

          proof

            given G be Subset-Family of M such that

             A48: G c= F and

             A49: [.((f . 0 ) - (r / (2 |^ ( 0 + 1)))), ((f . 0 ) + (r / (2 |^ ( 0 + 1)))).] c= ( union G) and

             A50: G is finite;

            the carrier of M c= ( union G) by A1, A24, A12, A49, TOPMETR: 10;

            then G is Cover of M by SETFAM_1:def 11;

            hence contradiction by A6, A48, A50;

          end;

          reconsider f as Real_Sequence;

           [.a, b.] is compact by RCOMP_1: 6;

          then

          consider s be Real_Sequence such that

           A51: s is subsequence of f and

           A52: s is convergent and

           A53: ( lim s) in [.a, b.] by A27, RCOMP_1:def 3;

          reconsider ls = ( lim s) as Point of M by A1, A53, TOPMETR: 10;

          consider Nseq be increasing sequence of NAT such that

           A54: s = (f * Nseq) by A51, VALUED_0:def 17;

          the carrier of M c= ( union F) by A5, SETFAM_1:def 11;

          then

          consider Z be set such that

           A55: ( lim s) in Z and

           A56: Z in F by A53, A46, TARSKI:def 4;

          consider p be Point of M, r0 be Real such that

           A57: Z = ( Ball (p,r0)) by A4, A56, TOPMETR:def 4;

          set G = {( Ball (p,r0))};

          G c= ( bool the carrier of M)

          proof

            let a be object;

            assume a in G;

            then a = ( Ball (p,r0)) by TARSKI:def 1;

            hence thesis;

          end;

          then

          reconsider G as Subset-Family of M;

          

           A58: G c= F by A56, A57, ZFMISC_1: 31;

          reconsider Ns = Nseq as Real_Sequence by RELSET_1: 7, NUMBERS: 19;

           not Ns is bounded_above

          proof

            let r be Real;

            consider n be Nat such that

             A59: n > r by SEQ_4: 3;

            ( rng Nseq) c= NAT by VALUED_0:def 6;

            then n <= (Ns . n) by Th2;

            hence thesis by A59, XXREAL_0: 2;

          end;

          then

           A60: (2 to_power Ns) is divergent_to+infty by Th3, LIMFUNC1: 31;

          then

           A61: ((2 to_power Ns) " ) is convergent by LIMFUNC1: 34;

          consider r1 be Real such that

           A62: r1 > 0 and

           A63: ( Ball (ls,r1)) c= ( Ball (p,r0)) by A55, A57, PCOMPS_1: 27;

          

           A64: (r1 / 2) > 0 by A62, XREAL_1: 139;

          then

          consider n be Nat such that

           A65: for m be Nat st m >= n holds |.((s . m) - ( lim s)).| < (r1 / 2) by A52, SEQ_2:def 7;

          

           A66: for m be Element of NAT holds for q be Point of M st (s . m) = q & m >= n holds ( dist (ls,q)) < (r1 / 2)

          proof

            let m be Element of NAT , q be Point of M;

            assume that

             A67: (s . m) = q and

             A68: m >= n;

             |.((s . m) - ( lim s)).| < (r1 / 2) by A65, A68;

            then

             A69: |.( - ((s . m) - ( lim s))).| < (r1 / 2) by COMPLEX1: 52;

            ( dist (ls,q)) = (the distance of M . (( lim s),(s . m))) by A67, METRIC_1:def 1

            .= (the distance of RealSpace . (ls,q)) by A67, TOPMETR:def 1

            .= |.(( lim s) - (s . m)).| by A67, METRIC_1:def 12, METRIC_1:def 13;

            hence thesis by A69;

          end;

          

           A70: for m be Element of NAT st m >= n holds ((f * Nseq) . m) in ( Ball (ls,(r1 / 2)))

          proof

            let m be Element of NAT such that

             A71: m >= n;

            ( dom f) = NAT & (s . m) = (f . (Nseq . m)) by A54, FUNCT_2: 15, FUNCT_2:def 1;

            then (s . m) in ( rng f) by FUNCT_1:def 3;

            then

            reconsider q = (s . m) as Point of M by A1, A27, TOPMETR: 10;

            ( dist (ls,q)) < (r1 / 2) by A66, A71;

            hence thesis by A54, METRIC_1: 11;

          end;

          ( lim ((2 to_power Ns) " )) = 0 by A60, LIMFUNC1: 34;

          

          then

           A72: ( lim (r (#) ((2 to_power Ns) " ))) = (r * 0 ) by A61, SEQ_2: 8

          .= 0 ;

          (r (#) ((2 to_power Ns) " )) is convergent by A61, SEQ_2: 7;

          then

          consider i such that

           A73: for m st i <= m holds |.(((r (#) ((2 to_power Ns) " )) . m) - 0 ).| < (r1 / 2) by A64, A72, SEQ_2:def 7;

          reconsider l = ((i + 1) + n) as Element of NAT by ORDINAL1:def 12;

          

           A74: l = ((n + 1) + i);

           [.((s . l) - (r * ((2 |^ ((Nseq . l) + 1)) " ))), ((s . l) + (r * ((2 |^ ((Nseq . l) + 1)) " ))).] c= ( Ball (ls,r1))

          proof

             |.(((r (#) ((2 to_power Ns) " )) . l) - 0 ).| < (r1 / 2) by A73, A74, NAT_1: 11;

            then |.(r * (((2 to_power Ns) " ) . l)).| < (r1 / 2) by SEQ_1: 9;

            then |.(r * (((2 to_power Ns) . l) " )).| < (r1 / 2) by VALUED_1: 10;

            then |.(r * ((2 to_power (Ns . l)) " )).| < (r1 / 2) by Def1;

            then

             A75: |.(r * ((2 |^ (Nseq . l)) " )).| < (r1 / 2) by POWER: 41;

            (2 |^ ((Nseq . l) + 1)) = (2 * (2 |^ (Nseq . l))) & (2 |^ (Nseq . l)) > 0 by NEWTON: 6, NEWTON: 83;

            then (1 / (2 |^ ((Nseq . l) + 1))) < ((2 |^ (Nseq . l)) " ) by XREAL_1: 88, XREAL_1: 155;

            then

             A76: (r * ((2 |^ ((Nseq . l) + 1)) " )) < (r * ((2 |^ (Nseq . l)) " )) by A2, XREAL_1: 68;

            (2 |^ ((Nseq . l) + 1)) > 0 & r >= 0 by A1, NEWTON: 83, XREAL_1: 48;

            then |.(r * ((2 |^ ((Nseq . l) + 1)) " )).| = (r * ((2 |^ ((Nseq . l) + 1)) " )) by ABSVALUE:def 1;

            then |.(r * ((2 |^ ((Nseq . l) + 1)) " )).| < |.(r * ((2 |^ (Nseq . l)) " )).| by A76, ABSVALUE: 5;

            then

             A77: |.(r * ((2 |^ ((Nseq . l) + 1)) " )).| < (r1 / 2) by A75, XXREAL_0: 2;

            (2 |^ ((Nseq . l) + 1)) > 0 & r >= 0 by A1, NEWTON: 83, XREAL_1: 48;

            then

             A78: (r * ((2 |^ ((Nseq . l) + 1)) " )) < (r1 / 2) by A77, ABSVALUE:def 1;

            

             A79: (s . l) in ( Ball (ls,(r1 / 2))) by A54, A70, NAT_1: 11;

            then

            reconsider sl = (s . l) as Point of M;

            ( dist (ls,sl)) < (r1 / 2) by A79, METRIC_1: 11;

            then

             A80: |.(( lim s) - (s . l)).| < (r1 / 2) by Th1;

            let z be object;

            

             A81: the carrier of M = [.a, b.] by A1, TOPMETR: 10;

            assume z in [.((s . l) - (r * ((2 |^ ((Nseq . l) + 1)) " ))), ((s . l) + (r * ((2 |^ ((Nseq . l) + 1)) " ))).];

            then z in { m where m be Real : ((s . l) - (r * ((2 |^ ((Nseq . l) + 1)) " ))) <= m & m <= ((s . l) + (r * ((2 |^ ((Nseq . l) + 1)) " ))) } by RCOMP_1:def 1;

            then

            consider x be Real such that

             A82: x = z and

             A83: ((s . l) - (r * ((2 |^ ((Nseq . l) + 1)) " ))) <= x and

             A84: x <= ((s . l) + (r * ((2 |^ ((Nseq . l) + 1)) " )));

            ((f . (Nseq . l)) - (r / (2 |^ ((Nseq . l) + 1)))) >= a by A26;

            then ((s . l) - (r * ((2 |^ ((Nseq . l) + 1)) " ))) >= a by A54, FUNCT_2: 15;

            then

             A85: x >= a by A83, XXREAL_0: 2;

            ((f . (Nseq . l)) + (r / (2 |^ ((Nseq . l) + 1)))) <= b by A26;

            then ((s . l) + (r * ((2 |^ ((Nseq . l) + 1)) " ))) <= b by A54, FUNCT_2: 15;

            then x <= b by A84, XXREAL_0: 2;

            then x in { m where m be Real : a <= m & m <= b } by A85;

            then

            reconsider x9 = x as Point of M by A81, RCOMP_1:def 1;

             |.(( lim s) - x).| = |.((( lim s) - (s . l)) + ((s . l) - x)).|;

            then

             A86: |.(( lim s) - x).| <= ( |.(( lim s) - (s . l)).| + |.((s . l) - x).|) by COMPLEX1: 56;

            (x - (s . l)) <= (r * ((2 |^ ((Nseq . l) + 1)) " )) by A84, XREAL_1: 20;

            then

             A87: ( - (x - (s . l))) >= ( - (r * ((2 |^ ((Nseq . l) + 1)) " ))) by XREAL_1: 24;

            (s . l) <= ((r * ((2 |^ ((Nseq . l) + 1)) " )) + x) by A83, XREAL_1: 20;

            then ((s . l) - x) <= (r * ((2 |^ ((Nseq . l) + 1)) " )) by XREAL_1: 20;

            then |.((s . l) - x).| <= (r * ((2 |^ ((Nseq . l) + 1)) " )) by A87, ABSVALUE: 5;

            then |.((s . l) - x).| < (r1 / 2) by A78, XXREAL_0: 2;

            then ( |.(( lim s) - (s . l)).| + |.((s . l) - x).|) < ((r1 / 2) + (r1 / 2)) by A80, XREAL_1: 8;

            then |.(( lim s) - x).| < ((r1 / 2) + (r1 / 2)) by A86, XXREAL_0: 2;

            then ( dist (ls,x9)) < r1 by Th1;

            hence thesis by A82, METRIC_1: 11;

          end;

          then [.((s . l) - (r / (2 |^ ((Nseq . l) + 1)))), ((s . l) + (r * ((2 |^ ((Nseq . l) + 1)) " ))).] c= ( Ball (p,r0)) by A63;

          then [.((f . (Nseq . l)) - (r / (2 |^ ((Nseq . l) + 1)))), ((s . l) + (r / (2 |^ ((Nseq . l) + 1)))).] c= ( Ball (p,r0)) by A54, FUNCT_2: 15;

          then

           A88: [.((f . (Nseq . l)) - (r / (2 |^ ((Nseq . l) + 1)))), ((f . (Nseq . l)) + (r / (2 |^ ((Nseq . l) + 1)))).] c= ( union {( Ball (p,r0))}) by A54, FUNCT_2: 15;

          for k holds R[k] from NAT_1:sch 2( A47, A32);

          hence contradiction by A58, A88;

        end;

      end;

      hence thesis;

    end;