clvect_1.miz



    begin

    definition

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

the ZeroF -> Element of the carrier,

the addF -> BinOp of the carrier,

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

       attr strict strict;

    end

    registration

      cluster non empty for CLSStruct;

      existence

      proof

        set ZS = the non empty set, O = the Element of ZS, F = the BinOp of ZS, G = the Function of [: COMPLEX , ZS:], ZS;

        take CLSStruct (# ZS, O, F, G #);

        thus the carrier of CLSStruct (# ZS, O, F, G #) is non empty;

      end;

    end

    definition

      let V be CLSStruct;

      mode VECTOR of V is Element of V;

    end

    definition

      let V be non empty CLSStruct, v be VECTOR of V, z be Complex;

      :: CLVECT_1:def1

      func z * v -> Element of V equals (the Mult of V . [z, v]);

      coherence

      proof

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

        (the Mult of V . [z, v]) is Element of V;

        hence thesis;

      end;

    end

    registration

      let ZS be non empty set, O be Element of ZS, F be BinOp of ZS, G be Function of [: COMPLEX , ZS:], ZS;

      cluster CLSStruct (# ZS, O, F, G #) -> non empty;

      coherence ;

    end

    reserve a,b for Complex;

    definition

      let IT be non empty CLSStruct;

      :: CLVECT_1:def2

      attr IT is vector-distributive means

      : Def2: for a holds for v,w be VECTOR of IT holds (a * (v + w)) = ((a * v) + (a * w));

      :: CLVECT_1:def3

      attr IT is scalar-distributive means

      : Def3: for a, b holds for v be VECTOR of IT holds ((a + b) * v) = ((a * v) + (b * v));

      :: CLVECT_1:def4

      attr IT is scalar-associative means

      : Def4: for a, b holds for v be VECTOR of IT holds ((a * b) * v) = (a * (b * v));

      :: CLVECT_1:def5

      attr IT is scalar-unital means

      : Def5: for v be VECTOR of IT holds ( 1r * v) = v;

    end

    definition

      :: CLVECT_1:def6

      func Trivial-CLSStruct -> strict CLSStruct equals CLSStruct (# { 0 }, op0 , op2 , ( pr2 ( COMPLEX , { 0 })) #);

      coherence ;

    end

    registration

      cluster Trivial-CLSStruct -> 1 -element;

      coherence ;

    end

    registration

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

      existence

      proof

        take S = Trivial-CLSStruct ;

        thus S is strict;

        thus S is Abelian by STRUCT_0:def 10;

        thus S is add-associative by STRUCT_0:def 10;

        thus S is right_zeroed by STRUCT_0:def 10;

        thus S is right_complementable

        proof

          let x be Element of S;

          take x;

          thus thesis by STRUCT_0:def 10;

        end;

        thus for a holds for v,w be VECTOR of S holds (a * (v + w)) = ((a * v) + (a * w)) by STRUCT_0:def 10;

        thus for a, b holds for v be VECTOR of S holds ((a + b) * v) = ((a * v) + (b * v)) by STRUCT_0:def 10;

        thus for a, b holds for v be VECTOR of S holds ((a * b) * v) = (a * (b * v)) by STRUCT_0:def 10;

        thus for v be VECTOR of S holds ( 1r * v) = v by STRUCT_0:def 10;

      end;

    end

    definition

      mode ComplexLinearSpace is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct;

    end

    reserve V,X,Y for ComplexLinearSpace;

    reserve u,u1,u2,v,v1,v2 for VECTOR of V;

    reserve z,z1,z2 for Complex;

    theorem :: CLVECT_1:1

    

     Th1: z = 0 or v = ( 0. V) implies (z * v) = ( 0. V)

    proof

      assume

       A1: z = 0 or v = ( 0. V);

      now

        per cases by A1;

          suppose

           A2: z = 0c ;

          (v + ( 0c * v)) = (( 1r * v) + ( 0c * v)) by Def5

          .= (( 1r + 0c ) * v) by Def3

          .= v by Def5

          .= (v + ( 0. V)) by RLVECT_1: 4;

          hence thesis by A2, RLVECT_1: 8;

        end;

          suppose

           A3: v = ( 0. V);

          ((z * ( 0. V)) + (z * ( 0. V))) = (z * (( 0. V) + ( 0. V))) by Def2

          .= (z * ( 0. V)) by RLVECT_1: 4

          .= ((z * ( 0. V)) + ( 0. V)) by RLVECT_1: 4;

          hence thesis by A3, RLVECT_1: 8;

        end;

      end;

      hence thesis;

    end;

    theorem :: CLVECT_1:2

    

     Th2: (z * v) = ( 0. V) implies z = 0 or v = ( 0. V)

    proof

      assume that

       A1: (z * v) = ( 0. V) and

       A2: z <> 0 ;

      

      thus v = ( 1r * v) by Def5

      .= (((z " ) * z) * v) by A2, XCMPLX_0:def 7

      .= ((z " ) * ( 0. V)) by A1, Def4

      .= ( 0. V) by Th1;

    end;

    theorem :: CLVECT_1:3

    

     Th3: ( - v) = (( - 1r ) * v)

    proof

      (v + (( - 1r ) * v)) = (( 1r * v) + (( - 1r ) * v)) by Def5

      .= (( 1r + ( - 1r )) * v) by Def3

      .= ( 0. V) by Th1;

      

      hence ( - v) = (( - v) + (v + (( - 1r ) * v))) by RLVECT_1: 4

      .= ((( - v) + v) + (( - 1r ) * v)) by RLVECT_1:def 3

      .= (( 0. V) + (( - 1r ) * v)) by RLVECT_1: 5

      .= (( - 1r ) * v) by RLVECT_1: 4;

    end;

    theorem :: CLVECT_1:4

    

     Th4: v = ( - v) implies v = ( 0. V)

    proof

      assume v = ( - v);

      

      then ( 0. V) = (v - ( - v)) by RLVECT_1: 15

      .= (v + v) by RLVECT_1: 17

      .= (( 1r * v) + v) by Def5

      .= (( 1r * v) + ( 1r * v)) by Def5

      .= (( 1r + 1r ) * v) by Def3;

      hence thesis by Th2;

    end;

    theorem :: CLVECT_1:5

    (v + v) = ( 0. V) implies v = ( 0. V)

    proof

      assume (v + v) = ( 0. V);

      then v = ( - v) by RLVECT_1:def 10;

      hence thesis by Th4;

    end;

    theorem :: CLVECT_1:6

    

     Th6: (z * ( - v)) = (( - z) * v)

    proof

      

      thus (z * ( - v)) = (z * (( - 1r ) * v)) by Th3

      .= ((z * ( - 1r )) * v) by Def4

      .= (( - z) * v);

    end;

    theorem :: CLVECT_1:7

    

     Th7: (z * ( - v)) = ( - (z * v))

    proof

      

      thus (z * ( - v)) = (( - ( 1r * z)) * v) by Th6

      .= ((( - 1r ) * z) * v)

      .= (( - 1r ) * (z * v)) by Def4

      .= ( - (z * v)) by Th3;

    end;

    theorem :: CLVECT_1:8

    (( - z) * ( - v)) = (z * v)

    proof

      

      thus (( - z) * ( - v)) = (( - ( - z)) * v) by Th6

      .= (z * v);

    end;

    theorem :: CLVECT_1:9

    

     Th9: (z * (v - u)) = ((z * v) - (z * u))

    proof

      

      thus (z * (v - u)) = ((z * v) + (z * ( - u))) by Def2

      .= ((z * v) - (z * u)) by Th7;

    end;

    theorem :: CLVECT_1:10

    

     Th10: ((z1 - z2) * v) = ((z1 * v) - (z2 * v))

    proof

      

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

      .= ((z1 * v) + (( - z2) * v)) by Def3

      .= ((z1 * v) + (z2 * ( - v))) by Th6

      .= ((z1 * v) - (z2 * v)) by Th7;

    end;

    theorem :: CLVECT_1:11

    z <> 0 & (z * v) = (z * u) implies v = u

    proof

      assume that

       A1: z <> 0 and

       A2: (z * v) = (z * u);

      ( 0. V) = ((z * v) - (z * u)) by A2, RLVECT_1: 15

      .= (z * (v - u)) by Th9;

      then (v - u) = ( 0. V) by A1, Th2;

      hence thesis by RLVECT_1: 21;

    end;

    theorem :: CLVECT_1:12

    v <> ( 0. V) & (z1 * v) = (z2 * v) implies z1 = z2

    proof

      assume that

       A1: v <> ( 0. V) and

       A2: (z1 * v) = (z2 * v);

      ( 0. V) = ((z1 * v) - (z2 * v)) by A2, RLVECT_1: 15

      .= ((z1 - z2) * v) by Th10;

      then (( - z2) + z1) = 0 by A1, Th2;

      hence thesis;

    end;

    

     Lm1: for V be non empty addLoopStr holds ( Sum ( <*> the carrier of V)) = ( 0. V)

    proof

      let V be non empty addLoopStr;

      set S = ( <*> the carrier of V);

      ex f be sequence of the carrier of V st ( Sum S) = (f . ( len S)) & (f . 0 ) = ( 0. V) & for j be Nat, v be Element of V st j < ( len S) & v = (S . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      hence thesis;

    end;

    

     Lm2: for V be non empty addLoopStr, F be FinSequence of the carrier of V holds ( len F) = 0 implies ( Sum F) = ( 0. V)

    proof

      let V be non empty addLoopStr;

      let F be FinSequence of the carrier of V;

      assume ( len F) = 0 ;

      then F = ( <*> the carrier of V);

      hence thesis by Lm1;

    end;

    theorem :: CLVECT_1:13

    for F,G be FinSequence of the carrier of V st ( len F) = ( len G) & (for k be Nat, v be VECTOR of V st k in ( dom F) & v = (G . k) holds (F . k) = (z * v)) holds ( Sum F) = (z * ( Sum G))

    proof

      let F,G be FinSequence of the carrier of V;

      defpred P[ set] means for H,I be FinSequence of the carrier of V st ( len H) = ( len I) & ( len H) = $1 & (for k be Nat, v be VECTOR of V st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (z * v)) holds ( Sum H) = (z * ( Sum I));

      

       A1: ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

      now

        let n be Nat;

        assume

         A2: for H,I be FinSequence of the carrier of V st ( len H) = ( len I) & ( len H) = n & for k be Nat, v be VECTOR of V st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (z * v) holds ( Sum H) = (z * ( Sum I));

        let H,I be FinSequence of the carrier of V;

        assume that

         A3: ( len H) = ( len I) and

         A4: ( len H) = (n + 1) and

         A5: for k be Nat, v be VECTOR of V st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (z * v);

        reconsider p = (H | ( Seg n)), q = (I | ( Seg n)) as FinSequence of the carrier of V by FINSEQ_1: 18;

        

         A6: n <= (n + 1) by NAT_1: 12;

        then

         A7: ( len q) = n by A3, A4, FINSEQ_1: 17;

        

         A8: ( len p) = n by A4, A6, FINSEQ_1: 17;

         A9:

        now

          ( len p) <= ( len H) by A4, A6, FINSEQ_1: 17;

          then

           A10: ( Seg ( len p)) c= ( Seg ( len H)) by FINSEQ_1: 5;

          

           A11: ( dom p) = ( Seg n) by A4, A6, FINSEQ_1: 17;

          let k be Nat;

          let v be VECTOR of V;

          assume that

           A12: k in ( Seg ( len p)) and

           A13: v = (q . k);

          ( dom q) = ( Seg n) by A3, A4, A6, FINSEQ_1: 17;

          then (I . k) = (q . k) by A8, A12, FUNCT_1: 47;

          then (H . k) = (z * v) by A5, A12, A13, A10;

          hence (p . k) = (z * v) by A8, A12, A11, FUNCT_1: 47;

        end;

        (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then (n + 1) in ( dom H) & (n + 1) in ( dom I) by A3, A4, FINSEQ_1:def 3;

        then

        reconsider v1 = (H . (n + 1)), v2 = (I . (n + 1)) as VECTOR of V by FUNCT_1: 102;

        

         A14: v1 = (z * v2) by A4, A5, FINSEQ_1: 4;

        

         A15: ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

        ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

        

        hence ( Sum H) = (( Sum p) + v1) by A4, A8, RLVECT_1: 38

        .= ((z * ( Sum q)) + (z * v2)) by A2, A8, A7, A9, A14

        .= (z * (( Sum q) + v2)) by Def2

        .= (z * ( Sum I)) by A3, A4, A7, A15, RLVECT_1: 38;

      end;

      then

       A16: for n be Nat st P[n] holds P[(n + 1)];

      now

        let H,I be FinSequence of the carrier of V;

        assume that

         A17: ( len H) = ( len I) and

         A18: ( len H) = 0 and for k be Nat, v be VECTOR of V st k in ( Seg ( len H)) & v = (I . k) holds (H . k) = (z * v);

        ( Sum H) = ( 0. V) by A18, Lm2;

        hence ( Sum H) = (z * ( Sum I)) by A17, A18, Lm2, Th1;

      end;

      then

       A19: P[ 0 ];

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

      hence thesis by A1;

    end;

    theorem :: CLVECT_1:14

    (z * ( Sum ( <*> the carrier of V))) = ( 0. V) by Lm1, Th1;

    theorem :: CLVECT_1:15

    (z * ( Sum <*v, u*>)) = ((z * v) + (z * u))

    proof

      

      thus (z * ( Sum <*v, u*>)) = (z * (v + u)) by RLVECT_1: 45

      .= ((z * v) + (z * u)) by Def2;

    end;

    theorem :: CLVECT_1:16

    (z * ( Sum <*u, v1, v2*>)) = (((z * u) + (z * v1)) + (z * v2))

    proof

      

      thus (z * ( Sum <*u, v1, v2*>)) = (z * ((u + v1) + v2)) by RLVECT_1: 46

      .= ((z * (u + v1)) + (z * v2)) by Def2

      .= (((z * u) + (z * v1)) + (z * v2)) by Def2;

    end;

    theorem :: CLVECT_1:17

    

     Th17: ( Sum <*v, v*>) = (( 1r + 1r ) * v)

    proof

      

      thus ( Sum <*v, v*>) = (v + v) by RLVECT_1: 45

      .= (( 1r * v) + v) by Def5

      .= (( 1r * v) + ( 1r * v)) by Def5

      .= (( 1r + 1r ) * v) by Def3;

    end;

    theorem :: CLVECT_1:18

    ( Sum <*( - v), ( - v)*>) = (( - ( 1r + 1r )) * v)

    proof

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

      

      thus ( Sum <*( - v), ( - v)*>) = ( - (v + v)) by RLVECT_1: 60

      .= ( - ( Sum <*v, v*>)) by RLVECT_1: 45

      .= ( - (( 1r + 1r ) * v)) by Th17

      .= (( - 1r ) * (2r * v)) by Th3

      .= ((( - 1r ) * 2r) * v) by Def4

      .= (( - ( 1r + 1r )) * v);

    end;

    theorem :: CLVECT_1:19

    ( Sum <*v, v, v*>) = ((( 1r + 1r ) + 1r ) * v)

    proof

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

      

      thus ( Sum <*v, v, v*>) = (( Sum <*v, v*>) + v) by RLVECT_1: 66

      .= ((( 1r + 1r ) * v) + v) by Th17

      .= ((( 1r + 1r ) * v) + ( 1r * v)) by Def5

      .= ((( 1r + 1r ) + 1r ) * v) by Def3;

    end;

    begin

    reserve V1,V2,V3 for Subset of V;

    definition

      let V, V1;

      :: CLVECT_1:def7

      attr V1 is linearly-closed means (for v,u be VECTOR of V st v in V1 & u in V1 holds (v + u) in V1) & for z be Complex, v be VECTOR of V st v in V1 holds (z * v) in V1;

    end

    theorem :: CLVECT_1:20

    

     Th20: V1 <> {} & V1 is linearly-closed implies ( 0. V) in V1

    proof

      assume that

       A1: V1 <> {} and

       A2: V1 is linearly-closed;

      set x = the Element of V1;

      reconsider x as Element of V by A1, TARSKI:def 3;

      ( 0c * x) in V1 by A1, A2;

      hence thesis by Th1;

    end;

    theorem :: CLVECT_1:21

    

     Th21: V1 is linearly-closed implies for v be VECTOR of V st v in V1 holds ( - v) in V1

    proof

      assume

       A1: V1 is linearly-closed;

      let v be VECTOR of V;

      assume v in V1;

      then (( - 1r ) * v) in V1 by A1;

      hence thesis by Th3;

    end;

    theorem :: CLVECT_1:22

    V1 is linearly-closed implies for v,u be VECTOR of V st v in V1 & u in V1 holds (v - u) in V1

    proof

      assume

       A1: V1 is linearly-closed;

      let v,u be VECTOR of V;

      assume that

       A2: v in V1 and

       A3: u in V1;

      ( - u) in V1 by A1, A3, Th21;

      hence thesis by A1, A2;

    end;

    theorem :: CLVECT_1:23

    

     Th23: {( 0. V)} is linearly-closed

    proof

      thus for v,u be VECTOR of V st v in {( 0. V)} & u in {( 0. V)} holds (v + u) in {( 0. V)}

      proof

        let v,u be VECTOR of V;

        assume v in {( 0. V)} & u in {( 0. V)};

        then v = ( 0. V) & u = ( 0. V) by TARSKI:def 1;

        then (v + u) = ( 0. V) by RLVECT_1: 4;

        hence thesis by TARSKI:def 1;

      end;

      let z;

      let v be VECTOR of V;

      assume

       A1: v in {( 0. V)};

      then v = ( 0. V) by TARSKI:def 1;

      hence thesis by A1, Th1;

    end;

    theorem :: CLVECT_1:24

    the carrier of V = V1 implies V1 is linearly-closed;

    theorem :: CLVECT_1:25

    V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) : v in V1 & u in V2 } implies V3 is linearly-closed

    proof

      assume that

       A1: V1 is linearly-closed & V2 is linearly-closed and

       A2: V3 = { (v + u) : v in V1 & u in V2 };

      thus for v,u be VECTOR of V st v in V3 & u in V3 holds (v + u) in V3

      proof

        let v,u be VECTOR of V;

        assume that

         A3: v in V3 and

         A4: u in V3;

        consider v2,v1 be VECTOR of V such that

         A5: v = (v1 + v2) and

         A6: v1 in V1 & v2 in V2 by A2, A3;

        consider u2,u1 be VECTOR of V such that

         A7: u = (u1 + u2) and

         A8: u1 in V1 & u2 in V2 by A2, A4;

        

         A9: (v + u) = (((v1 + v2) + u1) + u2) by A5, A7, RLVECT_1:def 3

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

        .= ((v1 + u1) + (v2 + u2)) by RLVECT_1:def 3;

        (v1 + u1) in V1 & (v2 + u2) in V2 by A1, A6, A8;

        hence thesis by A2, A9;

      end;

      let z be Complex, v be VECTOR of V;

      assume v in V3;

      then

      consider v2,v1 be VECTOR of V such that

       A10: v = (v1 + v2) and

       A11: v1 in V1 & v2 in V2 by A2;

      

       A12: (z * v) = ((z * v1) + (z * v2)) by A10, Def2;

      (z * v1) in V1 & (z * v2) in V2 by A1, A11;

      hence thesis by A2, A12;

    end;

    theorem :: CLVECT_1:26

    V1 is linearly-closed & V2 is linearly-closed implies (V1 /\ V2) is linearly-closed

    proof

      assume that

       A1: V1 is linearly-closed and

       A2: V2 is linearly-closed;

      thus for v,u be VECTOR of V st v in (V1 /\ V2) & u in (V1 /\ V2) holds (v + u) in (V1 /\ V2)

      proof

        let v,u be VECTOR of V;

        assume

         A3: v in (V1 /\ V2) & u in (V1 /\ V2);

        then v in V2 & u in V2 by XBOOLE_0:def 4;

        then

         A4: (v + u) in V2 by A2;

        v in V1 & u in V1 by A3, XBOOLE_0:def 4;

        then (v + u) in V1 by A1;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      let z be Complex, v be VECTOR of V;

      assume

       A5: v in (V1 /\ V2);

      then v in V2 by XBOOLE_0:def 4;

      then

       A6: (z * v) in V2 by A2;

      v in V1 by A5, XBOOLE_0:def 4;

      then (z * v) in V1 by A1;

      hence thesis by A6, XBOOLE_0:def 4;

    end;

    definition

      let V;

      :: CLVECT_1:def8

      mode Subspace of V -> ComplexLinearSpace means

      : Def8: the carrier of it c= the carrier of V & ( 0. it ) = ( 0. V) & the addF of it = (the addF of V || the carrier of it ) & the Mult of it = (the Mult of V | [: COMPLEX , the carrier of it :]);

      existence

      proof

        the addF of V = (the addF of V || the carrier of V) & the Mult of V = (the Mult of V | [: COMPLEX , the carrier of V:]) by RELSET_1: 19;

        hence thesis;

      end;

    end

    reserve W,W1,W2 for Subspace of V;

    reserve x for set;

    reserve w,w1,w2 for VECTOR of W;

    theorem :: CLVECT_1:27

    x in W1 & W1 is Subspace of W2 implies x in W2

    proof

      assume x in W1 & W1 is Subspace of W2;

      then x in the carrier of W1 & the carrier of W1 c= the carrier of W2 by Def8;

      hence thesis;

    end;

    theorem :: CLVECT_1:28

    

     Th28: for x be object holds x in W implies x in V

    proof

      let x be object;

      assume x in W;

      then

       A1: x in the carrier of W;

      the carrier of W c= the carrier of V by Def8;

      hence thesis by A1;

    end;

    theorem :: CLVECT_1:29

    

     Th29: w is VECTOR of V

    proof

      w in V by Th28, RLVECT_1: 1;

      hence thesis;

    end;

    theorem :: CLVECT_1:30

    ( 0. W) = ( 0. V) by Def8;

    theorem :: CLVECT_1:31

    ( 0. W1) = ( 0. W2)

    proof

      

      thus ( 0. W1) = ( 0. V) by Def8

      .= ( 0. W2) by Def8;

    end;

    theorem :: CLVECT_1:32

    

     Th32: w1 = v & w2 = u implies (w1 + w2) = (v + u)

    proof

      assume

       A1: v = w1 & u = w2;

      (w1 + w2) = ((the addF of V || the carrier of W) . [w1, w2]) by Def8;

      hence thesis by A1, FUNCT_1: 49;

    end;

    theorem :: CLVECT_1:33

    

     Th33: w = v implies (z * w) = (z * v)

    proof

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

      (z * w) = ((the Mult of V | [: COMPLEX , the carrier of W:]) . [z, w]) by Def8;

      hence thesis by FUNCT_1: 49;

    end;

    theorem :: CLVECT_1:34

    

     Th34: w = v implies ( - v) = ( - w)

    proof

      assume

       A1: w = v;

      ( - v) = (( - 1r ) * v) & ( - w) = (( - 1r ) * w) by Th3;

      hence thesis by A1, Th33;

    end;

    theorem :: CLVECT_1:35

    

     Th35: w1 = v & w2 = u implies (w1 - w2) = (v - u)

    proof

      assume that

       A1: w1 = v and

       A2: w2 = u;

      ( - w2) = ( - u) by A2, Th34;

      hence thesis by A1, Th32;

    end;

    

     Lm3: the carrier of W = V1 implies V1 is linearly-closed

    proof

      set VW = the carrier of W;

      reconsider WW = W as ComplexLinearSpace;

      assume

       A1: the carrier of W = V1;

      thus for v, u st v in V1 & u in V1 holds (v + u) in V1

      proof

        let v, u;

        assume v in V1 & u in V1;

        then

        reconsider vv = v, uu = u as VECTOR of WW by A1;

        reconsider vw = (vv + uu) as Element of VW;

        vw in V1 by A1;

        hence thesis by Th32;

      end;

      let z, v;

      assume v in V1;

      then

      reconsider vv = v as VECTOR of WW by A1;

      reconsider vw = (z * vv) as Element of VW;

      vw in V1 by A1;

      hence thesis by Th33;

    end;

    theorem :: CLVECT_1:36

    

     Th36: ( 0. V) in W

    proof

      ( 0. W) in W;

      hence thesis by Def8;

    end;

    theorem :: CLVECT_1:37

    ( 0. W1) in W2

    proof

      ( 0. W1) = ( 0. V) by Def8;

      hence thesis by Th36;

    end;

    theorem :: CLVECT_1:38

    ( 0. W) in V by Th28, RLVECT_1: 1;

    theorem :: CLVECT_1:39

    

     Th39: u in W & v in W implies (u + v) in W

    proof

      reconsider VW = the carrier of W as Subset of V by Def8;

      assume u in W & v in W;

      then

       A1: u in the carrier of W & v in the carrier of W;

      VW is linearly-closed by Lm3;

      then (u + v) in the carrier of W by A1;

      hence thesis;

    end;

    theorem :: CLVECT_1:40

    

     Th40: v in W implies (z * v) in W

    proof

      reconsider VW = the carrier of W as Subset of V by Def8;

      assume v in W;

      then

       A1: v in the carrier of W;

      VW is linearly-closed by Lm3;

      then (z * v) in the carrier of W by A1;

      hence thesis;

    end;

    theorem :: CLVECT_1:41

    

     Th41: v in W implies ( - v) in W

    proof

      assume v in W;

      then (( - 1r ) * v) in W by Th40;

      hence thesis by Th3;

    end;

    theorem :: CLVECT_1:42

    

     Th42: u in W & v in W implies (u - v) in W

    proof

      assume

       A1: u in W;

      assume v in W;

      then ( - v) in W by Th41;

      hence thesis by A1, Th39;

    end;

    reserve D for non empty set;

    reserve d1 for Element of D;

    reserve A for BinOp of D;

    reserve M for Function of [: COMPLEX , D:], D;

     Lm4:

    now

      let V, V1, D, d1, A, M, z;

      let w be VECTOR of CLSStruct (# D, d1, A, M #);

      let v be Element of V;

      assume that

       A1: V1 = D and

       A2: M = (the Mult of V | [: COMPLEX , V1:]) and

       A3: w = v;

      z in COMPLEX by XCMPLX_0:def 2;

      then [z, w] in [: COMPLEX , V1:] by A1, ZFMISC_1:def 2;

      hence (z * w) = (z * v) by A3, A2, FUNCT_1: 49;

    end;

    theorem :: CLVECT_1:43

    

     Th43: V1 = D & d1 = ( 0. V) & A = (the addF of V || V1) & M = (the Mult of V | [: COMPLEX , V1:]) implies CLSStruct (# D, d1, A, M #) is Subspace of V

    proof

      assume that

       A1: V1 = D and

       A2: d1 = ( 0. V) and

       A3: A = (the addF of V || V1) and

       A4: M = (the Mult of V | [: COMPLEX , V1:]);

      set W = CLSStruct (# D, d1, A, M #);

      

       A5: for x,y be VECTOR of W holds (x + y) = (the addF of V . [x, y]) by A1, A3, FUNCT_1: 49;

      

       A6: W is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital

      proof

        set MV = the Mult of V;

        set AV = the addF of V;

        thus for x,y be VECTOR of W holds (x + y) = (y + x)

        proof

          let x,y be VECTOR of W;

          reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;

          

          thus (x + y) = (x1 + y1) by A5

          .= (y1 + x1)

          .= (y + x) by A5;

        end;

        thus for x,y,z be VECTOR of W holds ((x + y) + z) = (x + (y + z))

        proof

          let x,y,z be VECTOR of W;

          reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def 3;

          

          thus ((x + y) + z) = (AV . [(x + y), z1]) by A5

          .= ((x1 + y1) + z1) by A5

          .= (x1 + (y1 + z1)) by RLVECT_1:def 3

          .= (AV . [x1, (y + z)]) by A5

          .= (x + (y + z)) by A5;

        end;

        thus for x be VECTOR of W holds (x + ( 0. W)) = x

        proof

          let x be VECTOR of W;

          reconsider y = x as VECTOR of V by A1, TARSKI:def 3;

          

          thus (x + ( 0. W)) = (y + ( 0. V)) by A2, A5

          .= x by RLVECT_1: 4;

        end;

        thus W is right_complementable

        proof

          let x be VECTOR of W;

          reconsider x1 = x as VECTOR of V by A1, TARSKI:def 3;

          consider v such that

           A7: (x1 + v) = ( 0. V) by ALGSTR_0:def 11;

          reconsider mj = ( - 1r ) as Element of COMPLEX by XCMPLX_0:def 2;

          v = ( - x1) by A7, RLVECT_1:def 10

          .= (( - 1r ) * x1) by Th3

          .= (MV . [mj, x])

          .= (( - 1r ) * x) by A1, A4, FUNCT_1: 49;

          then

          reconsider y = v as VECTOR of W;

          take y;

          thus thesis by A2, A5, A7;

        end;

        thus for z holds for x,y be VECTOR of W holds (z * (x + y)) = ((z * x) + (z * y))

        proof

          let z;

          let x,y be VECTOR of W;

          reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;

          

           A8: (z * x1) = (z * x) & (z * y1) = (z * y) by A1, A4, Lm4;

          

          thus (z * (x + y)) = (z * (x1 + y1)) by A1, A4, A5, Lm4

          .= ((z * x1) + (z * y1)) by Def2

          .= ((z * x) + (z * y)) by A5, A8;

        end;

        thus for z1, z2 holds for x be VECTOR of W holds ((z1 + z2) * x) = ((z1 * x) + (z2 * x))

        proof

          let z1, z2;

          let x be VECTOR of W;

          reconsider y = x as VECTOR of V by A1, TARSKI:def 3;

          

           A9: (z1 * y) = (z1 * x) & (z2 * y) = (z2 * x) by A1, A4, Lm4;

          

          thus ((z1 + z2) * x) = ((z1 + z2) * y) by A1, A4, Lm4

          .= ((z1 * y) + (z2 * y)) by Def3

          .= ((z1 * x) + (z2 * x)) by A5, A9;

        end;

        thus for z1, z2 holds for x be VECTOR of W holds ((z1 * z2) * x) = (z1 * (z2 * x))

        proof

          let z1, z2;

          let x be VECTOR of W;

          reconsider y = x as VECTOR of V by A1, TARSKI:def 3;

          

           A10: (z2 * y) = (z2 * x) by A1, A4, Lm4;

          

          thus ((z1 * z2) * x) = ((z1 * z2) * y) by A1, A4, Lm4

          .= (z1 * (z2 * y)) by Def4

          .= (z1 * (z2 * x)) by A1, A4, A10, Lm4;

        end;

        let x be VECTOR of W;

        reconsider y = x as VECTOR of V by A1, TARSKI:def 3;

        

        thus ( 1r * x) = ( 1r * y) by A1, A4, Lm4

        .= x by Def5;

      end;

      ( 0. W) = ( 0. V) by A2;

      hence thesis by A1, A3, A4, A6, Def8;

    end;

    theorem :: CLVECT_1:44

    

     Th44: V is Subspace of V

    proof

      thus the carrier of V c= the carrier of V & ( 0. V) = ( 0. V);

      thus thesis by RELSET_1: 19;

    end;

    theorem :: CLVECT_1:45

    

     Th45: for V,X be strict ComplexLinearSpace holds V is Subspace of X & X is Subspace of V implies V = X

    proof

      let V,X be strict ComplexLinearSpace;

      assume that

       A1: V is Subspace of X and

       A2: X is Subspace of V;

      set VX = the carrier of X;

      set VV = the carrier of V;

      VV c= VX & VX c= VV by A1, A2, Def8;

      then

       A3: VV = VX;

      set AX = the addF of X;

      set AV = the addF of V;

      AV = (AX || VV) & AX = (AV || VX) by A1, A2, Def8;

      then

       A4: AV = AX by A3, RELAT_1: 72;

      set MX = the Mult of X;

      set MV = the Mult of V;

      

       A5: MX = (MV | [: COMPLEX , VX:]) by A2, Def8;

      ( 0. V) = ( 0. X) & MV = (MX | [: COMPLEX , VV:]) by A1, Def8;

      hence thesis by A3, A4, A5, RELAT_1: 72;

    end;

    theorem :: CLVECT_1:46

    

     Th46: V is Subspace of X & X is Subspace of Y implies V is Subspace of Y

    proof

      assume that

       A1: V is Subspace of X and

       A2: X is Subspace of Y;

      the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y by A1, A2, Def8;

      hence the carrier of V c= the carrier of Y;

      ( 0. V) = ( 0. X) by A1, Def8;

      hence ( 0. V) = ( 0. Y) by A2, Def8;

      thus the addF of V = (the addF of Y || the carrier of V)

      proof

        set AY = the addF of Y;

        set VX = the carrier of X;

        set AX = the addF of X;

        set VV = the carrier of V;

        set AV = the addF of V;

        VV c= VX by A1, Def8;

        then

         A3: [:VV, VV:] c= [:VX, VX:] by ZFMISC_1: 96;

        AV = (AX || VV) by A1, Def8;

        then AV = ((AY || VX) || VV) by A2, Def8;

        hence thesis by A3, FUNCT_1: 51;

      end;

      set MY = the Mult of Y;

      set MX = the Mult of X;

      set MV = the Mult of V;

      set VX = the carrier of X;

      set VV = the carrier of V;

      VV c= VX by A1, Def8;

      then

       A4: [: COMPLEX , VV:] c= [: COMPLEX , VX:] by ZFMISC_1: 95;

      MV = (MX | [: COMPLEX , VV:]) by A1, Def8;

      then MV = ((MY | [: COMPLEX , VX:]) | [: COMPLEX , VV:]) by A2, Def8;

      hence thesis by A4, FUNCT_1: 51;

    end;

    theorem :: CLVECT_1:47

    

     Th47: the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2

    proof

      set VW1 = the carrier of W1;

      set VW2 = the carrier of W2;

      set AV = the addF of V;

      set MV = the Mult of V;

      assume

       A1: the carrier of W1 c= the carrier of W2;

      then

       A2: [:VW1, VW1:] c= [:VW2, VW2:] by ZFMISC_1: 96;

      ( 0. W1) = ( 0. V) by Def8;

      hence the carrier of W1 c= the carrier of W2 & ( 0. W1) = ( 0. W2) by A1, Def8;

      the addF of W1 = (AV || VW1) & the addF of W2 = (AV || VW2) by Def8;

      hence the addF of W1 = (the addF of W2 || the carrier of W1) by A2, FUNCT_1: 51;

      

       A3: [: COMPLEX , VW1:] c= [: COMPLEX , VW2:] by A1, ZFMISC_1: 95;

      the Mult of W1 = (MV | [: COMPLEX , VW1:]) & the Mult of W2 = (MV | [: COMPLEX , VW2:]) by Def8;

      hence thesis by A3, FUNCT_1: 51;

    end;

    theorem :: CLVECT_1:48

    (for v st v in W1 holds v in W2) implies W1 is Subspace of W2

    proof

      assume

       A1: for v st v in W1 holds v in W2;

      the carrier of W1 c= the carrier of W2

      proof

        let x be object;

        assume

         A2: x in the carrier of W1;

        the carrier of W1 c= the carrier of V by Def8;

        then

        reconsider v = x as VECTOR of V by A2;

        v in W1 by A2;

        then v in W2 by A1;

        hence thesis;

      end;

      hence thesis by Th47;

    end;

    registration

      let V;

      cluster strict for Subspace of V;

      existence

      proof

        the carrier of V is Subset of V iff the carrier of V c= the carrier of V;

        then

        reconsider V1 = the carrier of V as Subset of V;

        the addF of V = (the addF of V || V1) & the Mult of V = (the Mult of V | [: COMPLEX , V1:]) by RELSET_1: 19;

        then CLSStruct (# the carrier of V, ( 0. V), the addF of V, the Mult of V #) is Subspace of V by Th43;

        hence thesis;

      end;

    end

    theorem :: CLVECT_1:49

    

     Th49: for W1,W2 be strict Subspace of V holds the carrier of W1 = the carrier of W2 implies W1 = W2

    proof

      let W1,W2 be strict Subspace of V;

      assume the carrier of W1 = the carrier of W2;

      then W1 is Subspace of W2 & W2 is Subspace of W1 by Th47;

      hence thesis by Th45;

    end;

    theorem :: CLVECT_1:50

    

     Th50: for W1,W2 be strict Subspace of V holds (for v holds v in W1 iff v in W2) implies W1 = W2

    proof

      let W1,W2 be strict Subspace of V;

      assume

       A1: for v holds v in W1 iff v in W2;

      for x be object holds x in the carrier of W1 iff x in the carrier of W2

      proof

        let x be object;

        thus x in the carrier of W1 implies x in the carrier of W2

        proof

          assume

           A2: x in the carrier of W1;

          the carrier of W1 c= the carrier of V by Def8;

          then

          reconsider v = x as VECTOR of V by A2;

          v in W1 by A2;

          then v in W2 by A1;

          hence thesis;

        end;

        assume

         A3: x in the carrier of W2;

        the carrier of W2 c= the carrier of V by Def8;

        then

        reconsider v = x as VECTOR of V by A3;

        v in W2 by A3;

        then v in W1 by A1;

        hence thesis;

      end;

      then the carrier of W1 = the carrier of W2 by TARSKI: 2;

      hence thesis by Th49;

    end;

    theorem :: CLVECT_1:51

    for V be strict ComplexLinearSpace, W be strict Subspace of V holds the carrier of W = the carrier of V implies W = V

    proof

      let V be strict ComplexLinearSpace, W be strict Subspace of V;

      assume

       A1: the carrier of W = the carrier of V;

      V is Subspace of V by Th44;

      hence thesis by A1, Th49;

    end;

    theorem :: CLVECT_1:52

    for V be strict ComplexLinearSpace, W be strict Subspace of V holds (for v be VECTOR of V holds v in W iff v in V) implies W = V

    proof

      let V be strict ComplexLinearSpace, W be strict Subspace of V;

      assume

       A1: for v be VECTOR of V holds v in W iff v in V;

      V is Subspace of V by Th44;

      hence thesis by A1, Th50;

    end;

    theorem :: CLVECT_1:53

    the carrier of W = V1 implies V1 is linearly-closed by Lm3;

    theorem :: CLVECT_1:54

    

     Th54: V1 <> {} & V1 is linearly-closed implies ex W be strict Subspace of V st V1 = the carrier of W

    proof

      assume that

       A1: V1 <> {} and

       A2: V1 is linearly-closed;

      reconsider D = V1 as non empty set by A1;

      set M = (the Mult of V | [: COMPLEX , V1:]);

      set VV = the carrier of V;

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

      then

       A3: ( dom M) = ( [: COMPLEX , VV:] /\ [: COMPLEX , V1:]) by RELAT_1: 61;

       [: COMPLEX , V1:] c= [: COMPLEX , VV:] by ZFMISC_1: 95;

      then

       A4: ( dom M) = [: COMPLEX , D:] by A3, XBOOLE_1: 28;

      now

        let y be object;

        thus y in D implies ex x be object st x in ( dom M) & y = (M . x)

        proof

          assume

           A5: y in D;

          then

          reconsider v1 = y as Element of VV;

          

           A6: [ 1r , y] in [: COMPLEX , D:] by A5, ZFMISC_1: 87;

          

          then (M . [ 1r , y]) = ( 1r * v1) by FUNCT_1: 49

          .= y by Def5;

          hence thesis by A4, A6;

        end;

        given x be object such that

         A7: x in ( dom M) and

         A8: y = (M . x);

        consider x1,x2 be object such that

         A9: x1 in COMPLEX and

         A10: x2 in D and

         A11: x = [x1, x2] by A4, A7, ZFMISC_1:def 2;

        reconsider xx1 = x1 as Element of COMPLEX by A9;

        reconsider v2 = x2 as Element of VV by A10;

         [x1, x2] in [: COMPLEX , V1:] by A9, A10, ZFMISC_1: 87;

        then y = (xx1 * v2) by A8, A11, FUNCT_1: 49;

        hence y in D by A2, A10;

      end;

      then D = ( rng M) by FUNCT_1:def 3;

      then

      reconsider M as Function of [: COMPLEX , D:], D by A4, FUNCT_2:def 1, RELSET_1: 4;

      set A = (the addF of V || V1);

      reconsider d1 = ( 0. V) as Element of D by A2, Th20;

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

      then ( dom A) = ( [:VV, VV:] /\ [:V1, V1:]) by RELAT_1: 61;

      then

       A12: ( dom A) = [:D, D:] by XBOOLE_1: 28, ZFMISC_1: 96;

      now

        let y be object;

        thus y in D implies ex x be object st x in ( dom A) & y = (A . x)

        proof

          assume

           A13: y in D;

          then

          reconsider v1 = y, v0 = d1 as Element of VV;

          

           A14: [d1, y] in [:D, D:] by A13, ZFMISC_1: 87;

          

          then (A . [d1, y]) = (v0 + v1) by FUNCT_1: 49

          .= y by RLVECT_1: 4;

          hence thesis by A12, A14;

        end;

        given x be object such that

         A15: x in ( dom A) and

         A16: y = (A . x);

        consider x1,x2 be object such that

         A17: x1 in D & x2 in D and

         A18: x = [x1, x2] by A12, A15, ZFMISC_1:def 2;

        reconsider v1 = x1, v2 = x2 as Element of VV by A17;

         [x1, x2] in [:V1, V1:] by A17, ZFMISC_1: 87;

        then y = (v1 + v2) by A16, A18, FUNCT_1: 49;

        hence y in D by A2, A17;

      end;

      then D = ( rng A) by FUNCT_1:def 3;

      then

      reconsider A as Function of [:D, D:], D by A12, FUNCT_2:def 1, RELSET_1: 4;

      set W = CLSStruct (# D, d1, A, M #);

      W is Subspace of V by Th43;

      hence thesis;

    end;

    definition

      let V;

      :: CLVECT_1:def9

      func (0). V -> strict Subspace of V means

      : Def9: the carrier of it = {( 0. V)};

      correctness by Th23, Th49, Th54;

    end

    definition

      let V;

      :: CLVECT_1:def10

      func (Omega). V -> strict Subspace of V equals the CLSStruct of V;

      coherence

      proof

        set W = the CLSStruct of V;

        

         A1: for u,v,w be VECTOR of W holds ((u + v) + w) = (u + (v + w))

        proof

          let u,v,w be VECTOR of W;

          reconsider u9 = u, v9 = v, w9 = w as VECTOR of V;

          

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

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

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

        end;

        

         A2: for v be VECTOR of W holds (v + ( 0. W)) = v

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

          thus (v + ( 0. W)) = (v9 + ( 0. V))

          .= v by RLVECT_1: 4;

        end;

        

         A3: W is right_complementable

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          consider w9 be VECTOR of V such that

           A4: (v9 + w9) = ( 0. V) by ALGSTR_0:def 11;

          reconsider w = w9 as VECTOR of W;

          take w;

          thus thesis by A4;

        end;

        

         A5: for z1, z2 holds for v be VECTOR of W holds ((z1 * z2) * v) = (z1 * (z2 * v))

        proof

          let z1, z2;

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

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

          .= (z1 * (z2 * v9)) by Def4

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

        end;

        

         A6: for z1, z2 holds for v be VECTOR of W holds ((z1 + z2) * v) = ((z1 * v) + (z2 * v))

        proof

          let z1, z2;

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

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

          .= ((z1 * v9) + (z2 * v9)) by Def3

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

        end;

        

         A7: for z holds for v,w be VECTOR of W holds (z * (v + w)) = ((z * v) + (z * w))

        proof

          let z;

          let v,w be VECTOR of W;

          reconsider v9 = v, w9 = w as VECTOR of V;

          

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

          .= ((z * v9) + (z * w9)) by Def2

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

        end;

        

         A8: for z holds for v,w be VECTOR of W, v9,w9 be VECTOR of V st v = v9 & w = w9 holds (v + w) = (v9 + w9) & (z * v) = (z * v9);

        

         A9: for v,w be VECTOR of W holds (v + w) = (w + v)

        proof

          let v,w be VECTOR of W;

          reconsider v9 = v, w9 = w as VECTOR of V;

          

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

          .= (w + v);

        end;

        for v be VECTOR of W holds ( 1r * v) = v

        proof

          let v be VECTOR of W;

          reconsider v9 = v as VECTOR of V;

          

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

          .= v by Def5;

        end;

        then

        reconsider W as ComplexLinearSpace by A9, A1, A2, A3, A7, A6, A5, Def2, Def3, Def4, Def5, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

        

         A10: the Mult of W = (the Mult of V | [: COMPLEX , the carrier of W:]) by RELSET_1: 19;

        ( 0. W) = ( 0. V) & the addF of W = (the addF of V || the carrier of W) by RELSET_1: 19;

        hence thesis by A10, Def8;

      end;

    end

    theorem :: CLVECT_1:55

    

     Th55: ( (0). W) = ( (0). V)

    proof

      the carrier of ( (0). W) = {( 0. W)} & the carrier of ( (0). V) = {( 0. V)} by Def9;

      then

       A1: the carrier of ( (0). W) = the carrier of ( (0). V) by Def8;

      ( (0). W) is Subspace of V by Th46;

      hence thesis by A1, Th49;

    end;

    theorem :: CLVECT_1:56

    

     Th56: ( (0). W1) = ( (0). W2)

    proof

      ( (0). W1) = ( (0). V) by Th55;

      hence thesis by Th55;

    end;

    theorem :: CLVECT_1:57

    ( (0). W) is Subspace of V by Th46;

    theorem :: CLVECT_1:58

    ( (0). V) is Subspace of W

    proof

      the carrier of ( (0). V) = {( 0. V)} by Def9

      .= {( 0. W)} by Def8;

      hence thesis by Th47;

    end;

    theorem :: CLVECT_1:59

    ( (0). W1) is Subspace of W2

    proof

      ( (0). W1) = ( (0). W2) by Th56;

      hence thesis;

    end;

    theorem :: CLVECT_1:60

    for V be strict ComplexLinearSpace holds V is Subspace of ( (Omega). V);

    definition

      let V;

      let v, W;

      :: CLVECT_1:def11

      func v + W -> Subset of V equals { (v + u) : u in W };

      coherence

      proof

        set Y = { (v + u) : u in W };

        defpred P[ object] means ex u st $1 = (v + u) & u in W;

        consider X be set such that

         A1: for x be object holds x in X iff x in the carrier of V & P[x] from XBOOLE_0:sch 1;

        X c= the carrier of V by A1;

        then

        reconsider X as Subset of V;

        

         A2: Y c= X

        proof

          let x be object;

          assume x in Y;

          then ex u st x = (v + u) & u in W;

          hence thesis by A1;

        end;

        X c= Y

        proof

          let x be object;

          assume x in X;

          then ex u st x = (v + u) & u in W by A1;

          hence thesis;

        end;

        hence thesis by A2, XBOOLE_0:def 10;

      end;

    end

    

     Lm5: (( 0. V) + W) = the carrier of W

    proof

      set A = { (( 0. V) + u) : u in W };

      

       A1: the carrier of W c= A

      proof

        let x be object;

        assume x in the carrier of W;

        then

         A2: x in W;

        then x in V by Th28;

        then

        reconsider y = x as Element of V;

        (( 0. V) + y) = x by RLVECT_1: 4;

        hence thesis by A2;

      end;

      A c= the carrier of W

      proof

        let x be object;

        assume x in A;

        then

        consider u such that

         A3: x = (( 0. V) + u) and

         A4: u in W;

        x = u by A3, RLVECT_1: 4;

        hence thesis by A4;

      end;

      hence thesis by A1;

    end;

    definition

      let V;

      let W;

      :: CLVECT_1:def12

      mode Coset of W -> Subset of V means

      : Def12: ex v st it = (v + W);

      existence

      proof

        reconsider VW = the carrier of W as Subset of V by Def8;

        take VW;

        take ( 0. V);

        thus thesis by Lm5;

      end;

    end

    reserve B,C for Coset of W;

    theorem :: CLVECT_1:61

    

     Th61: ( 0. V) in (v + W) iff v in W

    proof

      thus ( 0. V) in (v + W) implies v in W

      proof

        assume ( 0. V) in (v + W);

        then

        consider u such that

         A1: ( 0. V) = (v + u) and

         A2: u in W;

        v = ( - u) by A1, RLVECT_1:def 10;

        hence thesis by A2, Th41;

      end;

      assume v in W;

      then

       A3: ( - v) in W by Th41;

      ( 0. V) = (v - v) by RLVECT_1: 15

      .= (v + ( - v));

      hence thesis by A3;

    end;

    theorem :: CLVECT_1:62

    

     Th62: v in (v + W)

    proof

      (v + ( 0. V)) = v & ( 0. V) in W by Th36, RLVECT_1: 4;

      hence thesis;

    end;

    theorem :: CLVECT_1:63

    (( 0. V) + W) = the carrier of W by Lm5;

    theorem :: CLVECT_1:64

    

     Th64: (v + ( (0). V)) = {v}

    proof

      thus (v + ( (0). V)) c= {v}

      proof

        let x be object;

        assume x in (v + ( (0). V));

        then

        consider u such that

         A1: x = (v + u) and

         A2: u in ( (0). V);

        

         A3: the carrier of ( (0). V) = {( 0. V)} by Def9;

        u in the carrier of ( (0). V) by A2;

        then u = ( 0. V) by A3, TARSKI:def 1;

        then x = v by A1, RLVECT_1: 4;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {v};

      then

       A4: x = v by TARSKI:def 1;

      ( 0. V) in ( (0). V) & v = (v + ( 0. V)) by Th36, RLVECT_1: 4;

      hence thesis by A4;

    end;

    

     Lm6: v in W iff (v + W) = the carrier of W

    proof

      ( 0. V) in W & (v + ( 0. V)) = v by Th36, RLVECT_1: 4;

      then

       A1: v in { (v + u) : u in W };

      thus v in W implies (v + W) = the carrier of W

      proof

        assume

         A2: v in W;

        thus (v + W) c= the carrier of W

        proof

          let x be object;

          assume x in (v + W);

          then

          consider u such that

           A3: x = (v + u) and

           A4: u in W;

          (v + u) in W by A2, A4, Th39;

          hence thesis by A3;

        end;

        let x be object;

        assume x in the carrier of W;

        then

        reconsider y = x, z = v as Element of W by A2;

        reconsider y1 = y, z1 = z as VECTOR of V by Th29;

        

         A5: (z + (y - z)) = ((y + z) - z) by RLVECT_1:def 3

        .= (y + (z - z)) by RLVECT_1:def 3

        .= (y + ( 0. W)) by RLVECT_1: 15

        .= x by RLVECT_1: 4;

        (y - z) in W;

        then

         A6: (y1 - z1) in W by Th35;

        (y - z) = (y1 - z1) by Th35;

        then (z1 + (y1 - z1)) = x by A5, Th32;

        hence thesis by A6;

      end;

      assume

       A7: (v + W) = the carrier of W;

      assume not v in W;

      hence thesis by A7, A1;

    end;

    theorem :: CLVECT_1:65

    

     Th65: (v + ( (Omega). V)) = the carrier of V by STRUCT_0:def 5, Lm6;

    theorem :: CLVECT_1:66

    

     Th66: ( 0. V) in (v + W) iff (v + W) = the carrier of W by Th61, Lm6;

    theorem :: CLVECT_1:67

    v in W iff (v + W) = the carrier of W by Lm6;

    theorem :: CLVECT_1:68

    

     Th68: v in W implies ((z * v) + W) = the carrier of W

    proof

      assume

       A1: v in W;

      thus ((z * v) + W) c= the carrier of W

      proof

        let x be object;

        assume x in ((z * v) + W);

        then

        consider u such that

         A2: x = ((z * v) + u) and

         A3: u in W;

        (z * v) in W by A1, Th40;

        then ((z * v) + u) in W by A3, Th39;

        hence thesis by A2;

      end;

      let x be object;

      assume

       A4: x in the carrier of W;

      then

       A5: x in W;

      the carrier of W c= the carrier of V by Def8;

      then

      reconsider y = x as Element of V by A4;

      

       A6: ((z * v) + (y - (z * v))) = ((y + (z * v)) - (z * v)) by RLVECT_1:def 3

      .= (y + ((z * v) - (z * v))) by RLVECT_1:def 3

      .= (y + ( 0. V)) by RLVECT_1: 15

      .= x by RLVECT_1: 4;

      (z * v) in W by A1, Th40;

      then (y - (z * v)) in W by A5, Th42;

      hence thesis by A6;

    end;

    theorem :: CLVECT_1:69

    

     Th69: z <> 0 & ((z * v) + W) = the carrier of W implies v in W

    proof

      assume that

       A1: z <> 0 and

       A2: ((z * v) + W) = the carrier of W;

      assume not v in W;

      then not ( 1r * v) in W by Def5;

      then not (((z " ) * z) * v) in W by A1, XCMPLX_0:def 7;

      then not ((z " ) * (z * v)) in W by Def4;

      then

       A3: not (z * v) in W by Th40;

      ( 0. V) in W & ((z * v) + ( 0. V)) = (z * v) by Th36, RLVECT_1: 4;

      then (z * v) in { ((z * v) + u) : u in W };

      hence contradiction by A2, A3;

    end;

    theorem :: CLVECT_1:70

    

     Th70: v in W iff (( - v) + W) = the carrier of W

    proof

      v in W iff ((( - 1r ) * v) + W) = the carrier of W by Th68, Th69;

      hence thesis by Th3;

    end;

    theorem :: CLVECT_1:71

    

     Th71: u in W iff (v + W) = ((v + u) + W)

    proof

      thus u in W implies (v + W) = ((v + u) + W)

      proof

        assume

         A1: u in W;

        thus (v + W) c= ((v + u) + W)

        proof

          let x be object;

          assume x in (v + W);

          then

          consider v1 such that

           A2: x = (v + v1) and

           A3: v1 in W;

          

           A4: ((v + u) + (v1 - u)) = (v + (u + (v1 - u))) by RLVECT_1:def 3

          .= (v + ((v1 + u) - u)) by RLVECT_1:def 3

          .= (v + (v1 + (u - u))) by RLVECT_1:def 3

          .= (v + (v1 + ( 0. V))) by RLVECT_1: 15

          .= x by A2, RLVECT_1: 4;

          (v1 - u) in W by A1, A3, Th42;

          hence thesis by A4;

        end;

        let x be object;

        assume x in ((v + u) + W);

        then

        consider v2 such that

         A5: x = ((v + u) + v2) and

         A6: v2 in W;

        

         A7: x = (v + (u + v2)) by A5, RLVECT_1:def 3;

        (u + v2) in W by A1, A6, Th39;

        hence thesis by A7;

      end;

      assume

       A8: (v + W) = ((v + u) + W);

      ( 0. V) in W & (v + ( 0. V)) = v by Th36, RLVECT_1: 4;

      then v in ((v + u) + W) by A8;

      then

      consider u1 such that

       A9: v = ((v + u) + u1) and

       A10: u1 in W;

      v = (v + ( 0. V)) & v = (v + (u + u1)) by A9, RLVECT_1: 4, RLVECT_1:def 3;

      then (u + u1) = ( 0. V) by RLVECT_1: 8;

      then u = ( - u1) by RLVECT_1:def 10;

      hence thesis by A10, Th41;

    end;

    theorem :: CLVECT_1:72

    u in W iff (v + W) = ((v - u) + W)

    proof

      

       A1: ( - u) in W implies u in W

      proof

        assume ( - u) in W;

        then ( - ( - u)) in W by Th41;

        hence thesis by RLVECT_1: 17;

      end;

      ( - u) in W iff (v + W) = ((v + ( - u)) + W) by Th71;

      hence thesis by A1, Th41;

    end;

    theorem :: CLVECT_1:73

    

     Th73: v in (u + W) iff (u + W) = (v + W)

    proof

      thus v in (u + W) implies (u + W) = (v + W)

      proof

        assume v in (u + W);

        then

        consider z be VECTOR of V such that

         A1: v = (u + z) and

         A2: z in W;

        thus (u + W) c= (v + W)

        proof

          let x be object;

          assume x in (u + W);

          then

          consider v1 such that

           A3: x = (u + v1) and

           A4: v1 in W;

          (v - z) = (u + (z - z)) by A1, RLVECT_1:def 3

          .= (u + ( 0. V)) by RLVECT_1: 15

          .= u by RLVECT_1: 4;

          

          then

           A5: x = (v + (v1 + ( - z))) by A3, RLVECT_1:def 3

          .= (v + (v1 - z));

          (v1 - z) in W by A2, A4, Th42;

          hence thesis by A5;

        end;

        let x be object;

        assume x in (v + W);

        then

        consider v2 such that

         A6: x = (v + v2) & v2 in W;

        (z + v2) in W & x = (u + (z + v2)) by A1, A2, A6, Th39, RLVECT_1:def 3;

        hence thesis;

      end;

      thus thesis by Th62;

    end;

    theorem :: CLVECT_1:74

    

     Th74: (v + W) = (( - v) + W) iff v in W

    proof

      thus (v + W) = (( - v) + W) implies v in W

      proof

        assume (v + W) = (( - v) + W);

        then v in (( - v) + W) by Th62;

        then

        consider u such that

         A1: v = (( - v) + u) and

         A2: u in W;

        ( 0. V) = (v - (( - v) + u)) by A1, RLVECT_1: 15

        .= ((v - ( - v)) - u) by RLVECT_1: 27

        .= ((v + v) - u) by RLVECT_1: 17

        .= ((( 1r * v) + v) - u) by Def5

        .= ((( 1r * v) + ( 1r * v)) - u) by Def5

        .= ((( 1r + 1r ) * v) - u) by Def3;

        then ((( 1r + 1r ) " ) * (( 1r + 1r ) * v)) = ((( 1r + 1r ) " ) * u) by RLVECT_1: 21;

        then (((( 1r + 1r ) " ) * ( 1r + 1r )) * v) = ((( 1r + 1r ) " ) * u) by Def4;

        then v = ((( 1r + 1r ) " ) * u) by Def5;

        hence thesis by A2, Th40;

      end;

      assume

       A3: v in W;

      then (v + W) = the carrier of W by Lm6;

      hence thesis by A3, Th70;

    end;

    theorem :: CLVECT_1:75

    

     Th75: u in (v1 + W) & u in (v2 + W) implies (v1 + W) = (v2 + W)

    proof

      assume that

       A1: u in (v1 + W) and

       A2: u in (v2 + W);

      consider x1 be VECTOR of V such that

       A3: u = (v1 + x1) and

       A4: x1 in W by A1;

      consider x2 be VECTOR of V such that

       A5: u = (v2 + x2) and

       A6: x2 in W by A2;

      thus (v1 + W) c= (v2 + W)

      proof

        let x be object;

        assume x in (v1 + W);

        then

        consider u1 such that

         A7: x = (v1 + u1) and

         A8: u1 in W;

        (x2 - x1) in W by A4, A6, Th42;

        then

         A9: ((x2 - x1) + u1) in W by A8, Th39;

        (u - x1) = (v1 + (x1 - x1)) by A3, RLVECT_1:def 3

        .= (v1 + ( 0. V)) by RLVECT_1: 15

        .= v1 by RLVECT_1: 4;

        

        then x = ((v2 + (x2 - x1)) + u1) by A5, A7, RLVECT_1:def 3

        .= (v2 + ((x2 - x1) + u1)) by RLVECT_1:def 3;

        hence thesis by A9;

      end;

      let x be object;

      assume x in (v2 + W);

      then

      consider u1 such that

       A10: x = (v2 + u1) and

       A11: u1 in W;

      (x1 - x2) in W by A4, A6, Th42;

      then

       A12: ((x1 - x2) + u1) in W by A11, Th39;

      (u - x2) = (v2 + (x2 - x2)) by A5, RLVECT_1:def 3

      .= (v2 + ( 0. V)) by RLVECT_1: 15

      .= v2 by RLVECT_1: 4;

      

      then x = ((v1 + (x1 - x2)) + u1) by A3, A10, RLVECT_1:def 3

      .= (v1 + ((x1 - x2) + u1)) by RLVECT_1:def 3;

      hence thesis by A12;

    end;

    theorem :: CLVECT_1:76

    u in (v + W) & u in (( - v) + W) implies v in W by Th75, Th74;

    theorem :: CLVECT_1:77

    

     Th77: z <> 1r & (z * v) in (v + W) implies v in W

    proof

      assume that

       A1: z <> 1r and

       A2: (z * v) in (v + W);

      

       A3: (z - 1r ) <> 0 by A1;

      consider u such that

       A4: (z * v) = (v + u) and

       A5: u in W by A2;

      u = (u + ( 0. V)) by RLVECT_1: 4

      .= (u + (v - v)) by RLVECT_1: 15

      .= ((z * v) - v) by A4, RLVECT_1:def 3

      .= ((z * v) - ( 1r * v)) by Def5

      .= ((z - 1r ) * v) by Th10;

      then (((z - 1r ) " ) * u) = ((((z - 1r ) " ) * (z - 1r )) * v) by Def4;

      then ( 1r * v) = (((z - 1r ) " ) * u) by A3, XCMPLX_0:def 7;

      then v = (((z - 1r ) " ) * u) by Def5;

      hence thesis by A5, Th40;

    end;

    theorem :: CLVECT_1:78

    

     Th78: v in W implies (z * v) in (v + W)

    proof

      assume v in W;

      then

       A1: ((z - 1r ) * v) in W by Th40;

      (z * v) = (((z - 1r ) + 1r ) * v)

      .= (((z - 1r ) * v) + ( 1r * v)) by Def3

      .= (v + ((z - 1r ) * v)) by Def5;

      hence thesis by A1;

    end;

    theorem :: CLVECT_1:79

    ( - v) in (v + W) iff v in W

    proof

      (( - 1r ) * v) = ( - v) by Th3;

      hence thesis by Th77, Th78;

    end;

    theorem :: CLVECT_1:80

    

     Th80: (u + v) in (v + W) iff u in W

    proof

      thus (u + v) in (v + W) implies u in W

      proof

        assume (u + v) in (v + W);

        then ex v1 st (u + v) = (v + v1) & v1 in W;

        hence thesis by RLVECT_1: 8;

      end;

      assume u in W;

      hence thesis;

    end;

    theorem :: CLVECT_1:81

    (v - u) in (v + W) iff u in W

    proof

      

       A1: (v - u) = (( - u) + v);

      

       A2: ( - u) in W implies ( - ( - u)) in W by Th41;

      u in W implies ( - u) in W by Th41;

      hence thesis by A1, A2, Th80, RLVECT_1: 17;

    end;

    theorem :: CLVECT_1:82

    

     Th82: u in (v + W) iff ex v1 st v1 in W & u = (v + v1)

    proof

      thus u in (v + W) implies ex v1 st v1 in W & u = (v + v1)

      proof

        assume u in (v + W);

        then ex v1 st u = (v + v1) & v1 in W;

        hence thesis;

      end;

      given v1 such that

       A1: v1 in W & u = (v + v1);

      thus thesis by A1;

    end;

    theorem :: CLVECT_1:83

    u in (v + W) iff ex v1 st v1 in W & u = (v - v1)

    proof

      thus u in (v + W) implies ex v1 st v1 in W & u = (v - v1)

      proof

        assume u in (v + W);

        then

        consider v1 such that

         A1: u = (v + v1) and

         A2: v1 in W;

        take x = ( - v1);

        thus x in W by A2, Th41;

        thus thesis by A1, RLVECT_1: 17;

      end;

      given v1 such that

       A3: v1 in W and

       A4: u = (v - v1);

      ( - v1) in W by A3, Th41;

      hence thesis by A4;

    end;

    theorem :: CLVECT_1:84

    

     Th84: (ex v st v1 in (v + W) & v2 in (v + W)) iff (v1 - v2) in W

    proof

      thus (ex v st v1 in (v + W) & v2 in (v + W)) implies (v1 - v2) in W

      proof

        given v such that

         A1: v1 in (v + W) and

         A2: v2 in (v + W);

        consider u2 such that

         A3: u2 in W and

         A4: v2 = (v + u2) by A2, Th82;

        consider u1 such that

         A5: u1 in W and

         A6: v1 = (v + u1) by A1, Th82;

        (v1 - v2) = ((u1 + v) + (( - v) - u2)) by A6, A4, RLVECT_1: 30

        .= (((u1 + v) + ( - v)) - u2) by RLVECT_1:def 3

        .= ((u1 + (v + ( - v))) - u2) by RLVECT_1:def 3

        .= ((u1 + ( 0. V)) - u2) by RLVECT_1: 5

        .= (u1 - u2) by RLVECT_1: 4;

        hence thesis by A5, A3, Th42;

      end;

      assume (v1 - v2) in W;

      then

       A7: ( - (v1 - v2)) in W by Th41;

      take v1;

      thus v1 in (v1 + W) by Th62;

      (v1 + ( - (v1 - v2))) = (v1 + (( - v1) + v2)) by RLVECT_1: 33

      .= ((v1 + ( - v1)) + v2) by RLVECT_1:def 3

      .= (( 0. V) + v2) by RLVECT_1: 5

      .= v2 by RLVECT_1: 4;

      hence thesis by A7;

    end;

    theorem :: CLVECT_1:85

    

     Th85: (v + W) = (u + W) implies ex v1 st v1 in W & (v + v1) = u

    proof

      assume (v + W) = (u + W);

      then v in (u + W) by Th62;

      then

      consider u1 such that

       A1: v = (u + u1) and

       A2: u1 in W;

      take v1 = (u - v);

      ( 0. V) = ((u + u1) - v) by A1, RLVECT_1: 15

      .= (u1 + (u - v)) by RLVECT_1:def 3;

      then v1 = ( - u1) by RLVECT_1:def 10;

      hence v1 in W by A2, Th41;

      

      thus (v + v1) = ((u + v) - v) by RLVECT_1:def 3

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

      .= (u + ( 0. V)) by RLVECT_1: 15

      .= u by RLVECT_1: 4;

    end;

    theorem :: CLVECT_1:86

    

     Th86: (v + W) = (u + W) implies ex v1 st v1 in W & (v - v1) = u

    proof

      assume (v + W) = (u + W);

      then u in (v + W) by Th62;

      then

      consider u1 such that

       A1: u = (v + u1) and

       A2: u1 in W;

      take v1 = (v - u);

      ( 0. V) = ((v + u1) - u) by A1, RLVECT_1: 15

      .= (u1 + (v - u)) by RLVECT_1:def 3;

      then v1 = ( - u1) by RLVECT_1:def 10;

      hence v1 in W by A2, Th41;

      

      thus (v - v1) = ((v - v) + u) by RLVECT_1: 29

      .= (( 0. V) + u) by RLVECT_1: 15

      .= u by RLVECT_1: 4;

    end;

    theorem :: CLVECT_1:87

    

     Th87: for W1,W2 be strict Subspace of V holds (v + W1) = (v + W2) iff W1 = W2

    proof

      let W1,W2 be strict Subspace of V;

      thus (v + W1) = (v + W2) implies W1 = W2

      proof

        assume

         A1: (v + W1) = (v + W2);

        the carrier of W1 = the carrier of W2

        proof

          

           A2: the carrier of W1 c= the carrier of V by Def8;

          thus the carrier of W1 c= the carrier of W2

          proof

            let x be object;

            assume

             A3: x in the carrier of W1;

            then

            reconsider y = x as Element of V by A2;

            set z = (v + y);

            x in W1 by A3;

            then z in (v + W2) by A1;

            then

            consider u such that

             A4: z = (v + u) and

             A5: u in W2;

            y = u by A4, RLVECT_1: 8;

            hence thesis by A5;

          end;

          let x be object;

          assume

           A6: x in the carrier of W2;

          the carrier of W2 c= the carrier of V by Def8;

          then

          reconsider y = x as Element of V by A6;

          set z = (v + y);

          x in W2 by A6;

          then z in (v + W1) by A1;

          then

          consider u such that

           A7: z = (v + u) and

           A8: u in W1;

          y = u by A7, RLVECT_1: 8;

          hence thesis by A8;

        end;

        hence thesis by Th49;

      end;

      thus thesis;

    end;

    theorem :: CLVECT_1:88

    

     Th88: for W1,W2 be strict Subspace of V holds (v + W1) = (u + W2) implies W1 = W2

    proof

      let W1,W2 be strict Subspace of V;

      assume

       A1: (v + W1) = (u + W2);

      set V2 = the carrier of W2;

      set V1 = the carrier of W1;

      assume

       A2: W1 <> W2;

       A3:

      now

        set x = the Element of (V1 \ V2);

        assume (V1 \ V2) <> {} ;

        then x in V1 by XBOOLE_0:def 5;

        then

         A4: x in W1;

        then x in V by Th28;

        then

        reconsider x as Element of V;

        set z = (v + x);

        z in (u + W2) by A1, A4;

        then

        consider u1 such that

         A5: z = (u + u1) and

         A6: u1 in W2;

        x = (( 0. V) + x) by RLVECT_1: 4

        .= ((v - v) + x) by RLVECT_1: 15

        .= (( - v) + (u + u1)) by A5, RLVECT_1:def 3;

        then

         A7: ((v + (( - v) + (u + u1))) + W1) = (v + W1) by A4, Th71;

        (v + (( - v) + (u + u1))) = ((v - v) + (u + u1)) by RLVECT_1:def 3

        .= (( 0. V) + (u + u1)) by RLVECT_1: 15

        .= (u + u1) by RLVECT_1: 4;

        then ((u + u1) + W2) = ((u + u1) + W1) by A1, A6, A7, Th71;

        hence thesis by A2, Th87;

      end;

       A8:

      now

        set x = the Element of (V2 \ V1);

        assume (V2 \ V1) <> {} ;

        then x in V2 by XBOOLE_0:def 5;

        then

         A9: x in W2;

        then x in V by Th28;

        then

        reconsider x as Element of V;

        set z = (u + x);

        z in (v + W1) by A1, A9;

        then

        consider u1 such that

         A10: z = (v + u1) and

         A11: u1 in W1;

        x = (( 0. V) + x) by RLVECT_1: 4

        .= ((u - u) + x) by RLVECT_1: 15

        .= (( - u) + (v + u1)) by A10, RLVECT_1:def 3;

        then

         A12: ((u + (( - u) + (v + u1))) + W2) = (u + W2) by A9, Th71;

        (u + (( - u) + (v + u1))) = ((u - u) + (v + u1)) by RLVECT_1:def 3

        .= (( 0. V) + (v + u1)) by RLVECT_1: 15

        .= (v + u1) by RLVECT_1: 4;

        then ((v + u1) + W1) = ((v + u1) + W2) by A1, A11, A12, Th71;

        hence thesis by A2, Th87;

      end;

      V1 <> V2 by A2, Th49;

      then not V1 c= V2 or not V2 c= V1;

      hence thesis by A3, A8, XBOOLE_1: 37;

    end;

    theorem :: CLVECT_1:89

    C is linearly-closed iff C = the carrier of W

    proof

      thus C is linearly-closed implies C = the carrier of W

      proof

        assume

         A1: C is linearly-closed;

        consider v such that

         A2: C = (v + W) by Def12;

        C <> {} by A2, Th62;

        then ( 0. V) in (v + W) by A1, A2, Th20;

        hence thesis by A2, Th66;

      end;

      thus thesis by Lm3;

    end;

    theorem :: CLVECT_1:90

    for W1,W2 be strict Subspace of V, C1 be Coset of W1, C2 be Coset of W2 holds C1 = C2 implies W1 = W2

    proof

      let W1,W2 be strict Subspace of V, C1 be Coset of W1, C2 be Coset of W2;

      (ex v1 st C1 = (v1 + W1)) & ex v2 st C2 = (v2 + W2) by Def12;

      hence thesis by Th88;

    end;

    theorem :: CLVECT_1:91

     {v} is Coset of ( (0). V)

    proof

      (v + ( (0). V)) = {v} by Th64;

      hence thesis by Def12;

    end;

    theorem :: CLVECT_1:92

    V1 is Coset of ( (0). V) implies ex v st V1 = {v}

    proof

      assume V1 is Coset of ( (0). V);

      then

      consider v such that

       A1: V1 = (v + ( (0). V)) by Def12;

      take v;

      thus thesis by A1, Th64;

    end;

    theorem :: CLVECT_1:93

    the carrier of W is Coset of W

    proof

      the carrier of W = (( 0. V) + W) by Lm5;

      hence thesis by Def12;

    end;

    theorem :: CLVECT_1:94

    the carrier of V is Coset of ( (Omega). V)

    proof

      set v = the VECTOR of V;

      the carrier of V is Subset of V iff the carrier of V c= the carrier of V;

      then

      reconsider A = the carrier of V as Subset of V;

      A = (v + ( (Omega). V)) by Th65;

      hence thesis by Def12;

    end;

    theorem :: CLVECT_1:95

    V1 is Coset of ( (Omega). V) implies V1 = the carrier of V

    proof

      assume V1 is Coset of ( (Omega). V);

      then ex v st V1 = (v + ( (Omega). V)) by Def12;

      hence thesis by Th65;

    end;

    theorem :: CLVECT_1:96

    ( 0. V) in C iff C = the carrier of W

    proof

      ex v st C = (v + W) by Def12;

      hence thesis by Th66;

    end;

    theorem :: CLVECT_1:97

    

     Th97: u in C iff C = (u + W)

    proof

      thus u in C implies C = (u + W)

      proof

        assume

         A1: u in C;

        ex v st C = (v + W) by Def12;

        hence thesis by A1, Th73;

      end;

      thus thesis by Th62;

    end;

    theorem :: CLVECT_1:98

    u in C & v in C implies ex v1 st v1 in W & (u + v1) = v

    proof

      assume u in C & v in C;

      then C = (u + W) & C = (v + W) by Th97;

      hence thesis by Th85;

    end;

    theorem :: CLVECT_1:99

    u in C & v in C implies ex v1 st v1 in W & (u - v1) = v

    proof

      assume u in C & v in C;

      then C = (u + W) & C = (v + W) by Th97;

      hence thesis by Th86;

    end;

    theorem :: CLVECT_1:100

    (ex C st v1 in C & v2 in C) iff (v1 - v2) in W

    proof

      thus (ex C st v1 in C & v2 in C) implies (v1 - v2) in W

      proof

        given C such that

         A1: v1 in C & v2 in C;

        ex v st C = (v + W) by Def12;

        hence thesis by A1, Th84;

      end;

      assume (v1 - v2) in W;

      then

      consider v such that

       A2: v1 in (v + W) & v2 in (v + W) by Th84;

      reconsider C = (v + W) as Coset of W by Def12;

      take C;

      thus thesis by A2;

    end;

    theorem :: CLVECT_1:101

    u in B & u in C implies B = C

    proof

      assume

       A1: u in B & u in C;

      (ex v1 st B = (v1 + W)) & ex v2 st C = (v2 + W) by Def12;

      hence thesis by A1, Th75;

    end;

    begin

    definition

      struct ( CLSStruct, N-ZeroStr) CNORMSTR (# 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 normF -> Function of the carrier, REAL #)

       attr strict strict;

    end

    registration

      cluster non empty for CNORMSTR;

      existence

      proof

        set A = the non empty set, Z = the Element of A, a = the BinOp of A, M = the Function of [: COMPLEX , A:], A, n = the Function of A, REAL ;

        take CNORMSTR (# A, Z, a, M, n #);

        thus the carrier of CNORMSTR (# A, Z, a, M, n #) is non empty;

      end;

    end

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

    set V = the ComplexLinearSpace;

    

     Lm7: the carrier of ( (0). V) = {( 0. V)} by Def9;

    reconsider niltonil = (the carrier of ( (0). V) --> ( In ( 0 , REAL ))) as Function of the carrier of ( (0). V), REAL ;

    ( 0. V) is VECTOR of ( (0). V) by Lm7, TARSKI:def 1;

    then

     Lm8: (niltonil . ( 0. V)) = 0 by FUNCOP_1: 7;

    

     Lm9: for u be VECTOR of ( (0). V), z holds (niltonil . (z * u)) = ( |.z.| * (niltonil . u))

    proof

      let u be VECTOR of ( (0). V);

      let z;

      (niltonil . u) = 0 by FUNCOP_1: 7;

      hence thesis by FUNCOP_1: 7;

    end;

    

     Lm10: for u,v be VECTOR of ( (0). V) holds (niltonil . (u + v)) <= ((niltonil . u) + (niltonil . v))

    proof

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

      u = ( 0. V) & v = ( 0. V) by Lm7, TARSKI:def 1;

      hence thesis by Lm7, Lm8, TARSKI:def 1;

    end;

    reconsider X = CNORMSTR (# the carrier of ( (0). V), ( 0. ( (0). V)), the addF of ( (0). V), the Mult of ( (0). V), niltonil #) as non empty CNORMSTR;

     Lm11:

    now

      let x,y be Point of X;

      let z;

      reconsider u = x, w = y as VECTOR of ( (0). V);

       09(X) = ( 0. V) by Def8;

      hence ||.x.|| = 0 iff x = 09(X) by Lm7, FUNCOP_1: 7, TARSKI:def 1;

      (z * x) = (z * u);

      hence ||.(z * x).|| = ( |.z.| * ||.x.||) by Lm9;

      (x + y) = (u + w);

      hence ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by Lm10;

    end;

    definition

      let IT be non empty CNORMSTR;

      :: CLVECT_1:def13

      attr IT is ComplexNormSpace-like means

      : Def13: for x,y be Point of IT, z holds ||.(z * x).|| = ( |.z.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||);

    end

    registration

      cluster reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict for non empty CNORMSTR;

      existence

      proof

        take X;

        thus X is reflexive by Lm11;

        thus X is discerning ComplexNormSpace-like by Lm11;

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

        proof

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

          proof

            let z;

            let v,w be VECTOR of X;

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

            

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

            .= ((z * v9) + (z * w9)) by Def2

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

          end;

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

          proof

            let z1, z2;

            let v be VECTOR of X;

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

            

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

            .= ((z1 * v9) + (z2 * v9)) by Def3

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

          end;

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

          proof

            let z1, z2;

            let v be VECTOR of X;

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

            

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

            .= (z1 * (z2 * v9)) by Def4

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

          end;

          let v be VECTOR of X;

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

          

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

          .= v by Def5;

        end;

        

         A1: for x,y be VECTOR of X holds for x9,y9 be VECTOR of ( (0). V) st x = x9 & y = y9 holds (x + y) = (x9 + y9) & for z holds (z * x) = (z * x9);

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

        proof

          let v,w be VECTOR of X;

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

          

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

          .= (w + v);

        end;

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

        proof

          let u,v,w be VECTOR of X;

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

          

          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 X holds (v + ( 0. X)) = v

        proof

          let v be VECTOR of X;

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

          

          thus (v + ( 0. X)) = (v9 + ( 0. ( (0). V)))

          .= v by RLVECT_1: 4;

        end;

        thus X is right_complementable

        proof

          let v be VECTOR of X;

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

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

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

          reconsider w = w9 as VECTOR of X;

          take w;

          thus thesis by A2;

        end;

        thus thesis;

      end;

    end

    definition

      mode ComplexNormSpace is reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty CNORMSTR;

    end

    reserve CNS for ComplexNormSpace;

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

    theorem :: CLVECT_1:102

     ||.( 0. CNS).|| = 0 ;

    theorem :: CLVECT_1:103

    

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

    proof

      

       A1: |.( - 1r ).| = 1 by COMPLEX1: 48, COMPLEX1: 52;

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

      .= ( |.( - 1r ).| * ||.x.||) by Def13;

      hence thesis by A1;

    end;

    theorem :: CLVECT_1:104

    

     Th104: ||.(x - y).|| <= ( ||.x.|| + ||.y.||)

    proof

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

      hence thesis by Th103;

    end;

    theorem :: CLVECT_1:105

    

     Th105: 0 <= ||.x.||

    proof

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

      .= 0 ;

      then 0 <= (( ||.x.|| + ||.x.||) / 2) by Th104;

      hence thesis;

    end;

    theorem :: CLVECT_1:106

     ||.((z1 * x) + (z2 * y)).|| <= (( |.z1.| * ||.x.||) + ( |.z2.| * ||.y.||))

    proof

       ||.((z1 * x) + (z2 * y)).|| <= ( ||.(z1 * x).|| + ||.(z2 * y).||) by Def13;

      then ||.((z1 * x) + (z2 * y)).|| <= (( |.z1.| * ||.x.||) + ||.(z2 * y).||) by Def13;

      hence thesis by Def13;

    end;

    theorem :: CLVECT_1:107

    

     Th107: ||.(x - y).|| = 0 iff x = y

    proof

       ||.(x - y).|| = 0 iff (x - y) = 09(CNS) by NORMSP_0:def 5;

      hence thesis by RLVECT_1: 15, RLVECT_1: 21;

    end;

    theorem :: CLVECT_1:108

    

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

    proof

      (x - y) = ( - (y - x)) by RLVECT_1: 33;

      hence thesis by Th103;

    end;

    theorem :: CLVECT_1:109

    

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

    proof

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

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

      .= x by RLVECT_1: 13;

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

      hence thesis by XREAL_1: 20;

    end;

    theorem :: CLVECT_1:110

    

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

    proof

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

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

      .= y by RLVECT_1: 13;

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

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

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

      then

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

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

      hence thesis by A1, ABSVALUE: 5;

    end;

    theorem :: CLVECT_1:111

    

     Th111: ||.(x - w).|| <= ( ||.(x - y).|| + ||.(y - w).||)

    proof

      (x - w) = (x + ( 09(CNS) + ( - w))) by RLVECT_1: 4

      .= (x + ((( - y) + y) + ( - w))) by RLVECT_1: 5

      .= (x + (( - y) + (y + ( - w)))) by RLVECT_1:def 3

      .= ((x - y) + (y - w)) by RLVECT_1:def 3;

      hence thesis by Def13;

    end;

    theorem :: CLVECT_1:112

    x <> y implies ||.(x - y).|| <> 0 by Th107;

    reserve S,S1,S2 for sequence of CNS;

    reserve n,m,m1,m2 for Nat;

    reserve r for Real;

    definition

      let CNS be ComplexLinearSpace;

      let S be sequence of CNS;

      let z;

      :: CLVECT_1:def14

      func z * S -> sequence of CNS means

      : Def14: for n holds (it . n) = (z * (S . n));

      existence

      proof

        deffunc F( Nat) = (z * (S . $1));

        consider S be sequence of CNS such that

         A1: for n be Element of NAT holds (S . n) = F(n) from FUNCT_2:sch 4;

        take S;

        let n;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of CNS;

        assume that

         A2: for n holds (S1 . n) = (z * (S . n)) and

         A3: for n holds (S2 . n) = (z * (S . n));

        for n be Element of NAT holds (S1 . n) = (S2 . n)

        proof

          let n be Element of NAT ;

          (S1 . n) = (z * (S . n)) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let CNS;

      let S;

      :: CLVECT_1:def15

      attr S is convergent means ex g st for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - g).|| < r;

    end

    theorem :: CLVECT_1:113

    

     Th113: S1 is convergent & S2 is convergent implies (S1 + S2) is convergent

    proof

      assume that

       A1: S1 is convergent and

       A2: S2 is convergent;

      consider g1 such that

       A3: for r st 0 < r holds ex m st for n st m <= n holds ||.((S1 . n) - g1).|| < r by A1;

      consider g2 such that

       A4: for r st 0 < r holds ex m st for n st m <= n holds ||.((S2 . n) - g2).|| < r by A2;

      take g = (g1 + g2);

      let r;

      assume

       A5: 0 < r;

      then

      consider m1 such that

       A6: for n st m1 <= n holds ||.((S1 . n) - g1).|| < (r / 2) by A3;

      consider m2 such that

       A7: for n st m2 <= n holds ||.((S2 . n) - g2).|| < (r / 2) by A4, A5;

      reconsider k = (m1 + m2) as Nat;

      take k;

      let n such that

       A8: k <= n;

      m2 <= k by NAT_1: 12;

      then m2 <= n by A8, XXREAL_0: 2;

      then

       A9: ||.((S2 . n) - g2).|| < (r / 2) by A7;

      

       A10: ||.(((S1 + S2) . n) - g).|| = ||.(( - (g1 + g2)) + ((S1 . n) + (S2 . n))).|| by NORMSP_1:def 2

      .= ||.((( - g1) + ( - g2)) + ((S1 . n) + (S2 . n))).|| by RLVECT_1: 31

      .= ||.(((S1 . n) + (( - g1) + ( - g2))) + (S2 . n)).|| by RLVECT_1:def 3

      .= ||.((((S1 . n) - g1) + ( - g2)) + (S2 . n)).|| by RLVECT_1:def 3

      .= ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| by RLVECT_1:def 3;

      

       A11: ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| <= ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) by Def13;

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

      then m1 <= n by A8, XXREAL_0: 2;

      then ||.((S1 . n) - g1).|| < (r / 2) by A6;

      then ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) < ((r / 2) + (r / 2)) by A9, XREAL_1: 8;

      hence thesis by A10, A11, XXREAL_0: 2;

    end;

    theorem :: CLVECT_1:114

    

     Th114: S1 is convergent & S2 is convergent implies (S1 - S2) is convergent

    proof

      assume that

       A1: S1 is convergent and

       A2: S2 is convergent;

      consider g1 such that

       A3: for r st 0 < r holds ex m st for n st m <= n holds ||.((S1 . n) - g1).|| < r by A1;

      consider g2 such that

       A4: for r st 0 < r holds ex m st for n st m <= n holds ||.((S2 . n) - g2).|| < r by A2;

      take g = (g1 - g2);

      let r;

      assume

       A5: 0 < r;

      then

      consider m1 such that

       A6: for n st m1 <= n holds ||.((S1 . n) - g1).|| < (r / 2) by A3;

      consider m2 such that

       A7: for n st m2 <= n holds ||.((S2 . n) - g2).|| < (r / 2) by A4, A5;

      take k = (m1 + m2);

      let n such that

       A8: k <= n;

      m2 <= k by NAT_1: 12;

      then m2 <= n by A8, XXREAL_0: 2;

      then

       A9: ||.((S2 . n) - g2).|| < (r / 2) by A7;

      

       A10: ||.(((S1 - S2) . n) - g).|| = ||.(((S1 . n) - (S2 . n)) - (g1 - g2)).|| by NORMSP_1:def 3

      .= ||.((((S1 . n) - (S2 . n)) - g1) + g2).|| by RLVECT_1: 29

      .= ||.(((S1 . n) - (g1 + (S2 . n))) + g2).|| by RLVECT_1: 27

      .= ||.((((S1 . n) - g1) - (S2 . n)) + g2).|| by RLVECT_1: 27

      .= ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| by RLVECT_1: 29;

      

       A11: ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| <= ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) by Th104;

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

      then m1 <= n by A8, XXREAL_0: 2;

      then ||.((S1 . n) - g1).|| < (r / 2) by A6;

      then ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) < ((r / 2) + (r / 2)) by A9, XREAL_1: 8;

      hence thesis by A10, A11, XXREAL_0: 2;

    end;

    theorem :: CLVECT_1:115

    

     Th115: S is convergent implies (S - x) is convergent

    proof

      assume S is convergent;

      then

      consider g such that

       A1: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - g).|| < r;

      take h = (g - x);

      let r;

      assume 0 < r;

      then

      consider m1 such that

       A2: for n st m1 <= n holds ||.((S . n) - g).|| < r by A1;

      take k = m1;

      let n;

      assume k <= n;

      then

       A3: ||.((S . n) - g).|| < r by A2;

       ||.((S . n) - g).|| = ||.(((S . n) - 09(CNS)) - g).|| by RLVECT_1: 13

      .= ||.(((S . n) - (x - x)) - g).|| by RLVECT_1: 15

      .= ||.((((S . n) - x) + x) - g).|| by RLVECT_1: 29

      .= ||.(((S . n) - x) + (( - g) + x)).|| by RLVECT_1:def 3

      .= ||.(((S . n) - x) - h).|| by RLVECT_1: 33;

      hence thesis by A3, NORMSP_1:def 4;

    end;

    theorem :: CLVECT_1:116

    

     Th116: S is convergent implies (z * S) is convergent

    proof

      assume S is convergent;

      then

      consider g such that

       A1: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - g).|| < r;

      take h = (z * g);

       A2:

      now

        assume

         A3: z <> 0c ;

        then

         A4: 0 < |.z.| by COMPLEX1: 47;

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A5: for n st m1 <= n holds ||.((S . n) - g).|| < (r / |.z.|) by A1, A4;

        take k = m1;

        let n;

        assume k <= n;

        then

         A6: ||.((S . n) - g).|| < (r / |.z.|) by A5;

        

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

        

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

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

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

        .= r;

         ||.((z * (S . n)) - (z * g)).|| = ||.(z * ((S . n) - g)).|| by Th9

        .= ( |.z.| * ||.((S . n) - g).||) by Def13;

        then ||.((z * (S . n)) - h).|| < r by A4, A6, A8, XREAL_1: 68;

        hence ||.(((z * S) . n) - h).|| < r by Def14;

      end;

      now

        assume

         A9: z = 0 ;

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A10: for n st m1 <= n holds ||.((S . n) - g).|| < r by A1;

        take k = m1;

        let n;

        assume k <= n;

        then

         A11: ||.((S . n) - g).|| < r by A10;

         ||.((z * (S . n)) - (z * g)).|| = ||.(( 0c * (S . n)) - 09(CNS)).|| by A9, Th1

        .= ||.( 09(CNS) - 09(CNS)).|| by Th1

        .= ||. 09(CNS).|| by RLVECT_1: 13

        .= 0 ;

        then ||.((z * (S . n)) - h).|| < r by A11, Th105;

        hence ||.(((z * S) . n) - h).|| < r by Def14;

      end;

      hence thesis by A2;

    end;

    theorem :: CLVECT_1:117

    

     Th117: S is convergent implies ||.S.|| is convergent

    proof

      assume S is convergent;

      then

      consider g such that

       A1: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - g).|| < r;

      now

        let r be Real;

        assume

         A2: 0 < r;

        consider m1 such that

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

        take k = m1;

        let n;

        assume k <= n;

        then

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

         |.( ||.(S . n).|| - ||.g.||).| <= ||.((S . n) - g).|| by Th110;

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

        hence |.(( ||.S.|| . n) - ||.g.||).| < r by NORMSP_0:def 4;

      end;

      hence thesis by SEQ_2:def 6;

    end;

    definition

      let CNS;

      let S;

      assume

       A1: S is convergent;

      :: CLVECT_1:def16

      func lim S -> Point of CNS means

      : Def16: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - it ).|| < r;

      existence by A1;

      uniqueness

      proof

        for x, y st (for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - x).|| < r) & (for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - y).|| < r) holds x = y

        proof

          given x, y such that

           A2: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - x).|| < r and

           A3: for r st 0 < r holds ex m st for n st m <= n holds ||.((S . n) - y).|| < r and

           A4: x <> y;

          

           A5: 0 <= ||.(x - y).|| by Th105;

          

           A6: ||.(x - y).|| <> 0 by A4, Th107;

          then

          consider m1 such that

           A7: for n st m1 <= n holds ||.((S . n) - x).|| < ( ||.(x - y).|| / 4) by A2, A5;

          consider m2 such that

           A8: for n st m2 <= n holds ||.((S . n) - y).|| < ( ||.(x - y).|| / 4) by A3, A6, A5;

           A9:

          now

             ||.(x - y).|| <= ( ||.(x - (S . m1)).|| + ||.((S . m1) - y).||) by Th111;

            then

             A10: ||.(x - y).|| <= ( ||.((S . m1) - x).|| + ||.((S . m1) - y).||) by Th108;

            assume m2 <= m1;

            then

             A11: ||.((S . m1) - y).|| < ( ||.(x - y).|| / 4) by A8;

             ||.((S . m1) - x).|| < ( ||.(x - y).|| / 4) by A7;

            then ( ||.((S . m1) - x).|| + ||.((S . m1) - y).||) < (( ||.(x - y).|| / 4) + ( ||.(x - y).|| / 4)) by A11, XREAL_1: 8;

            then not ( ||.(x - y).|| / 2) < ||.(x - y).|| by A10, XXREAL_0: 2;

            hence contradiction by A6, A5, XREAL_1: 216;

          end;

          now

             ||.(x - y).|| <= ( ||.(x - (S . m2)).|| + ||.((S . m2) - y).||) by Th111;

            then

             A12: ||.(x - y).|| <= ( ||.((S . m2) - x).|| + ||.((S . m2) - y).||) by Th108;

            assume m1 <= m2;

            then

             A13: ||.((S . m2) - x).|| < ( ||.(x - y).|| / 4) by A7;

             ||.((S . m2) - y).|| < ( ||.(x - y).|| / 4) by A8;

            then ( ||.((S . m2) - x).|| + ||.((S . m2) - y).||) < (( ||.(x - y).|| / 4) + ( ||.(x - y).|| / 4)) by A13, XREAL_1: 8;

            then not ( ||.(x - y).|| / 2) < ||.(x - y).|| by A12, XXREAL_0: 2;

            hence contradiction by A6, A5, XREAL_1: 216;

          end;

          hence contradiction by A9;

        end;

        hence thesis;

      end;

    end

    theorem :: CLVECT_1:118

    S is convergent & ( lim S) = g implies ||.(S - g).|| is convergent & ( lim ||.(S - g).||) = 0

    proof

      assume that

       A1: S is convergent and

       A2: ( lim S) = g;

       A3:

      now

        let r be Real;

        assume

         A4: 0 < r;

        consider m1 such that

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

        take k = m1;

        let n;

        assume k <= n;

        then ||.((S . n) - g).|| < r by A5;

        then

         A6: ||.(((S . n) - g) - 09(CNS)).|| < r by RLVECT_1: 13;

         |.( ||.((S . n) - g).|| - ||. 09(CNS).||).| <= ||.(((S . n) - g) - 09(CNS)).|| by Th110;

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

        then |.( ||.((S . n) - g).|| - 0 ).| < r;

        then |.( ||.((S - g) . n).|| - 0 ).| < r by NORMSP_1:def 4;

        hence |.(( ||.(S - g).|| . n) - 0 ).| < r by NORMSP_0:def 4;

      end;

       ||.(S - g).|| is convergent by A1, Th115, Th117;

      hence thesis by A3, SEQ_2:def 7;

    end;

    theorem :: CLVECT_1:119

    S1 is convergent & S2 is convergent implies ( lim (S1 + S2)) = (( lim S1) + ( lim S2))

    proof

      assume that

       A1: S1 is convergent and

       A2: S2 is convergent;

      set g2 = ( lim S2);

      set g1 = ( lim S1);

      set g = (g1 + g2);

       A3:

      now

        let r;

        assume

         A4: 0 < r;

        then

        consider m1 such that

         A5: for n st m1 <= n holds ||.((S1 . n) - g1).|| < (r / 2) by A1, Def16;

        consider m2 such that

         A6: for n st m2 <= n holds ||.((S2 . n) - g2).|| < (r / 2) by A2, A4, Def16;

        take k = (m1 + m2);

        let n such that

         A7: k <= n;

        m2 <= k by NAT_1: 12;

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

        then

         A8: ||.((S2 . n) - g2).|| < (r / 2) by A6;

        

         A9: ||.(((S1 + S2) . n) - g).|| = ||.(( - (g1 + g2)) + ((S1 . n) + (S2 . n))).|| by NORMSP_1:def 2

        .= ||.((( - g1) + ( - g2)) + ((S1 . n) + (S2 . n))).|| by RLVECT_1: 31

        .= ||.(((S1 . n) + (( - g1) + ( - g2))) + (S2 . n)).|| by RLVECT_1:def 3

        .= ||.((((S1 . n) - g1) + ( - g2)) + (S2 . n)).|| by RLVECT_1:def 3

        .= ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| by RLVECT_1:def 3;

        

         A10: ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| <= ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) by Def13;

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

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

        then ||.((S1 . n) - g1).|| < (r / 2) by A5;

        then ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) < ((r / 2) + (r / 2)) by A8, XREAL_1: 8;

        hence ||.(((S1 + S2) . n) - g).|| < r by A9, A10, XXREAL_0: 2;

      end;

      (S1 + S2) is convergent by A1, A2, Th113;

      hence thesis by A3, Def16;

    end;

    theorem :: CLVECT_1:120

    S1 is convergent & S2 is convergent implies ( lim (S1 - S2)) = (( lim S1) - ( lim S2))

    proof

      assume that

       A1: S1 is convergent and

       A2: S2 is convergent;

      set g2 = ( lim S2);

      set g1 = ( lim S1);

      set g = (g1 - g2);

       A3:

      now

        let r;

        assume

         A4: 0 < r;

        then

        consider m1 such that

         A5: for n st m1 <= n holds ||.((S1 . n) - g1).|| < (r / 2) by A1, Def16;

        consider m2 such that

         A6: for n st m2 <= n holds ||.((S2 . n) - g2).|| < (r / 2) by A2, A4, Def16;

        take k = (m1 + m2);

        let n such that

         A7: k <= n;

        m2 <= k by NAT_1: 12;

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

        then

         A8: ||.((S2 . n) - g2).|| < (r / 2) by A6;

        

         A9: ||.(((S1 - S2) . n) - g).|| = ||.(((S1 . n) - (S2 . n)) - (g1 - g2)).|| by NORMSP_1:def 3

        .= ||.((((S1 . n) - (S2 . n)) - g1) + g2).|| by RLVECT_1: 29

        .= ||.(((S1 . n) - (g1 + (S2 . n))) + g2).|| by RLVECT_1: 27

        .= ||.((((S1 . n) - g1) - (S2 . n)) + g2).|| by RLVECT_1: 27

        .= ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| by RLVECT_1: 29;

        

         A10: ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| <= ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) by Th104;

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

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

        then ||.((S1 . n) - g1).|| < (r / 2) by A5;

        then ( ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).||) < ((r / 2) + (r / 2)) by A8, XREAL_1: 8;

        hence ||.(((S1 - S2) . n) - g).|| < r by A9, A10, XXREAL_0: 2;

      end;

      (S1 - S2) is convergent by A1, A2, Th114;

      hence thesis by A3, Def16;

    end;

    theorem :: CLVECT_1:121

    S is convergent implies ( lim (S - x)) = (( lim S) - x)

    proof

      set g = ( lim S);

      set h = (g - x);

      assume

       A1: S is convergent;

       A2:

      now

        let r;

        assume 0 < r;

        then

        consider m1 such that

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

        take k = m1;

        let n;

        assume k <= n;

        then

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

         ||.((S . n) - g).|| = ||.(((S . n) - 09(CNS)) - g).|| by RLVECT_1: 13

        .= ||.(((S . n) - (x - x)) - g).|| by RLVECT_1: 15

        .= ||.((((S . n) - x) + x) - g).|| by RLVECT_1: 29

        .= ||.(((S . n) - x) + (( - g) + x)).|| by RLVECT_1:def 3

        .= ||.(((S . n) - x) - h).|| by RLVECT_1: 33;

        hence ||.(((S - x) . n) - h).|| < r by A4, NORMSP_1:def 4;

      end;

      (S - x) is convergent by A1, Th115;

      hence thesis by A2, Def16;

    end;

    theorem :: CLVECT_1:122

    S is convergent implies ( lim (z * S)) = (z * ( lim S))

    proof

      set g = ( lim S);

      set h = (z * g);

      assume

       A1: S is convergent;

       A2:

      now

        assume

         A3: z = 0 ;

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A4: for n st m1 <= n holds ||.((S . n) - g).|| < r by A1, Def16;

        take k = m1;

        let n;

        assume k <= n;

        then

         A5: ||.((S . n) - g).|| < r by A4;

         ||.((z * (S . n)) - (z * g)).|| = ||.(( 0c * (S . n)) - 09(CNS)).|| by A3, Th1

        .= ||.( 09(CNS) - 09(CNS)).|| by Th1

        .= ||. 09(CNS).|| by RLVECT_1: 13

        .= 0 ;

        then ||.((z * (S . n)) - h).|| < r by A5, Th105;

        hence ||.(((z * S) . n) - h).|| < r by Def14;

      end;

       A6:

      now

        assume

         A7: z <> 0c ;

        then

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

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A9: for n st m1 <= n holds ||.((S . n) - g).|| < (r / |.z.|) by A1, A8, Def16;

        take k = m1;

        let n;

        assume k <= n;

        then

         A10: ||.((S . n) - g).|| < (r / |.z.|) by A9;

        

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

        

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

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

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

        .= r;

         ||.((z * (S . n)) - (z * g)).|| = ||.(z * ((S . n) - g)).|| by Th9

        .= ( |.z.| * ||.((S . n) - g).||) by Def13;

        then ||.((z * (S . n)) - h).|| < r by A8, A10, A12, XREAL_1: 68;

        hence ||.(((z * S) . n) - h).|| < r by Def14;

      end;

      (z * S) is convergent by A1, Th116;

      hence thesis by A2, A6, Def16;

    end;

    theorem :: CLVECT_1:123

    for V, V1, v holds for w be VECTOR of CLSStruct (# D, d1, A, M #) st V1 = D & M = (the Mult of V | [: COMPLEX , V1:]) & w = v holds (z * w) = (z * v) by Lm4;