bhsp_2.miz



    begin

    reserve X for RealUnitarySpace;

    reserve x,y,z,g,g1,g2 for Point of X;

    reserve a,q,r for Real;

    reserve seq,seq1,seq2,seq9 for sequence of X;

    reserve k,n,m,m1,m2 for Nat;

    deffunc 09( RealUnitarySpace) = ( 0. $1);

    definition

      let X, seq;

      :: BHSP_2:def1

      attr seq is convergent means ex g st for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),g)) < r;

    end

    registration

      let X;

      cluster constant -> convergent for sequence of X;

      coherence

      proof

        let seq be sequence of X;

        assume seq is constant;

        then

        consider x such that

         A1: for n be Nat holds (seq . n) = x by VALUED_0:def 18;

        take g = x;

        let r such that

         A2: r > 0 ;

        take m = 0 ;

        let n such that n >= m;

        ( dist ((seq . n),g)) = ( dist (x,g)) by A1

        .= 0 by BHSP_1: 34;

        hence thesis by A2;

      end;

    end

    theorem :: BHSP_2:1

    seq is constant implies seq is convergent;

    theorem :: BHSP_2:2

    

     Th2: seq is convergent & (ex k st for n st k <= n holds (seq9 . n) = (seq . n)) implies seq9 is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: ex k st for n st k <= n holds (seq9 . n) = (seq . n);

      consider k such that

       A3: for n st n >= k holds (seq9 . n) = (seq . n) by A2;

      consider g such that

       A4: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),g)) < r by A1;

      take h = g;

      let r;

      assume r > 0 ;

      then

      consider m1 such that

       A5: for n st n >= m1 holds ( dist ((seq . n),h)) < r by A4;

       A6:

      now

        assume

         A7: m1 <= k;

        take m = k;

        let n;

        assume

         A8: n >= m;

        then n >= m1 by A7, XXREAL_0: 2;

        then ( dist ((seq . n),g)) < r by A5;

        hence ( dist ((seq9 . n),h)) < r by A3, A8;

      end;

      now

        assume

         A9: k <= m1;

        take m = m1;

        let n;

        assume

         A10: n >= m;

        then (seq9 . n) = (seq . n) by A3, A9, XXREAL_0: 2;

        hence ( dist ((seq9 . n),h)) < r by A5, A10;

      end;

      hence thesis by A6;

    end;

    theorem :: BHSP_2:3

    

     Th3: seq1 is convergent & seq2 is convergent implies (seq1 + seq2) is convergent

    proof

      assume that

       A1: seq1 is convergent and

       A2: seq2 is convergent;

      consider g1 such that

       A3: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq1 . n),g1)) < r by A1;

      consider g2 such that

       A4: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq2 . n),g2)) < r by A2;

      take g = (g1 + g2);

      let r;

      assume

       A5: r > 0 ;

      then

      consider m1 such that

       A6: for n st n >= m1 holds ( dist ((seq1 . n),g1)) < (r / 2) by A3, XREAL_1: 215;

      consider m2 such that

       A7: for n st n >= m2 holds ( dist ((seq2 . n),g2)) < (r / 2) by A4, A5, XREAL_1: 215;

      reconsider k = (m1 + m2) as Nat;

      take k;

      let n be Nat such that

       A8: n >= k;

      k >= m2 by NAT_1: 12;

      then n >= m2 by A8, XXREAL_0: 2;

      then

       A9: ( dist ((seq2 . n),g2)) < (r / 2) by A7;

      ( dist (((seq1 + seq2) . n),g)) = ( dist (((seq1 . n) + (seq2 . n)),(g1 + g2))) by NORMSP_1:def 2;

      then

       A10: ( dist (((seq1 + seq2) . n),g)) <= (( dist ((seq1 . n),g1)) + ( dist ((seq2 . n),g2))) by BHSP_1: 40;

      (m1 + m2) >= m1 by NAT_1: 12;

      then n >= m1 by A8, XXREAL_0: 2;

      then ( dist ((seq1 . n),g1)) < (r / 2) by A6;

      then (( dist ((seq1 . n),g1)) + ( dist ((seq2 . n),g2))) < ((r / 2) + (r / 2)) by A9, XREAL_1: 8;

      hence thesis by A10, XXREAL_0: 2;

    end;

    theorem :: BHSP_2:4

    

     Th4: seq1 is convergent & seq2 is convergent implies (seq1 - seq2) is convergent

    proof

      assume that

       A1: seq1 is convergent and

       A2: seq2 is convergent;

      consider g1 such that

       A3: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq1 . n),g1)) < r by A1;

      consider g2 such that

       A4: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq2 . n),g2)) < r by A2;

      take g = (g1 - g2);

      let r;

      assume

       A5: r > 0 ;

      then

      consider m1 such that

       A6: for n st n >= m1 holds ( dist ((seq1 . n),g1)) < (r / 2) by A3, XREAL_1: 215;

      consider m2 such that

       A7: for n st n >= m2 holds ( dist ((seq2 . n),g2)) < (r / 2) by A4, A5, XREAL_1: 215;

      take k = (m1 + m2);

      let n such that

       A8: n >= k;

      k >= m2 by NAT_1: 12;

      then n >= m2 by A8, XXREAL_0: 2;

      then

       A9: ( dist ((seq2 . n),g2)) < (r / 2) by A7;

      ( dist (((seq1 - seq2) . n),g)) = ( dist (((seq1 . n) - (seq2 . n)),(g1 - g2))) by NORMSP_1:def 3;

      then

       A10: ( dist (((seq1 - seq2) . n),g)) <= (( dist ((seq1 . n),g1)) + ( dist ((seq2 . n),g2))) by BHSP_1: 41;

      (m1 + m2) >= m1 by NAT_1: 12;

      then n >= m1 by A8, XXREAL_0: 2;

      then ( dist ((seq1 . n),g1)) < (r / 2) by A6;

      then (( dist ((seq1 . n),g1)) + ( dist ((seq2 . n),g2))) < ((r / 2) + (r / 2)) by A9, XREAL_1: 8;

      hence thesis by A10, XXREAL_0: 2;

    end;

    theorem :: BHSP_2:5

    

     Th5: seq is convergent implies (a * seq) is convergent

    proof

      assume seq is convergent;

      then

      consider g such that

       A1: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),g)) < r;

      take h = (a * g);

       A2:

      now

        

         A3: ( 0 / |.a.|) = 0 ;

        assume

         A4: a <> 0 ;

        then

         A5: |.a.| > 0 by COMPLEX1: 47;

        let r;

        assume r > 0 ;

        then

        consider m1 such that

         A6: for n st n >= m1 holds ( dist ((seq . n),g)) < (r / |.a.|) by A1, A5, A3, XREAL_1: 74;

        take k = m1;

        let n;

        assume n >= k;

        then

         A7: ( dist ((seq . n),g)) < (r / |.a.|) by A6;

        

         A8: |.a.| <> 0 by A4, COMPLEX1: 47;

        

         A9: ( |.a.| * (r / |.a.|)) = ( |.a.| * (( |.a.| " ) * r)) by XCMPLX_0:def 9

        .= (( |.a.| * ( |.a.| " )) * r)

        .= (1 * r) by A8, XCMPLX_0:def 7

        .= r;

        ( dist ((a * (seq . n)),(a * g))) = ||.((a * (seq . n)) - (a * g)).|| by BHSP_1:def 5

        .= ||.(a * ((seq . n) - g)).|| by RLVECT_1: 34

        .= ( |.a.| * ||.((seq . n) - g).||) by BHSP_1: 27

        .= ( |.a.| * ( dist ((seq . n),g))) by BHSP_1:def 5;

        then ( dist ((a * (seq . n)),h)) < r by A5, A7, A9, XREAL_1: 68;

        hence ( dist (((a * seq) . n),h)) < r by NORMSP_1:def 5;

      end;

      now

        assume

         A10: a = 0 ;

        let r;

        assume r > 0 ;

        then

        consider m1 such that

         A11: for n st n >= m1 holds ( dist ((seq . n),g)) < r by A1;

        take k = m1;

        let n;

        assume n >= k;

        then

         A12: ( dist ((seq . n),g)) < r by A11;

        ( dist ((a * (seq . n)),(a * g))) = ( dist (( 0 * (seq . n)), 09(X))) by A10, RLVECT_1: 10

        .= ( dist ( 09(X), 09(X))) by RLVECT_1: 10

        .= 0 by BHSP_1: 34;

        then ( dist ((a * (seq . n)),h)) < r by A12, BHSP_1: 37;

        hence ( dist (((a * seq) . n),h)) < r by NORMSP_1:def 5;

      end;

      hence thesis by A2;

    end;

    theorem :: BHSP_2:6

    

     Th6: seq is convergent implies ( - seq) is convergent

    proof

      assume seq is convergent;

      then (( - 1) * seq) is convergent by Th5;

      hence thesis by BHSP_1: 55;

    end;

    theorem :: BHSP_2:7

    

     Th7: seq is convergent implies (seq + x) is convergent

    proof

      assume seq is convergent;

      then

      consider g such that

       A1: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),g)) < r;

      take (g + x);

      let r;

      assume r > 0 ;

      then

      consider m1 such that

       A2: for n st n >= m1 holds ( dist ((seq . n),g)) < r by A1;

      take k = m1;

      let n;

      ( dist (((seq . n) + x),(g + x))) <= (( dist ((seq . n),g)) + ( dist (x,x))) by BHSP_1: 40;

      then

       A3: ( dist (((seq . n) + x),(g + x))) <= (( dist ((seq . n),g)) + 0 ) by BHSP_1: 34;

      assume n >= k;

      then ( dist ((seq . n),g)) < r by A2;

      then ( dist (((seq . n) + x),(g + x))) < r by A3, XXREAL_0: 2;

      hence thesis by BHSP_1:def 6;

    end;

    theorem :: BHSP_2:8

    

     Th8: seq is convergent implies (seq - x) is convergent

    proof

      assume seq is convergent;

      then (seq + ( - x)) is convergent by Th7;

      hence thesis by BHSP_1: 56;

    end;

    theorem :: BHSP_2:9

    

     Th9: seq is convergent iff ex g st for r st r > 0 holds ex m st for n st n >= m holds ||.((seq . n) - g).|| < r

    proof

      thus seq is convergent implies ex g st for r st r > 0 holds ex m st for n st n >= m holds ||.((seq . n) - g).|| < r

      proof

        assume seq is convergent;

        then

        consider g such that

         A1: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),g)) < r;

        take g;

        let r;

        assume r > 0 ;

        then

        consider m1 such that

         A2: for n st n >= m1 holds ( dist ((seq . n),g)) < r by A1;

        take k = m1;

        let n;

        assume n >= k;

        then ( dist ((seq . n),g)) < r by A2;

        hence thesis by BHSP_1:def 5;

      end;

      (ex g st for r st r > 0 holds ex m st for n st n >= m holds ||.((seq . n) - g).|| < r) implies seq is convergent

      proof

        given g such that

         A3: for r st r > 0 holds ex m st for n st n >= m holds ||.((seq . n) - g).|| < r;

        take g;

        let r;

        assume r > 0 ;

        then

        consider m1 such that

         A4: for n st n >= m1 holds ||.((seq . n) - g).|| < r by A3;

        take k = m1;

        let n;

        assume n >= k;

        then ||.((seq . n) - g).|| < r by A4;

        hence thesis by BHSP_1:def 5;

      end;

      hence thesis;

    end;

    definition

      let X, seq;

      assume

       A1: seq is convergent;

      :: BHSP_2:def2

      func lim seq -> Point of X means

      : Def2: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),it )) < r;

      existence by A1;

      uniqueness

      proof

        for x, y st (for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),x)) < r) & (for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),y)) < r) holds x = y

        proof

          given x, y such that

           A2: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),x)) < r and

           A3: for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq . n),y)) < r and

           A4: x <> y;

          

           A5: ( dist (x,y)) > 0 by A4, BHSP_1: 38;

          then

           A6: (( dist (x,y)) / 4) > ( 0 / 4) by XREAL_1: 74;

          then

          consider m1 such that

           A7: for n st n >= m1 holds ( dist ((seq . n),x)) < (( dist (x,y)) / 4) by A2;

          consider m2 such that

           A8: for n st n >= m2 holds ( dist ((seq . n),y)) < (( dist (x,y)) / 4) by A3, A6;

           A9:

          now

            assume m1 >= m2;

            then

             A10: ( dist ((seq . m1),y)) < (( dist (x,y)) / 4) by A8;

            ( dist (x,y)) = ( dist ((x - (seq . m1)),(y - (seq . m1)))) by BHSP_1: 42;

            then

             A11: ( dist (x,y)) <= (( dist ((seq . m1),x)) + ( dist ((seq . m1),y))) by BHSP_1: 43;

            ( dist ((seq . m1),x)) < (( dist (x,y)) / 4) by A7;

            then (( dist ((seq . m1),x)) + ( dist ((seq . m1),y))) < ((( dist (x,y)) / 4) + (( dist (x,y)) / 4)) by A10, XREAL_1: 8;

            then ( dist (x,y)) <= (( dist (x,y)) / 2) by A11, XXREAL_0: 2;

            hence contradiction by A5, XREAL_1: 216;

          end;

          now

            assume m1 <= m2;

            then

             A12: ( dist ((seq . m2),x)) < (( dist (x,y)) / 4) by A7;

            ( dist (x,y)) = ( dist ((x - (seq . m2)),(y - (seq . m2)))) by BHSP_1: 42;

            then

             A13: ( dist (x,y)) <= (( dist ((seq . m2),x)) + ( dist ((seq . m2),y))) by BHSP_1: 43;

            ( dist ((seq . m2),y)) < (( dist (x,y)) / 4) by A8;

            then (( dist ((seq . m2),x)) + ( dist ((seq . m2),y))) < ((( dist (x,y)) / 4) + (( dist (x,y)) / 4)) by A12, XREAL_1: 8;

            then ( dist (x,y)) <= (( dist (x,y)) / 2) by A13, XXREAL_0: 2;

            hence contradiction by A5, XREAL_1: 216;

          end;

          hence contradiction by A9;

        end;

        hence thesis;

      end;

    end

    theorem :: BHSP_2:10

    

     Th10: seq is constant & x in ( rng seq) implies ( lim seq) = x

    proof

      assume that

       A1: seq is constant and

       A2: x in ( rng seq);

      consider y such that

       A3: ( rng seq) = {y} by A1, FUNCT_2: 111;

      consider z such that

       A4: for n be Nat holds (seq . n) = z by A1, VALUED_0:def 18;

      

       A5: x = y by A2, A3, TARSKI:def 1;

       A6:

      now

        let r such that

         A7: r > 0 ;

        reconsider m = 0 as Nat;

        take m;

        let n such that n >= m;

        n in NAT by ORDINAL1:def 12;

        then n in ( dom seq) by NORMSP_1: 12;

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

        then z in ( rng seq) by A4;

        then z = x by A3, A5, TARSKI:def 1;

        then (seq . n) = x by A4;

        hence ( dist ((seq . n),x)) < r by A7, BHSP_1: 34;

      end;

      seq is convergent by A1;

      hence thesis by A6, Def2;

    end;

    theorem :: BHSP_2:11

    seq is constant & (ex n st (seq . n) = x) implies ( lim seq) = x

    proof

      assume that

       A1: seq is constant and

       A2: ex n st (seq . n) = x;

      consider n such that

       A3: (seq . n) = x by A2;

      n in NAT by ORDINAL1:def 12;

      then n in ( dom seq) by NORMSP_1: 12;

      then x in ( rng seq) by A3, FUNCT_1:def 3;

      hence thesis by A1, Th10;

    end;

    theorem :: BHSP_2:12

    seq is convergent & (ex k st for n st n >= k holds (seq9 . n) = (seq . n)) implies ( lim seq) = ( lim seq9)

    proof

      assume that

       A1: seq is convergent and

       A2: ex k st for n st n >= k holds (seq9 . n) = (seq . n);

      consider k such that

       A3: for n st n >= k holds (seq9 . n) = (seq . n) by A2;

       A4:

      now

        let r;

        assume r > 0 ;

        then

        consider m1 such that

         A5: for n st n >= m1 holds ( dist ((seq . n),( lim seq))) < r by A1, Def2;

         A6:

        now

          assume

           A7: m1 <= k;

          take m = k;

          let n;

          assume

           A8: n >= m;

          then n >= m1 by A7, XXREAL_0: 2;

          then ( dist ((seq . n),( lim seq))) < r by A5;

          hence ( dist ((seq9 . n),( lim seq))) < r by A3, A8;

        end;

        now

          assume

           A9: k <= m1;

          take m = m1;

          let n;

          assume

           A10: n >= m;

          then (seq9 . n) = (seq . n) by A3, A9, XXREAL_0: 2;

          hence ( dist ((seq9 . n),( lim seq))) < r by A5, A10;

        end;

        hence ex m st for n st n >= m holds ( dist ((seq9 . n),( lim seq))) < r by A6;

      end;

      seq9 is convergent by A1, A2, Th2;

      hence thesis by A4, Def2;

    end;

    theorem :: BHSP_2:13

    

     Th13: seq1 is convergent & seq2 is convergent implies ( lim (seq1 + seq2)) = (( lim seq1) + ( lim seq2))

    proof

      assume that

       A1: seq1 is convergent and

       A2: seq2 is convergent;

      set g2 = ( lim seq2);

      set g1 = ( lim seq1);

      set g = (g1 + g2);

       A3:

      now

        let r;

        assume r > 0 ;

        then

         A4: (r / 2) > 0 by XREAL_1: 215;

        then

        consider m1 such that

         A5: for n st n >= m1 holds ( dist ((seq1 . n),g1)) < (r / 2) by A1, Def2;

        consider m2 such that

         A6: for n st n >= m2 holds ( dist ((seq2 . n),g2)) < (r / 2) by A2, A4, Def2;

        take k = (m1 + m2);

        let n such that

         A7: n >= k;

        k >= m2 by NAT_1: 12;

        then n >= m2 by A7, XXREAL_0: 2;

        then

         A8: ( dist ((seq2 . n),g2)) < (r / 2) by A6;

        ( dist (((seq1 + seq2) . n),g)) = ( dist (((seq1 . n) + (seq2 . n)),(g1 + g2))) by NORMSP_1:def 2;

        then

         A9: ( dist (((seq1 + seq2) . n),g)) <= (( dist ((seq1 . n),g1)) + ( dist ((seq2 . n),g2))) by BHSP_1: 40;

        (m1 + m2) >= m1 by NAT_1: 12;

        then n >= m1 by A7, XXREAL_0: 2;

        then ( dist ((seq1 . n),g1)) < (r / 2) by A5;

        then (( dist ((seq1 . n),g1)) + ( dist ((seq2 . n),g2))) < ((r / 2) + (r / 2)) by A8, XREAL_1: 8;

        hence ( dist (((seq1 + seq2) . n),g)) < r by A9, XXREAL_0: 2;

      end;

      (seq1 + seq2) is convergent by A1, A2, Th3;

      hence thesis by A3, Def2;

    end;

    theorem :: BHSP_2:14

    

     Th14: seq1 is convergent & seq2 is convergent implies ( lim (seq1 - seq2)) = (( lim seq1) - ( lim seq2))

    proof

      assume that

       A1: seq1 is convergent and

       A2: seq2 is convergent;

      set g2 = ( lim seq2);

      set g1 = ( lim seq1);

      set g = (g1 - g2);

       A3:

      now

        let r;

        assume r > 0 ;

        then

         A4: (r / 2) > 0 by XREAL_1: 215;

        then

        consider m1 such that

         A5: for n st n >= m1 holds ( dist ((seq1 . n),g1)) < (r / 2) by A1, Def2;

        consider m2 such that

         A6: for n st n >= m2 holds ( dist ((seq2 . n),g2)) < (r / 2) by A2, A4, Def2;

        take k = (m1 + m2);

        let n such that

         A7: n >= k;

        k >= m2 by NAT_1: 12;

        then n >= m2 by A7, XXREAL_0: 2;

        then

         A8: ( dist ((seq2 . n),g2)) < (r / 2) by A6;

        ( dist (((seq1 - seq2) . n),g)) = ( dist (((seq1 . n) - (seq2 . n)),(g1 - g2))) by NORMSP_1:def 3;

        then

         A9: ( dist (((seq1 - seq2) . n),g)) <= (( dist ((seq1 . n),g1)) + ( dist ((seq2 . n),g2))) by BHSP_1: 41;

        (m1 + m2) >= m1 by NAT_1: 12;

        then n >= m1 by A7, XXREAL_0: 2;

        then ( dist ((seq1 . n),g1)) < (r / 2) by A5;

        then (( dist ((seq1 . n),g1)) + ( dist ((seq2 . n),g2))) < ((r / 2) + (r / 2)) by A8, XREAL_1: 8;

        hence ( dist (((seq1 - seq2) . n),g)) < r by A9, XXREAL_0: 2;

      end;

      (seq1 - seq2) is convergent by A1, A2, Th4;

      hence thesis by A3, Def2;

    end;

    theorem :: BHSP_2:15

    

     Th15: seq is convergent implies ( lim (a * seq)) = (a * ( lim seq))

    proof

      set g = ( lim seq);

      set h = (a * g);

      assume

       A1: seq is convergent;

       A2:

      now

        assume

         A3: a = 0 ;

        let r;

        assume r > 0 ;

        then

        consider m1 such that

         A4: for n st n >= m1 holds ( dist ((seq . n),g)) < r by A1, Def2;

        take k = m1;

        let n;

        assume n >= k;

        then

         A5: ( dist ((seq . n),g)) < r by A4;

        ( dist ((a * (seq . n)),(a * g))) = ( dist (( 0 * (seq . n)), 09(X))) by A3, RLVECT_1: 10

        .= ( dist ( 09(X), 09(X))) by RLVECT_1: 10

        .= 0 by BHSP_1: 34;

        then ( dist ((a * (seq . n)),h)) < r by A5, BHSP_1: 37;

        hence ( dist (((a * seq) . n),h)) < r by NORMSP_1:def 5;

      end;

       A6:

      now

        

         A7: ( 0 / |.a.|) = 0 ;

        assume

         A8: a <> 0 ;

        then

         A9: |.a.| > 0 by COMPLEX1: 47;

        let r;

        assume r > 0 ;

        then (r / |.a.|) > 0 by A9, A7, XREAL_1: 74;

        then

        consider m1 such that

         A10: for n st n >= m1 holds ( dist ((seq . n),g)) < (r / |.a.|) by A1, Def2;

        take k = m1;

        let n;

        assume n >= k;

        then

         A11: ( dist ((seq . n),g)) < (r / |.a.|) by A10;

        

         A12: |.a.| <> 0 by A8, COMPLEX1: 47;

        

         A13: ( |.a.| * (r / |.a.|)) = ( |.a.| * (( |.a.| " ) * r)) by XCMPLX_0:def 9

        .= (( |.a.| * ( |.a.| " )) * r)

        .= (1 * r) by A12, XCMPLX_0:def 7

        .= r;

        ( dist ((a * (seq . n)),(a * g))) = ||.((a * (seq . n)) - (a * g)).|| by BHSP_1:def 5

        .= ||.(a * ((seq . n) - g)).|| by RLVECT_1: 34

        .= ( |.a.| * ||.((seq . n) - g).||) by BHSP_1: 27

        .= ( |.a.| * ( dist ((seq . n),g))) by BHSP_1:def 5;

        then ( dist ((a * (seq . n)),h)) < r by A9, A11, A13, XREAL_1: 68;

        hence ( dist (((a * seq) . n),h)) < r by NORMSP_1:def 5;

      end;

      (a * seq) is convergent by A1, Th5;

      hence thesis by A2, A6, Def2;

    end;

    theorem :: BHSP_2:16

    

     Th16: seq is convergent implies ( lim ( - seq)) = ( - ( lim seq))

    proof

      assume seq is convergent;

      then ( lim (( - 1) * seq)) = (( - 1) * ( lim seq)) by Th15;

      then ( lim ( - seq)) = (( - 1) * ( lim seq)) by BHSP_1: 55;

      hence thesis by RLVECT_1: 16;

    end;

    theorem :: BHSP_2:17

    

     Th17: seq is convergent implies ( lim (seq + x)) = (( lim seq) + x)

    proof

      set g = ( lim seq);

      assume

       A1: seq is convergent;

       A2:

      now

        let r;

        assume r > 0 ;

        then

        consider m1 such that

         A3: for n st n >= m1 holds ( dist ((seq . n),g)) < r by A1, Def2;

        take k = m1;

        let n;

        assume n >= k;

        then

         A4: ( dist ((seq . n),g)) < r by A3;

        ( dist ((seq . n),g)) = ( dist (((seq . n) - ( - x)),(g - ( - x)))) by BHSP_1: 42

        .= ( dist (((seq . n) + ( - ( - x))),(g - ( - x)))) by RLVECT_1:def 11

        .= ( dist (((seq . n) + x),(g - ( - x)))) by RLVECT_1: 17

        .= ( dist (((seq . n) + x),(g + ( - ( - x))))) by RLVECT_1:def 11

        .= ( dist (((seq . n) + x),(g + x))) by RLVECT_1: 17;

        hence ( dist (((seq + x) . n),(g + x))) < r by A4, BHSP_1:def 6;

      end;

      (seq + x) is convergent by A1, Th7;

      hence thesis by A2, Def2;

    end;

    theorem :: BHSP_2:18

    seq is convergent implies ( lim (seq - x)) = (( lim seq) - x)

    proof

      assume seq is convergent;

      then ( lim (seq + ( - x))) = (( lim seq) + ( - x)) by Th17;

      then ( lim (seq - x)) = (( lim seq) + ( - x)) by BHSP_1: 56;

      hence thesis by RLVECT_1:def 11;

    end;

    theorem :: BHSP_2:19

    

     Th19: seq is convergent implies (( lim seq) = g iff for r st r > 0 holds ex m st for n st n >= m holds ||.((seq . n) - g).|| < r)

    proof

      assume

       A1: seq is convergent;

      thus ( lim seq) = g implies for r st r > 0 holds ex m st for n st n >= m holds ||.((seq . n) - g).|| < r

      proof

        assume

         A2: ( lim seq) = g;

        let r;

        assume r > 0 ;

        then

        consider m1 such that

         A3: for n st n >= m1 holds ( dist ((seq . n),g)) < r by A1, A2, Def2;

        take k = m1;

        let n;

        assume n >= k;

        then ( dist ((seq . n),g)) < r by A3;

        hence thesis by BHSP_1:def 5;

      end;

      (for r st r > 0 holds ex m st for n st n >= m holds ||.((seq . n) - g).|| < r) implies ( lim seq) = g

      proof

        assume

         A4: for r st r > 0 holds ex m st for n st n >= m holds ||.((seq . n) - g).|| < r;

        now

          let r;

          assume r > 0 ;

          then

          consider m1 such that

           A5: for n st n >= m1 holds ||.((seq . n) - g).|| < r by A4;

          take k = m1;

          let n;

          assume n >= k;

          then ||.((seq . n) - g).|| < r by A5;

          hence ( dist ((seq . n),g)) < r by BHSP_1:def 5;

        end;

        hence thesis by A1, Def2;

      end;

      hence thesis;

    end;

    definition

      let X, seq;

      :: BHSP_2:def3

      func ||.seq.|| -> Real_Sequence means

      : Def3: for n holds (it . n) = ||.(seq . n).||;

      existence

      proof

        deffunc F( Nat) = ||.(seq . $1).||;

        consider s be Real_Sequence such that

         A1: for n be Nat holds (s . n) = F(n) from SEQ_1:sch 1;

        take s;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let s,t be Real_Sequence;

        assume that

         A2: for n holds (s . n) = ||.(seq . n).|| and

         A3: for n holds (t . n) = ||.(seq . n).||;

        now

          let n be Element of NAT ;

          (s . n) = ||.(seq . n).|| by A2;

          hence (s . n) = (t . n) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: BHSP_2:20

    

     Th20: seq is convergent implies ||.seq.|| is convergent

    proof

      assume seq is convergent;

      then

      consider g such that

       A1: for r st r > 0 holds ex m st for n st n >= m holds ||.((seq . n) - g).|| < r by Th9;

      now

        let r be Real;

        assume

         A2: r > 0 ;

        consider m1 such that

         A3: for n st n >= m1 holds ||.((seq . n) - g).|| < r by A1, A2;

        reconsider k = m1 as Nat;

        take k;

        now

          let n be Nat;

          assume n >= k;

          then

           A4: ||.((seq . n) - g).|| < r by A3;

           |.( ||.(seq . n).|| - ||.g.||).| <= ||.((seq . n) - g).|| by BHSP_1: 33;

          then |.( ||.(seq . n).|| - ||.g.||).| < r by A4, XXREAL_0: 2;

          hence |.(( ||.seq.|| . n) - ||.g.||).| < r by Def3;

        end;

        hence for n be Nat st k <= n holds |.(( ||.seq.|| . n) - ||.g.||).| < r;

      end;

      hence thesis by SEQ_2:def 6;

    end;

    theorem :: BHSP_2:21

    

     Th21: seq is convergent & ( lim seq) = g implies ||.seq.|| is convergent & ( lim ||.seq.||) = ||.g.||

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) = g;

       A3:

      now

        let r be Real;

        assume

         A4: r > 0 ;

        consider m1 such that

         A5: for n st n >= m1 holds ||.((seq . n) - g).|| < r by A1, A2, A4, Th19;

        reconsider k = m1 as Nat;

        take k;

        now

          let n be Nat;

          assume n >= k;

          then

           A6: ||.((seq . n) - g).|| < r by A5;

           |.( ||.(seq . n).|| - ||.g.||).| <= ||.((seq . n) - g).|| by BHSP_1: 33;

          then |.( ||.(seq . n).|| - ||.g.||).| < r by A6, XXREAL_0: 2;

          hence |.(( ||.seq.|| . n) - ||.g.||).| < r by Def3;

        end;

        hence for n be Nat st k <= n holds |.(( ||.seq.|| . n) - ||.g.||).| < r;

      end;

       ||.seq.|| is convergent by A1, Th20;

      hence thesis by A3, SEQ_2:def 7;

    end;

    theorem :: BHSP_2:22

    

     Th22: seq is convergent & ( lim seq) = g implies ||.(seq - g).|| is convergent & ( lim ||.(seq - g).||) = 0

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) = g;

       A3:

      now

        let r be Real;

        assume

         A4: r > 0 ;

        consider m1 such that

         A5: for n st n >= m1 holds ||.((seq . n) - g).|| < r by A1, A2, A4, Th19;

        reconsider k = m1 as Nat;

        take k;

        let n be Nat;

        assume n >= k;

        then ||.((seq . n) - g).|| < r by A5;

        then

         A6: ||.(((seq . n) - g) - 09(X)).|| < r by RLVECT_1: 13;

         |.( ||.((seq . n) - g).|| - ||. 09(X).||).| <= ||.(((seq . n) - g) - 09(X)).|| by BHSP_1: 33;

        then |.( ||.((seq . n) - g).|| - ||. 09(X).||).| < r by A6, XXREAL_0: 2;

        then |.( ||.((seq . n) - g).|| - 0 ).| < r by BHSP_1: 26;

        then |.( ||.((seq - g) . n).|| - 0 ).| < r by NORMSP_1:def 4;

        hence |.(( ||.(seq - g).|| . n) - 0 ).| < r by Def3;

      end;

       ||.(seq - g).|| is convergent by A1, Th8, Th20;

      hence thesis by A3, SEQ_2:def 7;

    end;

    definition

      let X;

      let seq;

      let x;

      :: BHSP_2:def4

      func dist (seq,x) -> Real_Sequence means

      : Def4: for n holds (it . n) = ( dist ((seq . n),x));

      existence

      proof

        deffunc F( Nat) = ( dist ((seq . $1),x));

        consider s be Real_Sequence such that

         A1: for n be Nat holds (s . n) = F(n) from SEQ_1:sch 1;

        take s;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let s,t be Real_Sequence;

        assume that

         A2: for n holds (s . n) = ( dist ((seq . n),x)) and

         A3: for n holds (t . n) = ( dist ((seq . n),x));

        now

          let n be Element of NAT ;

          (s . n) = ( dist ((seq . n),x)) by A2;

          hence (s . n) = (t . n) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: BHSP_2:23

    

     Th23: seq is convergent & ( lim seq) = g implies ( dist (seq,g)) is convergent

    proof

      assume

       A1: seq is convergent & ( lim seq) = g;

      now

        let r be Real;

        assume

         A2: r > 0 ;

        consider m1 such that

         A3: for n st n >= m1 holds ( dist ((seq . n),g)) < r by A1, A2, Def2;

        reconsider k = m1 as Nat;

        take k;

        now

          let n be Nat;

          ( dist ((seq . n),g)) >= 0 by BHSP_1: 37;

          then

           A4: |.(( dist ((seq . n),g)) - 0 ).| = ( dist ((seq . n),g)) by ABSVALUE:def 1;

          assume n >= k;

          then ( dist ((seq . n),g)) < r by A3;

          hence |.((( dist (seq,g)) . n) - 0 ).| < r by A4, Def4;

        end;

        hence for n be Nat st k <= n holds |.((( dist (seq,g)) . n) - 0 ).| < r;

      end;

      hence thesis by SEQ_2:def 6;

    end;

    theorem :: BHSP_2:24

    

     Th24: seq is convergent & ( lim seq) = g implies ( dist (seq,g)) is convergent & ( lim ( dist (seq,g))) = 0

    proof

      assume

       A1: seq is convergent & ( lim seq) = g;

       A2:

      now

        let r be Real;

        assume

         A3: r > 0 ;

        consider m1 such that

         A4: for n st n >= m1 holds ( dist ((seq . n),g)) < r by A1, A3, Def2;

        reconsider k = m1 as Nat;

        take k;

        let n be Nat;

        ( dist ((seq . n),g)) >= 0 by BHSP_1: 37;

        then

         A5: |.(( dist ((seq . n),g)) - 0 ).| = ( dist ((seq . n),g)) by ABSVALUE:def 1;

        assume n >= k;

        then ( dist ((seq . n),g)) < r by A4;

        hence |.((( dist (seq,g)) . n) - 0 ).| < r by A5, Def4;

      end;

      ( dist (seq,g)) is convergent by A1, Th23;

      hence thesis by A2, SEQ_2:def 7;

    end;

    theorem :: BHSP_2:25

    seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2 implies ||.(seq1 + seq2).|| is convergent & ( lim ||.(seq1 + seq2).||) = ||.(g1 + g2).||

    proof

      assume seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2;

      then (seq1 + seq2) is convergent & ( lim (seq1 + seq2)) = (g1 + g2) by Th3, Th13;

      hence thesis by Th21;

    end;

    theorem :: BHSP_2:26

    seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2 implies ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & ( lim ||.((seq1 + seq2) - (g1 + g2)).||) = 0

    proof

      assume seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2;

      then (seq1 + seq2) is convergent & ( lim (seq1 + seq2)) = (g1 + g2) by Th3, Th13;

      hence thesis by Th22;

    end;

    theorem :: BHSP_2:27

    seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2 implies ||.(seq1 - seq2).|| is convergent & ( lim ||.(seq1 - seq2).||) = ||.(g1 - g2).||

    proof

      assume seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2;

      then (seq1 - seq2) is convergent & ( lim (seq1 - seq2)) = (g1 - g2) by Th4, Th14;

      hence thesis by Th21;

    end;

    theorem :: BHSP_2:28

    seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2 implies ||.((seq1 - seq2) - (g1 - g2)).|| is convergent & ( lim ||.((seq1 - seq2) - (g1 - g2)).||) = 0

    proof

      assume seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2;

      then (seq1 - seq2) is convergent & ( lim (seq1 - seq2)) = (g1 - g2) by Th4, Th14;

      hence thesis by Th22;

    end;

    theorem :: BHSP_2:29

    seq is convergent & ( lim seq) = g implies ||.(a * seq).|| is convergent & ( lim ||.(a * seq).||) = ||.(a * g).||

    proof

      assume seq is convergent & ( lim seq) = g;

      then (a * seq) is convergent & ( lim (a * seq)) = (a * g) by Th5, Th15;

      hence thesis by Th21;

    end;

    theorem :: BHSP_2:30

    seq is convergent & ( lim seq) = g implies ||.((a * seq) - (a * g)).|| is convergent & ( lim ||.((a * seq) - (a * g)).||) = 0

    proof

      assume seq is convergent & ( lim seq) = g;

      then (a * seq) is convergent & ( lim (a * seq)) = (a * g) by Th5, Th15;

      hence thesis by Th22;

    end;

    theorem :: BHSP_2:31

    seq is convergent & ( lim seq) = g implies ||.( - seq).|| is convergent & ( lim ||.( - seq).||) = ||.( - g).||

    proof

      assume seq is convergent & ( lim seq) = g;

      then ( - seq) is convergent & ( lim ( - seq)) = ( - g) by Th6, Th16;

      hence thesis by Th21;

    end;

    theorem :: BHSP_2:32

    seq is convergent & ( lim seq) = g implies ||.(( - seq) - ( - g)).|| is convergent & ( lim ||.(( - seq) - ( - g)).||) = 0

    proof

      assume seq is convergent & ( lim seq) = g;

      then ( - seq) is convergent & ( lim ( - seq)) = ( - g) by Th6, Th16;

      hence thesis by Th22;

    end;

    

     Lm1: seq is convergent & ( lim seq) = g implies ||.(seq + x).|| is convergent & ( lim ||.(seq + x).||) = ||.(g + x).||

    proof

      assume seq is convergent & ( lim seq) = g;

      then (seq + x) is convergent & ( lim (seq + x)) = (g + x) by Th7, Th17;

      hence thesis by Th21;

    end;

    theorem :: BHSP_2:33

    

     Th33: seq is convergent & ( lim seq) = g implies ||.((seq + x) - (g + x)).|| is convergent & ( lim ||.((seq + x) - (g + x)).||) = 0

    proof

      assume seq is convergent & ( lim seq) = g;

      then (seq + x) is convergent & ( lim (seq + x)) = (g + x) by Th7, Th17;

      hence thesis by Th22;

    end;

    theorem :: BHSP_2:34

    seq is convergent & ( lim seq) = g implies ||.(seq - x).|| is convergent & ( lim ||.(seq - x).||) = ||.(g - x).||

    proof

      assume

       A1: seq is convergent & ( lim seq) = g;

      then ( lim ||.(seq + ( - x)).||) = ||.(g + ( - x)).|| by Lm1;

      then

       A2: ( lim ||.(seq - x).||) = ||.(g + ( - x)).|| by BHSP_1: 56;

       ||.(seq + ( - x)).|| is convergent by A1, Lm1;

      hence thesis by A2, BHSP_1: 56, RLVECT_1:def 11;

    end;

    theorem :: BHSP_2:35

    seq is convergent & ( lim seq) = g implies ||.((seq - x) - (g - x)).|| is convergent & ( lim ||.((seq - x) - (g - x)).||) = 0

    proof

      assume

       A1: seq is convergent & ( lim seq) = g;

      then ( lim ||.((seq + ( - x)) - (g + ( - x))).||) = 0 by Th33;

      then

       A2: ( lim ||.((seq - x) - (g + ( - x))).||) = 0 by BHSP_1: 56;

       ||.((seq + ( - x)) - (g + ( - x))).|| is convergent by A1, Th33;

      then ||.((seq - x) - (g + ( - x))).|| is convergent by BHSP_1: 56;

      hence thesis by A2, RLVECT_1:def 11;

    end;

    theorem :: BHSP_2:36

    seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2 implies ( dist ((seq1 + seq2),(g1 + g2))) is convergent & ( lim ( dist ((seq1 + seq2),(g1 + g2)))) = 0

    proof

      assume seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2;

      then (seq1 + seq2) is convergent & ( lim (seq1 + seq2)) = (g1 + g2) by Th3, Th13;

      hence thesis by Th24;

    end;

    theorem :: BHSP_2:37

    seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2 implies ( dist ((seq1 - seq2),(g1 - g2))) is convergent & ( lim ( dist ((seq1 - seq2),(g1 - g2)))) = 0

    proof

      assume seq1 is convergent & ( lim seq1) = g1 & seq2 is convergent & ( lim seq2) = g2;

      then (seq1 - seq2) is convergent & ( lim (seq1 - seq2)) = (g1 - g2) by Th4, Th14;

      hence thesis by Th24;

    end;

    theorem :: BHSP_2:38

    seq is convergent & ( lim seq) = g implies ( dist ((a * seq),(a * g))) is convergent & ( lim ( dist ((a * seq),(a * g)))) = 0

    proof

      assume seq is convergent & ( lim seq) = g;

      then (a * seq) is convergent & ( lim (a * seq)) = (a * g) by Th5, Th15;

      hence thesis by Th24;

    end;

    theorem :: BHSP_2:39

    seq is convergent & ( lim seq) = g implies ( dist ((seq + x),(g + x))) is convergent & ( lim ( dist ((seq + x),(g + x)))) = 0

    proof

      assume seq is convergent & ( lim seq) = g;

      then (seq + x) is convergent & ( lim (seq + x)) = (g + x) by Th7, Th17;

      hence thesis by Th24;

    end;

    definition

      let X, x, r;

      :: BHSP_2:def5

      func Ball (x,r) -> Subset of X equals { y where y be Point of X : ||.(x - y).|| < r };

      coherence

      proof

        defpred P[ Point of X] means ||.(x - $1).|| < r;

        { y where y be Point of X : P[y] } c= the carrier of X from FRAENKEL:sch 10;

        hence thesis;

      end;

      :: BHSP_2:def6

      func cl_Ball (x,r) -> Subset of X equals { y where y be Point of X : ||.(x - y).|| <= r };

      coherence

      proof

        defpred P[ Point of X] means ||.(x - $1).|| <= r;

        { y where y be Point of X : P[y] } c= the carrier of X from FRAENKEL:sch 10;

        hence thesis;

      end;

      :: BHSP_2:def7

      func Sphere (x,r) -> Subset of X equals { y where y be Point of X : ||.(x - y).|| = r };

      coherence

      proof

        defpred P[ Point of X] means ||.(x - $1).|| = r;

        { y where y be Point of X : P[y] } c= the carrier of X from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: BHSP_2:40

    

     Th40: z in ( Ball (x,r)) iff ||.(x - z).|| < r

    proof

      thus z in ( Ball (x,r)) implies ||.(x - z).|| < r

      proof

        assume z in ( Ball (x,r));

        then ex y be Point of X st z = y & ||.(x - y).|| < r;

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: BHSP_2:41

    

     Th41: z in ( Ball (x,r)) iff ( dist (x,z)) < r

    proof

      thus z in ( Ball (x,r)) implies ( dist (x,z)) < r

      proof

        assume z in ( Ball (x,r));

        then ||.(x - z).|| < r by Th40;

        hence thesis by BHSP_1:def 5;

      end;

      assume ( dist (x,z)) < r;

      then ||.(x - z).|| < r by BHSP_1:def 5;

      hence thesis;

    end;

    theorem :: BHSP_2:42

    r > 0 implies x in ( Ball (x,r))

    proof

      

       A1: ( dist (x,x)) = 0 by BHSP_1: 34;

      assume r > 0 ;

      hence thesis by A1, Th41;

    end;

    theorem :: BHSP_2:43

    y in ( Ball (x,r)) & z in ( Ball (x,r)) implies ( dist (y,z)) < (2 * r)

    proof

      assume that

       A1: y in ( Ball (x,r)) and

       A2: z in ( Ball (x,r));

      ( dist (x,z)) < r by A2, Th41;

      then

       A3: (r + ( dist (x,z))) < (r + r) by XREAL_1: 6;

      

       A4: ( dist (y,z)) <= (( dist (y,x)) + ( dist (x,z))) by BHSP_1: 35;

      ( dist (x,y)) < r by A1, Th41;

      then (( dist (x,y)) + ( dist (x,z))) < (r + ( dist (x,z))) by XREAL_1: 6;

      then (( dist (x,y)) + ( dist (x,z))) < (2 * r) by A3, XXREAL_0: 2;

      hence thesis by A4, XXREAL_0: 2;

    end;

    theorem :: BHSP_2:44

    y in ( Ball (x,r)) implies (y - z) in ( Ball ((x - z),r))

    proof

      assume y in ( Ball (x,r));

      then

       A1: ( dist (x,y)) < r by Th41;

      ( dist ((x - z),(y - z))) = ( dist (x,y)) by BHSP_1: 42;

      hence thesis by A1, Th41;

    end;

    theorem :: BHSP_2:45

    y in ( Ball (x,r)) implies (y - x) in ( Ball (( 0. X),r))

    proof

      assume y in ( Ball (x,r));

      then ||.(x - y).|| < r by Th40;

      then ||.(( - y) + x).|| < r by RLVECT_1:def 11;

      then ||.( - (y - x)).|| < r by RLVECT_1: 33;

      then ||.( 09(X) - (y - x)).|| < r by RLVECT_1: 14;

      hence thesis;

    end;

    theorem :: BHSP_2:46

    y in ( Ball (x,r)) & r <= q implies y in ( Ball (x,q))

    proof

      assume that

       A1: y in ( Ball (x,r)) and

       A2: r <= q;

       ||.(x - y).|| < r by A1, Th40;

      then ||.(x - y).|| < q by A2, XXREAL_0: 2;

      hence thesis;

    end;

    theorem :: BHSP_2:47

    

     Th47: z in ( cl_Ball (x,r)) iff ||.(x - z).|| <= r

    proof

      thus z in ( cl_Ball (x,r)) implies ||.(x - z).|| <= r

      proof

        assume z in ( cl_Ball (x,r));

        then ex y be Point of X st z = y & ||.(x - y).|| <= r;

        hence thesis;

      end;

      assume ||.(x - z).|| <= r;

      hence thesis;

    end;

    theorem :: BHSP_2:48

    

     Th48: z in ( cl_Ball (x,r)) iff ( dist (x,z)) <= r

    proof

      thus z in ( cl_Ball (x,r)) implies ( dist (x,z)) <= r

      proof

        assume z in ( cl_Ball (x,r));

        then ||.(x - z).|| <= r by Th47;

        hence thesis by BHSP_1:def 5;

      end;

      assume ( dist (x,z)) <= r;

      then ||.(x - z).|| <= r by BHSP_1:def 5;

      hence thesis;

    end;

    theorem :: BHSP_2:49

    r >= 0 implies x in ( cl_Ball (x,r))

    proof

      assume r >= 0 ;

      then ( dist (x,x)) <= r by BHSP_1: 34;

      hence thesis by Th48;

    end;

    theorem :: BHSP_2:50

    

     Th50: y in ( Ball (x,r)) implies y in ( cl_Ball (x,r))

    proof

      assume y in ( Ball (x,r));

      then ||.(x - y).|| <= r by Th40;

      hence thesis;

    end;

    theorem :: BHSP_2:51

    

     Th51: z in ( Sphere (x,r)) iff ||.(x - z).|| = r

    proof

      thus z in ( Sphere (x,r)) implies ||.(x - z).|| = r

      proof

        assume z in ( Sphere (x,r));

        then ex y be Point of X st z = y & ||.(x - y).|| = r;

        hence thesis;

      end;

      assume ||.(x - z).|| = r;

      hence thesis;

    end;

    theorem :: BHSP_2:52

    z in ( Sphere (x,r)) iff ( dist (x,z)) = r

    proof

      thus z in ( Sphere (x,r)) implies ( dist (x,z)) = r

      proof

        assume z in ( Sphere (x,r));

        then ||.(x - z).|| = r by Th51;

        hence thesis by BHSP_1:def 5;

      end;

      assume ( dist (x,z)) = r;

      then ||.(x - z).|| = r by BHSP_1:def 5;

      hence thesis;

    end;

    theorem :: BHSP_2:53

    y in ( Sphere (x,r)) implies y in ( cl_Ball (x,r))

    proof

      assume y in ( Sphere (x,r));

      then ||.(x - y).|| = r by Th51;

      hence thesis;

    end;

    theorem :: BHSP_2:54

    

     Th54: ( Ball (x,r)) c= ( cl_Ball (x,r))

    proof

      for y holds y in ( Ball (x,r)) implies y in ( cl_Ball (x,r)) by Th50;

      hence thesis by SUBSET_1: 2;

    end;

    theorem :: BHSP_2:55

    

     Th55: ( Sphere (x,r)) c= ( cl_Ball (x,r))

    proof

      now

        let y;

        assume y in ( Sphere (x,r));

        then ||.(x - y).|| = r by Th51;

        hence y in ( cl_Ball (x,r));

      end;

      hence thesis by SUBSET_1: 2;

    end;

    theorem :: BHSP_2:56

    (( Ball (x,r)) \/ ( Sphere (x,r))) = ( cl_Ball (x,r))

    proof

      now

        let y;

        assume y in ( cl_Ball (x,r));

        then

         A1: ||.(x - y).|| <= r by Th47;

        now

          per cases by A1, XXREAL_0: 1;

            case ||.(x - y).|| < r;

            hence y in ( Ball (x,r));

          end;

            case ||.(x - y).|| = r;

            hence y in ( Sphere (x,r));

          end;

        end;

        hence y in (( Ball (x,r)) \/ ( Sphere (x,r))) by XBOOLE_0:def 3;

      end;

      then

       A2: ( cl_Ball (x,r)) c= (( Ball (x,r)) \/ ( Sphere (x,r))) by SUBSET_1: 2;

      ( Ball (x,r)) c= ( cl_Ball (x,r)) & ( Sphere (x,r)) c= ( cl_Ball (x,r)) by Th54, Th55;

      then (( Ball (x,r)) \/ ( Sphere (x,r))) c= ( cl_Ball (x,r)) by XBOOLE_1: 8;

      hence thesis by A2, XBOOLE_0:def 10;

    end;