csspace2.miz



    begin

    

     Lm1: for seq be Complex_Sequence holds ( Partial_Sums (seq *' )) = (( Partial_Sums seq) *' )

    proof

      let seq be Complex_Sequence;

      defpred P[ Nat] means (( Partial_Sums (seq *' )) . $1) = ((( Partial_Sums seq) *' ) . $1);

       A1:

      now

        let n be Nat;

        

         A2: n in NAT by ORDINAL1:def 12;

        assume

         A3: P[n];

        (( Partial_Sums (seq *' )) . (n + 1)) = ((( Partial_Sums (seq *' )) . n) + ((seq *' ) . (n + 1))) by SERIES_1:def 1

        .= (((( Partial_Sums seq) *' ) . n) + ((seq . (n + 1)) *' )) by A3, COMSEQ_2:def 2

        .= (((( Partial_Sums seq) . n) *' ) + ((seq . (n + 1)) *' )) by COMSEQ_2:def 2, A2

        .= (((( Partial_Sums seq) . n) + (seq . (n + 1))) *' ) by COMPLEX1: 32

        .= ((( Partial_Sums seq) . (n + 1)) *' ) by SERIES_1:def 1;

        hence P[(n + 1)] by COMSEQ_2:def 2;

      end;

      (( Partial_Sums (seq *' )) . 0 ) = ((seq *' ) . 0 ) by SERIES_1:def 1

      .= ((seq . 0 ) *' ) by COMSEQ_2:def 2

      .= ((( Partial_Sums seq) . 0 ) *' ) by SERIES_1:def 1;

      then

       A4: P[ 0 ] by COMSEQ_2:def 2;

      for n be Nat holds P[n] from NAT_1:sch 2( A4, A1);

      then for n be Element of NAT holds P[n];

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm2: for a,b be Real holds 0 <= ((a ^2 ) + (b ^2 ))

    proof

      let a,b be Real;

       0 <= (a ^2 ) & 0 <= (b ^2 ) by XREAL_1: 63;

      then ( 0 + 0 ) <= ((a ^2 ) + (b ^2 ));

      hence thesis;

    end;

    

     Lm3: for z1,z2 be Complex st (( Re z1) * ( Im z2)) = (( Re z2) * ( Im z1)) & ((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) >= 0 holds |.(z1 + z2).| = ( |.z1.| + |.z2.|)

    proof

      let z1,z2 be Complex;

      assume that

       A1: (( Re z1) * ( Im z2)) = (( Re z2) * ( Im z1)) and

       A2: ((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) >= 0 ;

      set r1 = ( Re z1), r2 = ( Re z2), i1 = ( Im z1), i2 = ( Im z2);

      

       A3: (( Re (z1 + z2)) ^2 ) = ((r1 + r2) ^2 ) by COMPLEX1: 8

      .= (((r1 ^2 ) + ((2 * r1) * r2)) + (r2 ^2 ));

      ((r1 * r2) + (i1 * i2)) = |.((r1 * r2) + (i1 * i2)).| by A2, ABSVALUE:def 1;

      then

       A4: ((r1 * r2) + (i1 * i2)) = ( sqrt (((r1 * r2) + (i1 * i2)) ^2 )) by COMPLEX1: 72;

      

       A5: (( Im (z1 + z2)) ^2 ) = ((i1 + i2) ^2 ) by COMPLEX1: 8

      .= (((i1 ^2 ) + ((2 * i1) * i2)) + (i2 ^2 ));

      

       A6: 0 <= ((r2 ^2 ) + (i2 ^2 )) by Lm2;

      then

       A7: (( sqrt ((r2 ^2 ) + (i2 ^2 ))) ^2 ) = ((r2 ^2 ) + (i2 ^2 )) by SQUARE_1:def 2;

      

       A8: 0 <= ( sqrt ((r2 ^2 ) + (i2 ^2 ))) by A6, SQUARE_1:def 2;

      

       A9: 0 <= ((r1 ^2 ) + (i1 ^2 )) by Lm2;

      then 0 <= ( sqrt ((r1 ^2 ) + (i1 ^2 ))) by SQUARE_1:def 2;

      then

       A10: ( 0 + 0 ) <= (( sqrt ((r1 ^2 ) + (i1 ^2 ))) + ( sqrt ((r2 ^2 ) + (i2 ^2 )))) by A8;

      ((((r1 ^2 ) + (i1 ^2 )) * ((r2 ^2 ) + (i2 ^2 ))) - (((r1 * r2) + (i1 * i2)) ^2 )) = (((r1 * i2) - (i1 * r2)) ^2 );

      then ( sqrt (((r1 * r2) + (i1 * i2)) ^2 )) = ( sqrt (((r1 ^2 ) + (i1 ^2 )) * ((r2 ^2 ) + (i2 ^2 )))) by A1, XCMPLX_1: 15;

      then

       A11: ( sqrt (((r1 * r2) + (i1 * i2)) ^2 )) = (( sqrt ((r1 ^2 ) + (i1 ^2 ))) * ( sqrt ((r2 ^2 ) + (i2 ^2 )))) by A9, A6, SQUARE_1: 29;

      (( sqrt ((r1 ^2 ) + (i1 ^2 ))) ^2 ) = ((r1 ^2 ) + (i1 ^2 )) by A9, SQUARE_1:def 2;

      then ( sqrt ((( Re (z1 + z2)) ^2 ) + (( Im (z1 + z2)) ^2 ))) = ( sqrt ((( sqrt ((r1 ^2 ) + (i1 ^2 ))) + ( sqrt ((r2 ^2 ) + (i2 ^2 )))) ^2 )) by A7, A3, A5, A4, A11;

      then ( sqrt ((( Re (z1 + z2)) ^2 ) + (( Im (z1 + z2)) ^2 ))) = (( sqrt ((r1 ^2 ) + (i1 ^2 ))) + ( sqrt ((r2 ^2 ) + (i2 ^2 )))) by A10, SQUARE_1: 22;

      then ( sqrt ((( Re (z1 + z2)) ^2 ) + (( Im (z1 + z2)) ^2 ))) = (( sqrt ((r1 ^2 ) + (i1 ^2 ))) + |.z2.|) by COMPLEX1:def 12;

      then ( sqrt ((( Re (z1 + z2)) ^2 ) + (( Im (z1 + z2)) ^2 ))) = ( |.z1.| + |.z2.|) by COMPLEX1:def 12;

      hence thesis by COMPLEX1:def 12;

    end;

    

     Lm4: for seq be Complex_Sequence, n be Nat st (for i be Nat holds (( Re seq) . i) >= 0 & (( Im seq) . i) = 0 ) holds ( |.( Partial_Sums seq).| . n) = (( Partial_Sums |.seq.|) . n)

    proof

      let seq be Complex_Sequence;

      let n be Nat;

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

      assume

       A1: for i be Nat holds (( Re seq) . i) >= 0 & (( Im seq) . i) = 0 ;

       A2:

      now

        let m be Nat;

        assume

         A3: P[m];

        thus P[(m + 1)]

        proof

          for i be Nat holds (( Partial_Sums ( Re seq)) . i) >= 0

          proof

            defpred Q1[ Nat] means (( Partial_Sums ( Re seq)) . $1) >= 0 ;

            let i be Nat;

             A4:

            now

              let k be Nat;

              assume

               A5: Q1[k];

              (( Partial_Sums ( Re seq)) . (k + 1)) = ((( Partial_Sums ( Re seq)) . k) + (( Re seq) . (k + 1))) & (( Re seq) . (k + 1)) >= 0 by A1, SERIES_1:def 1;

              then (( Partial_Sums ( Re seq)) . (k + 1)) >= ( 0 + 0 ) by A5;

              hence Q1[(k + 1)];

            end;

            (( Partial_Sums ( Re seq)) . 0 ) = (( Re seq) . 0 ) by SERIES_1:def 1;

            then

             A6: Q1[ 0 ] by A1;

            for i be Nat holds Q1[i] from NAT_1:sch 2( A6, A4);

            hence thesis;

          end;

          then (( Partial_Sums ( Re seq)) . m) >= 0 ;

          then (( Re ( Partial_Sums seq)) . m) >= 0 by COMSEQ_3: 26;

          then

           A7: ( Re (( Partial_Sums seq) . m)) >= 0 by COMSEQ_3:def 5;

          set z2 = (seq . (m + 1));

          set z1 = (( Partial_Sums seq) . m);

          

           A8: ( |.( Partial_Sums seq).| . (m + 1)) = |.(( Partial_Sums seq) . (m + 1)).| by VALUED_1: 18

          .= |.((( Partial_Sums seq) . m) + (seq . (m + 1))).| by SERIES_1:def 1;

          for i be Nat holds (( Partial_Sums ( Im seq)) . i) = 0

          proof

            defpred Q2[ Nat] means (( Partial_Sums ( Im seq)) . $1) = 0 ;

            let i be Nat;

             A9:

            now

              let k be Nat;

              

               A10: (( Partial_Sums ( Im seq)) . (k + 1)) = ((( Partial_Sums ( Im seq)) . k) + (( Im seq) . (k + 1))) by SERIES_1:def 1;

              assume Q2[k];

              hence Q2[(k + 1)] by A1, A10;

            end;

            (( Partial_Sums ( Im seq)) . 0 ) = (( Im seq) . 0 ) by SERIES_1:def 1;

            then

             A11: Q2[ 0 ] by A1;

            for i be Nat holds Q2[i] from NAT_1:sch 2( A11, A9);

            hence thesis;

          end;

          then (( Partial_Sums ( Im seq)) . m) = 0 ;

          then (( Im ( Partial_Sums seq)) . m) = 0 by COMSEQ_3: 26;

          then

           A12: ( Im (( Partial_Sums seq) . m)) = 0 by COMSEQ_3:def 6;

          (( Im seq) . (m + 1)) = 0 by A1;

          then ( Im (seq . (m + 1))) = 0 by COMSEQ_3:def 6;

          then

           A13: (( Re z1) * ( Im z2)) = (( Re z2) * ( Im z1)) by A12;

          (( Re seq) . (m + 1)) >= 0 by A1;

          then ( Re (seq . (m + 1))) >= 0 by COMSEQ_3:def 5;

          then ((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) >= 0 by A7, A12;

          

          then ( |.( Partial_Sums seq).| . (m + 1)) = ( |.(( Partial_Sums seq) . m).| + |.(seq . (m + 1)).|) by A8, A13, Lm3

          .= (( |.( Partial_Sums seq).| . m) + |.(seq . (m + 1)).|) by VALUED_1: 18

          .= ((( Partial_Sums |.seq.|) . m) + ( |.seq.| . (m + 1))) by A3, VALUED_1: 18;

          hence thesis by SERIES_1:def 1;

        end;

      end;

      ( |.( Partial_Sums seq).| . 0 ) = |.(( Partial_Sums seq) . 0 ).| by VALUED_1: 18

      .= |.(seq . 0 ).| by SERIES_1:def 1

      .= ( |.seq.| . 0 ) by VALUED_1: 18;

      then

       A14: P[ 0 ] by SERIES_1:def 1;

      for m be Nat holds P[m] from NAT_1:sch 2( A14, A2);

      hence thesis;

    end;

    

     Lm5: for seq be Complex_Sequence st seq is summable holds ( Sum (seq *' )) = (( Sum seq) *' )

    proof

      let seq be Complex_Sequence;

      assume

       A1: seq is summable;

      ( Sum (seq *' )) = ( lim ( Partial_Sums (seq *' ))) by COMSEQ_3:def 7

      .= ( lim (( Partial_Sums seq) *' )) by Lm1

      .= (( lim ( Partial_Sums seq)) *' ) by A1, COMSEQ_2: 12;

      hence thesis by COMSEQ_3:def 7;

    end;

    

     Lm6: for seq be Complex_Sequence st seq is absolutely_summable holds |.( Sum seq).| <= ( Sum |.seq.|)

    proof

      let seq be Complex_Sequence;

      

       A1: for k be Nat holds ( |.( Partial_Sums seq).| . k) <= (( Partial_Sums |.seq.|) . k)

      proof

        let k be Nat;

         |.(( Partial_Sums seq) . k).| <= (( Partial_Sums |.seq.|) . k) by COMSEQ_3: 30;

        hence thesis by VALUED_1: 18;

      end;

      assume

       A2: seq is absolutely_summable;

      then

      reconsider Pseq = ( Partial_Sums seq) as convergent Complex_Sequence;

      

       A3: |.( Sum seq).| = |.( lim ( Partial_Sums seq)).| by COMSEQ_3:def 7

      .= ( lim |.( Partial_Sums seq).|) by A2, SEQ_2: 27;

       |.Pseq.| is convergent & ( Partial_Sums |.seq.|) is convergent by A2, SERIES_1:def 2;

      then ( lim |.( Partial_Sums seq).|) <= ( lim ( Partial_Sums |.seq.|)) by A1, SEQ_2: 18;

      hence thesis by A3, SERIES_1:def 3;

    end;

    

     Lm7: for seq be Complex_Sequence st seq is summable & (for n be Nat holds (( Re seq) . n) >= 0 & (( Im seq) . n) = 0 ) holds |.( Sum seq).| = ( Sum |.seq.|)

    proof

      let seq be Complex_Sequence;

      assume that

       A1: seq is summable and

       A2: for n be Nat holds (( Re seq) . n) >= 0 & (( Im seq) . n) = 0 ;

      for x be object st x in NAT holds ( |.( Partial_Sums seq).| . x) = (( Partial_Sums |.seq.|) . x) by A2, Lm4;

      then |.( Partial_Sums seq).| = ( Partial_Sums |.seq.|) by FUNCT_2: 12;

      then ( lim |.( Partial_Sums seq).|) = ( Sum |.seq.|) by SERIES_1:def 3;

      then |.( lim ( Partial_Sums seq)).| = ( Sum |.seq.|) by A1, SEQ_2: 27;

      hence thesis by COMSEQ_3:def 7;

    end;

    

     Lm8: for seq be Complex_Sequence, n be Nat holds (( Re (seq (#) (seq *' ))) . n) >= 0 & (( Im (seq (#) (seq *' ))) . n) = 0

    proof

      let seq be Complex_Sequence;

      let n be Nat;

      

       A1: n in NAT by ORDINAL1:def 12;

      then

      reconsider nn = n as Element of NAT ;

      reconsider z1 = (seq . nn) as Element of COMPLEX ;

      

       A2: 0 <= (( Re z1) ^2 ) & 0 <= (( Im z1) ^2 ) by XREAL_1: 63;

      (( Re (seq (#) (seq *' ))) . n) = ( Re ((seq (#) (seq *' )) . n)) by COMSEQ_3:def 5

      .= ( Re ((seq . n) * ((seq *' ) . n))) by VALUED_1: 5

      .= ( Re ((seq . n) * ((seq . n) *' ))) by COMSEQ_2:def 2, A1

      .= ((( Re z1) ^2 ) + (( Im z1) ^2 )) by COMPLEX1: 40;

      then (( Re (seq (#) (seq *' ))) . n) >= ( 0 + 0 ) by A2;

      hence (( Re (seq (#) (seq *' ))) . n) >= 0 ;

      (( Im (seq (#) (seq *' ))) . n) = ( Im ((seq (#) (seq *' )) . n)) by COMSEQ_3:def 6

      .= ( Im ((seq . n) * ((seq *' ) . n))) by VALUED_1: 5

      .= ( Im ((seq . n) * ((seq . n) *' ))) by COMSEQ_2:def 2, A1;

      hence thesis by COMPLEX1: 40;

    end;

    

     Lm9: for x be set holds x is Element of Complex_l2_Space iff x is Complex_Sequence & ( |.( seq_id x).| (#) |.( seq_id x).|) is summable

    proof

      for x be set holds x is Element of Complex_l2_Space iff x is Complex_Sequence & ( |.( seq_id x).| (#) |.( seq_id x).|) is summable

      proof

        let x be set;

        x in the_set_of_ComplexSequences iff x is Complex_Sequence by FUNCT_2: 8, FUNCT_2: 66;

        hence thesis by CSSPACE:def 11;

      end;

      hence thesis;

    end;

    

     Lm10: ( 0. Complex_l2_Space ) = CZeroseq

    proof

      

      thus ( 0. Complex_l2_Space ) = ( 0. Linear_Space_of_ComplexSequences ) by CSSPACE:def 10

      .= CZeroseq ;

    end;

    

     Lm12: for u,v be VECTOR of Complex_l2_Space holds (u + v) = (( seq_id u) + ( seq_id v))

    proof

      set W = the_set_of_l2ComplexSequences ;

      set L1 = Linear_Space_of_ComplexSequences ;

      let u,v be VECTOR of Complex_l2_Space ;

      reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_ComplexSequences by CLVECT_1: 29, CSSPACE: 13;

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

      then

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

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

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

      hence thesis by CSSPACE: 15;

    end;

    

     Lm13: for r be Complex holds for u be VECTOR of Complex_l2_Space holds (r * u) = (r (#) ( seq_id u))

    proof

      set W = the_set_of_l2ComplexSequences ;

      set L1 = Linear_Space_of_ComplexSequences ;

      let r be Complex;

      let u be VECTOR of Complex_l2_Space ;

      reconsider u1 = u as VECTOR of Linear_Space_of_ComplexSequences by CLVECT_1: 29, CSSPACE: 13;

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

      then

       A1: ( dom (the Mult of Linear_Space_of_ComplexSequences | [: COMPLEX , W:])) = [: COMPLEX , W:] by RELAT_1: 62, ZFMISC_1: 96;

      reconsider r as Element of COMPLEX by XCMPLX_0:def 2;

      (r * u) = (the Mult of Complex_l2_Space . [r, u]) by CLVECT_1:def 1

      .= ((the Mult of Linear_Space_of_ComplexSequences | [: COMPLEX , W:]) . [r, u]) by CSSPACE:def 9

      .= (the Mult of Linear_Space_of_ComplexSequences . [r, u]) by A1, FUNCT_1: 47

      .= (r * u1) by CLVECT_1:def 1;

      hence thesis by CSSPACE: 15;

    end;

    

     Lm14: for u be VECTOR of Complex_l2_Space holds ( - u) = ( - ( seq_id u)) & ( seq_id ( - u)) = ( - ( seq_id u))

    proof

      let u be VECTOR of Complex_l2_Space ;

      ( - u) = (( - 1r ) * u) by CLVECT_1: 3

      .= (( - 1r ) (#) ( seq_id u)) by Lm13

      .= ( - ( seq_id u)) by COMSEQ_1: 11;

      hence thesis;

    end;

    

     Lm15: for u,v be VECTOR of Complex_l2_Space holds (u - v) = (( seq_id u) - ( seq_id v))

    proof

      let u,v be VECTOR of Complex_l2_Space ;

      

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

      .= (( seq_id u) - ( seq_id v)) by Lm14;

    end;

    

     Lm16: for v,w be VECTOR of Complex_l2_Space holds ( |.( seq_id v).| (#) |.( seq_id w).|) is summable

    proof

      set q0 = (1 / 2);

      let u,v be VECTOR of Complex_l2_Space ;

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

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

      set r = |.( |.( seq_id u).| (#) |.( seq_id v).|).|;

      

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

      proof

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

        let n be Nat;

        set tt = |.(rr . n).|;

        

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

      end;

      

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

        set sn = |.(s . n).|, tn = |.(t . n).|;

        set ss = |.sn.|, tt = |.tn.|;

        

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

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

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

        .= (( |.(s . n).| * ( |.s.| . n)) + (( |.t.| . n) * ( |.t.| . n))) by VALUED_1: 18

        .= ((sn ^2 ) + (( |.t.| . n) * ( |.t.| . n))) by VALUED_1: 18

        .= ((sn ^2 ) + ( |.(t . n).| * ( |.t.| . n))) by VALUED_1: 18

        .= (( |.sn.| ^2 ) + ( |.tn.| ^2 )) by VALUED_1: 18;

        

         A5: 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 * ( |.( |.( seq_id u).| . n).| * |.( |.( seq_id v).| . n).|)) by COMPLEX1: 65

        .= (2 * ( |. |.(( seq_id u) . n).|.| * |.( |.( seq_id v).| . n).|)) by VALUED_1: 18

        .= (2 * (ss * tt)) by VALUED_1: 18

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

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

        hence thesis;

      end;

      

       A6: (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 CSSPACE:def 11;

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

      then (2 (#) r) is summable by A1, A3, SERIES_1: 20;

      then r is summable by A6, SERIES_1: 10;

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

      hence thesis;

    end;

    

     Lm18: for seq be Complex_Sequence holds |.seq.| = |.(seq *' ).|

    proof

      let seq be Complex_Sequence;

      reconsider rseq1 = |.seq.| as Real_Sequence;

      reconsider rseq2 = |.(seq *' ).| as Real_Sequence;

      for n be Nat holds ( |.seq.| . n) = ( |.(seq *' ).| . n)

      proof

        let n be Nat;

        

         A1: n in NAT by ORDINAL1:def 12;

        ( |.(seq *' ).| . n) = |.((seq *' ) . n).| by VALUED_1: 18

        .= |.((seq . n) *' ).| by COMSEQ_2:def 2, A1

        .= |.(seq . n).| by COMPLEX1: 53;

        hence thesis by VALUED_1: 18;

      end;

      then for n be object st n in NAT holds (rseq1 . n) = (rseq2 . n);

      hence thesis by FUNCT_2: 12;

    end;

    

     Lm19: for x be set holds x is Element of Complex_l2_Space iff x is Complex_Sequence & (( seq_id x) (#) (( seq_id x) *' )) is absolutely_summable

    proof

      

       A1: for x be set holds x is Element of Complex_l2_Space implies x is Complex_Sequence & (( seq_id x) (#) (( seq_id x) *' )) is absolutely_summable

      proof

        let x be set;

        

         A2: |.( seq_id x).| = |.(( seq_id x) *' ).| by Lm18;

        assume

         A3: x is Element of Complex_l2_Space ;

        then x in the_set_of_ComplexSequences by CSSPACE:def 11;

        hence x is Complex_Sequence by FUNCT_2: 66;

        ( |.( seq_id x).| (#) |.( seq_id x).|) is summable by A3, Lm16;

        then |.(( seq_id x) (#) (( seq_id x) *' )).| is summable by A2, COMSEQ_1: 46;

        hence thesis by COMSEQ_3:def 9;

      end;

      for x be set holds x is Complex_Sequence & (( seq_id x) (#) (( seq_id x) *' )) is absolutely_summable implies x is Element of Complex_l2_Space

      proof

        let x be set;

        assume that

         A4: x is Complex_Sequence and

         A5: (( seq_id x) (#) (( seq_id x) *' )) is absolutely_summable;

         |.(( seq_id x) (#) (( seq_id x) *' )).| is summable by A5;

        then ( |.( seq_id x).| (#) |.(( seq_id x) *' ).|) is summable by COMSEQ_1: 46;

        then

         A6: ( |.( seq_id x).| (#) |.( seq_id x).|) is summable by Lm18;

        x in the_set_of_ComplexSequences by A4, FUNCT_2: 8;

        hence thesis by A6, CSSPACE:def 11;

      end;

      hence thesis by A1;

    end;

    theorem :: CSSPACE2:1

    the carrier of Complex_l2_Space = the_set_of_l2ComplexSequences & (for x be set holds x is Element of Complex_l2_Space iff x is Complex_Sequence & ( |.( seq_id x).| (#) |.( seq_id x).|) is summable) & (for x be set holds x is Element of Complex_l2_Space iff x is Complex_Sequence & (( seq_id x) (#) (( seq_id x) *' )) is absolutely_summable) & ( 0. Complex_l2_Space ) = CZeroseq & (for u be VECTOR of Complex_l2_Space holds u = ( seq_id u)) & (for u,v be VECTOR of Complex_l2_Space holds (u + v) = (( seq_id u) + ( seq_id v))) & (for r be Complex holds for u be VECTOR of Complex_l2_Space holds (r * u) = (r (#) ( seq_id u))) & (for u be VECTOR of Complex_l2_Space holds ( - u) = ( - ( seq_id u)) & ( seq_id ( - u)) = ( - ( seq_id u))) & (for u,v be VECTOR of Complex_l2_Space holds (u - v) = (( seq_id u) - ( seq_id v))) & for v,w be VECTOR of Complex_l2_Space holds ( |.( seq_id v).| (#) |.( seq_id w).|) is summable & for v,w be VECTOR of Complex_l2_Space holds (v .|. w) = ( Sum (( seq_id v) (#) (( seq_id w) *' ))) by Lm9, Lm10, Lm12, Lm13, Lm14, Lm15, Lm16, Lm19, CSSPACE:def 17;

    theorem :: CSSPACE2:2

    

     Th2: for x,y,z be Point of Complex_l2_Space holds for a be Complex holds ((x .|. x) = 0 iff x = ( 0. Complex_l2_Space )) & ( Re (x .|. x)) >= 0 & ( Im (x .|. x)) = 0 & (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 Complex_l2_Space ;

      let a be Complex;

      set seqx = ( seq_id x);

      

       A1: (x .|. x) = ( Sum (seqx (#) (seqx *' ))) by CSSPACE:def 17;

      

       A2: (seqx (#) (seqx *' )) is absolutely_summable by Lm19;

      then ( Sum (seqx (#) (seqx *' ))) = (( Sum ( Re (seqx (#) (seqx *' )))) + (( Sum ( Im (seqx (#) (seqx *' )))) * <i> )) by COMSEQ_3: 53;

      then

       A3: ( Re (x .|. x)) = ( Sum ( Re (seqx (#) (seqx *' )))) & ( Im (x .|. x)) = ( Sum ( Im (seqx (#) (seqx *' )))) by A1, COMPLEX1: 12;

       A4:

      now

        set seq = ( seq_id x);

        

         A5: (x .|. x) = ( Sum (( seq_id x) (#) (( seq_id x) *' ))) by CSSPACE:def 17;

        set rseq = ( Re (seq (#) (seq *' )));

        

         A6: for n be Nat holds (rseq . n) = ((( Re (seq . n)) ^2 ) + (( Im (seq . n)) ^2 ))

        proof

          let n be Nat;

          

           A7: n in NAT by ORDINAL1:def 12;

          (rseq . n) = (((( Re seq) (#) ( Re (seq *' ))) - (( Im seq) (#) ( Im (seq *' )))) . n) by COMSEQ_3: 21

          .= (((( Re seq) (#) ( Re (seq *' ))) . n) + (( - (( Im seq) (#) ( Im (seq *' )))) . n)) by SEQ_1: 7

          .= (((( Re seq) (#) ( Re (seq *' ))) . n) + ( - ((( Im seq) (#) ( Im (seq *' ))) . n))) by SEQ_1: 10

          .= (((( Re seq) (#) ( Re (seq *' ))) . n) - ((( Im seq) (#) ( Im (seq *' ))) . n))

          .= (((( Re seq) . n) * (( Re (seq *' )) . n)) - ((( Im seq) (#) ( Im (seq *' ))) . n)) by SEQ_1: 8

          .= (((( Re seq) . n) * (( Re (seq *' )) . n)) - ((( Im seq) . n) * (( Im (seq *' )) . n))) by SEQ_1: 8

          .= ((( Re (seq . n)) * (( Re (seq *' )) . n)) - ((( Im seq) . n) * (( Im (seq *' )) . n))) by COMSEQ_3:def 5

          .= ((( Re (seq . n)) * ( Re ((seq *' ) . n))) - ((( Im seq) . n) * (( Im (seq *' )) . n))) by COMSEQ_3:def 5

          .= ((( Re (seq . n)) * ( Re ((seq *' ) . n))) - (( Im (seq . n)) * (( Im (seq *' )) . n))) by COMSEQ_3:def 6

          .= ((( Re (seq . n)) * ( Re ((seq *' ) . n))) - (( Im (seq . n)) * ( Im ((seq *' ) . n)))) by COMSEQ_3:def 6

          .= ((( Re (seq . n)) * ( Re ((seq . n) *' ))) - (( Im (seq . n)) * ( Im ((seq *' ) . n)))) by COMSEQ_2:def 2, A7

          .= ((( Re (seq . n)) * ( Re ((seq . n) *' ))) - (( Im (seq . n)) * ( Im ((seq . n) *' )))) by COMSEQ_2:def 2, A7

          .= ((( Re (seq . n)) * ( Re (seq . n))) - (( Im (seq . n)) * ( Im ((seq . n) *' )))) by COMPLEX1: 27

          .= ((( Re (seq . n)) * ( Re (seq . n))) - (( Im (seq . n)) * ( - ( Im (seq . n))))) by COMPLEX1: 27

          .= ((( Re (seq . n)) ^2 ) + (( Im (seq . n)) * ( Im (seq . n))));

          hence thesis;

        end;

        

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

        proof

          let n be Nat;

          

           A9: (( Im (seq . n)) ^2 ) >= 0 by XREAL_1: 63;

          (rseq . n) = ((( Re (seq . n)) ^2 ) + (( Im (seq . n)) ^2 )) & (( Re (seq . n)) ^2 ) >= 0 by A6, XREAL_1: 63;

          then (rseq . n) >= ( 0 + 0 ) by A9;

          hence thesis;

        end;

        

         A10: (( seq_id x) (#) (( seq_id x) *' )) is absolutely_summable by Lm19;

        assume (x .|. x) = 0 ;

        then (( Sum ( Re (( seq_id x) (#) (( seq_id x) *' )))) + (( Sum ( Im (( seq_id x) (#) (( seq_id x) *' )))) * <i> )) = 0 by A5, A10, COMSEQ_3: 53;

        then

         A11: ( Sum ( Re (( seq_id x) (#) (( seq_id x) *' )))) = 0 by COMPLEX1: 4, COMPLEX1: 12;

        

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

        proof

          let n be Nat;

          (rseq . n) = ((( Re (seq . n)) ^2 ) + (( Im (seq . n)) ^2 )) by A6;

          then ((( Re (seq . n)) ^2 ) + (( Im (seq . n)) ^2 )) = 0 by A10, A11, A8, RSSPACE: 17;

          hence thesis by COMPLEX1: 5;

        end;

        x is Element of the_set_of_ComplexSequences by CSSPACE:def 11;

        hence x = ( 0. Complex_l2_Space ) by A12, Lm10, CSSPACE: 5;

      end;

       A13:

      now

        assume

         A14: x = ( 0. Complex_l2_Space );

        

         A15: 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 VALUED_1: 5

          .= ( 0c * ((( seq_id x) *' ) . n)) by A14, Lm10, CSSPACE: 4

          .= 0 ;

        end;

        

        thus (x .|. x) = ( Sum (( seq_id x) (#) (( seq_id x) *' ))) by CSSPACE:def 17

        .= 0 by A15, CSSPACE: 80;

      end;

      set seqy = ( seq_id y);

      

       A16: for n be Nat holds 0 <= (( Re (seqx (#) (seqx *' ))) . n)

      proof

        let n be Nat;

        

         A17: n in NAT by ORDINAL1:def 12;

        

         A18: (( Re (seqx . n)) ^2 ) >= 0 & (( Im (seqx . n)) ^2 ) >= 0 by XREAL_1: 63;

        (( Re (seqx (#) (seqx *' ))) . n) = ( Re ((seqx (#) (seqx *' )) . n)) by COMSEQ_3:def 5

        .= ( Re ((seqx . n) * ((seqx *' ) . n))) by VALUED_1: 5

        .= ( Re ((seqx . n) * ((seqx . n) *' ))) by COMSEQ_2:def 2, A17

        .= ((( Re (seqx . n)) ^2 ) + (( Im (seqx . n)) ^2 )) by COMPLEX1: 40;

        then (( Re (seqx (#) (seqx *' ))) . n) >= ( 0 + 0 ) by A18;

        hence thesis;

      end;

      ( |.seqx.| (#) |.seqy.|) is summable by Lm16;

      then ( |.(seqx *' ).| (#) |.seqy.|) is summable by Lm18;

      then |.((seqx *' ) (#) seqy).| is summable by COMSEQ_1: 46;

      then

       A19: ((seqx *' ) (#) seqy) is absolutely_summable by COMSEQ_3:def 9;

      set seqz = ( seq_id z);

      

       A20: for n be Nat holds (( Im (seqx (#) (seqx *' ))) . n) = 0

      proof

        let n be Nat;

        

         A21: n in NAT by ORDINAL1:def 12;

        (( Im (seqx (#) (seqx *' ))) . n) = ( Im ((seqx (#) (seqx *' )) . n)) by COMSEQ_3:def 6

        .= ( Im ((seqx . n) * ((seqx *' ) . n))) by VALUED_1: 5

        .= ( Im ((seqx . n) * ((seqx . n) *' ))) by COMSEQ_2:def 2, A21;

        hence thesis by COMPLEX1: 40;

      end;

      ( |.seqx.| (#) |.seqz.|) is summable by Lm16;

      then ( |.seqx.| (#) |.(seqz *' ).|) is summable by Lm18;

      then |.(seqx (#) (seqz *' )).| is summable by COMSEQ_1: 46;

      then

       A22: (seqx (#) (seqz *' )) is absolutely_summable by COMSEQ_3:def 9;

      ( |.seqy.| (#) |.seqz.|) is summable by Lm16;

      then ( |.seqy.| (#) |.(seqz *' ).|) is summable by Lm18;

      then |.(seqy (#) (seqz *' )).| is summable by COMSEQ_1: 46;

      then

       A23: (seqy (#) (seqz *' )) is absolutely_summable by COMSEQ_3:def 9;

      

       A24: ((x + y) .|. z) = ( Sum (( seq_id (x + y)) (#) (seqz *' ))) by CSSPACE:def 17

      .= ( Sum (( seq_id (seqx + seqy)) (#) (seqz *' ))) by Lm12

      .= ( Sum ((seqx (#) (seqz *' )) + (seqy (#) (seqz *' )))) by COMSEQ_1: 10

      .= (( Sum (seqx (#) (seqz *' ))) + ( Sum (seqy (#) (seqz *' )))) by A22, A23, COMSEQ_3: 54

      .= ((the scalar of Complex_l2_Space . (x,z)) + ( Sum (seqy (#) (seqz *' )))) by CSSPACE:def 17

      .= ((x .|. z) + (y .|. z)) by CSSPACE:def 17;

      ( |.seqx.| (#) |.seqy.|) is summable by Lm16;

      then ( |.seqx.| (#) |.(seqy *' ).|) is summable by Lm18;

      then |.(seqx (#) (seqy *' )).| is summable by COMSEQ_1: 46;

      then

       A25: (seqx (#) (seqy *' )) is absolutely_summable by COMSEQ_3:def 9;

      

       A26: ((a * x) .|. y) = ( Sum (( seq_id (a * x)) (#) (seqy *' ))) by CSSPACE:def 17

      .= ( Sum (( seq_id (a (#) seqx)) (#) (seqy *' ))) by Lm13

      .= ( Sum (a (#) (seqx (#) (seqy *' )))) by COMSEQ_1: 12

      .= (a * ( Sum (seqx (#) (seqy *' )))) by A25, COMSEQ_3: 56

      .= (a * (x .|. y)) by CSSPACE:def 17;

      (x .|. y) = ( Sum (((seqx *' ) *' ) (#) (seqy *' ))) by CSSPACE:def 17

      .= ( Sum (((seqx *' ) (#) seqy) *' )) by COMSEQ_2: 5

      .= (( Sum ((seqx *' ) (#) seqy)) *' ) by A19, Lm5

      .= ((y .|. x) *' ) by CSSPACE:def 17;

      hence thesis by A4, A13, A2, A3, A16, A20, A24, A26, RSSPACE: 16, SERIES_1: 18;

    end;

    registration

      cluster Complex_l2_Space -> ComplexUnitarySpace-like;

      coherence by Th2, CSSPACE:def 13;

    end

    

     Lm20: for x,y be Complex holds (2 * |.(x * y).|) <= (( |.x.| ^2 ) + ( |.y.| ^2 ))

    proof

      let x,y be Complex;

      set a = |.x.|;

      set b = |.y.|;

      ((a - b) ^2 ) = (((a * a) - ((a * b) + (a * b))) + (b * b));

      then (a * b) = |.(x * y).| & (((a * a) + (b * b)) - ((a * b) + (a * b))) >= 0 by COMPLEX1: 65, XREAL_1: 63;

      hence thesis by XREAL_1: 49;

    end;

    

     Lm21: for x,y be Complex holds ( |.(x + y).| * |.(x + y).|) <= (((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|)) & ( |.x.| * |.x.|) <= (((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|))

    proof

       A1:

      now

        let x,y be Complex;

        

         A2: |.(x * x).| = ( |.x.| * |.x.|) & |.(y * y).| = ( |.y.| * |.y.|) by COMPLEX1: 65;

         |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| <= ( |.(((x * x) + (x * y)) + (x * y)).| + |.(y * y).|) by COMPLEX1: 56;

        then

         A3: ( |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| - |.(y * y).|) <= |.(((x * x) + (x * y)) + (x * y)).| by XREAL_1: 20;

         |.(((x * x) + (x * y)) + (x * y)).| <= ( |.((x * x) + (x * y)).| + |.(x * y).|) by COMPLEX1: 56;

        then |.((x * x) + (x * y)).| <= ( |.(x * x).| + |.(x * y).|) & ( |.(((x * x) + (x * y)) + (x * y)).| - |.(x * y).|) <= |.((x * x) + (x * y)).| by COMPLEX1: 56, XREAL_1: 20;

        then ( |.(((x * x) + (x * y)) + (x * y)).| - |.(x * y).|) <= ( |.(x * x).| + |.(x * y).|) by XXREAL_0: 2;

        then

         A4: |.(((x * x) + (x * y)) + (x * y)).| <= (( |.(x * x).| + |.(x * y).|) + |.(x * y).|) by XREAL_1: 20;

        ( |.(x + y).| * |.(x + y).|) = |.((x + y) * (x + y)).| by COMPLEX1: 65

        .= |.((((x * x) + (x * y)) + (x * y)) + (y * y)).|;

        then (( |.(x + y).| * |.(x + y).|) - |.(y * y).|) <= ( |.(x * x).| + (2 * |.(x * y).|)) by A3, A4, XXREAL_0: 2;

        then

         A5: ((( |.(x + y).| * |.(x + y).|) - |.(y * y).|) - |.(x * x).|) <= (2 * |.(x * y).|) by XREAL_1: 20;

        (2 * |.(x * y).|) <= (( |.x.| ^2 ) + ( |.y.| ^2 )) by Lm20;

        then ((( |.(x + y).| * |.(x + y).|) - |.(y * y).|) - |.(x * x).|) <= (( |.x.| ^2 ) + ( |.y.| ^2 )) by A5, XXREAL_0: 2;

        then (( |.(x + y).| * |.(x + y).|) - ( |.y.| * |.y.|)) <= ((( |.x.| * |.x.|) + ( |.y.| * |.y.|)) + ( |.x.| * |.x.|)) by A2, XREAL_1: 20;

        then ( |.(x + y).| * |.(x + y).|) <= (((2 * ( |.x.| * |.x.|)) + ( |.y.| * |.y.|)) + ( |.y.| * |.y.|)) by XREAL_1: 20;

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

      end;

      now

        let x,y be Complex;

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

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

      end;

      hence thesis by A1;

    end;

    

     Lm22: for c be Complex, seq be Complex_Sequence st seq is convergent holds for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = ( |.((seq . m) - c).| * |.((seq . m) - c).|)) holds rseq is convergent & ( lim rseq) = ( |.(( lim seq) - c).| * |.(( lim seq) - c).|)

    proof

      let c be Complex;

      reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider cseq = ( NAT --> c1) as Complex_Sequence;

      

       A1: for n be Nat holds (cseq . n) = c by ORDINAL1:def 12, FUNCOP_1: 7;

      then

       A2: cseq is convergent by COMSEQ_2: 9;

      let seq be Complex_Sequence such that

       A3: seq is convergent;

      reconsider seq1 = (seq - cseq) as convergent Complex_Sequence by A3, A2;

       |.seq1.| is convergent;

      

      then

       A4: ( lim ( |.(seq - cseq).| (#) |.(seq - cseq).|)) = (( lim |.(seq - cseq).|) * ( lim |.(seq - cseq).|)) by SEQ_2: 15

      .= ( |.(( lim seq) - ( lim cseq)).| * ( lim |.(seq - cseq).|)) by A3, A2, SEQ_2: 31

      .= ( |.(( lim seq) - ( lim cseq)).| * |.(( lim seq) - ( lim cseq)).|) by A3, A2, SEQ_2: 31

      .= ( |.(( lim seq) - c).| * |.(( lim seq) - ( lim cseq)).|) by A1, COMSEQ_2: 10

      .= ( |.(( lim seq) - c).| * |.(( lim seq) - c).|) by A1, COMSEQ_2: 10;

      let rseq be Real_Sequence such that

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

      now

        let i be Nat;

        

         A6: i in NAT by ORDINAL1:def 12;

        

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

        .= ( |.((seq . i) - (cseq . i)).| * |.((seq . i) - c).|) by FUNCOP_1: 7, A6

        .= ( |.((seq . i) - (cseq . i)).| * |.((seq . i) - (cseq . i)).|) by FUNCOP_1: 7, A6

        .= ( |.((seq . i) + (( - cseq) . i)).| * |.((seq . i) + ( - (cseq . i))).|) by VALUED_1: 8

        .= ( |.((seq . i) + (( - cseq) . i)).| * |.((seq . i) + (( - cseq) . i)).|) by VALUED_1: 8

        .= ( |.((seq + ( - cseq)) . i).| * |.((seq . i) + (( - cseq) . i)).|) by VALUED_1: 1, A6

        .= ( |.((seq - cseq) . i).| * |.((seq + ( - cseq)) . i).|) by VALUED_1: 1, A6

        .= (( |.(seq - cseq).| . i) * |.((seq - cseq) . i).|) by VALUED_1: 18

        .= (( |.(seq - cseq).| . i) * ( |.(seq - cseq).| . i)) by VALUED_1: 18

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

      end;

      then

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

      ( |.seq1.| (#) |.seq1.|) is convergent;

      hence thesis by A7, A4, FUNCT_2: 12;

    end;

    

     Lm23: for c be Complex, seq1 be Real_Sequence, seq be Complex_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 Complex;

      let seq1 be Real_Sequence;

      let seq be Complex_Sequence;

      assume that

       A1: seq is convergent and

       A2: seq1 is convergent;

      reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider cseq = ( NAT --> c1) as Complex_Sequence;

      

       A3: for n be Nat holds (cseq . n) = c by ORDINAL1:def 12, FUNCOP_1: 7;

      then

       A4: cseq is convergent by COMSEQ_2: 9;

      then

      reconsider s = (seq - cseq) as convergent Complex_Sequence by A1;

      

       A5: |.s.| is convergent;

      then

       A6: ( |.(seq - cseq).| (#) |.(seq - cseq).|) is convergent;

      let rseq be Real_Sequence such that

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

        .= (( |.((seq . i) - (cseq . i)).| * |.((seq . i) - c).|) + (seq1 . i)) by FUNCOP_1: 7

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

        .= (( |.((seq . i) + (( - cseq) . i)).| * |.((seq . i) + ( - (cseq . i))).|) + (seq1 . i)) by VALUED_1: 8

        .= (( |.((seq . i) + (( - cseq) . i)).| * |.((seq . i) + (( - cseq) . i)).|) + (seq1 . i)) by VALUED_1: 8

        .= (( |.((seq + ( - cseq)) . i).| * |.((seq . i) + (( - cseq) . i)).|) + (seq1 . i)) by VALUED_1: 1

        .= (( |.((seq - cseq) . i).| * |.((seq + ( - cseq)) . i).|) + (seq1 . i)) by VALUED_1: 1

        .= ((( |.(seq - cseq).| . i) * |.((seq - cseq) . i).|) + (seq1 . i)) by VALUED_1: 18

        .= ((( |.(seq - cseq).| . i) * ( |.(seq - cseq).| . i)) + (seq1 . i)) by VALUED_1: 18

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

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

      end;

      then

       A8: rseq = (( |.(seq - cseq).| (#) |.(seq - cseq).|) + seq1) by FUNCT_2: 63;

      ( lim ( |.(seq - cseq).| (#) |.(seq - cseq).|)) = (( lim |.(seq - cseq).|) * ( lim |.(seq - cseq).|)) by A5, SEQ_2: 15

      .= ( |.(( lim seq) - ( lim cseq)).| * ( lim |.(seq - cseq).|)) by A1, A4, SEQ_2: 31

      .= ( |.(( lim seq) - ( lim cseq)).| * |.(( lim seq) - ( lim cseq)).|) by A1, A4, SEQ_2: 31

      .= ( |.(( lim seq) - c).| * |.(( lim seq) - ( lim cseq)).|) by A3, COMSEQ_2: 10

      .= ( |.(( lim seq) - c).| * |.(( lim seq) - c).|) by A3, COMSEQ_2: 10;

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

    end;

    registration

      cluster Complex_l2_Space -> complete;

      coherence

      proof

        let vseq be sequence of Complex_l2_Space such that

         A1: vseq is Cauchy;

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

        

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

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Nat;

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

          consider seqi be Complex_Sequence such that

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

          take ( lim seqi);

          thus ( lim seqi) in COMPLEX by XCMPLX_0:def 2;

          now

            let e be Real such that

             A4: e > 0 ;

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

            proof

              set e1 = e;

              consider k be Nat such that

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

              

               A6: i in NAT by ORDINAL1:def 12;

              now

                set vk = (vseq . k);

                let m be Nat such that

                 A7: k <= m;

                set vm = (vseq . m);

                 ||.(vm - vk).|| < e by A5, A7;

                then

                 A8: ( sqrt |.((vm - vk) .|. (vm - vk)).|) < e;

                set seqmk = ( seq_id (vm - vk));

                

                 A9: ( sqrt ( |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|)) = ( sqrt ( |.((seqi . m) - (seqi . k)).| ^2 ))

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

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

                .= (( seq_id (vseq . m)) + ( - ( seq_id (vseq . k))));

                

                then (seqmk . i) = ((( seq_id (vseq . m)) . i) + (( - ( seq_id (vseq . k))) . i)) by VALUED_1: 1, A6

                .= ((( seq_id (vseq . m)) . i) + ( - (( seq_id (vseq . k)) . i))) by VALUED_1: 8

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

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

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

                

                then ( |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|) = (( |.seqmk.| . i) * |.(seqmk . i).|) by VALUED_1: 18

                .= (( |.seqmk.| . i) * ( |.seqmk.| . i)) by VALUED_1: 18;

                then (( |.seqmk.| . i) * ( |.(seqmk *' ).| . i)) = ( |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|) by Lm18;

                then

                 A10: ( |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|) = (( |.seqmk.| (#) |.(seqmk *' ).|) . i) by SEQ_1: 8;

                 0 <= |.((seqi . m) - (seqi . k)).| by COMPLEX1: 46;

                then

                 A11: 0 <= ( |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|);

                (seqmk (#) (seqmk *' )) is absolutely_summable & for j be Nat holds (( Re (seqmk (#) (seqmk *' ))) . j) >= 0 & (( Im (seqmk (#) (seqmk *' ))) . j) = 0 by Lm8, Lm19;

                

                then |.( Sum (seqmk (#) (seqmk *' ))).| = ( Sum |.(seqmk (#) (seqmk *' )).|) by Lm7

                .= ( Sum ( |.seqmk.| (#) |.(seqmk *' ).|)) by COMSEQ_1: 46;

                then

                 A12: ( sqrt ( Sum ( |.seqmk.| (#) |.(seqmk *' ).|))) < e by A8, CSSPACE:def 17;

                

                 A13: for i be Nat holds 0 <= (( |.seqmk.| (#) |.(seqmk *' ).|) . i)

                proof

                  let i be Nat;

                  (( |.seqmk.| (#) |.(seqmk *' ).|) . i) = (( |.seqmk.| . i) * ( |.(seqmk *' ).| . i)) by SEQ_1: 8

                  .= (( |.seqmk.| . i) * ( |.seqmk.| . i)) by Lm18;

                  hence thesis by XREAL_1: 63;

                end;

                ( |.seqmk.| (#) |.seqmk.|) is summable by CSSPACE:def 11;

                then

                 A14: ( |.seqmk.| (#) |.(seqmk *' ).|) is summable by Lm18;

                then

                 A15: 0 <= ( Sum ( |.seqmk.| (#) |.(seqmk *' ).|)) by A13, SERIES_1: 18;

                then 0 <= ( sqrt ( Sum ( |.seqmk.| (#) |.(seqmk *' ).|))) by SQUARE_1:def 2;

                then (( sqrt ( Sum ( |.seqmk.| (#) |.(seqmk *' ).|))) ^2 ) < (e1 ^2 ) by A12, SQUARE_1: 16;

                then

                 A16: ( Sum ( |.seqmk.| (#) |.(seqmk *' ).|)) < (e * e) by A15, SQUARE_1:def 2;

                (( |.seqmk.| (#) |.(seqmk *' ).|) . i) <= ( Sum ( |.seqmk.| (#) |.(seqmk *' ).|)) by A14, A13, RSSPACE2: 3;

                then

                 A17: ( |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|) < (e * e) by A16, A10, XXREAL_0: 2;

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

                .= e by A4, SQUARE_1: 22;

                hence |.((seqi . m) - (seqi . k)).| < e by A11, A17, A9, SQUARE_1: 27;

              end;

              hence thesis;

            end;

          end;

          then seqi is convergent by COMSEQ_3: 46;

          hence thesis by A3;

        end;

        consider f be sequence of COMPLEX such that

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

        reconsider tseq = f as Complex_Sequence;

        set seqt = ( seq_id tseq);

         A19:

        now

          let i be Nat;

          reconsider x = i as set;

          i in NAT by ORDINAL1:def 12;

          then ex i0 be Nat st x = i0 & ex seqi be Complex_Sequence st (for n be Nat holds (seqi . n) = (( seq_id (vseq . n)) . i0)) & seqi is convergent & (f . x) = ( lim seqi) by A18;

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

        end;

        

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

        proof

          let e1 be Real such that

           A21: e1 > 0 ;

          set e = (e1 / 2);

          

           A22: e > 0 by A21;

          then

          consider k be Nat such that

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

          e < e1 by A21, XREAL_1: 216;

          then

           A24: (e * e) < (e1 * e1) by A22, XREAL_1: 97;

          

           A25: 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 A23;

            then

             A26: ( sqrt |.(((vseq . n) - (vseq . m)) .|. ((vseq . n) - (vseq . m))).|) < e;

            (( seq_id ((vseq . n) - (vseq . m))) (#) (( seq_id ((vseq . n) - (vseq . m))) *' )) is absolutely_summable & for j be Nat holds (( Re (( seq_id ((vseq . n) - (vseq . m))) (#) (( seq_id ((vseq . n) - (vseq . m))) *' ))) . j) >= 0 & (( Im (( seq_id ((vseq . n) - (vseq . m))) (#) (( seq_id ((vseq . n) - (vseq . m))) *' ))) . j) = 0 by Lm8, Lm19;

            

            then |.( Sum (( seq_id ((vseq . n) - (vseq . m))) (#) (( seq_id ((vseq . n) - (vseq . m))) *' ))).| = ( Sum |.(( seq_id ((vseq . n) - (vseq . m))) (#) (( seq_id ((vseq . n) - (vseq . m))) *' )).|) by Lm7

            .= ( Sum ( |.( seq_id ((vseq . n) - (vseq . m))).| (#) |.(( seq_id ((vseq . n) - (vseq . m))) *' ).|)) by COMSEQ_1: 46

            .= ( Sum ( |.( seq_id ((vseq . n) - (vseq . m))).| (#) |.( seq_id ((vseq . n) - (vseq . m))).|)) by Lm18

            .= ( Sum |.(( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))).|) by COMSEQ_1: 46;

            then

             A27: ( sqrt ( Sum |.(( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))).|)) < e by A26, CSSPACE:def 17;

            

             A28: 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))) (#) ( seq_id ((vseq . n) - (vseq . m)))).| . i) by COMSEQ_1: 46

              .= |.((( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))) . i).| by VALUED_1: 18;

              hence thesis by COMPLEX1: 46;

            end;

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

            then 0 <= ( Sum ( |.( seq_id ((vseq . n) - (vseq . m))).| (#) |.( seq_id ((vseq . n) - (vseq . m))).|)) by A28, SERIES_1: 18;

            then

             A29: 0 <= ( Sum |.(( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))).|) by COMSEQ_1: 46;

            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 A27, SQUARE_1: 16;

            then ( Sum |.(( seq_id ((vseq . n) - (vseq . m))) (#) ( seq_id ((vseq . n) - (vseq . m)))).|) < (e * e) by A29, SQUARE_1:def 2;

            hence thesis by A28, COMSEQ_1: 46, CSSPACE:def 11;

          end;

          

           A30: 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 ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( 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 ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|)) . $1));

            

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

            now

              let i be Nat such that

               A32: 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 ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( 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 ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( 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

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

                consider seq0 be Complex_Sequence such that

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

                 A35: seq0 is convergent and

                 A36: (tseq . (i + 1)) = ( lim seq0) by A19;

                let rseq be Real_Sequence such that

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

                 A38:

                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 A37

                  .= ((( |.( 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 A31

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

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

                  .= ((( |.(( 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 VALUED_1: 18

                  .= (( |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . (i + 1)).| * |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . (i + 1)).|) + (rseqb . m)) by VALUED_1: 18

                  .= (( |.((( 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 VALUED_1: 1

                  .= (( |.((( 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 VALUED_1: 1

                  .= (( |.((( 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 VALUED_1: 8

                  .= (( |.((( 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 VALUED_1: 8

                  .= (( |.((seq0 . m) - (( seq_id (vseq . n)) . (i + 1))).| * |.((( seq_id (vseq . m)) . (i + 1)) - (( seq_id (vseq . n)) . (i + 1))).|) + (rseqb . m)) by A34

                  .= (( |.((seq0 . m) - (( seq_id (vseq . n)) . (i + 1))).| * |.((seq0 . m) - (( seq_id (vseq . n)) . (i + 1))).|) + (rseqb . m)) by A34;

                end;

                

                 A39: rseqb is convergent by A32, A33;

                

                then ( lim rseq) = (( |.(( lim seq0) - (( seq_id (vseq . n)) . (i + 1))).| * |.(( lim seq0) - (( seq_id (vseq . n)) . (i + 1))).|) + ( lim rseqb)) by A35, A38, Lm23

                .= (( |.((tseq . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))).| * |.((tseq . (i + 1)) + ( - (( seq_id (vseq . n)) . (i + 1)))).|) + ( lim rseqb)) by A36, VALUED_1: 8

                .= (( |.((tseq . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))).| * |.((tseq . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))).|) + ( lim rseqb)) by VALUED_1: 8

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

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

                .= ((( |.(tseq + ( - ( seq_id (vseq . n)))).| . (i + 1)) * |.((tseq + ( - ( seq_id (vseq . n)))) . (i + 1)).|) + ( lim rseqb)) by VALUED_1: 18

                .= ((( |.(tseq - ( seq_id (vseq . n))).| . (i + 1)) * ( |.(tseq + ( - ( seq_id (vseq . n)))).| . (i + 1))) + ( lim rseqb)) by VALUED_1: 18

                .= ((( |.(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 ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|)) . i)) by A32, A33

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

                hence thesis by A39, A35, A38, Lm23;

              end;

            end;

            then

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

            now

              let rseq be Real_Sequence such that

               A41: 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 ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|)) . 0 )

              proof

                consider rseq0 be Complex_Sequence such that

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

                 A43: rseq0 is convergent and

                 A44: (tseq . 0 ) = ( lim rseq0) by A19;

                 A45:

                now

                  let m be Nat;

                  

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

                  .= (( |.( 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 A31

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

                  .= (( |.(( 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 VALUED_1: 18

                  .= ( |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . 0 ).| * |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . 0 ).|) by VALUED_1: 18

                  .= ( |.((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).| * |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . 0 ).|) by VALUED_1: 1

                  .= ( |.((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).| * |.((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).|) by VALUED_1: 1

                  .= ( |.((( seq_id (vseq . m)) . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))).| * |.((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).|) by VALUED_1: 8

                  .= ( |.((( seq_id (vseq . m)) . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))).| * |.((( seq_id (vseq . m)) . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))).|) by VALUED_1: 8

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

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

                end;

                

                then ( lim rseq) = ( |.((tseq . 0 ) - (( seq_id (vseq . n)) . 0 )).| * |.((tseq . 0 ) - (( seq_id (vseq . n)) . 0 )).|) by A43, A44, Lm22

                .= ( |.((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).| * |.((tseq . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))).|) by VALUED_1: 8

                .= ( |.((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).| * |.((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).|) by VALUED_1: 8

                .= ( |.((tseq + ( - ( seq_id (vseq . n)))) . 0 ).| * |.((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).|) by VALUED_1: 1

                .= ( |.((tseq - ( seq_id (vseq . n))) . 0 ).| * |.((tseq + ( - ( seq_id (vseq . n)))) . 0 ).|) by VALUED_1: 1

                .= (( |.(tseq - ( seq_id (vseq . n))).| . 0 ) * |.((tseq - ( seq_id (vseq . n))) . 0 ).|) by VALUED_1: 18

                .= (( |.(tseq - ( seq_id (vseq . n))).| . 0 ) * ( |.(tseq - ( seq_id (vseq . n))).| . 0 )) by VALUED_1: 18

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

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

                hence thesis by A43, A45, Lm22;

              end;

            end;

            then

             A46: P[ 0 ];

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

            hence thesis;

          end;

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

          proof

            let n be Nat such that

             A47: n >= k;

            

             A48: for i be Nat st 0 <= i holds (( Partial_Sums ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( 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

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

              

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

              proof

                let m be Nat such that

                 A51: 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 A25, A47, A51;

                then

                 A52: (( 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 RSSPACE2: 3;

                

                 A53: (rseq . m) = (( Partial_Sums ( |.( seq_id ((vseq . m) - (vseq . n))).| (#) |.( seq_id ((vseq . m) - (vseq . n))).|)) . i) by A49;

                ( Sum ( |.( seq_id ((vseq . m) - (vseq . n))).| (#) |.( seq_id ((vseq . m) - (vseq . n))).|)) < (e * e) by A25, A47, A51;

                hence thesis by A53, A52, XXREAL_0: 2;

              end;

              rseq is convergent & ( lim rseq) = (( Partial_Sums ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|)) . i) by A30, A49;

              hence thesis by A50, RSSPACE2: 5;

            end;

            now

              let i be Nat;

              (( Partial_Sums ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|)) . i) <= (e * e) by A48;

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

            end;

            then

             A54: ( Partial_Sums ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|)) is bounded_above by SEQ_2:def 3;

            

             A55: for i be Nat holds 0 <= (( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|) . i)

            proof

              let i be Nat;

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

              hence thesis by XREAL_1: 63;

            end;

            then

             A56: ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|) is summable by A54, SERIES_1: 17;

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

            then ( Sum ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|)) = ( lim ( Partial_Sums ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|))) & ( lim ( Partial_Sums ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|))) <= (e * e) by A48, RSSPACE2: 5, SERIES_1:def 3;

            then

             A57: ( Sum ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|)) < (e1 * e1) by A24, XXREAL_0: 2;

            ( |.(seqt - ( seq_id (vseq . n))).| (#) |.((seqt - ( seq_id (vseq . n))) *' ).|) is summable by A56, Lm18;

            then |.((seqt - ( seq_id (vseq . n))) (#) ((seqt - ( seq_id (vseq . n))) *' )).| is summable by COMSEQ_1: 46;

            then ((seqt - ( seq_id (vseq . n))) (#) ((seqt - ( seq_id (vseq . n))) *' )) is absolutely_summable by COMSEQ_3:def 9;

            then

             A58: |.( Sum ((seqt - ( seq_id (vseq . n))) (#) ((seqt - ( seq_id (vseq . n))) *' ))).| <= ( Sum |.((seqt - ( seq_id (vseq . n))) (#) ((seqt - ( seq_id (vseq . n))) *' )).|) by Lm6;

             |.(seqt - ( seq_id (vseq . n))).| = |.((seqt - ( seq_id (vseq . n))) *' ).| by Lm18;

            then ( Sum |.((seqt - ( seq_id (vseq . n))) (#) ((seqt - ( seq_id (vseq . n))) *' )).|) < (e1 * e1) by A57, COMSEQ_1: 46;

            hence thesis by A55, A54, A58, SERIES_1: 17, XXREAL_0: 2;

          end;

          hence thesis;

        end;

        

         A59: ( |.( seq_id tseq).| (#) |.( seq_id tseq).|) is summable

        proof

          set d = ( |.seqt.| (#) |.seqt.|);

          

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

           A61: for n be Nat st n >= m holds ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|) is summable & |.( Sum ((( seq_id tseq) - ( seq_id (vseq . n))) (#) ((( seq_id tseq) - ( seq_id (vseq . n))) *' ))).| < (1 * 1) by A20;

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

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

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

          then

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

          

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

          proof

            let i be Nat;

            

             A64: i in NAT by ORDINAL1:def 12;

            

             A65: (((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;

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

            set x = (seqt . i);

            

             A66: (2 * (b . i)) = (2 * (( |.( seq_id (vseq . m)).| . i) * ( |.( seq_id (vseq . m)).| . i))) by SEQ_1: 8

            .= (2 * ( |.y.| * ( |.( seq_id (vseq . m)).| . i))) by VALUED_1: 18

            .= (2 * ( |.y.| * |.y.|)) by VALUED_1: 18

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

            ( |.(seqt - ( seq_id (vseq . m))).| . i) = |.((seqt + ( - ( seq_id (vseq . m)))) . i).| by VALUED_1: 18

            .= |.((seqt . i) + (( - ( seq_id (vseq . m))) . i)).| by VALUED_1: 1, A64

            .= |.((seqt . i) + ( - (( seq_id (vseq . m)) . i))).| by VALUED_1: 8

            .= |.((seqt . i) - (( seq_id (vseq . m)) . i)).|;

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

            then

             A67: (2 * (a . i)) = ((2 * |.(x - y).|) * |.(x - y).|);

            (d . i) = (( |.seqt.| . i) * ( |.seqt.| . i)) by SEQ_1: 8

            .= ( |.(seqt . i).| * ( |.seqt.| . i)) by VALUED_1: 18

            .= ( |.(seqt . i).| * |.(seqt . i).|) by VALUED_1: 18;

            hence thesis by A65, A67, A66, Lm21;

          end;

          ( |.(seqt - ( seq_id (vseq . m))).| (#) |.(seqt - ( seq_id (vseq . m))).|) is summable by A61;

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

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

          hence thesis by A60, A63, SERIES_1: 20;

        end;

        tseq in the_set_of_ComplexSequences by FUNCT_2: 8;

        then

        reconsider tv = tseq as Point of Complex_l2_Space by A59, CSSPACE: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

           A68: e > 0 ;

          consider m be Nat such that

           A69: for n be Nat st n >= m holds ( |.(seqt - ( seq_id (vseq . n))).| (#) |.(seqt - ( seq_id (vseq . n))).|) is summable & |.( Sum ((seqt - ( seq_id (vseq . n))) (#) ((seqt - ( seq_id (vseq . n))) *' ))).| < (e * e) by A20, A68;

          now

            tseq in the_set_of_ComplexSequences by FUNCT_2: 8;

            then

            reconsider u = tseq as VECTOR of Complex_l2_Space by A59, CSSPACE:def 11;

            let n be Nat such that

             A70: n >= m;

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

            set seqvn = ( seq_id (vseq . n));

             0 <= ( Re ((u - v) .|. (u - v))) by CSSPACE:def 13;

            then

             A71: 0 <= |.((u - v) .|. (u - v)).| by CSSPACE: 34;

            

             A72: ( seq_id (u - v)) = (seqt - seqvn) by Lm15;

             |.( Sum ((seqt - seqvn) (#) ((seqt - seqvn) *' ))).| < (e * e) by A69, A70;

            then |.((u - v) .|. (u - v)).| < (e * e) by A72, CSSPACE:def 17;

            then

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

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

            .= ||.(tv - (vseq . n)).|| by CSSPACE: 47

            .= ( sqrt |.((u - v) .|. (u - v)).|);

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

          end;

          hence thesis;

        end;

        hence thesis by CLVECT_2: 9;

      end;

    end

    registration

      cluster complete for ComplexUnitarySpace;

      existence

      proof

        take Complex_l2_Space ;

        thus thesis;

      end;

    end

    definition

      mode ComplexHilbertSpace is complete ComplexUnitarySpace;

    end

    begin

    theorem :: CSSPACE2:3

    for z1,z2 be Complex st (( Re z1) * ( Im z2)) = (( Re z2) * ( Im z1)) & ((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) >= 0 holds |.(z1 + z2).| = ( |.z1.| + |.z2.|) by Lm3;

    theorem :: CSSPACE2:4

    for x,y be Complex holds (2 * |.(x * y).|) <= (( |.x.| ^2 ) + ( |.y.| ^2 )) by Lm20;

    theorem :: CSSPACE2:5

    for x,y be Complex holds ( |.(x + y).| * |.(x + y).|) <= (((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|)) & ( |.x.| * |.x.|) <= (((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|)) by Lm21;

    ::$Canceled

    theorem :: CSSPACE2:7

    for seq be Complex_Sequence holds ( Partial_Sums (seq *' )) = (( Partial_Sums seq) *' ) by Lm1;

    theorem :: CSSPACE2:8

    for seq be Complex_Sequence, n be Nat st (for i be Nat holds (( Re seq) . i) >= 0 & (( Im seq) . i) = 0 ) holds ( |.( Partial_Sums seq).| . n) = (( Partial_Sums |.seq.|) . n) by Lm4;

    theorem :: CSSPACE2:9

    for seq be Complex_Sequence st seq is summable holds ( Sum (seq *' )) = (( Sum seq) *' ) by Lm5;

    theorem :: CSSPACE2:10

    for seq be Complex_Sequence st seq is absolutely_summable holds |.( Sum seq).| <= ( Sum |.seq.|) by Lm6;

    theorem :: CSSPACE2:11

    for seq be Complex_Sequence st seq is summable & (for n be Nat holds (( Re seq) . n) >= 0 & (( Im seq) . n) = 0 ) holds |.( Sum seq).| = ( Sum |.seq.|) by Lm7;

    theorem :: CSSPACE2:12

    for seq be Complex_Sequence, n be Nat holds (( Re (seq (#) (seq *' ))) . n) >= 0 & (( Im (seq (#) (seq *' ))) . n) = 0 by Lm8;

    theorem :: CSSPACE2:13

    for seq be Complex_Sequence st seq is absolutely_summable & ( Sum |.seq.|) = 0 holds for n be Nat holds (seq . n) = 0c

    proof

      let seq be Complex_Sequence such that

       A1: seq is absolutely_summable and

       A2: ( Sum |.seq.|) = 0 ;

      

       A3: for n be Nat holds (( Partial_Sums |.seq.|) . n) <= ( Sum |.seq.|)

      proof

        let n be Nat;

        (( Partial_Sums |.seq.|) . n) <= ( lim ( Partial_Sums |.seq.|)) by A1, SEQ_4: 37;

        hence thesis by SERIES_1:def 3;

      end;

       A4:

      now

        assume ex n be Nat st ( |.seq.| . n) <> 0 ;

        then

        consider n1 be Nat such that

         A5: ( |.seq.| . n1) <> 0 ;

        

         A6: for n be Nat holds 0 <= (( Partial_Sums |.seq.|) . n)

        proof

          let n be Nat;

          ( |.seq.| . 0 ) = |.(seq . 0 ).| by VALUED_1: 18;

          then

           A7: 0 <= ( |.seq.| . 0 ) by COMPLEX1: 46;

          n = (n + 0 ) & (( Partial_Sums |.seq.|) . 0 ) = ( |.seq.| . 0 ) by SERIES_1:def 1;

          hence thesis by A7, SEQM_3: 5;

        end;

        (( Partial_Sums |.seq.|) . n1) > 0

        proof

          now

            per cases ;

              case n1 = 0 ;

              then (( Partial_Sums |.seq.|) . n1) <> 0 by A5, SERIES_1:def 1;

              hence thesis by A6;

            end;

              case

               A8: n1 <> 0 ;

              set nn = (n1 - 1);

              ( |.seq.| . n1) = |.(seq . n1).| by VALUED_1: 18;

              then

               A9: (nn + 1) = n1 & 0 <= ( |.seq.| . n1) by COMPLEX1: 46;

              ( 0 + 1) <= n1 by A8, INT_1: 7;

              then

               A10: nn in NAT by INT_1: 5;

              then 0 <= (( Partial_Sums |.seq.|) . nn) by A6;

              then (( |.seq.| . n1) + 0 ) <= (( |.seq.| . n1) + (( Partial_Sums |.seq.|) . nn)) by XREAL_1: 7;

              hence thesis by A5, A10, A9, SERIES_1:def 1;

            end;

          end;

          hence thesis;

        end;

        hence contradiction by A2, A3;

      end;

      for n be Nat holds (seq . n) = 0c

      proof

        let n be Nat;

         0 = ( |.seq.| . n) by A4

        .= |.(seq . n).| by VALUED_1: 18;

        hence thesis by COMPLEX1: 45;

      end;

      hence thesis;

    end;

    theorem :: CSSPACE2:14

    for seq be Complex_Sequence holds |.seq.| = |.(seq *' ).| by Lm18;

    theorem :: CSSPACE2:15

    for c be Complex, seq be Complex_Sequence st seq is convergent holds for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = ( |.((seq . m) - c).| * |.((seq . m) - c).|)) holds rseq is convergent & ( lim rseq) = ( |.(( lim seq) - c).| * |.(( lim seq) - c).|) by Lm22;

    theorem :: CSSPACE2:16

    for c be Complex, seq1 be Real_Sequence, seq be Complex_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)) by Lm23;