bhsp_3.miz



    begin

    reserve X for RealUnitarySpace,

x,g,g1,h for Point of X,

a,p,r,M,M1,M2 for Real,

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

Nseq for increasing sequence of NAT ,

k,l,l1,l2,l3,n,m,m1,m2 for Nat;

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

    registration

      let X;

      cluster constant for sequence of X;

      existence

      proof

        take the constant sequence of X;

        thus thesis;

      end;

    end

    definition

      let X;

      let seq;

      :: BHSP_3:def1

      attr seq is Cauchy means

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

    registration

      let X;

      cluster constant -> Cauchy for sequence of X;

      coherence

      proof

        let seq be sequence of X;

        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 BHSP_1: 34;

        hence thesis by A2;

      end;

    end

    ::$Canceled

    theorem :: BHSP_3:2

    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 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 BHSP_1:def 5;

      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 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 BHSP_1:def 5;

      end;

      hence thesis;

    end;

    registration

      let X;

      let seq1,seq2 be Cauchy sequence of X;

      cluster (seq1 + seq2) -> Cauchy;

      coherence

      proof

        let r;

        assume r > 0 ;

        then

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

        then

        consider m1 such that

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

        consider m2 such that

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

        take k = (m1 + m2);

        let n, m such that

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

        k >= m2 by NAT_1: 12;

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

        then

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

        ( 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

         A6: ( dist (((seq1 + seq2) . n),((seq1 + seq2) . m))) <= (( dist ((seq1 . n),(seq1 . m))) + ( dist ((seq2 . n),(seq2 . m)))) by BHSP_1: 40;

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

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

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

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

        hence thesis by A6, XXREAL_0: 2;

      end;

    end

    registration

      let X;

      let seq1,seq2 be Cauchy sequence of X;

      cluster (seq1 - seq2) -> Cauchy;

      coherence

      proof

        let r;

        assume r > 0 ;

        then

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

        then

        consider m1 such that

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

        consider m2 such that

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

        take k = (m1 + m2);

        let n, m such that

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

        k >= m2 by NAT_1: 12;

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

        then

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

        ( 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

         A6: ( dist (((seq1 - seq2) . n),((seq1 - seq2) . m))) <= (( dist ((seq1 . n),(seq1 . m))) + ( dist ((seq2 . n),(seq2 . m)))) by BHSP_1: 41;

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

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

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

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

        hence thesis by A6, XXREAL_0: 2;

      end;

    end

    registration

      let X, a;

      let seq be Cauchy sequence of X;

      cluster (a * seq) -> Cauchy;

      coherence

      proof

         A1:

        now

          

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

          assume

           A3: a <> 0 ;

          then

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

          let r;

          assume r > 0 ;

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

          then

          consider m1 such that

           A5: for n, m st n >= m1 & m >= m1 holds ( dist ((seq . n),(seq . m))) < (r / |.a.|) by Def1;

          take k = m1;

          let n, m;

          assume n >= k & m >= k;

          then

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

          

           A7: |.a.| <> 0 by A3, COMPLEX1: 47;

          

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

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

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

          .= r;

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

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

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

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

          then ( dist ((a * (seq . n)),(a * (seq . m)))) < r by A4, A6, A8, XREAL_1: 68;

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

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

        end;

        now

          assume

           A9: a = 0 ;

          let r;

          assume r > 0 ;

          then

          consider m1 such that

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

          take k = m1;

          let n, m;

          assume n >= k & m >= k;

          then

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

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

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

          .= 0 by BHSP_1: 34;

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

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

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

        end;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let seq be Cauchy sequence of X;

      cluster ( - seq) -> Cauchy;

      coherence

      proof

        (( - 1) * seq) is Cauchy;

        hence thesis by BHSP_1: 55;

      end;

    end

    registration

      let X, x;

      let seq be Cauchy sequence of X;

      cluster (seq + x) -> Cauchy;

      coherence

      proof

        let r;

        assume r > 0 ;

        then

        consider m1 such that

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

        take k = m1;

        let n, m;

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

        then

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

        assume n >= k & m >= k;

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

        then ( dist (((seq . n) + x),((seq . m) + x))) < r by A2, 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;

    end

    registration

      let X, x;

      let seq be Cauchy sequence of X;

      cluster (seq - x) -> Cauchy;

      coherence

      proof

        (seq + ( - x)) is Cauchy;

        hence thesis by BHSP_1: 56;

      end;

    end

    registration

      let X;

      cluster convergent -> Cauchy for sequence of X;

      coherence

      proof

        let seq be sequence of X;

        assume seq is convergent;

        then

        consider h such that

         A1: for r st r > 0 holds ex k be Nat st for n be Nat st n >= k holds ( dist ((seq . n),h)) < r by BHSP_2:def 1;

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

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

        reconsider k = m1 as Nat;

        take k;

        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 BHSP_1: 35, XREAL_1: 8;

        hence thesis by XXREAL_0: 2;

      end;

    end

    definition

      let X;

      let seq1, seq2;

      :: BHSP_3:def2

      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;

      reflexivity

      proof

        let seq1;

        let r such that

         A1: r > 0 ;

        take m = 0 ;

        let n such that n >= m;

        thus thesis by A1, BHSP_1: 34;

      end;

      symmetry

      proof

        let seq1, seq2;

        assume

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

        let r;

        assume r > 0 ;

        then

        consider k such that

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

        take m = k;

        let n;

        assume n >= m;

        hence thesis by A3;

      end;

    end

    ::$Canceled

    theorem :: BHSP_3:12

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

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

      consider m2 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 BHSP_1: 35;

      (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 :: BHSP_3:13

    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 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 BHSP_1:def 5;

      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 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 BHSP_1:def 5;

      end;

      hence thesis;

    end;

    theorem :: BHSP_3:14

    (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 BHSP_1: 34;

      hence thesis by A2;

    end;

    theorem :: BHSP_3:15

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

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

      consider m2 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 BHSP_1: 35;

      

       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 BHSP_1: 35;

      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 :: BHSP_3:16

    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 be Nat st n >= m1 holds ( dist ((seq1 . n),( lim seq1))) < (r / 2) by A1, BHSP_2:def 2;

        consider m2 such that

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

        reconsider m = (m1 + m2) as Nat;

        take m;

        let n be Nat 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 BHSP_1: 35;

        (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 by BHSP_2:def 1;

    end;

    theorem :: BHSP_3:17

    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 be Nat st n >= m1 holds ( dist ((seq1 . n),g)) < (r / 2) by A1, BHSP_2:def 2;

        consider m2 such that

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

        reconsider m = (m1 + m2) as Nat;

        take m;

        let n be Nat 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 BHSP_1: 35;

        (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 by BHSP_2:def 1;

      hence thesis by A3, BHSP_2:def 2;

    end;

    definition

      let X;

      let seq;

      :: BHSP_3:def3

      attr seq is bounded means

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

    end

    registration

      let X;

      cluster constant -> bounded 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;

        

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

        proof

          consider M be Real such that

           A3: M > 0 by XREAL_1: 1;

          reconsider M as Real;

          assume

           A4: x = 09(X);

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

          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, BHSP_1: 28;

          hence thesis by A5;

        end;

        hence thesis by A2;

      end;

    end

    registration

      let X;

      let seq1,seq2 be bounded sequence of X;

      cluster (seq1 + seq2) -> bounded;

      coherence

      proof

        consider M2 such that

         A1: M2 > 0 and

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

        consider M1 such that

         A3: M1 > 0 and

         A4: for n holds ||.(seq1 . n).|| <= M1 by Def3;

        now

          let n;

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

          then

           A5: ||.((seq1 + seq2) . n).|| <= ( ||.(seq1 . n).|| + ||.(seq2 . n).||) by BHSP_1: 30;

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

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

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

        end;

        hence thesis by A3, A1;

      end;

    end

    registration

      let X;

      let seq be bounded sequence of X;

      cluster ( - seq) -> bounded;

      coherence

      proof

        consider M such that

         A1: M > 0 and

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

        now

          let n;

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

          .= ||.(seq . n).|| by BHSP_1: 31;

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

        end;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let seq1,seq2 be bounded sequence of X;

      cluster (seq1 - seq2) -> bounded;

      coherence

      proof

        

         A1: (seq1 - seq2) = (seq1 + ( - seq2)) by BHSP_1: 49;

        thus thesis by A1;

      end;

    end

    registration

      let X, a;

      let seq be bounded sequence of X;

      cluster (a * seq) -> bounded;

      coherence

      proof

        consider M such that

         A1: M > 0 and

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

        

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

        proof

           A4:

          now

            let n;

            

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

             ||.((a * seq) . n).|| = ||.(a * (seq . n)).|| by NORMSP_1:def 5

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

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

          end;

          assume a <> 0 ;

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

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

          hence thesis by A4;

        end;

        a = 0 implies (a * seq) is bounded

        proof

          assume

           A6: a = 0 ;

          now

            let n;

             ||.((a * seq) . n).|| = ||.( 0 * (seq . n)).|| by A6, NORMSP_1:def 5

            .= ||. 09(X).|| by RLVECT_1: 10

            .= 0 by BHSP_1: 26;

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

          end;

          hence thesis by A1;

        end;

        hence thesis by A3;

      end;

    end

    ::$Canceled

    theorem :: BHSP_3:23

    

     Th8: 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 BHSP_1: 28, 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 BHSP_1: 28, 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;

    registration

      let X;

      cluster convergent -> bounded for sequence of X;

      coherence

      proof

        let seq;

        assume seq is convergent;

        then

        consider g such that

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

        consider m1 be Nat such that

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

         A3:

        now

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

          ( 0 + 0 ) < p by BHSP_1: 28, 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 BHSP_1: 32;

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

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

        end;

        now

          reconsider m1 as Nat;

          consider M2 such that

           A5: M2 > 0 and

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

          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;

    end

    ::$Canceled

    theorem :: BHSP_3:25

    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 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 BHSP_1:def 5;

          ( ||.(seq2 . n).|| - ||.(seq1 . n).||) <= ||.((seq2 . n) - (seq1 . n)).|| by BHSP_1: 32;

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

        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;

    registration

      let X;

      let seq be bounded sequence of X;

      cluster -> bounded for subsequence of seq;

      coherence

      proof

        let seq1 be subsequence of seq;

        consider Nseq such that

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

        consider M1 such that

         A2: M1 > 0 and

         A3: for n holds ||.(seq . n).|| <= M1 by Def3;

        take M = M1;

        now

          let n;

          

           A4: n in NAT by ORDINAL1:def 12;

          (seq1 . n) = (seq . (Nseq . n)) by A1, FUNCT_2: 15, A4;

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

        end;

        hence thesis by A2;

      end;

    end

    registration

      let X;

      let seq be convergent sequence of X;

      cluster -> convergent for subsequence of seq;

      coherence

      proof

        let seq1 be subsequence of seq;

        consider g1 such that

         A1: for r st r > 0 holds ex m be Nat st for n be Nat st n >= m holds ||.((seq . n) - g1).|| < r by BHSP_2: 9;

        consider Nseq such that

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

        now

          let r;

          assume r > 0 ;

          then

          consider m1 be Nat such that

           A3: for n be Nat st n >= m1 holds ||.((seq . n) - g1).|| < r by A1;

          take m = m1;

          let n be Nat such that

           A4: n >= m;

          

           A5: n in NAT by ORDINAL1:def 12;

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

          then

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

          (seq1 . n) = (seq . (Nseq . n)) by A2, FUNCT_2: 15, A5;

          hence ||.((seq1 . n) - g1).|| < r by A3, A6;

        end;

        hence thesis by BHSP_2: 9;

      end;

    end

    ::$Canceled

    theorem :: BHSP_3:28

    

     Th10: 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 be Nat st n >= m1 holds ( dist ((seq . n),( lim seq))) < r by A2, BHSP_2:def 2;

        take m = m1;

        let n be Nat such that

         A6: n >= m;

        

         A7: n in NAT by ORDINAL1:def 12;

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

        then

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

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

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

      end;

      seq1 is convergent by A1, A2;

      hence thesis by A4, BHSP_2:def 2;

    end;

    registration

      let X;

      let seq be Cauchy sequence of X;

      cluster -> Cauchy for subsequence of seq;

      coherence

      proof

        let seq1 be subsequence of seq;

        consider Nseq such that

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

        now

          let r;

          assume r > 0 ;

          then

          consider l such that

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

          take k = l;

          let n, m such that

           A3: n >= k and

           A4: m >= k;

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

          then

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

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

          then

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

          

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

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

          hence ( dist ((seq1 . n),(seq1 . m))) < r by A2, A5, A6;

        end;

        hence thesis;

      end;

    end

    ::$Canceled

    theorem :: BHSP_3:30

    ((seq ^\ k) ^\ m) = ((seq ^\ m) ^\ k)

    proof

      now

        let n be Element of NAT ;

        

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

        .= (seq . ((n + m) + k)) by NAT_1:def 3

        .= (seq . ((n + k) + m))

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BHSP_3:31

    ((seq ^\ k) ^\ m) = (seq ^\ (k + m))

    proof

      now

        let n be Element of NAT ;

        

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

        .= (seq . ((n + m) + k)) by NAT_1:def 3

        .= (seq . (n + (k + m)))

        .= ((seq ^\ (k + m)) . n) by NAT_1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BHSP_3:32

    

     Th13: ((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 :: BHSP_3:33

    

     Th14: (( - 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 :: BHSP_3:34

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

    proof

      

      thus ((seq1 - seq2) ^\ k) = ((seq1 + ( - seq2)) ^\ k) by BHSP_1: 49

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

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

      .= ((seq1 ^\ k) - (seq2 ^\ k)) by BHSP_1: 49;

    end;

    theorem :: BHSP_3:35

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

    proof

      now

        let n be Element of NAT ;

        

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

        .= (a * (seq . (n + k))) by NORMSP_1:def 5

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

        .= ((a * (seq ^\ k)) . n) by NORMSP_1:def 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BHSP_3:36

    seq is convergent implies (seq ^\ k) is convergent & ( lim (seq ^\ k)) = ( lim seq) by Th10;

    theorem :: BHSP_3:37

    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 be Nat st for n be Nat st n >= m holds ||.((seq . n) - g1).|| < r by A1, BHSP_2: 9;

      now

        take g = g1;

        let r;

        assume r > 0 ;

        then

        consider m1 be Nat such that

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

        reconsider m = (m1 + k) as Nat;

        take m;

        let n be Nat;

        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 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 BHSP_2: 9;

    end;

    theorem :: BHSP_3:38

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

    ::$Canceled

    theorem :: BHSP_3:40

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

    definition

      let X;

      :: BHSP_3:def4

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

    end

    ::$Canceled

    theorem :: BHSP_3:43

    X is complete & seq is Cauchy implies seq is bounded

    proof

      assume X is complete & seq is Cauchy;

      then seq is convergent;

      hence thesis;

    end;