clvect_2.miz



    begin

    reserve X for ComplexUnitarySpace;

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

    reserve z for Complex;

    reserve p,q,r,M,M1,M2 for Real;

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

    reserve k,n,m for Nat;

    reserve Nseq for increasing sequence of NAT ;

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

    definition

      let X, seq;

      :: CLVECT_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

    theorem :: CLVECT_2:1

    

     Th1: seq is constant implies seq is convergent

    proof

      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 CSSPACE: 50;

      hence thesis by A2;

    end;

    theorem :: CLVECT_2:2

    

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

    proof

      assume that

       A1: seq1 is convergent and

       A2: ex k st for n st k <= n holds (seq2 . n) = (seq1 . n);

      consider k such that

       A3: for n st n >= k holds (seq2 . n) = (seq1 . n) by A2;

      consider g such that

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

      take h = g;

      let r;

      assume r > 0 ;

      then

      consider m1 be Nat such that

       A5: for n st n >= m1 holds ( dist ((seq1 . 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 ((seq1 . n),g)) < r by A5;

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

      end;

      now

        assume

         A9: k <= m1;

        take m = m1;

        let n;

        assume

         A10: n >= m;

        then (seq2 . n) = (seq1 . n) by A3, A9, XXREAL_0: 2;

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

      end;

      hence thesis by A6;

    end;

    theorem :: CLVECT_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 be Point of X 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 be Nat such that

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

      consider m2 be Nat 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 2;

      then

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

      (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 :: CLVECT_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 be Point of X 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 be Nat such that

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

      consider m2 be Nat 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 CSSPACE: 57;

      (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 :: CLVECT_2:5

    

     Th5: seq is convergent implies (z * 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 = (z * g);

       A2:

      now

        

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

        assume

         A4: z <> 0 ;

        then

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

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

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

        take k = m1;

        let n;

        assume n >= k;

        then

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

        

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

        

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

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

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

        .= r;

        ( dist ((z * (seq . n)),(z * g))) = ||.((z * (seq . n)) - (z * g)).|| by CSSPACE:def 16

        .= ||.(z * ((seq . n) - g)).|| by CLVECT_1: 9

        .= ( |.z.| * ||.((seq . n) - g).||) by CSSPACE: 43

        .= ( |.z.| * ( dist ((seq . n),g))) by CSSPACE:def 16;

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

        hence ( dist (((z * seq) . n),h)) < r by CLVECT_1:def 14;

      end;

      now

        assume

         A10: z = 0 ;

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat 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 ((z * (seq . n)),(z * g))) = ( dist (( 0c * (seq . n)), 09(X))) by A10, CLVECT_1: 1

        .= ( dist ( 09(X), 09(X))) by CLVECT_1: 1

        .= 0 by CSSPACE: 50;

        then ( dist ((z * (seq . n)),h)) < r by A12, CSSPACE: 53;

        hence ( dist (((z * seq) . n),h)) < r by CLVECT_1:def 14;

      end;

      hence thesis by A2;

    end;

    theorem :: CLVECT_2:6

    

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

    proof

      assume seq is convergent;

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

      hence thesis by CSSPACE: 70;

    end;

    theorem :: CLVECT_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 be Nat 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 CSSPACE: 56;

      then

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

      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 :: CLVECT_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 CSSPACE: 71;

    end;

    theorem :: CLVECT_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 be Nat 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 CSSPACE:def 16;

      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 be Nat 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 CSSPACE:def 16;

      end;

      hence thesis;

    end;

    definition

      let X, seq;

      assume

       A1: seq is convergent;

      :: CLVECT_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, CSSPACE: 54;

          then

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

          then

          consider m1 be Nat such that

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

          consider m2 be Nat 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 CSSPACE: 58;

            then

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

            ( 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 CSSPACE: 58;

            then

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

            ( 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 :: CLVECT_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 w such that

       A4: for n be Nat holds (seq . n) = w 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 w in ( rng seq) by A4;

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

        then (seq . n) = x by A4;

        hence ( dist ((seq . n),x)) < r by A7, CSSPACE: 50;

      end;

      seq is convergent by A1, Th1;

      hence thesis by A6, Def2;

    end;

    theorem :: CLVECT_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 :: CLVECT_2:12

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

    proof

      assume that

       A1: seq1 is convergent and

       A2: ex k st for n st n >= k holds (seq2 . n) = (seq1 . n);

      consider k such that

       A3: for n st n >= k holds (seq2 . n) = (seq1 . n) by A2;

       A4:

      now

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

         A5: for n st n >= m1 holds ( dist ((seq1 . n),( lim seq1))) < 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 ((seq1 . n),( lim seq1))) < r by A5;

          hence ( dist ((seq2 . n),( lim seq1))) < r by A3, A8;

        end;

        now

          assume

           A9: k <= m1;

          take m = m1;

          let n;

          assume

           A10: n >= m;

          then (seq2 . n) = (seq1 . n) by A3, A9, XXREAL_0: 2;

          hence ( dist ((seq2 . n),( lim seq1))) < r by A5, A10;

        end;

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

      end;

      seq2 is convergent by A1, A2, Th2;

      hence thesis by A4, Def2;

    end;

    theorem :: CLVECT_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 be Nat such that

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

        consider m2 be Nat 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 CSSPACE: 56;

        (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 :: CLVECT_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 be Nat such that

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

        consider m2 be Nat 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 CSSPACE: 57;

        (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 :: CLVECT_2:15

    

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

    proof

      set g = ( lim seq);

      set h = (z * g);

       A1:

      now

        set m1 = the Nat;

        assume

         A2: z = 0 ;

        let r;

        assume

         A3: r > 0 ;

        take k = m1;

        let n;

        assume n >= k;

        ( dist ((z * (seq . n)),(z * g))) = ( dist (( 0c * (seq . n)), 09(X))) by A2, CLVECT_1: 1

        .= ( dist ( 09(X), 09(X))) by CLVECT_1: 1

        .= 0 by CSSPACE: 50;

        hence ( dist (((z * seq) . n),h)) < r by A3, CLVECT_1:def 14;

      end;

      assume

       A4: seq is convergent;

       A5:

      now

        

         A6: ( 0 / |.z.|) = 0 ;

        assume

         A7: z <> 0 ;

        then

         A8: |.z.| > 0 by COMPLEX1: 47;

        let r;

        assume r > 0 ;

        then (r / |.z.|) > 0 by A8, A6, XREAL_1: 74;

        then

        consider m1 be Nat such that

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

        take k = m1;

        let n;

        assume n >= k;

        then

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

        

         A11: |.z.| <> 0 by A7, COMPLEX1: 47;

        

         A12: ( |.z.| * (r / |.z.|)) = ( |.z.| * (( |.z.| " ) * r)) by XCMPLX_0:def 9

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

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

        .= r;

        ( dist ((z * (seq . n)),(z * g))) = ||.((z * (seq . n)) - (z * g)).|| by CSSPACE:def 16

        .= ||.(z * ((seq . n) - g)).|| by CLVECT_1: 9

        .= ( |.z.| * ||.((seq . n) - g).||) by CSSPACE: 43

        .= ( |.z.| * ( dist ((seq . n),g))) by CSSPACE:def 16;

        then ( dist ((z * (seq . n)),h)) < r by A8, A10, A12, XREAL_1: 68;

        hence ( dist (((z * seq) . n),h)) < r by CLVECT_1:def 14;

      end;

      (z * seq) is convergent by A4, Th5;

      hence thesis by A1, A5, Def2;

    end;

    theorem :: CLVECT_2:16

    

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

    proof

      assume seq is convergent;

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

      then ( lim ( - seq)) = (( - 1r ) * ( lim seq)) by CSSPACE: 70;

      hence thesis by CLVECT_1: 3;

    end;

    theorem :: CLVECT_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 be Nat 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 CSSPACE: 58

        .= ( 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 :: CLVECT_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 CSSPACE: 71;

      hence thesis by RLVECT_1:def 11;

    end;

    theorem :: CLVECT_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 be Nat 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 CSSPACE:def 16;

      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 be Nat 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 CSSPACE:def 16;

        end;

        hence thesis by A1, Def2;

      end;

      hence thesis;

    end;

    definition

      let X, seq;

      :: CLVECT_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 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 :: CLVECT_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 be Nat such that

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

        take k = m1;

        now

          let n;

          assume n >= k;

          then

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

           |.( ||.(seq . n).|| - ||.g.||).| <= ||.((seq . n) - g).|| by CSSPACE: 49;

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

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

        end;

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

      end;

      hence thesis by SEQ_2:def 6;

    end;

    theorem :: CLVECT_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 be Nat such that

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

        take k = m1;

        now

          let n;

          assume n >= k;

          then

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

           |.( ||.(seq . n).|| - ||.g.||).| <= ||.((seq . n) - g).|| by CSSPACE: 49;

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

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

        end;

        hence for n 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 :: CLVECT_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 be Nat such that

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

        take k = m1;

        let n;

        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 CSSPACE: 49;

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

        then |.( ||.((seq . n) - g).|| - 0 ).| < r by CSSPACE: 42;

        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, seq, x;

      :: CLVECT_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 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 :: CLVECT_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 be Nat such that

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

        take k = m1;

        now

          let n;

          ( dist ((seq . n),g)) >= 0 by CSSPACE: 53;

          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 st k <= n holds |.((( dist (seq,g)) . n) - 0 ).| < r;

      end;

      hence thesis by SEQ_2:def 6;

    end;

    theorem :: CLVECT_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 be Nat such that

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

        take k = m1;

        let n;

        ( dist ((seq . n),g)) >= 0 by CSSPACE: 53;

        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 :: CLVECT_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 :: CLVECT_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 :: CLVECT_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 :: CLVECT_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 :: CLVECT_2:29

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

    proof

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

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

      hence thesis by Th21;

    end;

    theorem :: CLVECT_2:30

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

    proof

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

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

      hence thesis by Th22;

    end;

    theorem :: CLVECT_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 :: CLVECT_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 :: CLVECT_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 :: CLVECT_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 CSSPACE: 71;

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

      hence thesis by A2, CSSPACE: 71, RLVECT_1:def 11;

    end;

    theorem :: CLVECT_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 CSSPACE: 71;

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

      then ||.((seq - x) - (g + ( - x))).|| is convergent by CSSPACE: 71;

      hence thesis by A2, RLVECT_1:def 11;

    end;

    theorem :: CLVECT_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 :: CLVECT_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 :: CLVECT_2:38

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

    proof

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

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

      hence thesis by Th24;

    end;

    theorem :: CLVECT_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;

      :: CLVECT_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;

      :: CLVECT_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;

      :: CLVECT_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 :: CLVECT_2:40

    

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

    proof

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

      proof

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

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

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: CLVECT_2:41

    

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

    proof

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

      proof

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

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

        hence thesis by CSSPACE:def 16;

      end;

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

      then ||.(x - w).|| < r by CSSPACE:def 16;

      hence thesis;

    end;

    theorem :: CLVECT_2:42

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

    proof

      

       A1: ( dist (x,x)) = 0 by CSSPACE: 50;

      assume r > 0 ;

      hence thesis by A1, Th41;

    end;

    theorem :: CLVECT_2:43

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

    proof

      assume that

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

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

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

      then

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

      

       A4: ( dist (y,w)) <= (( dist (y,x)) + ( dist (x,w))) by CSSPACE: 51;

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

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

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

      hence thesis by A4, XXREAL_0: 2;

    end;

    theorem :: CLVECT_2:44

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

    proof

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

      then

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

      ( dist ((x - w),(y - w))) = ( dist (x,y)) by CSSPACE: 58;

      hence thesis by A1, Th41;

    end;

    theorem :: CLVECT_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 :: CLVECT_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 :: CLVECT_2:47

    

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

    proof

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

      proof

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

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

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: CLVECT_2:48

    

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

    proof

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

      proof

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

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

        hence thesis by CSSPACE:def 16;

      end;

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

      then ||.(x - w).|| <= r by CSSPACE:def 16;

      hence thesis;

    end;

    theorem :: CLVECT_2:49

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

    proof

      assume r >= 0 ;

      then ( dist (x,x)) <= r by CSSPACE: 50;

      hence thesis by Th48;

    end;

    theorem :: CLVECT_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 :: CLVECT_2:51

    

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

    proof

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

      proof

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

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

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: CLVECT_2:52

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

    proof

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

      proof

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

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

        hence thesis by CSSPACE:def 16;

      end;

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

      then ||.(x - w).|| = r by CSSPACE:def 16;

      hence thesis;

    end;

    theorem :: CLVECT_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 :: CLVECT_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 :: CLVECT_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 :: CLVECT_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;

    begin

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

    definition

      let X;

      let seq;

      :: CLVECT_2:def8

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

    end

    theorem :: CLVECT_2:57

    seq is constant implies seq is Cauchy

    proof

      assume

       A1: seq is constant;

      let r such that

       A2: r > 0 ;

      take k = 0 ;

      let n, m such that n >= k and m >= k;

      ( dist ((seq . n),(seq . m))) = ( dist ((seq . n),(seq . n))) by A1, VALUED_0: 23

      .= 0 by CSSPACE: 50;

      hence thesis by A2;

    end;

    theorem :: CLVECT_2:58

    seq is Cauchy iff for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r

    proof

      thus seq is Cauchy implies for r st r > 0 holds ex k st for n, m st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r

      proof

        assume

         A1: seq is Cauchy;

        let r;

        assume r > 0 ;

        then

        consider l be Nat such that

         A2: for n, m st n >= l & m >= l holds ( dist ((seq . n),(seq . m))) < r by A1;

        take k = l;

        let n, m;

        assume n >= k & m >= k;

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

        hence thesis by CSSPACE:def 16;

      end;

      (for r st r > 0 holds ex k st for n, m st (n >= k & m >= k) holds ||.((seq . n) - (seq . m)).|| < r) implies seq is Cauchy

      proof

        assume

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

        let r;

        assume r > 0 ;

        then

        consider l be Nat such that

         A4: for n, m st n >= l & m >= l holds ||.((seq . n) - (seq . m)).|| < r by A3;

        take k = l;

        let n, m;

        assume n >= k & m >= k;

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

        hence thesis by CSSPACE:def 16;

      end;

      hence thesis;

    end;

    theorem :: CLVECT_2:59

    seq1 is Cauchy & seq2 is Cauchy implies (seq1 + seq2) is Cauchy

    proof

      assume that

       A1: seq1 is Cauchy and

       A2: seq2 is Cauchy;

      let r;

      assume r > 0 ;

      then

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

      then

      consider m1 be Nat such that

       A4: for n, m st n >= m1 & m >= m1 holds ( dist ((seq1 . n),(seq1 . m))) < (r / 2) by A1;

      consider m2 be Nat such that

       A5: for n, m st n >= m2 & m >= m2 holds ( dist ((seq2 . n),(seq2 . m))) < (r / 2) by A2, A3;

      take k = (m1 + m2);

      let n, m such that

       A6: n >= k & m >= k;

      k >= m2 by NAT_1: 12;

      then n >= m2 & m >= m2 by A6, XXREAL_0: 2;

      then

       A7: ( dist ((seq2 . n),(seq2 . m))) < (r / 2) by A5;

      ( dist (((seq1 + seq2) . n),((seq1 + seq2) . m))) = ( dist (((seq1 . n) + (seq2 . n)),((seq1 + seq2) . m))) by NORMSP_1:def 2

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

      then

       A8: ( dist (((seq1 + seq2) . n),((seq1 + seq2) . m))) <= (( dist ((seq1 . n),(seq1 . m))) + ( dist ((seq2 . n),(seq2 . m)))) by CSSPACE: 56;

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

      then n >= m1 & m >= m1 by A6, XXREAL_0: 2;

      then ( dist ((seq1 . n),(seq1 . m))) < (r / 2) by A4;

      then (( dist ((seq1 . n),(seq1 . m))) + ( dist ((seq2 . n),(seq2 . m)))) < ((r / 2) + (r / 2)) by A7, XREAL_1: 8;

      hence thesis by A8, XXREAL_0: 2;

    end;

    theorem :: CLVECT_2:60

    seq1 is Cauchy & seq2 is Cauchy implies (seq1 - seq2) is Cauchy

    proof

      assume that

       A1: seq1 is Cauchy and

       A2: seq2 is Cauchy;

      let r;

      assume r > 0 ;

      then

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

      then

      consider m1 be Nat such that

       A4: for n, m st n >= m1 & m >= m1 holds ( dist ((seq1 . n),(seq1 . m))) < (r / 2) by A1;

      consider m2 be Nat such that

       A5: for n, m st n >= m2 & m >= m2 holds ( dist ((seq2 . n),(seq2 . m))) < (r / 2) by A2, A3;

      take k = (m1 + m2);

      let n, m such that

       A6: n >= k & m >= k;

      k >= m2 by NAT_1: 12;

      then n >= m2 & m >= m2 by A6, XXREAL_0: 2;

      then

       A7: ( dist ((seq2 . n),(seq2 . m))) < (r / 2) by A5;

      ( dist (((seq1 - seq2) . n),((seq1 - seq2) . m))) = ( dist (((seq1 . n) - (seq2 . n)),((seq1 - seq2) . m))) by NORMSP_1:def 3

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

      then

       A8: ( dist (((seq1 - seq2) . n),((seq1 - seq2) . m))) <= (( dist ((seq1 . n),(seq1 . m))) + ( dist ((seq2 . n),(seq2 . m)))) by CSSPACE: 57;

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

      then n >= m1 & m >= m1 by A6, XXREAL_0: 2;

      then ( dist ((seq1 . n),(seq1 . m))) < (r / 2) by A4;

      then (( dist ((seq1 . n),(seq1 . m))) + ( dist ((seq2 . n),(seq2 . m)))) < ((r / 2) + (r / 2)) by A7, XREAL_1: 8;

      hence thesis by A8, XXREAL_0: 2;

    end;

    theorem :: CLVECT_2:61

    

     Th61: seq is Cauchy implies (z * seq) is Cauchy

    proof

      assume

       A1: seq is Cauchy;

       A2:

      now

        

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

        assume

         A4: z <> 0 ;

        then

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

        let r;

        assume r > 0 ;

        then (r / |.z.|) > 0 by A5, A3, XREAL_1: 74;

        then

        consider m1 be Nat such that

         A6: for n, m st n >= m1 & m >= m1 holds ( dist ((seq . n),(seq . m))) < (r / |.z.|) by A1;

        take k = m1;

        let n, m;

        assume n >= k & m >= k;

        then

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

        

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

        

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

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

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

        .= r;

        ( dist ((z * (seq . n)),(z * (seq . m)))) = ||.((z * (seq . n)) - (z * (seq . m))).|| by CSSPACE:def 16

        .= ||.(z * ((seq . n) - (seq . m))).|| by CLVECT_1: 9

        .= ( |.z.| * ||.((seq . n) - (seq . m)).||) by CSSPACE: 43

        .= ( |.z.| * ( dist ((seq . n),(seq . m)))) by CSSPACE:def 16;

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

        then ( dist (((z * seq) . n),(z * (seq . m)))) < r by CLVECT_1:def 14;

        hence ( dist (((z * seq) . n),((z * seq) . m))) < r by CLVECT_1:def 14;

      end;

      now

        assume

         A10: z = 0 ;

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

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

        take k = m1;

        let n, m;

        assume n >= k & m >= k;

        then

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

        ( dist ((z * (seq . n)),(z * (seq . m)))) = ( dist ( 09(X),( 0c * (seq . m)))) by A10, CLVECT_1: 1

        .= ( dist ( 09(X), 09(X))) by CLVECT_1: 1

        .= 0 by CSSPACE: 50;

        then ( dist ((z * (seq . n)),(z * (seq . m)))) < r by A12, CSSPACE: 53;

        then ( dist (((z * seq) . n),(z * (seq . m)))) < r by CLVECT_1:def 14;

        hence ( dist (((z * seq) . n),((z * seq) . m))) < r by CLVECT_1:def 14;

      end;

      hence thesis by A2;

    end;

    theorem :: CLVECT_2:62

    seq is Cauchy implies ( - seq) is Cauchy

    proof

      assume seq is Cauchy;

      then (( - 1r ) * seq) is Cauchy by Th61;

      hence thesis by CSSPACE: 70;

    end;

    theorem :: CLVECT_2:63

    

     Th63: seq is Cauchy implies (seq + x) is Cauchy

    proof

      assume

       A1: seq is Cauchy;

      let r;

      assume r > 0 ;

      then

      consider m1 be Nat such that

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

      take k = m1;

      let n, m;

      ( dist (((seq . n) + x),((seq . m) + x))) <= (( dist ((seq . n),(seq . m))) + ( dist (x,x))) by CSSPACE: 56;

      then

       A3: ( dist (((seq . n) + x),((seq . m) + x))) <= (( dist ((seq . n),(seq . m))) + 0 ) by CSSPACE: 50;

      assume n >= k & m >= k;

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

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

      then ( dist (((seq + x) . n),((seq . m) + x))) < r by BHSP_1:def 6;

      hence thesis by BHSP_1:def 6;

    end;

    theorem :: CLVECT_2:64

    seq is Cauchy implies (seq - x) is Cauchy

    proof

      assume seq is Cauchy;

      then (seq + ( - x)) is Cauchy by Th63;

      hence thesis by CSSPACE: 71;

    end;

    theorem :: CLVECT_2:65

    seq is convergent implies seq is Cauchy

    proof

      assume seq is convergent;

      then

      consider h be Point of X such that

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

      let r;

      assume r > 0 ;

      then

      consider m1 be Nat such that

       A2: for n st n >= m1 holds ( dist ((seq . n),h)) < (r / 2) by A1, XREAL_1: 215;

      take k = m1;

      let n, m;

      assume n >= k & m >= k;

      then ( dist ((seq . n),h)) < (r / 2) & ( dist ((seq . m),h)) < (r / 2) by A2;

      then ( dist ((seq . n),(seq . m))) <= (( dist ((seq . n),h)) + ( dist (h,(seq . m)))) & (( dist ((seq . n),h)) + ( dist (h,(seq . m)))) < ((r / 2) + (r / 2)) by CSSPACE: 51, XREAL_1: 8;

      hence thesis by XXREAL_0: 2;

    end;

    definition

      let X;

      let seq1, seq2;

      :: CLVECT_2:def9

      pred seq1 is_compared_to seq2 means for r st r > 0 holds ex m st for n st n >= m holds ( dist ((seq1 . n),(seq2 . n))) < r;

    end

    theorem :: CLVECT_2:66

    

     Th66: seq is_compared_to seq

    proof

      let r such that

       A1: r > 0 ;

      take m = 0 ;

      let n such that n >= m;

      thus thesis by A1, CSSPACE: 50;

    end;

    theorem :: CLVECT_2:67

    

     Th67: seq1 is_compared_to seq2 implies seq2 is_compared_to seq1

    proof

      assume

       A1: seq1 is_compared_to seq2;

      let r;

      assume r > 0 ;

      then

      consider k such that

       A2: for n st n >= k holds ( dist ((seq1 . n),(seq2 . n))) < r by A1;

      take m = k;

      let n;

      assume n >= m;

      hence thesis by A2;

    end;

    definition

      let X;

      let seq1, seq2;

      :: original: is_compared_to

      redefine

      pred seq1 is_compared_to seq2;

      reflexivity by Th66;

      symmetry by Th67;

    end

    theorem :: CLVECT_2:68

    seq1 is_compared_to seq2 & seq2 is_compared_to seq3 implies seq1 is_compared_to seq3

    proof

      assume that

       A1: seq1 is_compared_to seq2 and

       A2: seq2 is_compared_to seq3;

      let r;

      assume r > 0 ;

      then

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

      then

      consider m1 be Nat such that

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

      consider m2 be Nat such that

       A5: for n st n >= m2 holds ( dist ((seq2 . n),(seq3 . n))) < (r / 2) by A2, A3;

      take m = (m1 + m2);

      let n such that

       A6: n >= m;

      m >= m2 by NAT_1: 12;

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

      then

       A7: ( dist ((seq2 . n),(seq3 . n))) < (r / 2) by A5;

      

       A8: ( dist ((seq1 . n),(seq3 . n))) <= (( dist ((seq1 . n),(seq2 . n))) + ( dist ((seq2 . n),(seq3 . n)))) by CSSPACE: 51;

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

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

      then ( dist ((seq1 . n),(seq2 . n))) < (r / 2) by A4;

      then (( dist ((seq1 . n),(seq2 . n))) + ( dist ((seq2 . n),(seq3 . n)))) < ((r / 2) + (r / 2)) by A7, XREAL_1: 8;

      hence thesis by A8, XXREAL_0: 2;

    end;

    theorem :: CLVECT_2:69

    seq1 is_compared_to seq2 iff for r st r > 0 holds ex m st for n st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r

    proof

      thus seq1 is_compared_to seq2 implies for r st r > 0 holds ex m st for n st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r

      proof

        assume

         A1: seq1 is_compared_to seq2;

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

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

        take m = m1;

        let n;

        assume n >= m;

        then ( dist ((seq1 . n),(seq2 . n))) < r by A2;

        hence thesis by CSSPACE:def 16;

      end;

      (for r st r > 0 holds ex m st for n st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r) implies seq1 is_compared_to seq2

      proof

        assume

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

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

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

        take m = m1;

        let n;

        assume n >= m;

        then ||.((seq1 . n) - (seq2 . n)).|| < r by A4;

        hence thesis by CSSPACE:def 16;

      end;

      hence thesis;

    end;

    theorem :: CLVECT_2:70

    (ex k st for n st n >= k holds (seq1 . n) = (seq2 . n)) implies seq1 is_compared_to seq2

    proof

      assume ex k st for n st n >= k holds (seq1 . n) = (seq2 . n);

      then

      consider m such that

       A1: for n st n >= m holds (seq1 . n) = (seq2 . n);

      let r such that

       A2: r > 0 ;

      take k = m;

      let n;

      assume n >= k;

      

      then ( dist ((seq1 . n),(seq2 . n))) = ( dist ((seq1 . n),(seq1 . n))) by A1

      .= 0 by CSSPACE: 50;

      hence thesis by A2;

    end;

    theorem :: CLVECT_2:71

    seq1 is Cauchy & seq1 is_compared_to seq2 implies seq2 is Cauchy

    proof

      assume that

       A1: seq1 is Cauchy and

       A2: seq1 is_compared_to seq2;

      let r;

      assume r > 0 ;

      then

       A3: (r / 3) > 0 by XREAL_1: 222;

      then

      consider m1 be Nat such that

       A4: for n, m st n >= m1 & m >= m1 holds ( dist ((seq1 . n),(seq1 . m))) < (r / 3) by A1;

      consider m2 be Nat such that

       A5: for n st n >= m2 holds ( dist ((seq1 . n),(seq2 . n))) < (r / 3) by A2, A3;

      take k = (m1 + m2);

      let n, m such that

       A6: n >= k and

       A7: m >= k;

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

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

      then

       A8: ( dist ((seq1 . n),(seq1 . m))) < (r / 3) by A4;

      

       A9: ( dist ((seq2 . n),(seq1 . m))) <= (( dist ((seq2 . n),(seq1 . n))) + ( dist ((seq1 . n),(seq1 . m)))) by CSSPACE: 51;

      

       A10: k >= m2 by NAT_1: 12;

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

      then ( dist ((seq1 . n),(seq2 . n))) < (r / 3) by A5;

      then (( dist ((seq2 . n),(seq1 . n))) + ( dist ((seq1 . n),(seq1 . m)))) < ((r / 3) + (r / 3)) by A8, XREAL_1: 8;

      then

       A11: ( dist ((seq2 . n),(seq1 . m))) < ((r / 3) + (r / 3)) by A9, XXREAL_0: 2;

      

       A12: ( dist ((seq2 . n),(seq2 . m))) <= (( dist ((seq2 . n),(seq1 . m))) + ( dist ((seq1 . m),(seq2 . m)))) by CSSPACE: 51;

      m >= m2 by A7, A10, XXREAL_0: 2;

      then ( dist ((seq1 . m),(seq2 . m))) < (r / 3) by A5;

      then (( dist ((seq2 . n),(seq1 . m))) + ( dist ((seq1 . m),(seq2 . m)))) < (((r / 3) + (r / 3)) + (r / 3)) by A11, XREAL_1: 8;

      hence thesis by A12, XXREAL_0: 2;

    end;

    theorem :: CLVECT_2:72

    seq1 is convergent & seq1 is_compared_to seq2 implies seq2 is convergent

    proof

      assume that

       A1: seq1 is convergent and

       A2: seq1 is_compared_to seq2;

      now

        let r;

        assume r > 0 ;

        then

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

        then

        consider m1 be Nat such that

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

        consider m2 be Nat such that

         A5: for n st n >= m2 holds ( dist ((seq1 . n),(seq2 . n))) < (r / 2) by A2, A3;

        take m = (m1 + m2);

        let n such that

         A6: n >= m;

        m >= m2 by NAT_1: 12;

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

        then

         A7: ( dist ((seq1 . n),(seq2 . n))) < (r / 2) by A5;

        

         A8: ( dist ((seq2 . n),( lim seq1))) <= (( dist ((seq2 . n),(seq1 . n))) + ( dist ((seq1 . n),( lim seq1)))) by CSSPACE: 51;

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

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

        then ( dist ((seq1 . n),( lim seq1))) < (r / 2) by A4;

        then (( dist ((seq2 . n),(seq1 . n))) + ( dist ((seq1 . n),( lim seq1)))) < ((r / 2) + (r / 2)) by A7, XREAL_1: 8;

        hence ( dist ((seq2 . n),( lim seq1))) < r by A8, XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: CLVECT_2:73

    seq1 is convergent & ( lim seq1) = g & seq1 is_compared_to seq2 implies seq2 is convergent & ( lim seq2) = g

    proof

      assume that

       A1: seq1 is convergent & ( lim seq1) = g and

       A2: seq1 is_compared_to seq2;

       A3:

      now

        let r;

        assume r > 0 ;

        then

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

        then

        consider m1 be Nat such that

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

        consider m2 be Nat such that

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

        take m = (m1 + m2);

        let n such that

         A7: n >= m;

        m >= m2 by NAT_1: 12;

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

        then

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

        

         A9: ( dist ((seq2 . n),g)) <= (( dist ((seq2 . n),(seq1 . n))) + ( dist ((seq1 . n),g))) by CSSPACE: 51;

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

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

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

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

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

      end;

      then seq2 is convergent;

      hence thesis by A3, Def2;

    end;

    definition

      let X;

      let seq;

      :: CLVECT_2:def10

      attr seq is bounded means ex M st M > 0 & for n holds ||.(seq . n).|| <= M;

    end

    theorem :: CLVECT_2:74

    

     Th74: seq1 is bounded & seq2 is bounded implies (seq1 + seq2) is bounded

    proof

      assume that

       A1: seq1 is bounded and

       A2: seq2 is bounded;

      consider M2 such that

       A3: M2 > 0 and

       A4: for n holds ||.(seq2 . n).|| <= M2 by A2;

      consider M1 such that

       A5: M1 > 0 and

       A6: for n holds ||.(seq1 . n).|| <= M1 by A1;

      now

        let n;

         ||.((seq1 + seq2) . n).|| = ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def 2;

        then

         A7: ||.((seq1 + seq2) . n).|| <= ( ||.(seq1 . n).|| + ||.(seq2 . n).||) by CSSPACE: 46;

         ||.(seq1 . n).|| <= M1 & ||.(seq2 . n).|| <= M2 by A6, A4;

        then ( ||.(seq1 . n).|| + ||.(seq2 . n).||) <= (M1 + M2) by XREAL_1: 7;

        hence ||.((seq1 + seq2) . n).|| <= (M1 + M2) by A7, XXREAL_0: 2;

      end;

      hence thesis by A5, A3;

    end;

    theorem :: CLVECT_2:75

    

     Th75: seq is bounded implies ( - seq) is bounded

    proof

      assume seq is bounded;

      then

      consider M such that

       A1: M > 0 and

       A2: for n holds ||.(seq . n).|| <= M;

      now

        let n;

         ||.(( - seq) . n).|| = ||.( - (seq . n)).|| by BHSP_1: 44

        .= ||.(seq . n).|| by CSSPACE: 47;

        hence ||.(( - seq) . n).|| <= M by A2;

      end;

      hence thesis by A1;

    end;

    theorem :: CLVECT_2:76

    seq1 is bounded & seq2 is bounded implies (seq1 - seq2) is bounded

    proof

      assume that

       A1: seq1 is bounded and

       A2: seq2 is bounded;

      

       A3: (seq1 - seq2) = (seq1 + ( - seq2)) by CSSPACE: 64;

      ( - seq2) is bounded by A2, Th75;

      hence thesis by A1, A3, Th74;

    end;

    theorem :: CLVECT_2:77

    seq is bounded implies (z * seq) is bounded

    proof

      assume seq is bounded;

      then

      consider M such that

       A1: M > 0 and

       A2: for n holds ||.(seq . n).|| <= M;

      

       A3: z <> 0 implies (z * seq) is bounded

      proof

         A4:

        now

          let n;

          

           A5: |.z.| >= 0 by COMPLEX1: 46;

           ||.((z * seq) . n).|| = ||.(z * (seq . n)).|| by CLVECT_1:def 14

          .= ( |.z.| * ||.(seq . n).||) by CSSPACE: 43;

          hence ||.((z * seq) . n).|| <= ( |.z.| * M) by A2, A5, XREAL_1: 64;

        end;

        assume z <> 0 ;

        then |.z.| > 0 by COMPLEX1: 47;

        then ( |.z.| * M) > 0 by A1, XREAL_1: 129;

        hence thesis by A4;

      end;

      z = 0 implies (z * seq) is bounded

      proof

        assume

         A6: z = 0 ;

        now

          let n;

           ||.((z * seq) . n).|| = ||.( 0c * (seq . n)).|| by A6, CLVECT_1:def 14

          .= ||. 09(X).|| by CLVECT_1: 1

          .= 0 by CSSPACE: 42;

          hence ||.((z * seq) . n).|| <= M by A1;

        end;

        hence thesis by A1;

      end;

      hence thesis by A3;

    end;

    theorem :: CLVECT_2:78

    seq is constant implies seq is bounded

    proof

      assume seq is constant;

      then

      consider x such that

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

      

       A2: x = 09(X) implies seq is bounded

      proof

        consider M be Real such that

         A3: M > 0 by XREAL_1: 1;

        assume

         A4: x = 09(X);

        for n holds ||.(seq . n).|| <= M by A3, CSSPACE: 42, A1, A4;

        hence thesis by A3;

      end;

      x <> 09(X) implies seq is bounded

      proof

        assume x <> 09(X);

        consider M be Real such that

         A5: ||.x.|| < M by XREAL_1: 1;

        reconsider M as Real;

         ||.x.|| >= 0 & for n holds ||.(seq . n).|| <= M by A1, A5, CSSPACE: 44;

        hence thesis by A5;

      end;

      hence thesis by A2;

    end;

    theorem :: CLVECT_2:79

    

     Th79: for m holds ex M st (M > 0 & for n st n <= m holds ||.(seq . n).|| < M)

    proof

      defpred P[ Nat] means ex M st (M > 0 & for n st n <= $1 holds ||.(seq . n).|| < M);

      

       A1: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        given M1 such that

         A2: M1 > 0 and

         A3: for n st n <= m holds ||.(seq . n).|| < M1;

         A4:

        now

          assume

           A5: ||.(seq . (m + 1)).|| >= M1;

          take M = ( ||.(seq . (m + 1)).|| + 1);

          M > ( 0 + 0 ) by CSSPACE: 44, XREAL_1: 8;

          hence M > 0 ;

          let n such that

           A6: n <= (m + 1);

           A7:

          now

            assume m >= n;

            then ||.(seq . n).|| < M1 by A3;

            then ||.(seq . n).|| < ||.(seq . (m + 1)).|| by A5, XXREAL_0: 2;

            then ( ||.(seq . n).|| + 0 ) < M by XREAL_1: 8;

            hence ||.(seq . n).|| < M;

          end;

          now

            assume n = (m + 1);

            then ( ||.(seq . n).|| + 0 ) < M by XREAL_1: 8;

            hence ||.(seq . n).|| < M;

          end;

          hence ||.(seq . n).|| < M by A6, A7, NAT_1: 8;

        end;

        now

          assume

           A8: ||.(seq . (m + 1)).|| <= M1;

          take M = (M1 + 1);

          thus M > 0 by A2;

          let n such that

           A9: n <= (m + 1);

           A10:

          now

            assume m >= n;

            then

             A11: ||.(seq . n).|| < M1 by A3;

            M > (M1 + 0 ) by XREAL_1: 8;

            hence ||.(seq . n).|| < M by A11, XXREAL_0: 2;

          end;

          now

            

             A12: M > (M1 + 0 ) by XREAL_1: 8;

            assume n = (m + 1);

            hence ||.(seq . n).|| < M by A8, A12, XXREAL_0: 2;

          end;

          hence ||.(seq . n).|| < M by A9, A10, NAT_1: 8;

        end;

        hence thesis by A4;

      end;

      

       A13: P[ 0 ]

      proof

        take M = ( ||.(seq . 0 ).|| + 1);

        ( ||.(seq . 0 ).|| + 1) > ( 0 + 0 ) by CSSPACE: 44, XREAL_1: 8;

        hence M > 0 ;

        let n;

        assume n <= 0 ;

        then n = 0 ;

        then ( ||.(seq . n).|| + 0 ) < M by XREAL_1: 8;

        hence thesis;

      end;

      thus for m holds P[m] from NAT_1:sch 2( A13, A1);

    end;

    theorem :: CLVECT_2:80

    

     Th80: seq is convergent implies seq is bounded

    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;

      consider m1 be Nat such that

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

       A3:

      now

        take p = ( ||.g.|| + 1);

        ( 0 + 0 ) < p by CSSPACE: 44, XREAL_1: 8;

        hence p > 0 ;

        let n;

        assume n >= m1;

        then

         A4: ||.((seq . n) - g).|| < 1 by A2;

        ( ||.(seq . n).|| - ||.g.||) <= ||.((seq . n) - g).|| by CSSPACE: 48;

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

        hence ||.(seq . n).|| < p by XREAL_1: 19;

      end;

      now

        consider M2 such that

         A5: M2 > 0 and

         A6: for n st n <= m1 holds ||.(seq . n).|| < M2 by Th79;

        consider M1 such that

         A7: M1 > 0 and

         A8: for n st n >= m1 holds ||.(seq . n).|| < M1 by A3;

        take M = (M1 + M2);

        thus M > 0 by A7, A5;

        let n;

        

         A9: M > ( 0 + M2) by A7, XREAL_1: 8;

         A10:

        now

          assume n <= m1;

          then ||.(seq . n).|| < M2 by A6;

          hence ||.(seq . n).|| <= M by A9, XXREAL_0: 2;

        end;

        

         A11: M > (M1 + 0 ) by A5, XREAL_1: 8;

        now

          assume n >= m1;

          then ||.(seq . n).|| < M1 by A8;

          hence ||.(seq . n).|| <= M by A11, XXREAL_0: 2;

        end;

        hence ||.(seq . n).|| <= M by A10;

      end;

      hence thesis;

    end;

    theorem :: CLVECT_2:81

    seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded

    proof

      assume that

       A1: seq1 is bounded and

       A2: seq1 is_compared_to seq2;

      consider m1 be Nat such that

       A3: for n st n >= m1 holds ( dist ((seq1 . n),(seq2 . n))) < 1 by A2;

      consider p such that

       A4: p > 0 and

       A5: for n holds ||.(seq1 . n).|| <= p by A1;

      

       A6: ex M st (M > 0 & for n st n >= m1 holds ||.(seq2 . n).|| < M)

      proof

        take M = (p + 1);

        now

          let n;

          assume n >= m1;

          then ( dist ((seq1 . n),(seq2 . n))) < 1 by A3;

          then

           A7: ||.((seq2 . n) - (seq1 . n)).|| < 1 by CSSPACE:def 16;

          ( ||.(seq2 . n).|| - ||.(seq1 . n).||) <= ||.((seq2 . n) - (seq1 . n)).|| by CSSPACE: 48;

          then ( ||.(seq2 . n).|| - ||.(seq1 . n).||) < 1 by A7, XXREAL_0: 2;

          then

           A8: ||.(seq2 . n).|| < ( ||.(seq1 . n).|| + 1) by XREAL_1: 19;

           ||.(seq1 . n).|| <= p by A5;

          then ( ||.(seq1 . n).|| + 1) <= (p + 1) by XREAL_1: 6;

          hence ||.(seq2 . n).|| < M by A8, XXREAL_0: 2;

        end;

        hence thesis by A4;

      end;

      now

        consider M2 such that

         A9: M2 > 0 and

         A10: for n st n <= m1 holds ||.(seq2 . n).|| < M2 by Th79;

        consider M1 such that

         A11: M1 > 0 and

         A12: for n st n >= m1 holds ||.(seq2 . n).|| < M1 by A6;

        take M = (M1 + M2);

        thus M > 0 by A11, A9;

        let n;

        

         A13: M > ( 0 + M2) by A11, XREAL_1: 8;

         A14:

        now

          assume n <= m1;

          then ||.(seq2 . n).|| < M2 by A10;

          hence ||.(seq2 . n).|| <= M by A13, XXREAL_0: 2;

        end;

        

         A15: M > (M1 + 0 ) by A9, XREAL_1: 8;

        now

          assume n >= m1;

          then ||.(seq2 . n).|| < M1 by A12;

          hence ||.(seq2 . n).|| <= M by A15, XXREAL_0: 2;

        end;

        hence ||.(seq2 . n).|| <= M by A14;

      end;

      hence thesis;

    end;

    theorem :: CLVECT_2:82

    

     Th82: seq is bounded & seq1 is subsequence of seq implies seq1 is bounded

    proof

      assume that

       A1: seq is bounded and

       A2: seq1 is subsequence of seq;

      consider Nseq such that

       A3: seq1 = (seq * Nseq) by A2, VALUED_0:def 17;

      consider M1 such that

       A4: M1 > 0 and

       A5: for n holds ||.(seq . n).|| <= M1 by A1;

      take M = M1;

      now

        let n;

        n in NAT by ORDINAL1:def 12;

        then (seq1 . n) = (seq . (Nseq . n)) by A3, FUNCT_2: 15;

        hence ||.(seq1 . n).|| <= M by A5;

      end;

      hence thesis by A4;

    end;

    theorem :: CLVECT_2:83

    

     Th83: seq is convergent & seq1 is subsequence of seq implies seq1 is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: seq1 is subsequence of seq;

      consider Nseq such that

       A3: seq1 = (seq * Nseq) by A2, VALUED_0:def 17;

      consider g1 such that

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

      now

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

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

        take m = m1;

        let n such that

         A6: n >= m;

        (Nseq . n) >= n by SEQM_3: 14;

        then

         A7: (Nseq . n) >= m by A6, XXREAL_0: 2;

        n in NAT by ORDINAL1:def 12;

        then (seq1 . n) = (seq . (Nseq . n)) by A3, FUNCT_2: 15;

        hence ||.((seq1 . n) - g1).|| < r by A5, A7;

      end;

      hence thesis by Th9;

    end;

    theorem :: CLVECT_2:84

    

     Th84: seq1 is subsequence of seq & seq is convergent implies ( lim seq1) = ( lim seq)

    proof

      assume that

       A1: seq1 is subsequence of seq and

       A2: seq is convergent;

      consider Nseq such that

       A3: seq1 = (seq * Nseq) by A1, VALUED_0:def 17;

       A4:

      now

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

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

        take m = m1;

        let n such that

         A6: n >= m;

        (Nseq . n) >= n by SEQM_3: 14;

        then

         A7: (Nseq . n) >= m by A6, XXREAL_0: 2;

        n in NAT by ORDINAL1:def 12;

        then (seq1 . n) = (seq . (Nseq . n)) by A3, FUNCT_2: 15;

        hence ( dist ((seq1 . n),( lim seq))) < r by A5, A7;

      end;

      seq1 is convergent by A1, A2, Th83;

      hence thesis by A4, Def2;

    end;

    theorem :: CLVECT_2:85

    

     Th85: seq is Cauchy & seq1 is subsequence of seq implies seq1 is Cauchy

    proof

      assume that

       A1: seq is Cauchy and

       A2: seq1 is subsequence of seq;

      consider Nseq such that

       A3: seq1 = (seq * Nseq) by A2, VALUED_0:def 17;

      now

        let r;

        assume r > 0 ;

        then

        consider l be Nat such that

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

        take k = l;

        let n, m such that

         A5: n >= k and

         A6: m >= k;

        

         A7: n in NAT & m in NAT by ORDINAL1:def 12;

        (Nseq . n) >= n by SEQM_3: 14;

        then

         A8: (Nseq . n) >= k by A5, XXREAL_0: 2;

        (Nseq . m) >= m by SEQM_3: 14;

        then

         A9: (Nseq . m) >= k by A6, XXREAL_0: 2;

        (seq1 . n) = (seq . (Nseq . n)) & (seq1 . m) = (seq . (Nseq . m)) by A3, FUNCT_2: 15, A7;

        hence ( dist ((seq1 . n),(seq1 . m))) < r by A4, A8, A9;

      end;

      hence thesis;

    end;

    theorem :: CLVECT_2:86

    

     Th86: ((seq1 + seq2) ^\ k) = ((seq1 ^\ k) + (seq2 ^\ k))

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq1 + seq2) ^\ k) . n) = ((seq1 + seq2) . (n + k)) by NAT_1:def 3

        .= ((seq1 . (n + k)) + (seq2 . (n + k))) by NORMSP_1:def 2

        .= (((seq1 ^\ k) . n) + (seq2 . (n + k))) by NAT_1:def 3

        .= (((seq1 ^\ k) . n) + ((seq2 ^\ k) . n)) by NAT_1:def 3

        .= (((seq1 ^\ k) + (seq2 ^\ k)) . n) by NORMSP_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLVECT_2:87

    

     Th87: (( - seq) ^\ k) = ( - (seq ^\ k))

    proof

      now

        let n be Element of NAT ;

        

        thus ((( - seq) ^\ k) . n) = (( - seq) . (n + k)) by NAT_1:def 3

        .= ( - (seq . (n + k))) by BHSP_1: 44

        .= ( - ((seq ^\ k) . n)) by NAT_1:def 3

        .= (( - (seq ^\ k)) . n) by BHSP_1: 44;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLVECT_2:88

    ((seq1 - seq2) ^\ k) = ((seq1 ^\ k) - (seq2 ^\ k))

    proof

      

      thus ((seq1 - seq2) ^\ k) = ((seq1 + ( - seq2)) ^\ k) by CSSPACE: 64

      .= ((seq1 ^\ k) + (( - seq2) ^\ k)) by Th86

      .= ((seq1 ^\ k) + ( - (seq2 ^\ k))) by Th87

      .= ((seq1 ^\ k) - (seq2 ^\ k)) by CSSPACE: 64;

    end;

    theorem :: CLVECT_2:89

    ((z * seq) ^\ k) = (z * (seq ^\ k))

    proof

      now

        let n be Element of NAT ;

        

        thus (((z * seq) ^\ k) . n) = ((z * seq) . (n + k)) by NAT_1:def 3

        .= (z * (seq . (n + k))) by CLVECT_1:def 14

        .= (z * ((seq ^\ k) . n)) by NAT_1:def 3

        .= ((z * (seq ^\ k)) . n) by CLVECT_1:def 14;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CLVECT_2:90

    seq is convergent implies (seq ^\ k) is convergent & ( lim (seq ^\ k)) = ( lim seq) by Th83, Th84;

    theorem :: CLVECT_2:91

    seq is convergent & (ex k st seq = (seq1 ^\ k)) implies seq1 is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: ex k st seq = (seq1 ^\ k);

      consider k such that

       A3: seq = (seq1 ^\ k) by A2;

      consider g1 such that

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

      now

        take g = g1;

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

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

        take m = (m1 + k);

        let n;

        assume

         A6: n >= m;

        then

        consider m2 be Nat such that

         A7: n = ((m1 + k) + m2) by NAT_1: 10;

        reconsider m2 as Nat;

        (n - k) = (m1 + m2) by A7;

        then

        consider l be Nat such that

         A8: l = (n - k);

        now

          assume l < m1;

          then (l + k) < (m1 + k) by XREAL_1: 6;

          hence contradiction by A6, A8;

        end;

        then

         A9: ||.((seq . l) - g).|| < r by A5;

        (l + k) = n by A8;

        hence ||.((seq1 . n) - g).|| < r by A3, A9, NAT_1:def 3;

      end;

      hence thesis by Th9;

    end;

    theorem :: CLVECT_2:92

    seq is Cauchy & (ex k st seq = (seq1 ^\ k)) implies seq1 is Cauchy

    proof

      assume that

       A1: seq is Cauchy and

       A2: ex k st seq = (seq1 ^\ k);

      consider k such that

       A3: seq = (seq1 ^\ k) by A2;

      let r;

      assume r > 0 ;

      then

      consider l1 be Nat such that

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

      take l = (l1 + k);

      let n, m;

      assume that

       A5: n >= l and

       A6: m >= l;

      consider m1 be Nat such that

       A7: n = ((l1 + k) + m1) by A5, NAT_1: 10;

      reconsider m1 as Nat;

      (n - k) = (l1 + m1) by A7;

      then

      consider l2 be Nat such that

       A8: l2 = (n - k);

      consider m2 be Nat such that

       A9: m = ((l1 + k) + m2) by A6, NAT_1: 10;

      reconsider m2 as Nat;

      (m - k) = (l1 + m2) by A9;

      then

      consider l3 be Nat such that

       A10: l3 = (m - k);

       A11:

      now

        assume l2 < l1;

        then (l2 + k) < (l1 + k) by XREAL_1: 6;

        hence contradiction by A5, A8;

      end;

      

       A12: (l2 + k) = n by A8;

      now

        assume l3 < l1;

        then (l3 + k) < (l1 + k) by XREAL_1: 6;

        hence contradiction by A6, A10;

      end;

      then ( dist ((seq . l2),(seq . l3))) < r by A4, A11;

      then

       A13: ( dist ((seq1 . n),(seq . l3))) < r by A3, A12, NAT_1:def 3;

      (l3 + k) = m by A10;

      hence thesis by A3, A13, NAT_1:def 3;

    end;

    theorem :: CLVECT_2:93

    seq is Cauchy implies (seq ^\ k) is Cauchy by Th85;

    theorem :: CLVECT_2:94

    seq1 is_compared_to seq2 implies (seq1 ^\ k) is_compared_to (seq2 ^\ k)

    proof

      assume

       A1: seq1 is_compared_to seq2;

      let r;

      assume r > 0 ;

      then

      consider m1 be Nat such that

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

      take m = m1;

      let n such that

       A3: n >= m;

      (n + k) >= n by NAT_1: 11;

      then (n + k) >= m by A3, XXREAL_0: 2;

      then ( dist ((seq1 . (n + k)),(seq2 . (n + k)))) < r by A2;

      then ( dist (((seq1 ^\ k) . n),(seq2 . (n + k)))) < r by NAT_1:def 3;

      hence thesis by NAT_1:def 3;

    end;

    theorem :: CLVECT_2:95

    seq is bounded implies (seq ^\ k) is bounded by Th82;

    theorem :: CLVECT_2:96

    seq is constant implies (seq ^\ k) is constant;

    definition

      let X;

      :: CLVECT_2:def11

      attr X is complete means for seq holds seq is Cauchy implies seq is convergent;

    end

    theorem :: CLVECT_2:97

    X is complete & seq is Cauchy implies seq is bounded by Th80;