rsspace2.miz



    begin

    theorem :: RSSPACE2:1

    

     Th1: the carrier of l2_Space = the_set_of_l2RealSequences & (for x be set holds x is VECTOR of l2_Space iff x is Real_Sequence & (( seq_id x) (#) ( seq_id x)) is summable) & ( 0. l2_Space ) = Zeroseq & (for u be VECTOR of l2_Space holds u = ( seq_id u)) & (for u,v be VECTOR of l2_Space holds (u + v) = (( seq_id u) + ( seq_id v))) & (for r be Real holds for u be VECTOR of l2_Space holds (r * u) = (r (#) ( seq_id u))) & (for u be VECTOR of l2_Space holds ( - u) = ( - ( seq_id u)) & ( seq_id ( - u)) = ( - ( seq_id u))) & (for u,v be VECTOR of l2_Space holds (u - v) = (( seq_id u) - ( seq_id v))) & (for v,w be VECTOR of l2_Space holds (( seq_id v) (#) ( seq_id w)) is summable) & for v,w be VECTOR of l2_Space holds (v .|. w) = ( Sum (( seq_id v) (#) ( seq_id w)))

    proof

      thus the carrier of l2_Space = the_set_of_l2RealSequences ;

      thus for x be set holds x is Element of l2_Space iff x is Real_Sequence & (( seq_id x) (#) ( seq_id x)) is summable

      proof

        let x be set;

        x in the_set_of_RealSequences iff x is Real_Sequence by FUNCT_2: 8, FUNCT_2: 66;

        hence thesis by RSSPACE:def 11;

      end;

      

      thus ( 0. l2_Space ) = ( 0. Linear_Space_of_RealSequences ) by RSSPACE:def 10

      .= Zeroseq ;

      thus for u be VECTOR of l2_Space holds u = ( seq_id u);

      set W = the_set_of_l2RealSequences ;

      set L1 = Linear_Space_of_RealSequences ;

      thus

       A10: for u,v be VECTOR of l2_Space holds (u + v) = (( seq_id u) + ( seq_id v))

      proof

        let u,v be VECTOR of l2_Space ;

        reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by RLSUB_1: 10, RSSPACE: 12;

        ( dom the addF of L1) = [:the carrier of L1, the carrier of L1:] by FUNCT_2:def 1;

        then ( dom (the addF of Linear_Space_of_RealSequences || W)) = [:W, W:] by RELAT_1: 62, ZFMISC_1: 96;

        then

         A11: [u, v] in ( dom (the addF of Linear_Space_of_RealSequences || W)) by ZFMISC_1: 87;

        (u + v) = ((the addF of Linear_Space_of_RealSequences || W) . [u, v]) by RSSPACE:def 8

        .= (u1 + v1) by A11, FUNCT_1: 47;

        hence thesis by RSSPACE: 2;

      end;

      thus

       A12: for r be Real holds for u be VECTOR of l2_Space holds (r * u) = (r (#) ( seq_id u))

      proof

        let r be Real;

        reconsider r as Element of REAL by XREAL_0:def 1;

        let u be VECTOR of l2_Space ;

        reconsider u1 = u as VECTOR of Linear_Space_of_RealSequences by RLSUB_1: 10, RSSPACE: 12;

        ( dom the Mult of L1) = [: REAL , the carrier of L1:] by FUNCT_2:def 1;

        then ( dom (the Mult of Linear_Space_of_RealSequences | [: REAL , W:])) = [: REAL , W:] by RELAT_1: 62, ZFMISC_1: 96;

        then

         A13: [r, u] in ( dom (the Mult of Linear_Space_of_RealSequences | [: REAL , W:])) by ZFMISC_1: 87;

        (r * u) = ((the Mult of Linear_Space_of_RealSequences | [: REAL , W:]) . [r, u]) by RSSPACE:def 9

        .= (r * u1) by A13, FUNCT_1: 47;

        hence thesis by RSSPACE: 3;

      end;

      thus

       A15: for u be VECTOR of l2_Space holds ( - u) = ( - ( seq_id u)) & ( seq_id ( - u)) = ( - ( seq_id u))

      proof

        let u be VECTOR of l2_Space ;

        ( - u) = (( - 1) * u) by RLVECT_1: 16

        .= (( - 1) (#) ( seq_id u)) by A12

        .= ( - ( seq_id u)) by SEQ_1: 17;

        hence thesis;

      end;

      thus for u,v be VECTOR of l2_Space holds (u - v) = (( seq_id u) - ( seq_id v))

      proof

        let u,v be VECTOR of l2_Space ;

        

        thus (u - v) = (( seq_id u) + ( seq_id ( - v))) by A10

        .= (( seq_id u) + ( - ( seq_id v))) by A15

        .= (( seq_id u) - ( seq_id v)) by SEQ_1: 11;

      end;

      thus for u,v be VECTOR of l2_Space holds (( seq_id u) (#) ( seq_id v)) is summable

      proof

        set q0 = (1 / 2);

        let u,v be VECTOR of l2_Space ;

        set p = (( seq_id v) (#) ( seq_id v));

        set q = (( seq_id u) (#) ( seq_id u));

        set r = ( abs (( seq_id u) (#) ( seq_id v)));

        

         A2: for n be Nat holds 0 <= ((2 (#) r) . n)

        proof

          set rr = (( seq_id u) (#) ( seq_id v));

          let n be Nat;

          reconsider tt = |.(rr . n).| as Real;

          

           A3: 0 <= tt by COMPLEX1: 46;

          ((2 (#) r) . n) = (2 * (r . n)) by SEQ_1: 9

          .= (2 * |.(rr . n).|) by SEQ_1: 12;

          hence thesis by A3;

        end;

        

         A4: for n be Nat holds ((2 (#) r) . n) <= ((p + q) . n)

        proof

          set s = ( seq_id v), t = ( seq_id u);

          let n be Nat;

          reconsider sn = (s . n), tn = (t . n) as Real;

          reconsider ss = |.sn.|, tt = |.tn.| as Real;

          

           A5: ((p + q) . n) = ((p . n) + (q . n)) by SEQ_1: 7

          .= (((s . n) * (s . n)) + (q . n)) by SEQ_1: 8

          .= ((sn ^2 ) + ((t . n) * (t . n))) by SEQ_1: 8

          .= (( |.sn.| ^2 ) + (tn ^2 )) by COMPLEX1: 75

          .= (( |.sn.| ^2 ) + ( |.tn.| ^2 )) by COMPLEX1: 75;

          

           A6: 0 <= (( |.sn.| - |.tn.|) ^2 ) by XREAL_1: 63;

          ((2 (#) r) . n) = (2 * (r . n)) by SEQ_1: 9

          .= (2 * |.((( seq_id u) (#) ( seq_id v)) . n).|) by SEQ_1: 12

          .= (2 * |.((( seq_id u) . n) * (( seq_id v) . n)).|) by SEQ_1: 8

          .= (2 * (ss * tt)) by COMPLEX1: 65

          .= ((2 * |.sn.|) * |.tn.|);

          then ( 0 + ((2 (#) r) . n)) <= ((((p + q) . n) - ((2 (#) r) . n)) + ((2 (#) r) . n)) by A5, A6, XREAL_1: 7;

          hence thesis;

        end;

        

         A7: (q0 (#) (2 (#) r)) = ((q0 * 2) (#) r) by SEQ_1: 23

        .= r by SEQ_1: 27;

        (( seq_id v) (#) ( seq_id v)) is summable & (( seq_id u) (#) ( seq_id u)) is summable by RSSPACE:def 11;

        then (p + q) is summable by SERIES_1: 7;

        then (2 (#) r) is summable by A2, A4, SERIES_1: 20;

        then r is summable by A7, SERIES_1: 10;

        then (( seq_id u) (#) ( seq_id v)) is absolutely_summable by SERIES_1:def 4;

        hence thesis;

      end;

      thus for v,w be VECTOR of l2_Space holds (v .|. w) = ( Sum (( seq_id v) (#) ( seq_id w)))

      proof

        let v,w be VECTOR of l2_Space ;

        

        thus (v .|. w) = (the scalar of l2_Space . (v,w)) by BHSP_1:def 1

        .= ( Sum (( seq_id v) (#) ( seq_id w))) by RSSPACE:def 12;

      end;

    end;

    theorem :: RSSPACE2:2

    

     Th2: for x,y,z be Point of l2_Space holds for a be Real holds ((x .|. x) = 0 iff x = ( 0. l2_Space )) & 0 <= (x .|. x) & (x .|. y) = (y .|. x) & ((x + y) .|. z) = ((x .|. z) + (y .|. z)) & ((a * x) .|. y) = (a * (x .|. y))

    proof

      let x,y,z be Point of l2_Space ;

      let a be Real;

      

       A1: for n be Nat holds 0 <= ((( seq_id x) (#) ( seq_id x)) . n)

      proof

        let n be Nat;

        ((( seq_id x) (#) ( seq_id x)) . n) = ((( seq_id x) . n) * (( seq_id x) . n)) by SEQ_1: 8;

        hence thesis by XREAL_1: 63;

      end;

      

       A2: (( seq_id x) (#) ( seq_id x)) is summable & (x .|. x) = ( Sum (( seq_id x) (#) ( seq_id x))) by Th1;

       A3:

      now

        

         A4: for n be Nat holds 0 <= ((( seq_id x) (#) ( seq_id x)) . n)

        proof

          let n be Nat;

          ((( seq_id x) (#) ( seq_id x)) . n) = ((( seq_id x) . n) * (( seq_id x) . n)) by SEQ_1: 8;

          hence thesis by XREAL_1: 63;

        end;

        assume

         A5: (x .|. x) = 0 ;

        

         A6: (x .|. x) = ( Sum (( seq_id x) (#) ( seq_id x))) & (( seq_id x) (#) ( seq_id x)) is summable by Th1;

        

         A7: for n be Nat holds 0 = (( seq_id x) . n)

        proof

          let n be Nat;

           0 = ((( seq_id x) (#) ( seq_id x)) . n) by A5, A4, A6, RSSPACE: 17

          .= ((( seq_id x) . n) * (( seq_id x) . n)) by SEQ_1: 8;

          hence thesis by XCMPLX_1: 6;

        end;

        x is Element of the_set_of_RealSequences by RSSPACE:def 11;

        hence x = ( 0. l2_Space ) by A7, Th1, RSSPACE: 5;

      end;

      

       A8: (x .|. y) = ( Sum (( seq_id x) (#) ( seq_id y))) by Th1

      .= (y .|. x) by Th1;

       A9:

      now

        assume

         A10: x = ( 0. l2_Space );

        

         A11: for n be Nat holds ((( seq_id x) (#) ( seq_id x)) . n) = 0

        proof

          let n be Nat;

          

          thus ((( seq_id x) (#) ( seq_id x)) . n) = ((( seq_id x) . n) * (( seq_id x) . n)) by SEQ_1: 8

          .= ((( seq_id x) . n) * 0 ) by A10, Th1

          .= 0 ;

        end;

        

        thus (x .|. x) = ( Sum (( seq_id x) (#) ( seq_id x))) by Th1

        .= 0 by A11, RSSPACE: 16;

      end;

      

       A12: (( seq_id x) (#) ( seq_id y)) is summable by Th1;

      

       A13: ((a * x) .|. y) = ( Sum (( seq_id (a * x)) (#) ( seq_id y))) by Th1

      .= ( Sum ((a (#) ( seq_id x)) (#) ( seq_id y))) by Th1

      .= ( Sum (a (#) (( seq_id x) (#) ( seq_id y)))) by SEQ_1: 18

      .= (a * ( Sum (( seq_id x) (#) ( seq_id y)))) by A12, SERIES_1: 10

      .= (a * (x .|. y)) by Th1;

      

       A14: (( seq_id x) (#) ( seq_id z)) is summable & (( seq_id y) (#) ( seq_id z)) is summable by Th1;

      ((x + y) .|. z) = ( Sum (( seq_id (x + y)) (#) ( seq_id z))) by Th1

      .= ( Sum ((( seq_id x) + ( seq_id y)) (#) ( seq_id z))) by Th1

      .= ( Sum ((( seq_id x) (#) ( seq_id z)) + (( seq_id y) (#) ( seq_id z)))) by SEQ_1: 16

      .= (( Sum (( seq_id x) (#) ( seq_id z))) + ( Sum (( seq_id y) (#) ( seq_id z)))) by A14, SERIES_1: 7

      .= ((x .|. z) + ( Sum (( seq_id y) (#) ( seq_id z)))) by Th1

      .= ((x .|. z) + (y .|. z)) by Th1;

      hence thesis by A3, A9, A1, A2, A8, A13, SERIES_1: 18;

    end;

    registration

      cluster l2_Space -> RealUnitarySpace-like;

      coherence by Th2, BHSP_1:def 2;

    end

    

     Lm1: for rseq be Real_Sequence st (for n be Nat holds 0 <= (rseq . n)) holds (for n be Nat holds 0 <= (( Partial_Sums rseq) . n)) & (for n be Nat holds (rseq . n) <= (( Partial_Sums rseq) . n)) & (rseq is summable implies (for n be Nat holds (( Partial_Sums rseq) . n) <= ( Sum rseq)) & for n be Nat holds (rseq . n) <= ( Sum rseq))

    proof

      let rseq be Real_Sequence such that

       A1: for n be Nat holds 0 <= (rseq . n);

      

       A2: ( Partial_Sums rseq) is non-decreasing by A1, SERIES_1: 16;

      thus

       A3: for n be Nat holds 0 <= (( Partial_Sums rseq) . n)

      proof

        let n be Nat;

        

         A4: n = (n + 0 ) & (( Partial_Sums rseq) . 0 ) = (rseq . 0 ) by SERIES_1:def 1;

         0 <= (rseq . 0 ) by A1;

        hence thesis by A2, A4, SEQM_3: 5;

      end;

      thus

       A5: for n be Nat holds (rseq . n) <= (( Partial_Sums rseq) . n)

      proof

        let n be Nat;

        now

          per cases ;

            case n = 0 ;

            hence thesis by SERIES_1:def 1;

          end;

            case

             A6: n <> 0 ;

            

             A7: n in NAT by ORDINAL1:def 12;

            set nn = (n - 1);

            ( 0 + 1) <= n by A6, INT_1: 7, A7;

            then

             A8: nn in NAT by INT_1: 5, A7;

            then 0 <= (( Partial_Sums rseq) . nn) by A3;

            then (nn + 1) = n & ((rseq . n) + 0 ) <= ((rseq . n) + (( Partial_Sums rseq) . nn)) by XREAL_1: 7;

            hence thesis by A8, SERIES_1:def 1;

          end;

        end;

        hence thesis;

      end;

      assume rseq is summable;

      then

       A9: ( Partial_Sums rseq) is bounded_above by A1, SERIES_1: 17;

      thus

       A10: for n be Nat holds (( Partial_Sums rseq) . n) <= ( Sum rseq)

      proof

        let n be Nat;

        (( Partial_Sums rseq) . n) <= ( lim ( Partial_Sums rseq)) by A1, A9, SEQ_4: 37, SERIES_1: 16;

        hence thesis by SERIES_1:def 3;

      end;

      let n be Nat;

      

       A11: (rseq . n) <= (( Partial_Sums rseq) . n) by A5;

      (( Partial_Sums rseq) . n) <= ( Sum rseq) by A10;

      hence thesis by A11, XXREAL_0: 2;

    end;

    

     Lm2: (for x,y be Real holds ((x + y) * (x + y)) <= (((2 * x) * x) + ((2 * y) * y))) & for x,y be Real holds (x * x) <= (((2 * (x - y)) * (x - y)) + ((2 * y) * y))

    proof

       A1:

      now

        let x,y be Real;

         0 <= ((x - y) ^2 ) by XREAL_1: 63;

        then ( 0 + ((x + y) * (x + y))) <= (((((2 * x) * x) + ((2 * y) * y)) - ((x + y) * (x + y))) + ((x + y) * (x + y))) by XREAL_1: 7;

        hence ((x + y) * (x + y)) <= (((2 * x) * x) + ((2 * y) * y));

      end;

      now

        let x,y be Real;

        ((x - y) + y) = x;

        hence (x * x) <= (((2 * (x - y)) * (x - y)) + ((2 * y) * y)) by A1;

      end;

      hence thesis by A1;

    end;

    

     Lm3: for e be Real holds for seq be Real_Sequence st (seq is convergent & ex k be Nat st for i be Nat st k <= i holds (seq . i) <= e) holds ( lim seq) <= e

    proof

      let e be Real;

      let seq be Real_Sequence such that

       A1: seq is convergent and

       A2: ex k be Nat st for i be Nat st k <= i holds (seq . i) <= e;

      consider k be Nat such that

       A3: for i be Nat st k <= i holds (seq . i) <= e by A2;

      reconsider ee = e as Element of REAL by XREAL_0:def 1;

      set cseq = ( seq_const e);

      

       A4: ( lim cseq) = (cseq . 0 ) by SEQ_4: 26

      .= e by SEQ_1: 57;

       A5:

      now

        let i be Nat;

        ((seq ^\ k) . i) = (seq . (k + i)) & (seq . (k + i)) <= e by A3, NAT_1: 11, NAT_1:def 3;

        hence ((seq ^\ k) . i) <= (cseq . i) by SEQ_1: 57;

      end;

      ( lim (seq ^\ k)) = ( lim seq) by A1, SEQ_4: 20;

      hence thesis by A1, A5, A4, SEQ_2: 18;

    end;

    

     Lm4: for c be Real, seq be Real_Sequence st seq is convergent holds for rseq be Real_Sequence st (for i be Nat holds (rseq . i) = (((seq . i) - c) * ((seq . i) - c))) holds rseq is convergent & ( lim rseq) = ((( lim seq) - c) * (( lim seq) - c))

    proof

      let c be Real;

      reconsider cc = c as Element of REAL by XREAL_0:def 1;

      set cseq = ( seq_const c);

      let seq be Real_Sequence such that

       A1: seq is convergent;

      

       A2: (seq - cseq) is convergent by A1;

      then

       A3: ((seq - cseq) (#) (seq - cseq)) is convergent;

      let rseq be Real_Sequence such that

       A4: for i be Nat holds (rseq . i) = (((seq . i) - c) * ((seq . i) - c));

      now

        let i be Element of NAT ;

        

        thus (rseq . i) = (((seq . i) - c) * ((seq . i) - c)) by A4

        .= (((seq . i) - (cseq . i)) * ((seq . i) - c)) by SEQ_1: 57

        .= (((seq . i) - (cseq . i)) * ((seq . i) + ( - (cseq . i)))) by SEQ_1: 57

        .= (((seq . i) + (( - cseq) . i)) * ((seq . i) + ( - (cseq . i)))) by SEQ_1: 10

        .= (((seq . i) + (( - cseq) . i)) * ((seq . i) + (( - cseq) . i))) by SEQ_1: 10

        .= (((seq + ( - cseq)) . i) * ((seq . i) + (( - cseq) . i))) by SEQ_1: 7

        .= (((seq - cseq) . i) * ((seq + ( - cseq)) . i)) by SEQ_1: 7, SEQ_1: 11

        .= (((seq - cseq) . i) * ((seq - cseq) . i)) by SEQ_1: 11

        .= (((seq - cseq) (#) (seq - cseq)) . i) by SEQ_1: 8;

      end;

      then

       A5: for x be object st x in NAT holds (rseq . x) = (((seq - cseq) (#) (seq - cseq)) . x);

      ( lim ((seq - cseq) (#) (seq - cseq))) = (( lim (seq - cseq)) * ( lim (seq - cseq))) by A2, SEQ_2: 15

      .= ((( lim seq) - ( lim cseq)) * ( lim (seq - cseq))) by A1, SEQ_2: 12

      .= ((( lim seq) - ( lim cseq)) * (( lim seq) - ( lim cseq))) by A1, SEQ_2: 12

      .= ((( lim seq) - (cseq . 0 )) * (( lim seq) - ( lim cseq))) by SEQ_4: 26

      .= ((( lim seq) - (cseq . 0 )) * (( lim seq) - (cseq . 0 ))) by SEQ_4: 26

      .= ((( lim seq) - c) * (( lim seq) - (cseq . 0 ))) by SEQ_1: 57

      .= ((( lim seq) - c) * (( lim seq) - c)) by SEQ_1: 57;

      hence thesis by A5, A3, FUNCT_2: 12;

    end;

    

     Lm5: for c be Real, seq,seq1 be Real_Sequence st seq is convergent & seq1 is convergent holds for rseq be Real_Sequence st (for i be Nat holds (rseq . i) = ((((seq . i) - c) * ((seq . i) - c)) + (seq1 . i))) holds rseq is convergent & ( lim rseq) = (((( lim seq) - c) * (( lim seq) - c)) + ( lim seq1))

    proof

      let c be Real;

      let seq,seq1 be Real_Sequence such that

       A1: seq is convergent and

       A2: seq1 is convergent;

      reconsider cc = c as Element of REAL by XREAL_0:def 1;

      set cseq = ( seq_const c);

      

       A3: (seq - cseq) is convergent by A1;

      then

       A4: ((seq - cseq) (#) (seq - cseq)) is convergent;

      let rseq be Real_Sequence such that

       A5: for i be Nat holds (rseq . i) = ((((seq . i) - c) * ((seq . i) - c)) + (seq1 . i));

      now

        let i be Element of NAT ;

        

        thus (rseq . i) = ((((seq . i) - c) * ((seq . i) - c)) + (seq1 . i)) by A5

        .= ((((seq . i) - (cseq . i)) * ((seq . i) - c)) + (seq1 . i)) by SEQ_1: 57

        .= ((((seq . i) - (cseq . i)) * ((seq . i) + ( - (cseq . i)))) + (seq1 . i)) by SEQ_1: 57

        .= ((((seq . i) + (( - cseq) . i)) * ((seq . i) + ( - (cseq . i)))) + (seq1 . i)) by SEQ_1: 10

        .= ((((seq . i) + (( - cseq) . i)) * ((seq . i) + (( - cseq) . i))) + (seq1 . i)) by SEQ_1: 10

        .= ((((seq + ( - cseq)) . i) * ((seq . i) + (( - cseq) . i))) + (seq1 . i)) by SEQ_1: 7

        .= ((((seq - cseq) . i) * ((seq + ( - cseq)) . i)) + (seq1 . i)) by SEQ_1: 7, SEQ_1: 11

        .= ((((seq - cseq) . i) * ((seq - cseq) . i)) + (seq1 . i)) by SEQ_1: 11

        .= ((((seq - cseq) (#) (seq - cseq)) . i) + (seq1 . i)) by SEQ_1: 8

        .= ((((seq - cseq) (#) (seq - cseq)) + seq1) . i) by SEQ_1: 7;

      end;

      then

       A6: rseq = (((seq - cseq) (#) (seq - cseq)) + seq1) by FUNCT_2: 63;

      ( lim ((seq - cseq) (#) (seq - cseq))) = (( lim (seq - cseq)) * ( lim (seq - cseq))) by A3, SEQ_2: 15

      .= ((( lim seq) - ( lim cseq)) * ( lim (seq - cseq))) by A1, SEQ_2: 12

      .= ((( lim seq) - ( lim cseq)) * (( lim seq) - ( lim cseq))) by A1, SEQ_2: 12

      .= ((( lim seq) - (cseq . 0 )) * (( lim seq) - ( lim cseq))) by SEQ_4: 26

      .= ((( lim seq) - (cseq . 0 )) * (( lim seq) - (cseq . 0 ))) by SEQ_4: 26

      .= ((( lim seq) - c) * (( lim seq) - (cseq . 0 ))) by SEQ_1: 57

      .= ((( lim seq) - c) * (( lim seq) - c)) by SEQ_1: 57;

      hence thesis by A2, A6, A4, SEQ_2: 6;

    end;

    registration

      cluster l2_Space -> complete;

      coherence

      proof

        let vseq be sequence of l2_Space such that

         A1: vseq is Cauchy;

        defpred P[ object, object] means ex i be Nat st $1 = i & ex rseqi be Real_Sequence st (for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i)) & rseqi is convergent & $2 = ( lim rseqi);

        

         A2: for x be object st x in NAT holds ex y be object st y in REAL & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Element of NAT ;

          deffunc F( set) = (( seq_id (vseq . $1)) . i);

          consider rseqi be Real_Sequence such that

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

          reconsider lr = ( lim rseqi) as Element of REAL by XREAL_0:def 1;

          take lr;

          now

            let e be Real such that

             A4: e > 0 ;

            thus ex k be Nat st for m be Nat st k <= m holds |.((rseqi . m) - (rseqi . k)).| < e

            proof

              consider k be Nat such that

               A5: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, A4, BHSP_3: 2;

              now

                let m be Nat;

                assume k <= m;

                then ||.((vseq . m) - (vseq . k)).|| < e by A5;

                then ( sqrt (((vseq . m) - (vseq . k)) .|. ((vseq . m) - (vseq . k)))) < e by BHSP_1:def 4;

                then

                 A6: ( sqrt ( Sum (( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k)))))) < e by Th1;

                reconsider e1 = e as Real;

                

                 A7: ( sqrt ( |.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).|)) = ( sqrt ( |.((rseqi . m) - (rseqi . k)).| ^2 ))

                .= |.((rseqi . m) - (rseqi . k)).| by COMPLEX1: 46, SQUARE_1: 22;

                ( seq_id ((vseq . m) - (vseq . k))) = (( seq_id (vseq . m)) - ( seq_id (vseq . k))) by Th1

                .= (( seq_id (vseq . m)) + ( - ( seq_id (vseq . k)))) by SEQ_1: 11;

                

                then (( seq_id ((vseq . m) - (vseq . k))) . i) = ((( seq_id (vseq . m)) . i) + (( - ( seq_id (vseq . k))) . i)) by SEQ_1: 7

                .= ((( seq_id (vseq . m)) . i) + ( - (( seq_id (vseq . k)) . i))) by SEQ_1: 10

                .= ((( seq_id (vseq . m)) . i) - (( seq_id (vseq . k)) . i))

                .= ((rseqi . m) - (( seq_id (vseq . k)) . i)) by A3

                .= ((rseqi . m) - (rseqi . k)) by A3;

                

                then ((( seq_id ((vseq . m) - (vseq . k))) . i) * (( seq_id ((vseq . m) - (vseq . k))) . i)) = (((rseqi . m) - (rseqi . k)) ^2 )

                .= ( |.((rseqi . m) - (rseqi . k)).| ^2 ) by COMPLEX1: 75

                .= ( |.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).|);

                then

                 A8: ( |.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).|) = ((( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k)))) . i) by SEQ_1: 8;

                

                 A9: for i be Nat holds 0 <= ((( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k)))) . i)

                proof

                  let i be Nat;

                  ((( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k)))) . i) = ((( seq_id ((vseq . m) - (vseq . k))) . i) * (( seq_id ((vseq . m) - (vseq . k))) . i)) by SEQ_1: 8;

                  hence thesis by XREAL_1: 63;

                end;

                

                 A10: (( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k)))) is summable by RSSPACE:def 11;

                then

                 A11: 0 <= ( Sum (( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k))))) by A9, SERIES_1: 18;

                then 0 <= ( sqrt ( Sum (( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k)))))) by SQUARE_1:def 2;

                then (( sqrt ( Sum (( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k)))))) ^2 ) < (e1 ^2 ) by A6, SQUARE_1: 16;

                then

                 A12: ( Sum (( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k))))) < (e * e) by A11, SQUARE_1:def 2;

                ((( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k)))) . i) <= ( Sum (( seq_id ((vseq . m) - (vseq . k))) (#) ( seq_id ((vseq . m) - (vseq . k))))) by A10, A9, Lm1;

                then

                 A13: 0 <= |.((rseqi . m) - (rseqi . k)).| & ( |.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).|) < (e * e) by A12, A8, COMPLEX1: 46, XXREAL_0: 2;

                ( sqrt (e * e)) = ( sqrt (e1 ^2 ))

                .= e by A4, SQUARE_1: 22;

                hence |.((rseqi . m) - (rseqi . k)).| < e by A13, A7, SQUARE_1: 27;

              end;

              hence thesis;

            end;

          end;

          then rseqi is convergent by SEQ_4: 41;

          hence thesis by A3;

        end;

        consider f be sequence of REAL such that

         A14: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A2);

        reconsider tseq = f as Real_Sequence;

         A15:

        now

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          then ex i0 be Nat st i = i0 & ex rseqi be Real_Sequence st (for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i0)) & rseqi is convergent & (f . i) = ( lim rseqi) by A14;

          hence ex rseqi be Real_Sequence st (for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i)) & rseqi is convergent & (tseq . i) = ( lim rseqi);

        end;

        

         A16: for e be Real st e > 0 holds ex k be Nat st for n be Nat st n >= k holds ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n)))) is summable & ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) < (e * e)

        proof

          let e1 be Real such that

           A17: e1 > 0 ;

          set e = (e1 / 2);

          

           A18: e > 0 by A17, XREAL_1: 215;

          then

          consider k be Nat such that

           A19: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, BHSP_3: 2;

          e < e1 by A17, XREAL_1: 216;

          then

           A20: (e * e) < (e1 * e1) by A18, XREAL_1: 97;

          

           A21: for m,n be Nat st n >= k & m >= k holds ((( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))) is summable & ( Sum (( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m))))) < (e * e) & for i be Nat holds 0 <= ((( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))) . i))

          proof

            let m,n be Nat;

            assume n >= k & m >= k;

            then ||.((vseq . n) - (vseq . m)).|| < e by A19;

            then ( sqrt (((vseq . n) - (vseq . m)) .|. ((vseq . n) - (vseq . m)))) < e by BHSP_1:def 4;

            then

             A22: ( sqrt ( Sum (( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))))) < e by Th1;

            

             A23: for i be Nat holds 0 <= ((( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))) . i)

            proof

              let i be Nat;

              ((( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))) . i) = ((( seq_id ((vseq . n) - (vseq . m))) . i) * (( seq_id ((vseq . n) - (vseq . m))) . i)) by SEQ_1: 8;

              hence thesis by XREAL_1: 63;

            end;

            (( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))) is summable by RSSPACE:def 11;

            then

             A24: 0 <= ( Sum (( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m))))) by A23, SERIES_1: 18;

            then 0 <= ( sqrt ( Sum (( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))))) by SQUARE_1:def 2;

            then (( sqrt ( Sum (( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))))) ^2 ) < (e ^2 ) by A22, SQUARE_1: 16;

            hence thesis by A23, A24, RSSPACE:def 11, SQUARE_1:def 2;

          end;

          

           A25: for n,i be Nat holds for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . i)) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . i)

          proof

            let n be Nat;

            defpred P[ Nat] means for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . $1)) holds (rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . $1));

            

             A26: for m,k be Nat holds ( seq_id ((vseq . m) - (vseq . k))) = (( seq_id (vseq . m)) - ( seq_id (vseq . k))) by Th1;

            for i be Nat st P[i] holds P[(i + 1)]

            proof

              let i be Nat such that

               A27: for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . i)) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . i);

              thus for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . (i + 1))) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . (i + 1))

              proof

                deffunc F( Nat) = (( Partial_Sums (( seq_id ((vseq . $1) - (vseq . n))) (#) ( seq_id ((vseq . $1) - (vseq . n))))) . i);

                consider rseqb be Real_Sequence such that

                 A28: for m be Nat holds (rseqb . m) = F(m) from SEQ_1:sch 1;

                consider rseq0 be Real_Sequence such that

                 A29: for m be Nat holds (rseq0 . m) = (( seq_id (vseq . m)) . (i + 1)) and

                 A30: rseq0 is convergent and

                 A31: (tseq . (i + 1)) = ( lim rseq0) by A15;

                let rseq be Real_Sequence such that

                 A32: for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . (i + 1));

                 A33:

                now

                  let m be Nat;

                  

                  thus (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . (i + 1)) by A32

                  .= (((( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . i)) by SERIES_1:def 1

                  .= ((((( seq_id (vseq . m)) - ( seq_id (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . i)) by A26

                  .= ((((( seq_id (vseq . m)) - ( seq_id (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + (rseqb . m)) by A28

                  .= ((((( seq_id (vseq . m)) - ( seq_id (vseq . n))) (#) (( seq_id (vseq . m)) - ( seq_id (vseq . n)))) . (i + 1)) + (rseqb . m)) by A26

                  .= ((((( seq_id (vseq . m)) - ( seq_id (vseq . n))) . (i + 1)) * ((( seq_id (vseq . m)) - ( seq_id (vseq . n))) . (i + 1))) + (rseqb . m)) by SEQ_1: 8

                  .= ((((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . (i + 1)) * ((( seq_id (vseq . m)) - ( seq_id (vseq . n))) . (i + 1))) + (rseqb . m)) by SEQ_1: 11

                  .= ((((( seq_id (vseq . m)) . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))) * ((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . (i + 1))) + (rseqb . m)) by SEQ_1: 7, SEQ_1: 11

                  .= ((((( seq_id (vseq . m)) . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))) * ((( seq_id (vseq . m)) . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1)))) + (rseqb . m)) by SEQ_1: 7

                  .= ((((( seq_id (vseq . m)) . (i + 1)) + ( - (( seq_id (vseq . n)) . (i + 1)))) * ((( seq_id (vseq . m)) . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1)))) + (rseqb . m)) by SEQ_1: 10

                  .= ((((( seq_id (vseq . m)) . (i + 1)) - (( seq_id (vseq . n)) . (i + 1))) * ((( seq_id (vseq . m)) . (i + 1)) + ( - (( seq_id (vseq . n)) . (i + 1))))) + (rseqb . m)) by SEQ_1: 10

                  .= ((((rseq0 . m) - (( seq_id (vseq . n)) . (i + 1))) * ((( seq_id (vseq . m)) . (i + 1)) - (( seq_id (vseq . n)) . (i + 1)))) + (rseqb . m)) by A29

                  .= ((((rseq0 . m) - (( seq_id (vseq . n)) . (i + 1))) * ((rseq0 . m) - (( seq_id (vseq . n)) . (i + 1)))) + (rseqb . m)) by A29;

                end;

                

                 A34: rseqb is convergent by A27, A28;

                

                then ( lim rseq) = ((((tseq . (i + 1)) + ( - (( seq_id (vseq . n)) . (i + 1)))) * ((tseq . (i + 1)) - (( seq_id (vseq . n)) . (i + 1)))) + ( lim rseqb)) by A30, A31, A33, Lm5

                .= ((((tseq . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))) * ((tseq . (i + 1)) + ( - (( seq_id (vseq . n)) . (i + 1))))) + ( lim rseqb)) by SEQ_1: 10

                .= ((((tseq . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))) * ((tseq . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1)))) + ( lim rseqb)) by SEQ_1: 10

                .= ((((tseq + ( - ( seq_id (vseq . n)))) . (i + 1)) * ((tseq . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1)))) + ( lim rseqb)) by SEQ_1: 7

                .= ((((tseq - ( seq_id (vseq . n))) . (i + 1)) * ((tseq + ( - ( seq_id (vseq . n)))) . (i + 1))) + ( lim rseqb)) by SEQ_1: 7, SEQ_1: 11

                .= ((((tseq - ( seq_id (vseq . n))) . (i + 1)) * ((tseq - ( seq_id (vseq . n))) . (i + 1))) + ( lim rseqb)) by SEQ_1: 11

                .= ((((tseq - ( seq_id (vseq . n))) (#) (tseq - ( seq_id (vseq . n)))) . (i + 1)) + ( lim rseqb)) by SEQ_1: 8

                .= ((((tseq - ( seq_id (vseq . n))) (#) (tseq - ( seq_id (vseq . n)))) . (i + 1)) + (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . i)) by A27, A28

                .= (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . (i + 1)) by SERIES_1:def 1;

                hence thesis by A34, A30, A33, Lm5;

              end;

            end;

            then

             A35: for i be Nat st P[i] holds P[(i + 1)];

            now

              let rseq be Real_Sequence such that

               A36: for m be Nat holds (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . 0 );

              thus rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . 0 )

              proof

                consider rseq0 be Real_Sequence such that

                 A37: for m be Nat holds (rseq0 . m) = (( seq_id (vseq . m)) . 0 ) and

                 A38: rseq0 is convergent and

                 A39: (tseq . 0 ) = ( lim rseq0) by A15;

                 A40:

                now

                  let m be Nat;

                  

                  thus (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . 0 ) by A36

                  .= ((( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n)))) . 0 ) by SERIES_1:def 1

                  .= (((( seq_id (vseq . m)) - ( seq_id (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n)))) . 0 ) by A26

                  .= (((( seq_id (vseq . m)) - ( seq_id (vseq . n))) (#) (( seq_id (vseq . m)) - ( seq_id (vseq . n)))) . 0 ) by A26

                  .= (((( seq_id (vseq . m)) - ( seq_id (vseq . n))) . 0 ) * ((( seq_id (vseq . m)) - ( seq_id (vseq . n))) . 0 )) by SEQ_1: 8

                  .= (((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . 0 ) * ((( seq_id (vseq . m)) - ( seq_id (vseq . n))) . 0 )) by SEQ_1: 11

                  .= (((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 )) * ((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . 0 )) by SEQ_1: 7, SEQ_1: 11

                  .= (((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 )) * ((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 ))) by SEQ_1: 7

                  .= (((( seq_id (vseq . m)) . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))) * ((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 ))) by SEQ_1: 10

                  .= (((( seq_id (vseq . m)) . 0 ) - (( seq_id (vseq . n)) . 0 )) * ((( seq_id (vseq . m)) . 0 ) + ( - (( seq_id (vseq . n)) . 0 )))) by SEQ_1: 10

                  .= (((rseq0 . m) - (( seq_id (vseq . n)) . 0 )) * ((( seq_id (vseq . m)) . 0 ) - (( seq_id (vseq . n)) . 0 ))) by A37

                  .= (((rseq0 . m) - (( seq_id (vseq . n)) . 0 )) * ((rseq0 . m) - (( seq_id (vseq . n)) . 0 ))) by A37;

                end;

                

                then ( lim rseq) = (((tseq . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))) * ((tseq . 0 ) - (( seq_id (vseq . n)) . 0 ))) by A38, A39, Lm4

                .= (((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 )) * ((tseq . 0 ) + ( - (( seq_id (vseq . n)) . 0 )))) by SEQ_1: 10

                .= (((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 )) * ((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 ))) by SEQ_1: 10

                .= (((tseq + ( - ( seq_id (vseq . n)))) . 0 ) * ((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 ))) by SEQ_1: 7

                .= (((tseq - ( seq_id (vseq . n))) . 0 ) * ((tseq + ( - ( seq_id (vseq . n)))) . 0 )) by SEQ_1: 7, SEQ_1: 11

                .= (((tseq - ( seq_id (vseq . n))) . 0 ) * ((tseq - ( seq_id (vseq . n))) . 0 )) by SEQ_1: 11

                .= (((tseq - ( seq_id (vseq . n))) (#) (tseq - ( seq_id (vseq . n)))) . 0 ) by SEQ_1: 8

                .= (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . 0 ) by SERIES_1:def 1;

                hence thesis by A38, A40, Lm4;

              end;

            end;

            then

             A41: P[ 0 ];

            for i be Nat holds P[i] from NAT_1:sch 2( A41, A35);

            hence thesis;

          end;

          for n be Nat st n >= k holds ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n)))) is summable & ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) < (e1 * e1)

          proof

            let n be Nat such that

             A42: n >= k;

            

             A43: for i be Nat st 0 <= i holds (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . i) <= (e * e)

            proof

              let i be Nat such that 0 <= i;

              deffunc F( Nat) = (( Partial_Sums (( seq_id ((vseq . $1) - (vseq . n))) (#) ( seq_id ((vseq . $1) - (vseq . n))))) . i);

              consider rseq be Real_Sequence such that

               A44: for m be Nat holds (rseq . m) = F(m) from SEQ_1:sch 1;

              

               A45: for m be Nat st m >= k holds (rseq . m) <= (e * e)

              proof

                let m be Nat such that

                 A46: m >= k;

                (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n)))) is summable & for i be Nat holds 0 <= ((( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n)))) . i) by A21, A42, A46;

                then

                 A47: (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . i) <= ( Sum (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) by Lm1;

                

                 A48: (rseq . m) = (( Partial_Sums (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) . i) by A44;

                ( Sum (( seq_id ((vseq . m) - (vseq . n))) (#) ( seq_id ((vseq . m) - (vseq . n))))) < (e * e) by A21, A42, A46;

                hence thesis by A48, A47, XXREAL_0: 2;

              end;

              rseq is convergent & ( lim rseq) = (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . i) by A25, A44;

              hence thesis by A45, Lm3;

            end;

            now

              let i be Nat;

              (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . i) <= (e * e) by A43;

              hence (( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) . i) < (e1 * e1) by A20, XXREAL_0: 2;

            end;

            then

             A49: ( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) is bounded_above by SEQ_2:def 3;

            

             A50: for i be Nat holds 0 <= (((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n)))) . i)

            proof

              let i be Nat;

              (((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n)))) . i) = (((( seq_id tseq) - ( seq_id (vseq . n))) . i) * ((( seq_id tseq) - ( seq_id (vseq . n))) . i)) by SEQ_1: 8;

              hence thesis by XREAL_1: 63;

            end;

            then ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n)))) is summable by A49, SERIES_1: 17;

            then ( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) is convergent by SERIES_1:def 2;

            then ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) = ( lim ( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n)))))) & ( lim ( Partial_Sums ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n)))))) <= (e * e) by A43, Lm3, SERIES_1:def 3;

            hence thesis by A20, A50, A49, SERIES_1: 17, XXREAL_0: 2;

          end;

          hence thesis;

        end;

        

         A51: (( seq_id tseq) (#) ( seq_id tseq)) is summable

        proof

          set d = (( seq_id tseq) (#) ( seq_id tseq));

          

           A52: for i be Nat holds 0 <= ((( seq_id tseq) (#) ( seq_id tseq)) . i)

          proof

            let i be Nat;

            ((( seq_id tseq) (#) ( seq_id tseq)) . i) = ((( seq_id tseq) . i) * (( seq_id tseq) . i)) by SEQ_1: 8;

            hence thesis by XREAL_1: 63;

          end;

          consider m be Nat such that

           A53: for n be Nat st n >= m holds ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n)))) is summable & ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) < (1 * 1) by A16;

          set b = (( seq_id (vseq . m)) (#) ( seq_id (vseq . m)));

          set a = ((( seq_id tseq) - ( seq_id (vseq . m))) (#) (( seq_id tseq) - ( seq_id (vseq . m))));

          (( seq_id (vseq . m)) (#) ( seq_id (vseq . m))) is summable by RSSPACE:def 11;

          then

           A54: (2 (#) b) is summable by SERIES_1: 10;

          

           A55: for i be Nat holds (d . i) <= (((2 (#) a) + (2 (#) b)) . i)

          proof

            let i be Nat;

            set x = (( seq_id tseq) . i);

            set y = (( seq_id (vseq . m)) . i);

            

             A56: (2 * (b . i)) = (2 * (y * y)) by SEQ_1: 8

            .= ((2 * y) * y);

            ((( seq_id tseq) - ( seq_id (vseq . m))) . i) = ((( seq_id tseq) + ( - ( seq_id (vseq . m)))) . i) by SEQ_1: 11

            .= ((( seq_id tseq) . i) + (( - ( seq_id (vseq . m))) . i)) by SEQ_1: 7

            .= ((( seq_id tseq) . i) + ( - (( seq_id (vseq . m)) . i))) by SEQ_1: 10

            .= ((( seq_id tseq) . i) - (( seq_id (vseq . m)) . i));

            then (a . i) = (((( seq_id tseq) . i) - (( seq_id (vseq . m)) . i)) * ((( seq_id tseq) . i) - (( seq_id (vseq . m)) . i))) by SEQ_1: 8;

            then

             A57: (d . i) = ((( seq_id tseq) . i) * (( seq_id tseq) . i)) & (2 * (a . i)) = ((2 * (x - y)) * (x - y)) by SEQ_1: 8;

            (((2 (#) a) + (2 (#) b)) . i) = (((2 (#) a) . i) + ((2 (#) b) . i)) by SEQ_1: 7

            .= ((2 * (a . i)) + ((2 (#) b) . i)) by SEQ_1: 9

            .= ((2 * (a . i)) + (2 * (b . i))) by SEQ_1: 9;

            hence thesis by A57, A56, Lm2;

          end;

          ((( seq_id tseq) - ( seq_id (vseq . m))) (#) (( seq_id tseq) - ( seq_id (vseq . m)))) is summable by A53;

          then (2 (#) a) is summable by SERIES_1: 10;

          then ((2 (#) a) + (2 (#) b)) is summable by A54, SERIES_1: 7;

          hence thesis by A52, A55, SERIES_1: 20;

        end;

        tseq in the_set_of_RealSequences by FUNCT_2: 8;

        then

        reconsider tv = tseq as Point of l2_Space by A51, RSSPACE:def 11;

        for e be Real st e > 0 holds ex m be Nat st for n be Nat st n >= m holds ||.((vseq . n) - tv).|| < e

        proof

          let e be Real such that

           A58: e > 0 ;

          consider m be Nat such that

           A59: for n be Nat st n >= m holds ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n)))) is summable & ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) < (e * e) by A16, A58;

          now

            tseq in the_set_of_RealSequences by FUNCT_2: 8;

            then

            reconsider u = tseq as VECTOR of l2_Space by A51, RSSPACE:def 11;

            let n be Nat;

            assume n >= m;

            then

             A60: ( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) (#) (( seq_id tseq) - ( seq_id (vseq . n))))) < (e * e) by A59;

            reconsider v = (vseq . n) as VECTOR of l2_Space ;

            ( seq_id (u - v)) = (( seq_id tseq) - ( seq_id (vseq . n))) by Th1;

            then

             A61: ((u - v) .|. (u - v)) < (e * e) by A60, Th1;

            

             A62: ||.((vseq . n) - tv).|| = ||.( - (tv - (vseq . n))).|| by RLVECT_1: 33

            .= ||.(tv - (vseq . n)).|| by BHSP_1: 31

            .= ( sqrt ((u - v) .|. (u - v))) by BHSP_1:def 4;

             0 <= ((u - v) .|. (u - v)) by BHSP_1:def 2;

            then ( sqrt ((u - v) .|. (u - v))) < ( sqrt (e ^2 )) by A61, SQUARE_1: 27;

            hence ||.((vseq . n) - tv).|| < e by A58, A62, SQUARE_1: 22;

          end;

          hence thesis;

        end;

        hence thesis by BHSP_2: 9;

      end;

    end

    registration

      cluster complete for RealUnitarySpace;

      existence

      proof

        take l2_Space ;

        thus thesis;

      end;

    end

    definition

      mode RealHilbertSpace is complete RealUnitarySpace;

    end

    begin

    theorem :: RSSPACE2:3

    for r be Real_Sequence st (for n be Nat holds 0 <= (r . n)) holds (for n be Nat holds 0 <= (( Partial_Sums r) . n)) & (for n be Nat holds (r . n) <= (( Partial_Sums r) . n)) & (r is summable implies (for n be Nat holds (( Partial_Sums r) . n) <= ( Sum r)) & for n be Nat holds (r . n) <= ( Sum r)) by Lm1;

    theorem :: RSSPACE2:4

    (for x,y be Real holds ((x + y) * (x + y)) <= (((2 * x) * x) + ((2 * y) * y))) & for x,y be Real holds (x * x) <= (((2 * (x - y)) * (x - y)) + ((2 * y) * y)) by Lm2;

    theorem :: RSSPACE2:5

    for e be Real, s be Real_Sequence st (s is convergent & ex k be Nat st for i be Nat st k <= i holds (s . i) <= e) holds ( lim s) <= e by Lm3;

    theorem :: RSSPACE2:6

    for c be Real, s be Real_Sequence st s is convergent holds for r be Real_Sequence st (for i be Nat holds (r . i) = (((s . i) - c) * ((s . i) - c))) holds r is convergent & ( lim r) = ((( lim s) - c) * (( lim s) - c)) by Lm4;

    theorem :: RSSPACE2:7

    for c be Real, s,s1 be Real_Sequence st s is convergent & s1 is convergent holds for r be Real_Sequence st (for i be Nat holds (r . i) = ((((s . i) - c) * ((s . i) - c)) + (s1 . i))) holds r is convergent & ( lim r) = (((( lim s) - c) * (( lim s) - c)) + ( lim s1)) by Lm5;