csspace.miz

    begin

    definition

      :: CSSPACE:def1

      func the_set_of_ComplexSequences -> non empty set equals ( Funcs ( NAT , COMPLEX ));

      coherence ;

    end

    definition

      let z be object;

      :: CSSPACE:def2

      func seq_id (z) -> Complex_Sequence equals

      : Def2: z;

      coherence by A1, FUNCT_2: 66;

    end

    registration

      let z be Element of the_set_of_ComplexSequences ;

      reduce ( seq_id z) to z;

      reducibility by Def2;

    end

    definition

      let z be object;

      :: CSSPACE:def3

      func C_id (z) -> Complex equals

      : Def3: z;

      coherence by A1;

    end

    registration

      let z be Complex;

      reduce ( C_id z) to z;

      reducibility by Def3;

    end

    definition

      ::$Canceled

      :: CSSPACE:def6

      func CZeroseq -> Element of the_set_of_ComplexSequences equals ( NAT --> 0c );

      coherence by FUNCT_2: 8;

    end

    registration

      let x be Complex_Sequence;

      reduce ( seq_id x) to x;

      reducibility

      proof

        x in the_set_of_ComplexSequences by FUNCT_2: 8;

        hence thesis by Def2;

      end;

    end

    theorem :: CSSPACE:1

    for x be Complex_Sequence holds ( seq_id x) = x;

    definition

      :: CSSPACE:def7

      func Linear_Space_of_ComplexSequences -> strict non empty CLSStruct equals ( ComplexVectSpace NAT );

      coherence ;

    end

    registration

      cluster Linear_Space_of_ComplexSequences -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence ;

    end

    registration

      let z be VECTOR of Linear_Space_of_ComplexSequences ;

      reduce ( seq_id z) to z;

      reducibility by Def2;

    end

    theorem :: CSSPACE:2



     Th2: for v,w be VECTOR of Linear_Space_of_ComplexSequences holds (v + w) = (( seq_id v) + ( seq_id w))

    proof

      let v,w be VECTOR of Linear_Space_of_ComplexSequences ;

      reconsider v1 = v, w1 = w as Element of ( Funcs ( NAT , COMPLEX ));

      reconsider f = (( ComplexFuncAdd NAT ) . (v1,w1)) as Function of NAT , COMPLEX by FUNCT_2: 66;

      f = (( seq_id v) + ( seq_id w))

      proof

        let n be Element of NAT ;



        thus (f . n) = ((v1 . n) + (w1 . n)) by CFUNCDOM: 1

        .= ((( seq_id v) + ( seq_id w)) . n) by VALUED_1: 1;

      end;

      hence thesis;

    end;

    theorem :: CSSPACE:3



     Th3: for z be Complex, v be VECTOR of Linear_Space_of_ComplexSequences holds (z * v) = (z (#) ( seq_id v))

    proof

      let z be Complex;

      let v be VECTOR of Linear_Space_of_ComplexSequences ;

      reconsider r1 = z as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider v1 = v as Element of ( Funcs ( NAT , COMPLEX ));

      reconsider h = (( ComplexFuncExtMult NAT ) . (r1,v1)) as Complex_Sequence by FUNCT_2: 66;

      h = (z (#) ( seq_id v))

      proof

        let n be Element of NAT ;



        thus (h . n) = (z * (v1 . n)) by CFUNCDOM: 4

        .= ((z (#) ( seq_id v)) . n) by VALUED_1: 6;

      end;

      hence thesis;

    end;

    theorem :: CSSPACE:4



     Th4: for n be object holds (( seq_id CZeroseq ) . n) = 0

    proof

      set f = ( seq_id CZeroseq );

      let n be object;

      per cases ;

        suppose

         A1: n in ( dom f);

        ( dom f) = NAT by FUNCT_2:def 1;

        hence thesis by A1, FUNCOP_1: 7;

      end;

        suppose not n in ( dom f);

        hence thesis by FUNCT_1:def 2;

      end;

    end;

    theorem :: CSSPACE:5

    for f be Element of the_set_of_ComplexSequences st for n be Nat holds (( seq_id f) . n) = 0 holds f = CZeroseq

    proof

      let f be Element of the_set_of_ComplexSequences ;

      set g = ( seq_id f);

      assume

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



       A2: ( dom g) = NAT by FUNCT_2:def 1;

      for z be object st z in ( dom g) holds (g . z) = 0 by A1;

      hence f = CZeroseq by A2, FUNCOP_1: 11;

    end;

    ::$Canceled

    definition

      let X be ComplexLinearSpace;

      let X1 be Subset of X;

      :: CSSPACE:def8

      func Add_ (X1,X) -> BinOp of X1 equals

      : Def6: (the addF of X || X1);

      correctness

      proof



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



         A3: for z be object st z in [:X1, X1:] holds ((the addF of X || X1) . z) in X1

        proof

          let z be object such that

           A4: z in [:X1, X1:];

          consider r,x be object such that

           A5: r in X1 and

           A6: x in X1 and

           A7: z = [r, x] by A4, ZFMISC_1:def 2;

          reconsider y = x, r1 = r as VECTOR of X by A5, A6;

           [r, x] in ( dom (the addF of X || X1)) by A2, A4, A7, RELAT_1: 62, ZFMISC_1: 96;

          then ((the addF of X || X1) . z) = (r1 + y) by A7, FUNCT_1: 47;

          hence thesis by A1, A5, A6;

        end;

        ( dom (the addF of X || X1)) = [:X1, X1:] by A2, RELAT_1: 62, ZFMISC_1: 96;

        hence thesis by A3, FUNCT_2: 3;

      end;

    end

    definition

      let X be ComplexLinearSpace;

      let X1 be Subset of X;

      :: CSSPACE:def9

      func Mult_ (X1,X) -> Function of [: COMPLEX , X1:], X1 equals

      : Def7: (the Mult of X | [: COMPLEX , X1:]);

      correctness

      proof



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



         A3: [: COMPLEX , X1:] c= [: COMPLEX , the carrier of X:] by ZFMISC_1: 95;



         A4: for z be object st z in [: COMPLEX , X1:] holds ((the Mult of X | [: COMPLEX , X1:]) . z) in X1

        proof

          let z be object such that

           A5: z in [: COMPLEX , X1:];

          consider r,x be object such that

           A6: r in COMPLEX and

           A7: x in X1 and

           A8: z = [r, x] by A5, ZFMISC_1:def 2;

          reconsider r as Complex by A6;

          reconsider y = x as VECTOR of X by A7;

           [r, x] in ( dom (the Mult of X | [: COMPLEX , X1:])) by A3, A2, A5, A8, RELAT_1: 62;

          then ((the Mult of X | [: COMPLEX , X1:]) . z) = (r * y) by A8, FUNCT_1: 47;

          hence thesis by A1, A7;

        end;

        ( dom (the Mult of X | [: COMPLEX , X1:])) = [: COMPLEX , X1:] by A3, A2, RELAT_1: 62;

        hence thesis by A4, FUNCT_2: 3;

      end;

    end

    definition

      let X be ComplexLinearSpace, X1 be Subset of X;

      :: CSSPACE:def10

      func Zero_ (X1,X) -> Element of X1 equals

      : Def8: ( 0. X);

      correctness

      proof

        set v = the Element of X1;

        v in X1 by A2;

        then

        reconsider v as Element of X;

        (v - v) = ( 0. X) by RLVECT_1: 15;

        hence thesis by A1, A2, CLVECT_1: 22;

      end;

    end

    theorem :: CSSPACE:11



     Th6: for V be ComplexLinearSpace, V1 be Subset of V st V1 is linearly-closed non empty holds CLSStruct (# V1, ( Zero_ (V1,V)), ( Add_ (V1,V)), ( Mult_ (V1,V)) #) is Subspace of V

    proof

      let V be ComplexLinearSpace;

      let V1 be Subset of V such that

       A1: V1 is linearly-closed and

       A2: V1 is non empty;



       A3: ( Add_ (V1,V)) = (the addF of V || V1) by A1, Def6;



       A4: ( Mult_ (V1,V)) = (the Mult of V | [: COMPLEX , V1:]) by A1, Def7;

      ( Zero_ (V1,V)) = ( 0. V) by A1, A2, Def8;

      hence thesis by A2, A3, A4, CLVECT_1: 43;

    end;

    definition

      :: CSSPACE:def11

      func the_set_of_l2ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means

      : Def9: for x be object holds x in it iff x in the_set_of_ComplexSequences & ( |.( seq_id x).| (#) |.( seq_id x).|) is summable;

      existence

      proof

        defpred P[ object] means ( |.( seq_id $1).| (#) |.( seq_id $1).|) is summable;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in the_set_of_ComplexSequences & P[x] from XBOOLE_0:sch 1;

        for x be object st x in IT holds x in the_set_of_ComplexSequences by A1;

        then IT is Subset of the_set_of_ComplexSequences by TARSKI:def 3;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of Linear_Space_of_ComplexSequences ;

        assume that

         A2: for x be object holds x in X1 iff x in the_set_of_ComplexSequences & ( |.( seq_id x).| (#) |.( seq_id x).|) is summable and

         A3: for x be object holds x in X2 iff x in the_set_of_ComplexSequences & ( |.( seq_id x).| (#) |.( seq_id x).|) is summable;



         A4: X2 c= X1

        proof

          let x be object;

          assume

           A5: x in X2;

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

          hence thesis by A2, A5;

        end;

        X1 c= X2

        proof

          let x be object;

          assume

           A6: x in X1;

          then ( |.( seq_id x).| (#) |.( seq_id x).|) is summable by A2;

          hence thesis by A3, A6;

        end;

        hence thesis by A4, XBOOLE_0:def 10;

      end;

    end



     Lm1: ( |.( seq_id CZeroseq ).| (#) |.( seq_id CZeroseq ).|) is absolutely_summable

    proof

      set f = ( seq_id CZeroseq );

      now

        let n be Nat;



         A1: (f . n) = 0 by Th4;



        thus (( |.f.| (#) |.f.|) . n) = (( |.f.| . n) * ( |.f.| . n)) by SEQ_1: 8

        .= (( |.f.| . n) * |.(f . n).|) by VALUED_1: 18

        .= 0 by A1, COMPLEX1: 44;

      end;

      hence thesis by COMSEQ_3: 3;

    end;

    registration

      cluster the_set_of_l2ComplexSequences -> non empty;

      coherence by Lm1, Def9;

    end

    theorem :: CSSPACE:12



     Th7: the_set_of_l2ComplexSequences is linearly-closed

    proof

      set W = the_set_of_l2ComplexSequences ;

      hereby

        let v,u be VECTOR of Linear_Space_of_ComplexSequences such that

         A1: v in W and

         A2: u in W;

        ( |.( seq_id (v + u)).| (#) |.( seq_id (v + u)).|) is summable

        proof

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

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

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



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

          proof

            let n be Nat;

            (r . n) = (( |.( seq_id (v + u)).| . n) * ( |.( seq_id (v + u)).| . n)) by SEQ_1: 8;

            hence thesis by XREAL_1: 63;

          end;



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

          proof

            set t = |.( seq_id u).|;

            set s = |.( seq_id v).|;

            let n be Nat;



             A5: n in NAT by ORDINAL1:def 12;

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



             A6: (r . n) = (( |.( seq_id (v + u)).| . n) ^2 ) by SEQ_1: 8;

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

            .= ((2 * (p . n)) + ((2 (#) q) . n)) by SEQ_1: 9

            .= ((2 * (p . n)) + (2 * (q . n))) by SEQ_1: 9

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

            .= ((2 * (sn ^2 )) + (2 * (tn ^2 ))) by SEQ_1: 8;

            then

             A7: ((((2 (#) p) + (2 (#) q)) . n) - (((sn ^2 ) + ((2 * sn) * tn)) + (tn ^2 ))) = ((sn - tn) ^2 );



             A8: (v + u) = (( seq_id v) + ( seq_id u)) by Th2;

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

            .= |.((( seq_id v) . n) + (( seq_id u) . n)).| by A8, VALUED_1: 1, A5;

            then ( |.( seq_id (v + u)).| . n) <= ( |.(( seq_id v) . n).| + |.(( seq_id u) . n).|) by COMPLEX1: 56;

            then ( |.( seq_id (v + u)).| . n) <= ((s . n) + |.(( seq_id u) . n).|) by VALUED_1: 18;

            then

             A9: ( |.( seq_id (v + u)).| . n) <= ((s . n) + (t . n)) by VALUED_1: 18;



             A10: ( 0 + (((sn ^2 ) + ((2 * sn) * tn)) + (tn ^2 ))) <= (((2 (#) p) + (2 (#) q)) . n) by A7, XREAL_1: 19, XREAL_1: 63;

             0 <= |.(( seq_id (v + u)) . n).| by COMPLEX1: 46;

            then 0 <= ( |.( seq_id (v + u)).| . n) by VALUED_1: 18;

            then (( |.( seq_id (v + u)).| . n) ^2 ) <= (((s . n) + (t . n)) ^2 ) by A9, SQUARE_1: 15;

            hence thesis by A6, A10, XXREAL_0: 2;

          end;

          ( |.( seq_id u).| (#) |.( seq_id u).|) is summable by A2, Def9;

          then

           A11: (2 (#) q) is summable by SERIES_1: 10;

          ( |.( seq_id v).| (#) |.( seq_id v).|) is summable by A1, Def9;

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

          then ((2 (#) p) + (2 (#) q)) is summable by A11, SERIES_1: 7;

          hence thesis by A3, A4, SERIES_1: 20;

        end;

        hence (v + u) in W by Def9;

      end;

      let z be Complex;

      let v be VECTOR of Linear_Space_of_ComplexSequences ;

      assume v in W;

      then

       A12: ( |.( seq_id v).| (#) |.( seq_id v).|) is summable by Def9;

      (z * v) = (z (#) ( seq_id v)) by Th3;

      then |.( seq_id (z * v)).| = ( |.z.| (#) |.( seq_id v).|) by COMSEQ_1: 50;



      then ( |.( seq_id (z * v)).| (#) |.( seq_id (z * v)).|) = ( |.z.| (#) (( |.z.| (#) |.( seq_id v).|) (#) |.( seq_id v).|)) by SEQ_1: 18

      .= ( |.z.| (#) ( |.z.| (#) ( |.( seq_id v).| (#) |.( seq_id v).|))) by SEQ_1: 18

      .= (( |.z.| * |.z.|) (#) ( |.( seq_id v).| (#) |.( seq_id v).|)) by SEQ_1: 23;

      then ( |.( seq_id (z * v)).| (#) |.( seq_id (z * v)).|) is summable by A12, SERIES_1: 10;

      hence thesis by Def9;

    end;

    registration

      cluster the_set_of_l2ComplexSequences -> linearly-closed;

      coherence by Th7;

    end

    registration

      let z be Element of the_set_of_l2ComplexSequences ;

      reduce ( seq_id z) to z;

      reducibility ;

    end

    theorem :: CSSPACE:13

     CLSStruct (# the_set_of_l2ComplexSequences , ( Zero_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )) #) is Subspace of Linear_Space_of_ComplexSequences by Th6;

    theorem :: CSSPACE:14



     Th9: CLSStruct (# the_set_of_l2ComplexSequences , ( Zero_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )) #) is ComplexLinearSpace by Th6;

    theorem :: CSSPACE:15

    the carrier of Linear_Space_of_ComplexSequences = the_set_of_ComplexSequences & (for x be set holds x is VECTOR of Linear_Space_of_ComplexSequences iff x is Complex_Sequence) & (for u be VECTOR of Linear_Space_of_ComplexSequences holds u = ( seq_id u)) & (for u,v be VECTOR of Linear_Space_of_ComplexSequences holds (u + v) = (( seq_id u) + ( seq_id v))) & for z be Complex holds for u be VECTOR of Linear_Space_of_ComplexSequences holds (z * u) = (z (#) ( seq_id u)) by FUNCT_2: 8, FUNCT_2: 66, Th2, Th3;

    begin

    definition

      struct ( CLSStruct) CUNITSTR (# the carrier -> set,

the ZeroF -> Element of the carrier,

the addF -> BinOp of the carrier,

the Mult -> Function of [: COMPLEX , the carrier:], the carrier,

the scalar -> Function of [: the carrier, the carrier:], COMPLEX #)

       attr strict strict;

    end

    registration

      cluster non empty strict for CUNITSTR;

      existence

      proof

        set D = the non empty set, Z = the Element of D, a = the BinOp of D, m = the Function of [: COMPLEX , D:], D, s = the Function of [:D, D:], COMPLEX ;

        take CUNITSTR (# D, Z, a, m, s #);

        thus thesis;

      end;

    end

    registration

      let D be non empty set, Z be Element of D, a be BinOp of D, m be Function of [: COMPLEX , D:], D, s be Function of [:D, D:], COMPLEX ;

      cluster CUNITSTR (# D, Z, a, m, s #) -> non empty;

      coherence ;

    end

    reserve X for non empty CUNITSTR;

    reserve a,b for Complex;

    reserve x,y for Point of X;

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

    definition

      let X;

      let x, y;

      :: CSSPACE:def12

      func x .|. y -> Complex equals (the scalar of X . (x,y));

      correctness ;

    end

    set V0 = the ComplexLinearSpace;



     Lm2: the carrier of ( (0). V0) = {( 0. V0)} by CLVECT_1:def 9;

    reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> 0c ) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], COMPLEX ;



     Lm3: for x,y be VECTOR of ( (0). V0) holds (nilfunc . [x, y]) = 0c by FUNCOP_1: 7;

    ( 0. V0) in the carrier of ( (0). V0) by Lm2, TARSKI:def 1;

    then

     Lm4: (nilfunc . [( 0. V0), ( 0. V0)]) = 0c by Lm3;



     Lm5: for u be VECTOR of ( (0). V0) holds 0 <= ( Re (nilfunc . [u, u])) & ( Im (nilfunc . [u, u])) = 0 by COMPLEX1: 4, FUNCOP_1: 7;



     Lm6: for u,v be VECTOR of ( (0). V0) holds (nilfunc . [u, v]) = ((nilfunc . [v, u]) *' )

    proof

      let u,v be VECTOR of ( (0). V0);



       A1: v = ( 0. V0) by Lm2, TARSKI:def 1;

      u = ( 0. V0) by Lm2, TARSKI:def 1;

      hence thesis by A1, Lm4, COMPLEX1: 28;

    end;



     Lm7: for u,v,w be VECTOR of ( (0). V0) holds (nilfunc . [(u + v), w]) = ((nilfunc . [u, w]) + (nilfunc . [v, w]))

    proof

      let u,v,w be VECTOR of ( (0). V0);



       A1: v = ( 0. V0) by Lm2, TARSKI:def 1;



       A2: w = ( 0. V0) by Lm2, TARSKI:def 1;

      u = ( 0. V0) by Lm2, TARSKI:def 1;

      hence thesis by A1, A2, Lm2, Lm4, TARSKI:def 1;

    end;



     Lm8: for u,v be VECTOR of ( (0). V0), a holds (nilfunc . [(a * u), v]) = (a * (nilfunc . [u, v]))

    proof

      let u,v be VECTOR of ( (0). V0);

      let a;



       A1: v = ( 0. V0) by Lm2, TARSKI:def 1;

      u = ( 0. V0) by Lm2, TARSKI:def 1;

      hence thesis by A1, Lm2, Lm4, TARSKI:def 1;

    end;

    set X0 = CUNITSTR (# the carrier of ( (0). V0), ( 0. ( (0). V0)), the addF of ( (0). V0), the Mult of ( (0). V0), nilfunc #);

     Lm9:

    now

      let x,y,z be Point of X0;

      let a;

       09(X0) = ( 0. V0) by CLVECT_1: 30;

      hence (x .|. x) = 0c iff x = 09(X0) by Lm2, Lm3, TARSKI:def 1;

      thus 0 <= ( Re (x .|. x)) & 0 = ( Im (x .|. x)) by Lm5;

      thus (x .|. y) = ((y .|. x) *' ) by Lm6;

      thus ((x + y) .|. z) = ((x .|. z) + (y .|. z))

      proof

        reconsider u = x, v = y, w = z as VECTOR of ( (0). V0);

        ((x + y) .|. z) = (nilfunc . [(u + v), w]);

        hence thesis by Lm7;

      end;

      thus ((a * x) .|. y) = (a * (x .|. y))

      proof

        reconsider u = x, v = y as VECTOR of ( (0). V0);

        ((a * x) .|. y) = (nilfunc . [(a * u), v]);

        hence thesis by Lm8;

      end;

    end;

    definition

      let IT be non empty CUNITSTR;

      :: CSSPACE:def13

      attr IT is ComplexUnitarySpace-like means

      : Def11: for x,y,w be Point of IT, a holds ((x .|. x) = 0 iff x = ( 0. IT)) & 0 <= ( Re (x .|. x)) & 0 = ( Im (x .|. x)) & (x .|. y) = ((y .|. x) *' ) & ((x + y) .|. w) = ((x .|. w) + (y .|. w)) & ((a * x) .|. y) = (a * (x .|. y));

    end

    registration

      cluster ComplexUnitarySpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict for non empty CUNITSTR;

      existence

      proof

        take X0;

        thus X0 is ComplexUnitarySpace-like by Lm9;

        thus X0 is vector-distributive scalar-distributive scalar-associative scalar-unital

        proof

          thus for a holds for v,w be VECTOR of X0 holds (a * (v + w)) = ((a * v) + (a * w))

          proof

            let a;

            let v,w be VECTOR of X0;

            reconsider v9 = v, w9 = w as VECTOR of ( (0). V0);



            thus (a * (v + w)) = (a * (v9 + w9))

            .= ((a * v9) + (a * w9)) by CLVECT_1:def 2

            .= ((a * v) + (a * w));

          end;

          thus for a, b holds for v be VECTOR of X0 holds ((a + b) * v) = ((a * v) + (b * v))

          proof

            let a, b;

            let v be VECTOR of X0;

            reconsider v9 = v as VECTOR of ( (0). V0);



            thus ((a + b) * v) = ((a + b) * v9)

            .= ((a * v9) + (b * v9)) by CLVECT_1:def 3

            .= ((a * v) + (b * v));

          end;

          thus for a, b holds for v be VECTOR of X0 holds ((a * b) * v) = (a * (b * v))

          proof

            let a, b;

            let v be VECTOR of X0;

            reconsider v9 = v as VECTOR of ( (0). V0);



            thus ((a * b) * v) = ((a * b) * v9)

            .= (a * (b * v9)) by CLVECT_1:def 4

            .= (a * (b * v));

          end;

          let v be VECTOR of X0;

          reconsider v9 = v as VECTOR of ( (0). V0);



          thus ( 1r * v) = ( 1r * v9)

          .= v by CLVECT_1:def 5;

        end;



         A1: for x,y be VECTOR of X0 holds for x9,y9 be VECTOR of ( (0). V0) st x = x9 & y = y9 holds (x + y) = (x9 + y9) & for a holds (a * x) = (a * x9);

        thus for v,w be VECTOR of X0 holds (v + w) = (w + v)

        proof

          let v,w be VECTOR of X0;

          reconsider v9 = v, w9 = w as VECTOR of ( (0). V0);



          thus (v + w) = (w9 + v9) by A1

          .= (w + v);

        end;

        thus for u,v,w be VECTOR of X0 holds ((u + v) + w) = (u + (v + w))

        proof

          let u,v,w be VECTOR of X0;

          reconsider u9 = u, v9 = v, w9 = w as VECTOR of ( (0). V0);



          thus ((u + v) + w) = ((u9 + v9) + w9)

          .= (u9 + (v9 + w9)) by RLVECT_1:def 3

          .= (u + (v + w));

        end;

        thus for v be VECTOR of X0 holds (v + ( 0. X0)) = v

        proof

          let v be VECTOR of X0;

          reconsider v9 = v as VECTOR of ( (0). V0);



          thus (v + ( 0. X0)) = (v9 + ( 0. ( (0). V0)))

          .= v by RLVECT_1: 4;

        end;

        thus X0 is right_complementable

        proof

          let v be VECTOR of X0;

          reconsider v9 = v as VECTOR of ( (0). V0);

          consider w9 be VECTOR of ( (0). V0) such that

           A2: (v9 + w9) = ( 0. ( (0). V0)) by ALGSTR_0:def 11;

          reconsider w = w9 as VECTOR of X0;

          take w;

          thus thesis by A2;

        end;

        thus thesis;

      end;

    end

    definition

      mode ComplexUnitarySpace is ComplexUnitarySpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty CUNITSTR;

    end

    reserve X for ComplexUnitarySpace;

    reserve x,y,z,u,v for Point of X;

    theorem :: CSSPACE:16

    (( 0. X) .|. ( 0. X)) = 0 by Def11;

    theorem :: CSSPACE:17



     Th12: (x .|. (y + z)) = ((x .|. y) + (x .|. z))

    proof



      thus (x .|. (y + z)) = (((y + z) .|. x) *' ) by Def11

      .= (((y .|. x) + (z .|. x)) *' ) by Def11

      .= (((y .|. x) *' ) + ((z .|. x) *' )) by COMPLEX1: 32

      .= ((x .|. y) + ((z .|. x) *' )) by Def11

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

    end;

    theorem :: CSSPACE:18



     Th13: (x .|. (a * y)) = ((a *' ) * (x .|. y))

    proof



      thus (x .|. (a * y)) = (((a * y) .|. x) *' ) by Def11

      .= ((a * (y .|. x)) *' ) by Def11

      .= ((a *' ) * ((y .|. x) *' )) by COMPLEX1: 35

      .= ((a *' ) * (x .|. y)) by Def11;

    end;

    theorem :: CSSPACE:19



     Th14: ((a * x) .|. y) = (x .|. ((a *' ) * y))

    proof

      ((a * x) .|. y) = (a * (x .|. y)) by Def11

      .= (((a *' ) *' ) * ((y .|. x) *' )) by Def11

      .= (((a *' ) * (y .|. x)) *' ) by COMPLEX1: 35

      .= ((((a *' ) * y) .|. x) *' ) by Def11;

      hence thesis by Def11;

    end;

    theorem :: CSSPACE:20



     Th15: (((a * x) + (b * y)) .|. z) = ((a * (x .|. z)) + (b * (y .|. z)))

    proof

      (((a * x) + (b * y)) .|. z) = (((a * x) .|. z) + ((b * y) .|. z)) by Def11

      .= ((a * (x .|. z)) + ((b * y) .|. z)) by Def11;

      hence thesis by Def11;

    end;

    theorem :: CSSPACE:21



     Th16: (x .|. ((a * y) + (b * z))) = (((a *' ) * (x .|. y)) + ((b *' ) * (x .|. z)))

    proof

      (x .|. ((a * y) + (b * z))) = ((((a * y) + (b * z)) .|. x) *' ) by Def11

      .= (((a * (y .|. x)) + (b * (z .|. x))) *' ) by Th15

      .= (((a * (y .|. x)) *' ) + ((b * (z .|. x)) *' )) by COMPLEX1: 32

      .= (((a *' ) * ((y .|. x) *' )) + ((b * (z .|. x)) *' )) by COMPLEX1: 35

      .= (((a *' ) * ((y .|. x) *' )) + ((b *' ) * ((z .|. x) *' ))) by COMPLEX1: 35

      .= (((a *' ) * (x .|. y)) + ((b *' ) * ((z .|. x) *' ))) by Def11;

      hence thesis by Def11;

    end;

    theorem :: CSSPACE:22



     Th17: (( - x) .|. y) = (x .|. ( - y))

    proof

      (( - x) .|. y) = ((( - 1r ) * x) .|. y) by CLVECT_1: 3

      .= (x .|. ((( - 1r ) *' ) * y)) by Th14

      .= (x .|. (( - 1r ) * y)) by COMPLEX1: 30, COMPLEX1: 33;

      hence thesis by CLVECT_1: 3;

    end;

    theorem :: CSSPACE:23



     Th18: (( - x) .|. y) = ( - (x .|. y))

    proof

      (( - x) .|. y) = ((( - 1r ) * x) .|. y) by CLVECT_1: 3

      .= (( - 1) * (x .|. y)) by Def11, COMPLEX1:def 4;

      hence thesis;

    end;

    theorem :: CSSPACE:24



     Th19: (x .|. ( - y)) = ( - (x .|. y))

    proof

      (x .|. ( - y)) = (( - x) .|. y) by Th17;

      hence thesis by Th18;

    end;

    theorem :: CSSPACE:25



     Th20: (( - x) .|. ( - y)) = (x .|. y)

    proof

      (( - x) .|. ( - y)) = ( - (x .|. ( - y))) by Th18

      .= ( - ( - (x .|. y))) by Th19;

      hence thesis;

    end;

    theorem :: CSSPACE:26



     Th21: ((x - y) .|. z) = ((x .|. z) - (y .|. z))

    proof

      ((x - y) .|. z) = ((x .|. z) + (( - y) .|. z)) by Def11

      .= ((x .|. z) + ( - (y .|. z))) by Th18;

      hence thesis;

    end;

    theorem :: CSSPACE:27



     Th22: (x .|. (y - z)) = ((x .|. y) - (x .|. z))

    proof

      (x .|. (y - z)) = ((x .|. y) + (x .|. ( - z))) by Th12

      .= ((x .|. y) + ( - (x .|. z))) by Th19;

      hence thesis;

    end;

    theorem :: CSSPACE:28

    ((x - y) .|. (u - v)) = ((((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v))

    proof

      ((x - y) .|. (u - v)) = ((x .|. (u - v)) - (y .|. (u - v))) by Th21

      .= (((x .|. u) - (x .|. v)) - (y .|. (u - v))) by Th22

      .= (((x .|. u) - (x .|. v)) - ((y .|. u) - (y .|. v))) by Th22;

      hence thesis;

    end;

    theorem :: CSSPACE:29



     Th24: (( 0. X) .|. x) = 0

    proof

      ( 09(X) .|. x) = ((x + ( - x)) .|. x) by RLVECT_1: 5

      .= ((x .|. x) + (( - x) .|. x)) by Def11

      .= ((x .|. x) + ( - (x .|. x))) by Th18;

      hence thesis;

    end;

    theorem :: CSSPACE:30



     Th25: (x .|. ( 0. X)) = 0

    proof

      (x .|. ( 0. X)) = ((( 0. X) .|. x) *' ) by Def11

      .= 0c by Th24, COMPLEX1: 28;

      hence thesis;

    end;

    theorem :: CSSPACE:31



     Th26: ((x + y) .|. (x + y)) = ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))

    proof

      ((x + y) .|. (x + y)) = ((x .|. (x + y)) + (y .|. (x + y))) by Def11

      .= (((x .|. x) + (x .|. y)) + (y .|. (x + y))) by Th12

      .= (((x .|. x) + (x .|. y)) + ((y .|. x) + (y .|. y))) by Th12;

      hence thesis;

    end;

    theorem :: CSSPACE:32

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

    proof

      ((x + y) .|. (x - y)) = ((x .|. (x - y)) + (y .|. (x - y))) by Def11

      .= (((x .|. x) - (x .|. y)) + (y .|. (x - y))) by Th22

      .= (((x .|. x) - (x .|. y)) + ((y .|. x) - (y .|. y))) by Th22

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

      hence thesis;

    end;

    theorem :: CSSPACE:33



     Th28: ((x - y) .|. (x - y)) = ((((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y))

    proof

      ((x - y) .|. (x - y)) = ((x .|. (x - y)) - (y .|. (x - y))) by Th21

      .= (((x .|. x) - (x .|. y)) - (y .|. (x - y))) by Th22

      .= (((x .|. x) - (x .|. y)) - ((y .|. x) - (y .|. y))) by Th22;

      hence thesis;

    end;



     Lm10: for p,q be Complex, x,y be Point of X holds (((p * x) + (q * y)) .|. ((p * x) + (q * y))) = (((((p * (p *' )) * (x .|. x)) + ((p * (q *' )) * (x .|. y))) + (((p *' ) * q) * (y .|. x))) + ((q * (q *' )) * (y .|. y)))

    proof

      let p,q be Complex;

      let x,y be Point of X;

      (((p * x) + (q * y)) .|. ((p * x) + (q * y))) = ((p * (x .|. ((p * x) + (q * y)))) + (q * (y .|. ((p * x) + (q * y))))) by Th15

      .= ((p * (((p *' ) * (x .|. x)) + ((q *' ) * (x .|. y)))) + (q * (y .|. ((p * x) + (q * y))))) by Th16

      .= ((((p * (p *' )) * (x .|. x)) + ((p * (q *' )) * (x .|. y))) + (q * (((p *' ) * (y .|. x)) + ((q *' ) * (y .|. y))))) by Th16

      .= ((((p * (p *' )) * (x .|. x)) + ((p * (q *' )) * (x .|. y))) + (((q * (p *' )) * (y .|. x)) + ((q * (q *' )) * (y .|. y))));

      hence thesis;

    end;

    theorem :: CSSPACE:34



     Th29: |.(x .|. x).| = ( Re (x .|. x))

    proof



       A1: ( Im (x .|. x)) = 0 by Def11;

      ( Re (x .|. x)) >= 0 by Def11;

      then |.(( Re (x .|. x)) + (( Im (x .|. x)) * <i> )).| = ( Re (x .|. x)) by A1, ABSVALUE:def 1;

      hence thesis by COMPLEX1: 13;

    end;

    theorem :: CSSPACE:35



     Th30: |.(x .|. y).| <= (( sqrt |.(x .|. x).|) * ( sqrt |.(y .|. y).|))

    proof



       A1: y <> 09(X) implies |.(x .|. y).| <= (( sqrt |.(x .|. x).|) * ( sqrt |.(y .|. y).|))

      proof

        assume y <> 09(X);

        then (y .|. y) <> 0c by Def11;

        then

         A2: |.(y .|. y).| <> 0 by COMPLEX1: 45;



         A3: (( Re (x .|. y)) ^2 ) >= 0 by XREAL_1: 63;

        set c2 = ( - (x .|. y));

        reconsider c1 = ( |.(y .|. y).| + ( 0 * <i> )) as Element of COMPLEX by XCMPLX_0:def 2;



         A4: ( Re (c1 * ((c1 * (x .|. x)) + (c2 * (y .|. x))))) = ((( Re c1) * ( Re ((c1 * (x .|. x)) + (c2 * (y .|. x))))) - (( Im c1) * ( Im ((c1 * (x .|. x)) + (c2 * (y .|. x)))))) by COMPLEX1: 9

        .= ((( Re c1) * ( Re ((c1 * (x .|. x)) + (c2 * (y .|. x))))) - ( 0 * ( Im ((c1 * (x .|. x)) + (c2 * (y .|. x)))))) by COMPLEX1: 12

        .= (( Re c1) * ( Re ((c1 * (x .|. x)) + (c2 * (y .|. x)))));



         A5: ( Re (c2 * (y .|. x))) = ( Re ( - ((x .|. y) * (y .|. x))))

        .= ( - ( Re ((x .|. y) * (y .|. x)))) by COMPLEX1: 17

        .= ( - ( Re ((x .|. y) * ((x .|. y) *' )))) by Def11;



         A6: ( Im ((x .|. y) * ((x .|. y) *' ))) = 0 by COMPLEX1: 40;



         A7: ( Im (y .|. y)) = 0 by Def11;



         A8: ( Re (y .|. y)) >= 0 by Def11;

        then |.(( Re (y .|. y)) + (( Im (y .|. y)) * <i> )).| = ( Re (y .|. y)) by A7, ABSVALUE:def 1;

        then

         A9: |.(y .|. y).| = ( Re (y .|. y)) by COMPLEX1: 13;

        then

         A10: (y .|. y) = c1 by A7, COMPLEX1: 13;

        (((c1 * x) + (c2 * y)) .|. ((c1 * x) + (c2 * y))) = (((((c1 * (c1 *' )) * (x .|. x)) + ((c1 * (c2 *' )) * (x .|. y))) + (((c1 *' ) * c2) * (y .|. x))) + ((c2 * (c2 *' )) * (y .|. y))) by Lm10

        .= ((((c1 * ((c1 *' ) * (x .|. x))) + (c1 * ((c2 *' ) * (x .|. y)))) + ((c1 *' ) * (c2 * (y .|. x)))) + (c1 * (c2 * (c2 *' )))) by A7, A9, COMPLEX1: 13

        .= (((c1 * (((c1 *' ) * (x .|. x)) + ((c2 *' ) * (x .|. y)))) + (c1 * (c2 * (y .|. x)))) + (c1 * (c2 * (c2 *' )))) by A10, Def11

        .= (c1 * (((((c1 *' ) * (x .|. x)) + ((c2 *' ) * (x .|. y))) + (c2 * (y .|. x))) + (c2 * (c2 *' ))))

        .= (c1 * ((((c1 * (x .|. x)) + ((x .|. y) * (c2 *' ))) + (c2 * (y .|. x))) + (c2 * (c2 *' )))) by A10, Def11

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

        then ( Re c1) >= 0 & ( Re ((c1 * (x .|. x)) + (c2 * (y .|. x)))) >= 0 or ( Re c1) <= 0 & ( Re ((c1 * (x .|. x)) + (c2 * (y .|. x)))) <= 0 by A4, Def11;

        then (( Re (c1 * (x .|. x))) + ( Re (c2 * (y .|. x)))) >= 0 by A8, A7, A9, A2, COMPLEX1: 8, COMPLEX1: 13;

        then (( Re (c1 * (x .|. x))) - ( Re ((x .|. y) * ((x .|. y) *' )))) >= 0 by A5;

        then

         A11: ( Re (c1 * (x .|. x))) >= (( Re ((x .|. y) * ((x .|. y) *' ))) + 0 ) by XREAL_1: 19;



         A12: ( Im (x .|. x)) = 0 by Def11;



         A13: (( Im (x .|. y)) ^2 ) >= 0 by XREAL_1: 63;

        ( Im c1) = 0 by A7, A9, COMPLEX1: 13;

        then ( Im (c1 * (x .|. x))) = ((( Re c1) * 0 ) + (( Re (x .|. x)) * 0 )) by A12, COMPLEX1: 9;

        then

         A14: |.(c1 * (x .|. x)).| = |.( Re (c1 * (x .|. x))).| by COMPLEX1: 50;

        ( Re ((x .|. y) * ((x .|. y) *' ))) = ((( Re (x .|. y)) ^2 ) + (( Im (x .|. y)) ^2 )) by COMPLEX1: 40;

        then

         A15: ( Re ((x .|. y) * ((x .|. y) *' ))) >= ( 0 + 0 ) by A3, A13;

        then |.( Re ((x .|. y) * ((x .|. y) *' ))).| = ( Re ((x .|. y) * ((x .|. y) *' ))) by ABSVALUE:def 1;

        then |.( Re (c1 * (x .|. x))).| >= |.( Re ((x .|. y) * ((x .|. y) *' ))).| by A11, A15, ABSVALUE:def 1;

        then |.(c1 * (x .|. x)).| >= |.((x .|. y) * ((x .|. y) *' )).| by A6, A14, COMPLEX1: 50;

        then ( |.(x .|. x).| * |.(y .|. y).|) >= |.((x .|. y) * ((x .|. y) *' )).| by A10, COMPLEX1: 65;

        then ( |.(x .|. x).| * |.(y .|. y).|) >= ( |.(x .|. y).| * |.((x .|. y) *' ).|) by COMPLEX1: 65;

        then

         A16: ( |.(x .|. x).| * |.(y .|. y).|) >= ( |.(x .|. y).| * |.(x .|. y).|) by COMPLEX1: 53;

        ( |.(x .|. y).| ^2 ) >= 0 by XREAL_1: 63;

        then

         A17: ( sqrt ( |.(x .|. x).| * |.(y .|. y).|)) >= ( sqrt ( |.(x .|. y).| ^2 )) by A16, SQUARE_1: 26;



         A18: |.(y .|. y).| >= 0 by COMPLEX1: 46;

         |.(x .|. x).| >= 0 by COMPLEX1: 46;

        then (( sqrt |.(x .|. x).|) * ( sqrt |.(y .|. y).|)) >= ( sqrt ( |.(x .|. y).| ^2 )) by A17, A18, SQUARE_1: 29;

        hence thesis by COMPLEX1: 46, SQUARE_1: 22;

      end;

      y = 09(X) implies |.(x .|. y).| <= (( sqrt |.(x .|. x).|) * ( sqrt |.(y .|. y).|))

      proof

        assume

         A19: y = 09(X);

        then (y .|. y) = 0c by Def11;

        hence thesis by A19, Th25, COMPLEX1: 44, SQUARE_1: 17;

      end;

      hence thesis by A1;

    end;

    definition

      let X;

      let x, y;

      :: CSSPACE:def14

      pred x,y are_orthogonal means

      : Def12: (x .|. y) = 0 ;

      symmetry by Def11, COMPLEX1: 28;

    end

    theorem :: CSSPACE:36

    (x,y) are_orthogonal implies (x,( - y)) are_orthogonal

    proof

      assume (x,y) are_orthogonal ;

      then ( - (x .|. y)) = ( - 0 );

      hence thesis by Th19;

    end;

    theorem :: CSSPACE:37

    (x,y) are_orthogonal implies (( - x),y) are_orthogonal

    proof

      assume (x,y) are_orthogonal ;

      then ( - (x .|. y)) = ( - 0 );

      hence thesis by Th18;

    end;

    theorem :: CSSPACE:38

    (x,y) are_orthogonal implies (( - x),( - y)) are_orthogonal by Th20;

    theorem :: CSSPACE:39

    (x,( 0. X)) are_orthogonal

    proof

      (( 0. X) .|. x) = 0 by Th24;

      hence thesis by Def12;

    end;

    theorem :: CSSPACE:40

    (x,y) are_orthogonal implies ((x + y) .|. (x + y)) = ((x .|. x) + (y .|. y))

    proof

      assume

       A1: (x,y) are_orthogonal ;

      then (y .|. x) = 0c by Def12;

      then ((x + y) .|. (x + y)) = (((x .|. x) + 0c ) + (y .|. y)) by A1, Th26;

      hence thesis;

    end;

    theorem :: CSSPACE:41

    (x,y) are_orthogonal implies ((x - y) .|. (x - y)) = ((x .|. x) + (y .|. y))

    proof

      assume

       A1: (x,y) are_orthogonal ;

      ((x - y) .|. (x - y)) = ((((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y)) by Th28

      .= (((x .|. x) + (y .|. y)) - 0 ) by A1, Def12;

      hence thesis;

    end;

    definition

      let X, x;

      :: CSSPACE:def15

      func ||.x.|| -> Real equals ( sqrt |.(x .|. x).|);

      correctness ;

    end

    theorem :: CSSPACE:42



     Th37: ||.x.|| = 0 iff x = ( 0. X)

    proof

      thus ||.x.|| = 0 implies x = 09(X)

      proof

         0 <= ( Re (x .|. x)) by Def11;

        then

         A1: 0 <= |.(x .|. x).| by Th29;

        assume ||.x.|| = 0 ;

        then |.(x .|. x).| = 0 by A1, SQUARE_1: 24;

        then (x .|. x) = 0c by COMPLEX1: 45;

        hence thesis by Def11;

      end;

      assume x = 09(X);

      hence thesis by Def11, COMPLEX1: 44, SQUARE_1: 17;

    end;

    theorem :: CSSPACE:43



     Th38: ||.(a * x).|| = ( |.a.| * ||.x.||)

    proof



       A1: 0 <= |.(a * a).| by COMPLEX1: 46;

       0 <= ( Re (x .|. x)) by Def11;

      then

       A2: 0 <= |.(x .|. x).| by Th29;

       ||.(a * x).|| = ( sqrt |.(a * (x .|. (a * x))).|) by Def11

      .= ( sqrt |.(a * ((a *' ) * (x .|. x))).|) by Th13

      .= ( sqrt |.((a * (a *' )) * (x .|. x)).|)

      .= ( sqrt ( |.(a * (a *' )).| * |.(x .|. x).|)) by COMPLEX1: 65

      .= ( sqrt ( |.(a * a).| * |.(x .|. x).|)) by COMPLEX1: 69

      .= (( sqrt |.(a * a).|) * ( sqrt |.(x .|. x).|)) by A1, A2, SQUARE_1: 29

      .= (( sqrt ( |.a.| ^2 )) * ( sqrt |.(x .|. x).|)) by COMPLEX1: 65

      .= ( |.a.| * ( sqrt |.(x .|. x).|)) by COMPLEX1: 46, SQUARE_1: 22;

      hence thesis;

    end;

    theorem :: CSSPACE:44



     Th39: 0 <= ||.x.||

    proof

       0 <= ( Re (x .|. x)) by Def11;

      then 0 <= |.(x .|. x).| by Th29;

      hence thesis by SQUARE_1:def 2;

    end;

    theorem :: CSSPACE:45

     |.(x .|. y).| <= ( ||.x.|| * ||.y.||) by Th30;

    theorem :: CSSPACE:46



     Th41: ||.(x + y).|| <= ( ||.x.|| + ||.y.||)

    proof



       A1: ( ||.(x + y).|| ^2 ) >= 0 by XREAL_1: 63;

      ( Re ((x + y) .|. (x + y))) >= 0 by Def11;

      then

       A2: |.((x + y) .|. (x + y)).| >= 0 by Th29;

      ( sqrt ( ||.(x + y).|| ^2 )) = ( sqrt |.((x + y) .|. (x + y)).|) by Th39, SQUARE_1: 22;

      then

       A3: ( ||.(x + y).|| ^2 ) = |.((x + y) .|. (x + y)).| by A2, A1, SQUARE_1: 28;

       |.(y .|. y).| >= 0 by COMPLEX1: 46;

      then

       A4: |.(y .|. y).| = ( ||.y.|| ^2 ) by SQUARE_1:def 2;



       A5: ( - ( Im (x .|. y))) = ( Im ((x .|. y) *' )) by COMPLEX1: 27

      .= ( Im (y .|. x)) by Def11;

      ( Im ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))) = (( Im (((x .|. x) + (x .|. y)) + (y .|. x))) + ( Im (y .|. y))) by COMPLEX1: 8

      .= ((( Im ((x .|. x) + (x .|. y))) + ( Im (y .|. x))) + ( Im (y .|. y))) by COMPLEX1: 8

      .= (((( Im (x .|. x)) + ( Im (x .|. y))) + ( Im (y .|. x))) + ( Im (y .|. y))) by COMPLEX1: 8

      .= ((( 0 + ( Im (x .|. y))) + ( Im (y .|. x))) + ( Im (y .|. y))) by Def11

      .= ((( Im (x .|. y)) + ( Im (y .|. x))) + 0 ) by Def11;

      then

       A6: ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) = (( Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))) + ( 0 * <i> )) by A5, COMPLEX1: 13;



       A7: ( Re (x .|. y)) = ( Re ((x .|. y) *' )) by COMPLEX1: 27

      .= ( Re (y .|. x)) by Def11;



       A8: ( Re (x .|. y)) <= |.(x .|. y).| by COMPLEX1: 54;

       |.(x .|. y).| <= ( ||.x.|| * ||.y.||) by Th30;

      then ( Re (x .|. y)) <= ( ||.x.|| * ||.y.||) by A8, XXREAL_0: 2;

      then

       A9: (2 * ( Re (x .|. y))) <= (2 * ( ||.x.|| * ||.y.||)) by XREAL_1: 64;

      ( Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))) = ( Re ((x + y) .|. (x + y))) by Th26;

      then

       A10: ( Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))) >= 0 by Def11;

      ( Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))) = (( Re (((x .|. x) + (x .|. y)) + (y .|. x))) + ( Re (y .|. y))) by COMPLEX1: 8

      .= ((( Re ((x .|. x) + (x .|. y))) + ( Re (y .|. x))) + ( Re (y .|. y))) by COMPLEX1: 8

      .= (((( Re (x .|. x)) + ( Re (x .|. y))) + ( Re (y .|. x))) + ( Re (y .|. y))) by COMPLEX1: 8

      .= ((( |.(x .|. x).| + ( Re (x .|. y))) + ( Re (y .|. x))) + ( Re (y .|. y))) by Th29

      .= ((( |.(x .|. x).| + ( Re (x .|. y))) + ( Re (y .|. x))) + |.(y .|. y).|) by Th29;

      then |.((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)).| = (( |.(x .|. x).| + (2 * ( Re (x .|. y)))) + |.(y .|. y).|) by A7, A10, A6, ABSVALUE:def 1;

      then

       A11: ( ||.(x + y).|| ^2 ) = ((2 * ( Re (x .|. y))) + ( |.(x .|. x).| + |.(y .|. y).|)) by A3, Th26;



       A12: ||.y.|| >= 0 by Th39;

       |.(x .|. x).| >= 0 by COMPLEX1: 46;

      then (( sqrt |.(x .|. x).|) ^2 ) = |.(x .|. x).| by SQUARE_1:def 2;

      then ( ||.(x + y).|| ^2 ) <= ((2 * ( ||.x.|| * ||.y.||)) + (( ||.x.|| ^2 ) + |.(y .|. y).|)) by A11, A9, XREAL_1: 6;

      then

       A13: ( ||.(x + y).|| ^2 ) <= (( ||.x.|| + ||.y.||) ^2 ) by A4;

       ||.x.|| >= 0 by Th39;

      hence thesis by A12, A13, SQUARE_1: 16;

    end;

    theorem :: CSSPACE:47



     Th42: ||.( - x).|| = ||.x.||

    proof

       ||.( - x).|| = ||.(( - 1r ) * x).|| by CLVECT_1: 3

      .= ( |.( - 1r ).| * ||.x.||) by Th38

      .= ( |. 1r .| * ||.x.||) by COMPLEX1: 52;

      hence thesis by COMPLEX1: 48;

    end;

    theorem :: CSSPACE:48



     Th43: ( ||.x.|| - ||.y.||) <= ||.(x - y).||

    proof

      ((x - y) + y) = (x - (y - y)) by RLVECT_1: 29

      .= (x - 09(X)) by RLVECT_1: 15

      .= x by RLVECT_1: 13;

      then ||.x.|| <= ( ||.(x - y).|| + ||.y.||) by Th41;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: CSSPACE:49

     |.( ||.x.|| - ||.y.||).| <= ||.(x - y).||

    proof

      ((y - x) + x) = (y - (x - x)) by RLVECT_1: 29

      .= (y - 09(X)) by RLVECT_1: 15

      .= y by RLVECT_1: 13;

      then ||.y.|| <= ( ||.(y - x).|| + ||.x.||) by Th41;

      then ( ||.y.|| - ||.x.||) <= ||.(y - x).|| by XREAL_1: 20;

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

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

      then

       A1: ( - ||.(x - y).||) <= ( - ( ||.y.|| - ||.x.||)) by XREAL_1: 24;

      ( ||.x.|| - ||.y.||) <= ||.(x - y).|| by Th43;

      hence thesis by A1, ABSVALUE: 5;

    end;

    definition

      let X, x, y;

      :: CSSPACE:def16

      func dist (x,y) -> Real equals ||.(x - y).||;

      correctness ;

    end

    definition

      let X, x, y;

      :: original: dist

      redefine

      func dist (x,y);

      commutativity

      proof

        let x, y;



        thus ( dist (x,y)) = ||.( - (y - x)).|| by RLVECT_1: 33

        .= ( dist (y,x)) by Th42;

      end;

    end

    theorem :: CSSPACE:50



     Th45: ( dist (x,x)) = 0

    proof



      thus ( dist (x,x)) = ||. 09(X).|| by RLVECT_1: 15

      .= 0 by Th37;

    end;

    theorem :: CSSPACE:51

    ( dist (x,z)) <= (( dist (x,y)) + ( dist (y,z)))

    proof

      ( dist (x,z)) = ||.((x - z) + 09(X)).|| by RLVECT_1: 4

      .= ||.((x - z) + (y - y)).|| by RLVECT_1: 15

      .= ||.(x - (z - (y - y))).|| by RLVECT_1: 29

      .= ||.(x - (y + (z - y))).|| by RLVECT_1: 29

      .= ||.((x - y) - (z - y)).|| by RLVECT_1: 27

      .= ||.((x - y) + (y - z)).|| by RLVECT_1: 33;

      hence thesis by Th41;

    end;

    theorem :: CSSPACE:52



     Th47: x <> y iff ( dist (x,y)) <> 0

    proof

      thus x <> y implies ( dist (x,y)) <> 0

      proof

        assume that

         A1: x <> y and

         A2: ( dist (x,y)) = 0 ;

        (x - y) = 09(X) by A2, Th37;

        hence contradiction by A1, RLVECT_1: 21;

      end;

      thus thesis by Th45;

    end;

    theorem :: CSSPACE:53

    ( dist (x,y)) >= 0 by Th39;

    theorem :: CSSPACE:54

    x <> y iff ( dist (x,y)) > 0

    proof

      thus x <> y implies ( dist (x,y)) > 0

      proof

        assume x <> y;

        then ( dist (x,y)) <> 0 by Th47;

        hence thesis by Th39;

      end;

      thus thesis by Th45;

    end;

    theorem :: CSSPACE:55

    ( dist (x,y)) = ( sqrt |.((x - y) .|. (x - y)).|);

    theorem :: CSSPACE:56

    ( dist ((x + y),(u + v))) <= (( dist (x,u)) + ( dist (y,v)))

    proof

      ( dist ((x + y),(u + v))) = ||.((( - u) + ( - v)) + (x + y)).|| by RLVECT_1: 31

      .= ||.((x + (( - u) + ( - v))) + y).|| by RLVECT_1:def 3

      .= ||.(((x - u) + ( - v)) + y).|| by RLVECT_1:def 3

      .= ||.((x - u) + (y - v)).|| by RLVECT_1:def 3;

      hence thesis by Th41;

    end;

    theorem :: CSSPACE:57

    ( dist ((x - y),(u - v))) <= (( dist (x,u)) + ( dist (y,v)))

    proof

      ( dist ((x - y),(u - v))) = ||.(((x - y) - u) + v).|| by RLVECT_1: 29

      .= ||.((x - (u + y)) + v).|| by RLVECT_1: 27

      .= ||.(((x - u) - y) + v).|| by RLVECT_1: 27

      .= ||.((x - u) - (y - v)).|| by RLVECT_1: 29

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

      then ( dist ((x - y),(u - v))) <= ( ||.(x - u).|| + ||.( - (y - v)).||) by Th41;

      hence thesis by Th42;

    end;

    theorem :: CSSPACE:58

    ( dist ((x - z),(y - z))) = ( dist (x,y))

    proof



      thus ( dist ((x - z),(y - z))) = ||.(((x - z) - y) + z).|| by RLVECT_1: 29

      .= ||.((x - (y + z)) + z).|| by RLVECT_1: 27

      .= ||.(((x - y) - z) + z).|| by RLVECT_1: 27

      .= ||.((x - y) - (z - z)).|| by RLVECT_1: 29

      .= ||.((x - y) - 09(X)).|| by RLVECT_1: 15

      .= ( dist (x,y)) by RLVECT_1: 13;

    end;

    theorem :: CSSPACE:59

    ( dist ((x - z),(y - z))) <= (( dist (z,x)) + ( dist (z,y)))

    proof

      ( dist ((x - z),(y - z))) = ||.((x - z) + (z - y)).|| by RLVECT_1: 33

      .= ||.(( - (z - x)) + (z - y)).|| by RLVECT_1: 33;

      then ( dist ((x - z),(y - z))) <= ( ||.( - (z - x)).|| + ||.(z - y).||) by Th41;

      hence thesis by Th42;

    end;

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

    reserve n for Nat;

    definition

      let X, seq1, seq2;

      :: original: +

      redefine

      func seq1 + seq2;

      commutativity

      proof

        let seq1, seq2;

        now

          let n be Element of NAT ;



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

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

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: CSSPACE:60

    (seq1 + (seq2 + seq3)) = ((seq1 + seq2) + seq3)

    proof

      now

        let n be Element of NAT ;



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

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

        .= (((seq1 . n) + (seq2 . n)) + (seq3 . n)) by RLVECT_1:def 3

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:61

    seq1 is constant & seq2 is constant & seq = (seq1 + seq2) implies seq is constant

    proof

      assume that

       A1: seq1 is constant and

       A2: seq2 is constant and

       A3: seq = (seq1 + seq2);

      consider x such that

       A4: for n be Nat holds (seq1 . n) = x by A1;

      consider y such that

       A5: for n be Nat holds (seq2 . n) = y by A2;

      take z = (x + y);

      let n be Nat;



      thus (seq . n) = ((seq1 . n) + (seq2 . n)) by A3, NORMSP_1:def 2

      .= (x + (seq2 . n)) by A4

      .= z by A5;

    end;

    theorem :: CSSPACE:62

    seq1 is constant & seq2 is constant & seq = (seq1 - seq2) implies seq is constant

    proof

      assume that

       A1: seq1 is constant and

       A2: seq2 is constant and

       A3: seq = (seq1 - seq2);

      consider x such that

       A4: for n be Nat holds (seq1 . n) = x by A1;

      consider y such that

       A5: for n be Nat holds (seq2 . n) = y by A2;

      take z = (x - y);

      let n be Nat;



      thus (seq . n) = ((seq1 . n) - (seq2 . n)) by A3, NORMSP_1:def 3

      .= (x - (seq2 . n)) by A4

      .= z by A5;

    end;

    theorem :: CSSPACE:63

    seq1 is constant & seq = (a * seq1) implies seq is constant

    proof

      assume that

       A1: seq1 is constant and

       A2: seq = (a * seq1);

      consider x such that

       A3: for n be Nat holds (seq1 . n) = x by A1;

      take z = (a * x);

      let n be Nat;



      thus (seq . n) = (a * (seq1 . n)) by A2, CLVECT_1:def 14

      .= z by A3;

    end;

    theorem :: CSSPACE:64

    (seq1 - seq2) = (seq1 + ( - seq2))

    proof

      now

        let n be Element of NAT ;



        thus ((seq1 - seq2) . n) = ((seq1 . n) - (seq2 . n)) by NORMSP_1:def 3

        .= ((seq1 . n) + (( - seq2) . n)) by BHSP_1: 44

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:65

    seq = (seq + ( 0. X))

    proof

      now

        let n be Element of NAT ;



        thus ((seq + 09(X)) . n) = ((seq . n) + 09(X)) by BHSP_1:def 6

        .= (seq . n) by RLVECT_1: 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:66

    (a * (seq1 + seq2)) = ((a * seq1) + (a * seq2))

    proof

      now

        let n be Element of NAT ;



        thus ((a * (seq1 + seq2)) . n) = (a * ((seq1 + seq2) . n)) by CLVECT_1:def 14

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

        .= ((a * (seq1 . n)) + (a * (seq2 . n))) by CLVECT_1:def 2

        .= (((a * seq1) . n) + (a * (seq2 . n))) by CLVECT_1:def 14

        .= (((a * seq1) . n) + ((a * seq2) . n)) by CLVECT_1:def 14

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:67

    ((a + b) * seq) = ((a * seq) + (b * seq))

    proof

      now

        let n be Element of NAT ;



        thus (((a + b) * seq) . n) = ((a + b) * (seq . n)) by CLVECT_1:def 14

        .= ((a * (seq . n)) + (b * (seq . n))) by CLVECT_1:def 3

        .= (((a * seq) . n) + (b * (seq . n))) by CLVECT_1:def 14

        .= (((a * seq) . n) + ((b * seq) . n)) by CLVECT_1:def 14

        .= (((a * seq) + (b * seq)) . n) by NORMSP_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:68

    ((a * b) * seq) = (a * (b * seq))

    proof

      now

        let n be Element of NAT ;



        thus (((a * b) * seq) . n) = ((a * b) * (seq . n)) by CLVECT_1:def 14

        .= (a * (b * (seq . n))) by CLVECT_1:def 4

        .= (a * ((b * seq) . n)) by CLVECT_1:def 14

        .= ((a * (b * seq)) . n) by CLVECT_1:def 14;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:69

    ( 1r * seq) = seq

    proof

      now

        let n be Element of NAT ;



        thus (( 1r * seq) . n) = ( 1r * (seq . n)) by CLVECT_1:def 14

        .= (seq . n) by CLVECT_1:def 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:70

    (( - 1r ) * seq) = ( - seq)

    proof

      now

        let n be Element of NAT ;



        thus ((( - 1r ) * seq) . n) = (( - 1r ) * (seq . n)) by CLVECT_1:def 14

        .= ( - (seq . n)) by CLVECT_1: 3

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:71

    (seq - x) = (seq + ( - x))

    proof

      now

        let n be Element of NAT ;



        thus ((seq - x) . n) = ((seq . n) - x) by NORMSP_1:def 4

        .= ((seq + ( - x)) . n) by BHSP_1:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:72

    (seq1 - seq2) = ( - (seq2 - seq1))

    proof

      now

        let n be Element of NAT ;



        thus ((seq1 - seq2) . n) = ((seq1 . n) - (seq2 . n)) by NORMSP_1:def 3

        .= ( - ((seq2 . n) - (seq1 . n))) by RLVECT_1: 33

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

        .= (( - (seq2 - seq1)) . n) by BHSP_1: 44;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:73

    seq = (seq - ( 0. X))

    proof

      now

        let n be Element of NAT ;



        thus ((seq - 09(X)) . n) = ((seq . n) - 09(X)) by NORMSP_1:def 4

        .= (seq . n) by RLVECT_1: 13;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:74

    seq = ( - ( - seq))

    proof

      now

        let n be Element of NAT ;



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

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

        .= (seq . n) by RLVECT_1: 17;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:75

    (seq1 - (seq2 + seq3)) = ((seq1 - seq2) - seq3)

    proof

      now

        let n be Element of NAT ;



        thus ((seq1 - (seq2 + seq3)) . n) = ((seq1 . n) - ((seq2 + seq3) . n)) by NORMSP_1:def 3

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

        .= (((seq1 . n) - (seq2 . n)) - (seq3 . n)) by RLVECT_1: 27

        .= (((seq1 - seq2) . n) - (seq3 . n)) by NORMSP_1:def 3

        .= (((seq1 - seq2) - seq3) . n) by NORMSP_1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:76

    ((seq1 + seq2) - seq3) = (seq1 + (seq2 - seq3))

    proof

      now

        let n be Element of NAT ;



        thus (((seq1 + seq2) - seq3) . n) = (((seq1 + seq2) . n) - (seq3 . n)) by NORMSP_1:def 3

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

        .= ((seq1 . n) + ((seq2 . n) - (seq3 . n))) by RLVECT_1:def 3

        .= ((seq1 . n) + ((seq2 - seq3) . n)) by NORMSP_1:def 3

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:77

    (seq1 - (seq2 - seq3)) = ((seq1 - seq2) + seq3)

    proof

      now

        let n be Element of NAT ;



        thus ((seq1 - (seq2 - seq3)) . n) = ((seq1 . n) - ((seq2 - seq3) . n)) by NORMSP_1:def 3

        .= ((seq1 . n) - ((seq2 . n) - (seq3 . n))) by NORMSP_1:def 3

        .= (((seq1 . n) - (seq2 . n)) + (seq3 . n)) by RLVECT_1: 29

        .= (((seq1 - seq2) . n) + (seq3 . n)) by NORMSP_1:def 3

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CSSPACE:78

    (a * (seq1 - seq2)) = ((a * seq1) - (a * seq2))

    proof

      now

        let n be Element of NAT ;



        thus ((a * (seq1 - seq2)) . n) = (a * ((seq1 - seq2) . n)) by CLVECT_1:def 14

        .= (a * ((seq1 . n) - (seq2 . n))) by NORMSP_1:def 3

        .= ((a * (seq1 . n)) - (a * (seq2 . n))) by CLVECT_1: 9

        .= (((a * seq1) . n) - (a * (seq2 . n))) by CLVECT_1:def 14

        .= (((a * seq1) . n) - ((a * seq2) . n)) by CLVECT_1:def 14

        .= (((a * seq1) - (a * seq2)) . n) by NORMSP_1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    definition

      :: CSSPACE:def17

      func cl_scalar -> Function of [: the_set_of_l2ComplexSequences , the_set_of_l2ComplexSequences :], COMPLEX means for x,y be object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds (it . (x,y)) = ( Sum (( seq_id x) (#) (( seq_id y) *' )));

      existence

      proof

        deffunc F( object, object) = ( Sum (( seq_id $1) (#) (( seq_id $2) *' )));

        set X = the_set_of_l2ComplexSequences ;



         A1: for x,y be object st x in X & y in X holds F(x,y) in COMPLEX ;

        ex f be Function of [:X, X:], COMPLEX st for x,y be object st x in X & y in X holds (f . (x,y)) = F(x,y) from BINOP_1:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        set X = the_set_of_l2ComplexSequences ;

        let scalar1,scalar2 be Function of [:X, X:], COMPLEX such that

         A2: for x,y be object st x in X & y in X holds (scalar1 . (x,y)) = ( Sum (( seq_id x) (#) (( seq_id y) *' ))) and

         A3: for x,y be object st x in X & y in X holds (scalar2 . (x,y)) = ( Sum (( seq_id x) (#) (( seq_id y) *' )));

        for x,y be set st x in X & y in X holds (scalar1 . (x,y)) = (scalar2 . (x,y))

        proof

          let x,y be set such that

           A4: x in X and

           A5: y in X;



          thus (scalar1 . (x,y)) = ( Sum (( seq_id x) (#) (( seq_id y) *' ))) by A2, A4, A5

          .= (scalar2 . (x,y)) by A3, A4, A5;

        end;

        hence thesis;

      end;

    end

    registration

      cluster CUNITSTR (# the_set_of_l2ComplexSequences , ( Zero_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), cl_scalar #) -> non empty;

      coherence ;

    end

    definition

      :: CSSPACE:def18

      func Complex_l2_Space -> non empty CUNITSTR equals CUNITSTR (# the_set_of_l2ComplexSequences , ( Zero_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_l2ComplexSequences , Linear_Space_of_ComplexSequences )), cl_scalar #);

      correctness ;

    end

    theorem :: CSSPACE:79



     Th74: for l be CLSStruct st the CLSStruct of l is ComplexLinearSpace holds l is ComplexLinearSpace

    proof

      let l be CLSStruct such that

       A1: the CLSStruct of l is ComplexLinearSpace;

      reconsider l as non empty CLSStruct by A1;

      reconsider l0 = CLSStruct (# the carrier of l, ( 0. l), the addF of l, the Mult of l #) as ComplexLinearSpace by A1;



       A2: l is Abelian

      proof

        let v,w be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;

        reconsider w1 = w as VECTOR of l0;



        thus (v + w) = (v1 + w1)

        .= (w1 + v1)

        .= (w + v);

      end;



       A3: l is add-associative

      proof

        let u,v,w be VECTOR of l;

        reconsider u1 = u as VECTOR of l0;

        reconsider v1 = v as VECTOR of l0;

        reconsider w1 = w as VECTOR of l0;



        thus ((u + v) + w) = ((u1 + v1) + w1)

        .= (u1 + (v1 + w1)) by RLVECT_1:def 3

        .= (u + (v + w));

      end;



       A4: l is vector-distributive scalar-distributive scalar-associative scalar-unital

      proof

        thus for z be Complex, v,w be VECTOR of l holds (z * (v + w)) = ((z * v) + (z * w))

        proof

          let z be Complex;

          let v,w be VECTOR of l;

          reconsider v1 = v, w1 = w as VECTOR of l0;



          thus (z * (v + w)) = (z * (v1 + w1))

          .= ((z * v1) + (z * w1)) by CLVECT_1:def 2

          .= ((z * v) + (z * w));

        end;

        thus for z1,z2 be Complex, v be VECTOR of l holds ((z1 + z2) * v) = ((z1 * v) + (z2 * v))

        proof

          let z1,z2 be Complex;

          let v be VECTOR of l;

          reconsider v1 = v as VECTOR of l0;



          thus ((z1 + z2) * v) = ((z1 + z2) * v1)

          .= ((z1 * v1) + (z2 * v1)) by CLVECT_1:def 3

          .= ((z1 * v) + (z2 * v));

        end;

        thus for z1,z2 be Complex, v be VECTOR of l holds ((z1 * z2) * v) = (z1 * (z2 * v))

        proof

          let z1,z2 be Complex;

          let v be VECTOR of l;

          reconsider v1 = v as VECTOR of l0;



          thus ((z1 * z2) * v) = ((z1 * z2) * v1)

          .= (z1 * (z2 * v1)) by CLVECT_1:def 4

          .= (z1 * (z2 * v));

        end;

        let v be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;



        thus ( 1r * v) = ( 1r * v1)

        .= v by CLVECT_1:def 5;

      end;



       A5: l is right_complementable

      proof

        let v be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;

        consider w1 be VECTOR of l0 such that

         A6: (v1 + w1) = ( 0. l0) by ALGSTR_0:def 11;

        reconsider w = w1 as VECTOR of l;

        take w;

        thus thesis by A6;

      end;

      l is right_zeroed

      proof

        let v be VECTOR of l;

        reconsider v1 = v as VECTOR of l0;



        thus (v + ( 0. l)) = (v1 + ( 0. l0))

        .= v by RLVECT_1:def 4;

      end;

      hence thesis by A2, A3, A5, A4;

    end;

    theorem :: CSSPACE:80

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

    proof

      let seq be Complex_Sequence such that

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



       A2: for m be Nat holds (( Partial_Sums seq) . m) = 0c

      proof

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

        let m be Nat;



         A3: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A4: (seq . k) = (( Partial_Sums seq) . k);



          thus (seq . (k + 1)) = ( 0c + (seq . (k + 1)))

          .= ((seq . k) + (seq . (k + 1))) by A1

          .= (( Partial_Sums seq) . (k + 1)) by A4, SERIES_1:def 1;

        end;



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

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



        hence (( Partial_Sums seq) . m) = (seq . m)

        .= 0c by A1;

      end;



       A6: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((( Partial_Sums seq) . m) - 0c ).| < p

      proof

        let p be Real such that

         A7: 0 < p;

        take 0 ;

        let m be Nat such that 0 <= m;

        thus thesis by A2, A7, COMPLEX1: 44;

      end;

      then

       A8: ( Partial_Sums seq) qua Complex_Sequence is convergent by COMSEQ_2:def 5;

      then ( lim ( Partial_Sums seq)) = 0c by A6, COMSEQ_2:def 6;

      hence thesis by A8, COMSEQ_3:def 7, COMSEQ_3:def 8;

    end;

    registration

      cluster Complex_l2_Space -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Th9, Th74;

    end

    theorem :: CSSPACE:81

    ( |.( seq_id CZeroseq ).| (#) |.( seq_id CZeroseq ).|) is absolutely_summable by Lm1;