vectsp_6.miz



    begin

    reserve p,q,r for FinSequence,

x,y,y1,y2 for set,

i,k for Element of NAT ,

GF for add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr,

V for Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over GF,

u,v,v1,v2,v3,w for Element of V,

a,b for Element of GF,

F,G,H for FinSequence of V,

A,B for Subset of V,

f for Function of V, GF;

    definition

      let GF be non empty ZeroStr;

      let V be non empty ModuleStr over GF;

      :: VECTSP_6:def1

      mode Linear_Combination of V -> Element of ( Funcs (the carrier of V,the carrier of GF)) means

      : Def1: ex T be finite Subset of V st for v be Element of V st not v in T holds (it . v) = ( 0. GF);

      existence

      proof

        reconsider f = (the carrier of V --> ( 0. GF)) as Function of the carrier of V, the carrier of GF;

        reconsider f as Element of ( Funcs (the carrier of V,the carrier of GF)) by FUNCT_2: 8;

        take f, ( {} V);

        thus thesis by FUNCOP_1: 7;

      end;

    end

    reserve L,L1,L2,L3 for Linear_Combination of V;

    definition

      let GF be non empty ZeroStr;

      let V be non empty ModuleStr over GF;

      let L be Linear_Combination of V;

      :: VECTSP_6:def2

      func Carrier (L) -> finite Subset of V equals { v where v be Element of V : (L . v) <> ( 0. GF) };

      coherence

      proof

        set A = { v where v be Element of V : (L . v) <> ( 0. GF) };

        consider T be finite Subset of V such that

         A1: for v be Element of V st not v in T holds (L . v) = ( 0. GF) by Def1;

        A c= T

        proof

          let x be object;

          assume x in A;

          then ex v be Element of V st x = v & (L . v) <> ( 0. GF);

          hence thesis by A1;

        end;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    theorem :: VECTSP_6:1

    x in ( Carrier L) iff ex v st x = v & (L . v) <> ( 0. GF);

    theorem :: VECTSP_6:2

    (L . v) = ( 0. GF) iff not v in ( Carrier L)

    proof

      thus (L . v) = ( 0. GF) implies not v in ( Carrier L)

      proof

        assume

         A1: (L . v) = ( 0. GF);

        assume not thesis;

        then ex u st u = v & (L . u) <> ( 0. GF);

        hence thesis by A1;

      end;

      assume not v in ( Carrier L);

      hence thesis;

    end;

    definition

      let GF be non empty ZeroStr;

      let V be non empty ModuleStr over GF;

      :: VECTSP_6:def3

      func ZeroLC (V) -> Linear_Combination of V means

      : Def3: ( Carrier it ) = {} ;

      existence

      proof

        reconsider f = (the carrier of V --> ( 0. GF)) as Function of the carrier of V, the carrier of GF;

        reconsider f as Element of ( Funcs (the carrier of V,the carrier of GF)) by FUNCT_2: 8;

        f is Linear_Combination of V

        proof

          reconsider T = ( {} V) as empty finite Subset of V;

          take T;

          thus thesis by FUNCOP_1: 7;

        end;

        then

        reconsider f as Linear_Combination of V;

        take f;

        set C = { v where v be Element of V : (f . v) <> ( 0. GF) };

        now

          set x = the Element of C;

          assume C <> {} ;

          then x in C;

          then ex v be Element of V st x = v & (f . v) <> ( 0. GF);

          hence contradiction by FUNCOP_1: 7;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let L,L9 be Linear_Combination of V;

        reconsider K = L, K9 = L9 as Function of the carrier of V, the carrier of GF;

        assume that

         A1: ( Carrier L) = {} and

         A2: ( Carrier L9) = {} ;

        now

          let x be object;

          assume x in the carrier of V;

          then

          reconsider v = x as Element of V;

           A3:

          now

            assume (L9 . v) <> ( 0. GF);

            then v in { u where u be Element of V : (L9 . u) <> ( 0. GF) };

            hence contradiction by A2;

          end;

          now

            assume (L . v) <> ( 0. GF);

            then v in { u where u be Element of V : (L . u) <> ( 0. GF) };

            hence contradiction by A1;

          end;

          hence (K . x) = (K9 . x) by A3;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: VECTSP_6:3

    

     Th3: (( ZeroLC V) . v) = ( 0. GF)

    proof

      ( Carrier ( ZeroLC V)) = {} & not v in {} by Def3;

      hence thesis;

    end;

    definition

      let GF be non empty ZeroStr;

      let V be non empty ModuleStr over GF;

      let A be Subset of V;

      :: VECTSP_6:def4

      mode Linear_Combination of A -> Linear_Combination of V means

      : Def4: ( Carrier it ) c= A;

      existence

      proof

        take L = ( ZeroLC V);

        ( Carrier L) = {} by Def3;

        hence thesis;

      end;

    end

    reserve l for Linear_Combination of A;

    theorem :: VECTSP_6:4

    A c= B implies l is Linear_Combination of B

    proof

      assume

       A1: A c= B;

      ( Carrier l) c= A by Def4;

      then ( Carrier l) c= B by A1;

      hence thesis by Def4;

    end;

    theorem :: VECTSP_6:5

    

     Th5: ( ZeroLC V) is Linear_Combination of A

    proof

      ( Carrier ( ZeroLC V)) = {} & {} c= A by Def3;

      hence thesis by Def4;

    end;

    theorem :: VECTSP_6:6

    

     Th6: for l be Linear_Combination of ( {} the carrier of V) holds l = ( ZeroLC V)

    proof

      let l be Linear_Combination of ( {} the carrier of V);

      ( Carrier l) c= {} by Def4;

      then ( Carrier l) = {} ;

      hence thesis by Def3;

    end;

    theorem :: VECTSP_6:7

    L is Linear_Combination of ( Carrier L) by Def4;

    definition

      let GF be non empty addLoopStr;

      let V be non empty ModuleStr over GF;

      let F be FinSequence of the carrier of V;

      let f be Function of V, GF;

      :: VECTSP_6:def5

      func f (#) F -> FinSequence of V means

      : Def5: ( len it ) = ( len F) & for i be Nat st i in ( dom it ) holds (it . i) = ((f . (F /. i)) * (F /. i));

      existence

      proof

        deffunc G( Nat) = ((f . (F /. $1)) * (F /. $1));

        consider G be FinSequence such that

         A1: ( len G) = ( len F) and

         A2: for n be Nat st n in ( dom G) holds (G . n) = G(n) from FINSEQ_1:sch 2;

        ( rng G) c= the carrier of V

        proof

          let x be object;

          assume x in ( rng G);

          then

          consider y be object such that

           A3: y in ( dom G) and

           A4: (G . y) = x by FUNCT_1:def 3;

          y in ( Seg ( len F)) by A1, A3, FINSEQ_1:def 3;

          then

          reconsider y as Element of NAT ;

          (G . y) = ((f . (F /. y)) * (F /. y)) by A2, A3;

          hence thesis by A4;

        end;

        then

        reconsider G as FinSequence of the carrier of V by FINSEQ_1:def 4;

        take G;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let H1,H2 be FinSequence of the carrier of V;

        assume that

         A5: ( len H1) = ( len F) and

         A6: for i be Nat st i in ( dom H1) holds (H1 . i) = ((f . (F /. i)) * (F /. i)) and

         A7: ( len H2) = ( len F) and

         A8: for i be Nat st i in ( dom H2) holds (H2 . i) = ((f . (F /. i)) * (F /. i));

        now

          let k be Nat;

          assume 1 <= k & k <= ( len H1);

          then

           A9: k in ( Seg ( len H1)) by FINSEQ_1: 1;

          then k in ( dom H1) by FINSEQ_1:def 3;

          then

           A10: (H1 . k) = ((f . (F /. k)) * (F /. k)) by A6;

          k in ( dom H2) by A5, A7, A9, FINSEQ_1:def 3;

          hence (H1 . k) = (H2 . k) by A8, A10;

        end;

        hence thesis by A5, A7, FINSEQ_1: 14;

      end;

    end

    theorem :: VECTSP_6:8

    

     Th8: i in ( dom F) & v = (F . i) implies ((f (#) F) . i) = ((f . v) * v)

    proof

      assume that

       A1: i in ( dom F) and

       A2: v = (F . i);

      

       A3: (F /. i) = (F . i) by A1, PARTFUN1:def 6;

      ( len (f (#) F)) = ( len F) by Def5;

      then i in ( dom (f (#) F)) by A1, FINSEQ_3: 29;

      hence thesis by A2, A3, Def5;

    end;

    theorem :: VECTSP_6:9

    (f (#) ( <*> the carrier of V)) = ( <*> the carrier of V)

    proof

      ( len (f (#) ( <*> the carrier of V))) = ( len ( <*> the carrier of V)) by Def5

      .= 0 ;

      hence thesis;

    end;

    theorem :: VECTSP_6:10

    

     Th10: (f (#) <*v*>) = <*((f . v) * v)*>

    proof

      

       A1: 1 in {1} by TARSKI:def 1;

      

       A2: ( len (f (#) <*v*>)) = ( len <*v*>) by Def5

      .= 1 by FINSEQ_1: 40;

      then ( dom (f (#) <*v*>)) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

      

      then ((f (#) <*v*>) . 1) = ((f . ( <*v*> /. 1)) * ( <*v*> /. 1)) by A1, Def5

      .= ((f . ( <*v*> /. 1)) * v) by FINSEQ_4: 16

      .= ((f . v) * v) by FINSEQ_4: 16;

      hence thesis by A2, FINSEQ_1: 40;

    end;

    theorem :: VECTSP_6:11

    

     Th11: (f (#) <*v1, v2*>) = <*((f . v1) * v1), ((f . v2) * v2)*>

    proof

      

       A1: ( len (f (#) <*v1, v2*>)) = ( len <*v1, v2*>) by Def5

      .= 2 by FINSEQ_1: 44;

      then

       A2: ( dom (f (#) <*v1, v2*>)) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      2 in {1, 2} by TARSKI:def 2;

      

      then

       A3: ((f (#) <*v1, v2*>) . 2) = ((f . ( <*v1, v2*> /. 2)) * ( <*v1, v2*> /. 2)) by A2, Def5

      .= ((f . ( <*v1, v2*> /. 2)) * v2) by FINSEQ_4: 17

      .= ((f . v2) * v2) by FINSEQ_4: 17;

      1 in {1, 2} by TARSKI:def 2;

      

      then ((f (#) <*v1, v2*>) . 1) = ((f . ( <*v1, v2*> /. 1)) * ( <*v1, v2*> /. 1)) by A2, Def5

      .= ((f . ( <*v1, v2*> /. 1)) * v1) by FINSEQ_4: 17

      .= ((f . v1) * v1) by FINSEQ_4: 17;

      hence thesis by A1, A3, FINSEQ_1: 44;

    end;

    theorem :: VECTSP_6:12

    (f (#) <*v1, v2, v3*>) = <*((f . v1) * v1), ((f . v2) * v2), ((f . v3) * v3)*>

    proof

      

       A1: ( len (f (#) <*v1, v2, v3*>)) = ( len <*v1, v2, v3*>) by Def5

      .= 3 by FINSEQ_1: 45;

      then

       A2: ( dom (f (#) <*v1, v2, v3*>)) = {1, 2, 3} by FINSEQ_1:def 3, FINSEQ_3: 1;

      3 in {1, 2, 3} by ENUMSET1:def 1;

      

      then

       A3: ((f (#) <*v1, v2, v3*>) . 3) = ((f . ( <*v1, v2, v3*> /. 3)) * ( <*v1, v2, v3*> /. 3)) by A2, Def5

      .= ((f . ( <*v1, v2, v3*> /. 3)) * v3) by FINSEQ_4: 18

      .= ((f . v3) * v3) by FINSEQ_4: 18;

      2 in {1, 2, 3} by ENUMSET1:def 1;

      

      then

       A4: ((f (#) <*v1, v2, v3*>) . 2) = ((f . ( <*v1, v2, v3*> /. 2)) * ( <*v1, v2, v3*> /. 2)) by A2, Def5

      .= ((f . ( <*v1, v2, v3*> /. 2)) * v2) by FINSEQ_4: 18

      .= ((f . v2) * v2) by FINSEQ_4: 18;

      1 in {1, 2, 3} by ENUMSET1:def 1;

      

      then ((f (#) <*v1, v2, v3*>) . 1) = ((f . ( <*v1, v2, v3*> /. 1)) * ( <*v1, v2, v3*> /. 1)) by A2, Def5

      .= ((f . ( <*v1, v2, v3*> /. 1)) * v1) by FINSEQ_4: 18

      .= ((f . v1) * v1) by FINSEQ_4: 18;

      hence thesis by A1, A4, A3, FINSEQ_1: 45;

    end;

    theorem :: VECTSP_6:13

    

     Th13: (f (#) (F ^ G)) = ((f (#) F) ^ (f (#) G))

    proof

      set H = ((f (#) F) ^ (f (#) G));

      set I = (F ^ G);

      

       A1: ( len F) = ( len (f (#) F)) by Def5;

      

       A2: ( len H) = (( len (f (#) F)) + ( len (f (#) G))) by FINSEQ_1: 22

      .= (( len F) + ( len (f (#) G))) by Def5

      .= (( len F) + ( len G)) by Def5

      .= ( len I) by FINSEQ_1: 22;

      

       A3: ( len G) = ( len (f (#) G)) by Def5;

      now

        let k be Nat;

        assume

         A4: k in ( dom H);

        now

          per cases by A4, FINSEQ_1: 25;

            suppose

             A5: k in ( dom (f (#) F));

            then

             A6: k in ( dom F) by A1, FINSEQ_3: 29;

            then

             A7: k in ( dom (F ^ G)) by FINSEQ_3: 22;

            

             A8: (F /. k) = (F . k) by A6, PARTFUN1:def 6

            .= ((F ^ G) . k) by A6, FINSEQ_1:def 7

            .= ((F ^ G) /. k) by A7, PARTFUN1:def 6;

            

            thus (H . k) = ((f (#) F) . k) by A5, FINSEQ_1:def 7

            .= ((f . (I /. k)) * (I /. k)) by A5, A8, Def5;

          end;

            suppose

             A9: ex n be Nat st n in ( dom (f (#) G)) & k = (( len (f (#) F)) + n);

            

             A10: k in ( dom I) by A2, A4, FINSEQ_3: 29;

            consider n be Nat such that

             A11: n in ( dom (f (#) G)) and

             A12: k = (( len (f (#) F)) + n) by A9;

            

             A13: n in ( dom G) by A3, A11, FINSEQ_3: 29;

            

            then

             A14: (G /. n) = (G . n) by PARTFUN1:def 6

            .= ((F ^ G) . k) by A1, A12, A13, FINSEQ_1:def 7

            .= ((F ^ G) /. k) by A10, PARTFUN1:def 6;

            

            thus (H . k) = ((f (#) G) . n) by A11, A12, FINSEQ_1:def 7

            .= ((f . (I /. k)) * (I /. k)) by A11, A14, Def5;

          end;

        end;

        hence (H . k) = ((f . (I /. k)) * (I /. k));

      end;

      hence thesis by A2, Def5;

    end;

    definition

      let GF be non empty addLoopStr;

      let V be non empty ModuleStr over GF;

      let L be Linear_Combination of V;

      assume

       A1: V is Abelian add-associative right_zeroed right_complementable;

      :: VECTSP_6:def6

      func Sum (L) -> Element of V means

      : Def6: ex F be FinSequence of the carrier of V st F is one-to-one & ( rng F) = ( Carrier L) & it = ( Sum (L (#) F));

      existence

      proof

        consider F be FinSequence such that

         A2: ( rng F) = ( Carrier L) and

         A3: F is one-to-one by FINSEQ_4: 58;

        reconsider F as FinSequence of the carrier of V by A2, FINSEQ_1:def 4;

        take ( Sum (L (#) F)), F;

        thus F is one-to-one & ( rng F) = ( Carrier L) by A2, A3;

        thus thesis;

      end;

      uniqueness

      proof

        let v1,v2 be Element of V;

        given F1 be FinSequence of the carrier of V such that

         A4: F1 is one-to-one and

         A5: ( rng F1) = ( Carrier L) and

         A6: v1 = ( Sum (L (#) F1));

        given F2 be FinSequence of the carrier of V such that

         A7: F2 is one-to-one and

         A8: ( rng F2) = ( Carrier L) and

         A9: v2 = ( Sum (L (#) F2));

        defpred P[ object, object] means {$2} = (F1 " {(F2 . $1)});

        

         A10: ( len F1) = ( len F2) by A4, A5, A7, A8, FINSEQ_1: 48;

        

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

        

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

        

         A13: for x be object st x in ( dom F1) holds ex y be object st y in ( dom F1) & P[x, y]

        proof

          let x be object;

          assume x in ( dom F1);

          then (F2 . x) in ( rng F1) by A5, A8, A10, A11, A12, FUNCT_1:def 3;

          then

          consider y be object such that

           A14: (F1 " {(F2 . x)}) = {y} by A4, FUNCT_1: 74;

          take y;

          y in (F1 " {(F2 . x)}) by A14, TARSKI:def 1;

          hence y in ( dom F1) by FUNCT_1:def 7;

          thus thesis by A14;

        end;

        consider f be Function of ( dom F1), ( dom F1) such that

         A15: for x be object st x in ( dom F1) holds P[x, (f . x)] from FUNCT_2:sch 1( A13);

        

         A16: ( rng f) = ( dom F1)

        proof

          thus ( rng f) c= ( dom F1) by RELAT_1:def 19;

          let y be object;

          assume

           A17: y in ( dom F1);

          then (F1 . y) in ( rng F2) by A5, A8, FUNCT_1:def 3;

          then

          consider x be object such that

           A18: x in ( dom F2) and

           A19: (F2 . x) = (F1 . y) by FUNCT_1:def 3;

          (F1 " {(F2 . x)}) = (F1 " ( Im (F1,y))) by A17, A19, FUNCT_1: 59;

          then (F1 " {(F2 . x)}) c= {y} by A4, FUNCT_1: 82;

          then {(f . x)} c= {y} by A10, A11, A12, A15, A18;

          then

           A20: (f . x) = y by ZFMISC_1: 18;

          x in ( dom f) by A10, A11, A12, A18, FUNCT_2:def 1;

          hence thesis by A20, FUNCT_1:def 3;

        end;

        reconsider G1 = (L (#) F1) as FinSequence of V;

        

         A21: ( len G1) = ( len F1) by Def5;

        

         A22: f is one-to-one

        proof

          let y1,y2 be object;

          assume that

           A23: y1 in ( dom f) and

           A24: y2 in ( dom f) and

           A25: (f . y1) = (f . y2);

          ( dom F1) = ( dom f) by FUNCT_2: 52;

          then

           A26: ( dom F1) <> {} by A23;

          

           A27: y2 in ( dom F1) by A26, A24, FUNCT_2:def 1;

          then

           A28: (F1 " {(F2 . y2)}) = {(f . y2)} by A15;

          

           A29: y1 in ( dom F1) by A26, A23, FUNCT_2:def 1;

          then (F2 . y1) in ( rng F1) by A5, A8, A10, A11, A12, FUNCT_1:def 3;

          then

           A30: {(F2 . y1)} c= ( rng F1) by ZFMISC_1: 31;

          (F2 . y2) in ( rng F1) by A5, A8, A10, A11, A12, A27, FUNCT_1:def 3;

          then

           A31: {(F2 . y2)} c= ( rng F1) by ZFMISC_1: 31;

          (F1 " {(F2 . y1)}) = {(f . y1)} by A15, A29;

          then {(F2 . y1)} = {(F2 . y2)} by A25, A28, A30, A31, FUNCT_1: 91;

          then

           A32: (F2 . y1) = (F2 . y2) by ZFMISC_1: 3;

          y1 in ( dom F2) & y2 in ( dom F2) by A10, A11, A12, A26, A23, A24, FUNCT_2:def 1;

          hence thesis by A7, A32;

        end;

        set G2 = (L (#) F2);

        

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

        reconsider f as Permutation of ( dom F1) by A16, A22, FUNCT_2: 57;

        ( dom F1) = ( Seg ( len F1)) & ( dom G1) = ( Seg ( len G1)) by FINSEQ_1:def 3;

        then

        reconsider f as Permutation of ( dom G1) by A21;

        

         A34: ( len G2) = ( len F2) by Def5;

        

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

        now

          let i be Nat;

          assume

           A36: i in ( dom G2);

          then

           A37: (G2 . i) = ((L . (F2 /. i)) * (F2 /. i)) & (F2 . i) = (F2 /. i) by A34, A12, A33, Def5, PARTFUN1:def 6;

          i in ( dom F2) by A34, A36, FINSEQ_3: 29;

          then

          reconsider u = (F2 . i) as Element of V by FINSEQ_2: 11;

          i in ( dom f) by A10, A21, A34, A35, A33, A36, FUNCT_2:def 1;

          then

           A38: (f . i) in ( dom F1) by A16, FUNCT_1:def 3;

          then

          reconsider m = (f . i) as Element of NAT by A11;

          reconsider v = (F1 . m) as Element of V by A38, FINSEQ_2: 11;

           {(F1 . (f . i))} = ( Im (F1,(f . i))) by A38, FUNCT_1: 59

          .= (F1 .: (F1 " {(F2 . i)})) by A10, A34, A11, A33, A15, A36;

          then

           A39: u = v by FUNCT_1: 75, ZFMISC_1: 18;

          (F1 . m) = (F1 /. m) by A38, PARTFUN1:def 6;

          hence (G2 . i) = (G1 . (f . i)) by A21, A11, A35, A38, A39, A37, Def5;

        end;

        hence thesis by A1, A4, A5, A6, A7, A8, A9, A21, A34, FINSEQ_1: 48, RLVECT_2: 6;

      end;

    end

    

     Lm1: ( Sum ( ZeroLC V)) = ( 0. V)

    proof

      consider F such that F is one-to-one and

       A1: ( rng F) = ( Carrier ( ZeroLC V)) and

       A2: ( Sum ( ZeroLC V)) = ( Sum (( ZeroLC V) (#) F)) by Def6;

      ( Carrier ( ZeroLC V)) = {} by Def3;

      then F = {} by A1, RELAT_1: 41;

      then ( len F) = 0 ;

      then ( len (( ZeroLC V) (#) F)) = 0 by Def5;

      hence thesis by A2, RLVECT_1: 75;

    end;

    theorem :: VECTSP_6:14

    ( 0. GF) <> ( 1. GF) implies (A <> {} & A is linearly-closed iff for l holds ( Sum l) in A)

    proof

      assume

       A1: ( 0. GF) <> ( 1. GF);

      thus A <> {} & A is linearly-closed implies for l holds ( Sum l) in A

      proof

        defpred P[ Nat] means for l st ( card ( Carrier l)) = $1 holds ( Sum l) in A;

        assume that

         A2: A <> {} and

         A3: A is linearly-closed;

        

         A4: P[ 0 ]

        proof

          let l;

          assume ( card ( Carrier l)) = 0 ;

          then ( Carrier l) = {} ;

          then l = ( ZeroLC V) by Def3;

          then ( Sum l) = ( 0. V) by Lm1;

          hence thesis by A2, A3, VECTSP_4: 1;

        end;

        

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

        proof

          let k be Nat;

          assume

           A6: P[k];

          let l;

          deffunc F( Element of V) = (l . $1);

          consider F such that

           A7: F is one-to-one and

           A8: ( rng F) = ( Carrier l) and

           A9: ( Sum l) = ( Sum (l (#) F)) by Def6;

          reconsider G = (F | ( Seg k)) as FinSequence of the carrier of V by FINSEQ_1: 18;

          assume

           A10: ( card ( Carrier l)) = (k + 1);

          then

           A11: ( len F) = (k + 1) by A7, A8, FINSEQ_4: 62;

          then

           A12: ( len (l (#) F)) = (k + 1) by Def5;

          

           A13: (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

          then

           A14: (k + 1) in ( dom F) by A11, FINSEQ_1:def 3;

          (k + 1) in ( dom F) by A11, A13, FINSEQ_1:def 3;

          then

          reconsider v = (F . (k + 1)) as Element of V by FINSEQ_2: 11;

          consider f be Function of the carrier of V, the carrier of GF such that

           A15: (f . v) = ( 0. GF) and

           A16: for u be Element of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

          reconsider f as Element of ( Funcs (the carrier of V,the carrier of GF)) by FUNCT_2: 8;

          

           A17: v in ( Carrier l) by A8, A14, FUNCT_1:def 3;

          now

            let u;

            assume

             A18: not u in ( Carrier l);

            

            hence (f . u) = (l . u) by A17, A16

            .= ( 0. GF) by A18;

          end;

          then

          reconsider f as Linear_Combination of V by Def1;

          

           A19: (A \ {v}) c= A by XBOOLE_1: 36;

          

           A20: ( Carrier l) c= A by Def4;

          then

           A21: ((l . v) * v) in A by A3, A17;

          

           A22: ( Carrier f) = (( Carrier l) \ {v})

          proof

            thus ( Carrier f) c= (( Carrier l) \ {v})

            proof

              let x be object;

              assume x in ( Carrier f);

              then

              consider u such that

               A23: u = x and

               A24: (f . u) <> ( 0. GF);

              (f . u) = (l . u) by A15, A16, A24;

              then

               A25: x in ( Carrier l) by A23, A24;

               not x in {v} by A15, A23, A24, TARSKI:def 1;

              hence thesis by A25, XBOOLE_0:def 5;

            end;

            let x be object;

            assume

             A26: x in (( Carrier l) \ {v});

            then x in ( Carrier l) by XBOOLE_0:def 5;

            then

            consider u such that

             A27: x = u and

             A28: (l . u) <> ( 0. GF);

             not x in {v} by A26, XBOOLE_0:def 5;

            then x <> v by TARSKI:def 1;

            then (l . u) = (f . u) by A16, A27;

            hence thesis by A27, A28;

          end;

          then ( Carrier f) c= (A \ {v}) by A20, XBOOLE_1: 33;

          then ( Carrier f) c= A by A19;

          then

          reconsider f as Linear_Combination of A by Def4;

          

           A29: ( len G) = k by A11, FINSEQ_3: 53;

          then

           A30: ( len (f (#) G)) = k by Def5;

          

           A31: ( rng G) = ( Carrier f)

          proof

            thus ( rng G) c= ( Carrier f)

            proof

              let x be object;

              assume x in ( rng G);

              then

              consider y be object such that

               A32: y in ( dom G) and

               A33: (G . y) = x by FUNCT_1:def 3;

              reconsider y as Element of NAT by A32, FINSEQ_3: 23;

              

               A34: ( dom G) c= ( dom F) & (G . y) = (F . y) by A32, FUNCT_1: 47, RELAT_1: 60;

              now

                assume x = v;

                then

                 A35: (k + 1) = y by A7, A14, A32, A33, A34;

                

                 A36: k in NAT by ORDINAL1:def 12;

                y <= k by A29, A32, FINSEQ_3: 25;

                hence contradiction by A35, XREAL_1: 29, A36;

              end;

              then

               A37: not x in {v} by TARSKI:def 1;

              x in ( rng F) by A32, A33, A34, FUNCT_1:def 3;

              hence thesis by A8, A22, A37, XBOOLE_0:def 5;

            end;

            let x be object;

            assume

             A38: x in ( Carrier f);

            then x in ( rng F) by A8, A22, XBOOLE_0:def 5;

            then

            consider y be object such that

             A39: y in ( dom F) and

             A40: (F . y) = x by FUNCT_1:def 3;

            reconsider y as Element of NAT by A39, FINSEQ_3: 23;

            now

              assume not y in ( Seg k);

              then y in (( dom F) \ ( Seg k)) by A39, XBOOLE_0:def 5;

              then y in (( Seg (k + 1)) \ ( Seg k)) by A11, FINSEQ_1:def 3;

              then y in {(k + 1)} by FINSEQ_3: 15;

              then y = (k + 1) by TARSKI:def 1;

              then not v in {v} by A22, A38, A40, XBOOLE_0:def 5;

              hence contradiction by TARSKI:def 1;

            end;

            then y in (( dom F) /\ ( Seg k)) by A39, XBOOLE_0:def 4;

            then

             A41: y in ( dom G) by RELAT_1: 61;

            then (G . y) = (F . y) by FUNCT_1: 47;

            hence thesis by A40, A41, FUNCT_1:def 3;

          end;

          (( Seg (k + 1)) /\ ( Seg k)) = ( Seg k) by FINSEQ_1: 7, NAT_1: 12

          .= ( dom (f (#) G)) by A30, FINSEQ_1:def 3;

          then

           A42: ( dom (f (#) G)) = (( dom (l (#) F)) /\ ( Seg k)) by A12, FINSEQ_1:def 3;

          now

            let x be object;

            

             A43: ( rng F) c= the carrier of V by FINSEQ_1:def 4;

            assume

             A44: x in ( dom (f (#) G));

            then

            reconsider n = x as Element of NAT by FINSEQ_3: 23;

            n in ( dom (l (#) F)) by A42, A44, XBOOLE_0:def 4;

            then

             A45: n in ( dom F) by A11, A12, FINSEQ_3: 29;

            then (F . n) in ( rng F) by FUNCT_1:def 3;

            then

            reconsider w = (F . n) as Element of V by A43;

            

             A46: n in ( dom G) by A29, A30, A44, FINSEQ_3: 29;

            then

             A47: (G . n) in ( rng G) by FUNCT_1:def 3;

            ( rng G) c= the carrier of V by FINSEQ_1:def 4;

            then

            reconsider u = (G . n) as Element of V by A47;

             not u in {v} by A22, A31, A47, XBOOLE_0:def 5;

            then

             A48: u <> v by TARSKI:def 1;

            

             A49: ((f (#) G) . n) = ((f . u) * u) by A46, Th8

            .= ((l . u) * u) by A16, A48;

            w = u by A46, FUNCT_1: 47;

            hence ((f (#) G) . x) = ((l (#) F) . x) by A49, A45, Th8;

          end;

          then (f (#) G) = ((l (#) F) | ( Seg k)) by A42, FUNCT_1: 46;

          then

           A50: (f (#) G) = ((l (#) F) | ( dom (f (#) G))) by A30, FINSEQ_1:def 3;

          v in ( rng F) by A14, FUNCT_1:def 3;

          then {v} c= ( Carrier l) by A8, ZFMISC_1: 31;

          

          then ( card ( Carrier f)) = ((k + 1) - ( card {v})) by A10, A22, CARD_2: 44

          .= ((k + 1) - 1) by CARD_1: 30

          .= k by XCMPLX_1: 26;

          then

           A51: ( Sum f) in A by A6;

          G is one-to-one by A7, FUNCT_1: 52;

          then

           A52: ( Sum (f (#) G)) = ( Sum f) by A31, Def6;

          ((l (#) F) . ( len F)) = ((l . v) * v) by A11, A14, Th8;

          then ( Sum (l (#) F)) = (( Sum (f (#) G)) + ((l . v) * v)) by A11, A12, A30, A50, RLVECT_1: 38;

          hence thesis by A3, A9, A21, A52, A51;

        end;

        let l;

        

         A53: ( card ( Carrier l)) = ( card ( Carrier l));

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

        hence thesis by A53;

      end;

      assume

       A54: for l holds ( Sum l) in A;

      hence A <> {} ;

      ( ZeroLC V) is Linear_Combination of A & ( Sum ( ZeroLC V)) = ( 0. V) by Lm1, Th5;

      then

       A55: ( 0. V) in A by A54;

      

       A56: for a, v st v in A holds (a * v) in A

      proof

        let a, v;

        assume

         A57: v in A;

        now

          per cases ;

            suppose a = ( 0. GF);

            hence thesis by A55, VECTSP_1: 14;

          end;

            suppose

             A58: a <> ( 0. GF);

            deffunc F( set) = ( 0. GF);

            consider f such that

             A59: (f . v) = a and

             A60: for u be Element of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

            reconsider f as Element of ( Funcs (the carrier of V,the carrier of GF)) by FUNCT_2: 8;

            now

              let u;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (f . u) = ( 0. GF) by A60;

            end;

            then

            reconsider f as Linear_Combination of V by Def1;

            

             A61: ( Carrier f) = {v}

            proof

              thus ( Carrier f) c= {v}

              proof

                let x be object;

                assume x in ( Carrier f);

                then

                consider u such that

                 A62: x = u and

                 A63: (f . u) <> ( 0. GF);

                u = v by A60, A63;

                hence thesis by A62, TARSKI:def 1;

              end;

              let x be object;

              assume x in {v};

              then x = v by TARSKI:def 1;

              hence thesis by A58, A59;

            end;

             {v} c= A by A57, ZFMISC_1: 31;

            then

            reconsider f as Linear_Combination of A by A61, Def4;

            consider F such that

             A64: F is one-to-one & ( rng F) = ( Carrier f) and

             A65: ( Sum (f (#) F)) = ( Sum f) by Def6;

            F = <*v*> by A61, A64, FINSEQ_3: 97;

            then (f (#) F) = <*((f . v) * v)*> by Th10;

            then ( Sum f) = (a * v) by A59, A65, RLVECT_1: 44;

            hence thesis by A54;

          end;

        end;

        hence thesis;

      end;

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

      proof

        let v, u;

        assume that

         A66: v in A and

         A67: u in A;

        now

          per cases ;

            suppose u = v;

            

            then (v + u) = ((( 1. GF) * v) + v) by VECTSP_1:def 17

            .= ((( 1. GF) * v) + (( 1. GF) * v)) by VECTSP_1:def 17

            .= ((( 1. GF) + ( 1. GF)) * v) by VECTSP_1:def 15;

            hence thesis by A56, A66;

          end;

            suppose

             A68: v <> u;

            deffunc F( set) = ( 0. GF);

            consider f such that

             A69: (f . v) = ( 1. GF) & (f . u) = ( 1. GF) and

             A70: for w be Element of V st w <> v & w <> u holds (f . w) = F(w) from FUNCT_2:sch 7( A68);

            reconsider f as Element of ( Funcs (the carrier of V,the carrier of GF)) by FUNCT_2: 8;

            now

              let w;

              assume not w in {v, u};

              then w <> v & w <> u by TARSKI:def 2;

              hence (f . w) = ( 0. GF) by A70;

            end;

            then

            reconsider f as Linear_Combination of V by Def1;

            

             A71: ( Carrier f) = {v, u}

            proof

              thus ( Carrier f) c= {v, u}

              proof

                let x be object;

                assume x in ( Carrier f);

                then ex w st x = w & (f . w) <> ( 0. GF);

                then x = v or x = u by A70;

                hence thesis by TARSKI:def 2;

              end;

              let x be object;

              assume x in {v, u};

              then x = v or x = u by TARSKI:def 2;

              hence thesis by A1, A69;

            end;

            then

             A72: ( Carrier f) c= A by A66, A67, ZFMISC_1: 32;

            

             A73: (( 1. GF) * u) = u & (( 1. GF) * v) = v by VECTSP_1:def 17;

            reconsider f as Linear_Combination of A by A72, Def4;

            consider F such that

             A74: F is one-to-one & ( rng F) = ( Carrier f) and

             A75: ( Sum (f (#) F)) = ( Sum f) by Def6;

            F = <*v, u*> or F = <*u, v*> by A68, A71, A74, FINSEQ_3: 99;

            then (f (#) F) = <*(( 1. GF) * v), (( 1. GF) * u)*> or (f (#) F) = <*(( 1. GF) * u), (( 1. GF) * v)*> by A69, Th11;

            then ( Sum f) = (v + u) by A75, A73, RLVECT_1: 45;

            hence thesis by A54;

          end;

        end;

        hence thesis;

      end;

      thus thesis by A56;

    end;

    theorem :: VECTSP_6:15

    ( Sum ( ZeroLC V)) = ( 0. V) by Lm1;

    theorem :: VECTSP_6:16

    for l be Linear_Combination of ( {} the carrier of V) holds ( Sum l) = ( 0. V)

    proof

      let l be Linear_Combination of ( {} the carrier of V);

      l = ( ZeroLC V) by Th6;

      hence thesis by Lm1;

    end;

    theorem :: VECTSP_6:17

    

     Th17: for l be Linear_Combination of {v} holds ( Sum l) = ((l . v) * v)

    proof

      let l be Linear_Combination of {v};

      

       A1: ( Carrier l) c= {v} by Def4;

      now

        per cases by A1, ZFMISC_1: 33;

          suppose ( Carrier l) = {} ;

          then

           A2: l = ( ZeroLC V) by Def3;

          

          hence ( Sum l) = ( 0. V) by Lm1

          .= (( 0. GF) * v) by VECTSP_1: 14

          .= ((l . v) * v) by A2, Th3;

        end;

          suppose ( Carrier l) = {v};

          then

          consider F such that

           A3: F is one-to-one & ( rng F) = {v} and

           A4: ( Sum l) = ( Sum (l (#) F)) by Def6;

          F = <*v*> by A3, FINSEQ_3: 97;

          then (l (#) F) = <*((l . v) * v)*> by Th10;

          hence thesis by A4, RLVECT_1: 44;

        end;

      end;

      hence thesis;

    end;

    theorem :: VECTSP_6:18

    

     Th18: v1 <> v2 implies for l be Linear_Combination of {v1, v2} holds ( Sum l) = (((l . v1) * v1) + ((l . v2) * v2))

    proof

      assume

       A1: v1 <> v2;

      let l be Linear_Combination of {v1, v2};

      

       A2: ( Carrier l) c= {v1, v2} by Def4;

      now

        per cases by A2, ZFMISC_1: 36;

          suppose ( Carrier l) = {} ;

          then

           A3: l = ( ZeroLC V) by Def3;

          

          hence ( Sum l) = ( 0. V) by Lm1

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

          .= ((( 0. GF) * v1) + ( 0. V)) by VECTSP_1: 14

          .= ((( 0. GF) * v1) + (( 0. GF) * v2)) by VECTSP_1: 14

          .= (((l . v1) * v1) + (( 0. GF) * v2)) by A3, Th3

          .= (((l . v1) * v1) + ((l . v2) * v2)) by A3, Th3;

        end;

          suppose

           A4: ( Carrier l) = {v1};

          then

          reconsider L = l as Linear_Combination of {v1} by Def4;

          

           A5: not v2 in ( Carrier l) by A1, A4, TARSKI:def 1;

          

          thus ( Sum l) = ( Sum L)

          .= ((l . v1) * v1) by Th17

          .= (((l . v1) * v1) + ( 0. V)) by RLVECT_1: 4

          .= (((l . v1) * v1) + (( 0. GF) * v2)) by VECTSP_1: 14

          .= (((l . v1) * v1) + ((l . v2) * v2)) by A5;

        end;

          suppose

           A6: ( Carrier l) = {v2};

          then

          reconsider L = l as Linear_Combination of {v2} by Def4;

          

           A7: not v1 in ( Carrier l) by A1, A6, TARSKI:def 1;

          

          thus ( Sum l) = ( Sum L)

          .= ((l . v2) * v2) by Th17

          .= (( 0. V) + ((l . v2) * v2)) by RLVECT_1: 4

          .= ((( 0. GF) * v1) + ((l . v2) * v2)) by VECTSP_1: 14

          .= (((l . v1) * v1) + ((l . v2) * v2)) by A7;

        end;

          suppose ( Carrier l) = {v1, v2};

          then

          consider F such that

           A8: F is one-to-one & ( rng F) = {v1, v2} and

           A9: ( Sum l) = ( Sum (l (#) F)) by Def6;

          F = <*v1, v2*> or F = <*v2, v1*> by A1, A8, FINSEQ_3: 99;

          then (l (#) F) = <*((l . v1) * v1), ((l . v2) * v2)*> or (l (#) F) = <*((l . v2) * v2), ((l . v1) * v1)*> by Th11;

          hence thesis by A9, RLVECT_1: 45;

        end;

      end;

      hence thesis;

    end;

    theorem :: VECTSP_6:19

    ( Carrier L) = {} implies ( Sum L) = ( 0. V)

    proof

      assume ( Carrier L) = {} ;

      then L = ( ZeroLC V) by Def3;

      hence thesis by Lm1;

    end;

    theorem :: VECTSP_6:20

    ( Carrier L) = {v} implies ( Sum L) = ((L . v) * v)

    proof

      assume ( Carrier L) = {v};

      then L is Linear_Combination of {v} by Def4;

      hence thesis by Th17;

    end;

    theorem :: VECTSP_6:21

    ( Carrier L) = {v1, v2} & v1 <> v2 implies ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2))

    proof

      assume that

       A1: ( Carrier L) = {v1, v2} and

       A2: v1 <> v2;

      L is Linear_Combination of {v1, v2} by A1, Def4;

      hence thesis by A2, Th18;

    end;

    definition

      let GF be non empty ZeroStr;

      let V be non empty ModuleStr over GF;

      let L1,L2 be Linear_Combination of V;

      :: original: =

      redefine

      :: VECTSP_6:def7

      pred L1 = L2 means for v be Element of V holds (L1 . v) = (L2 . v);

      compatibility by FUNCT_2: 63;

    end

    definition

      let GF, V, L1, L2;

      :: VECTSP_6:def8

      func L1 + L2 -> Linear_Combination of V equals (L1 + L2);

      coherence

      proof

        set f = (L1 + L2);

        

         A1: ( dom L1) = the carrier of V & ( dom L2) = the carrier of V by FUNCT_2:def 1;

        

         A2: ( dom f) = (( dom L1) /\ ( dom L2)) by VFUNCT_1:def 1;

        then f is Function of V, GF by A1, FUNCT_2: 67;

        then

         A3: f is Element of ( Funcs (the carrier of V,the carrier of GF)) by FUNCT_2: 8;

        now

          let v;

          assume

           A4: not v in (( Carrier L1) \/ ( Carrier L2));

          then not v in ( Carrier L2) by XBOOLE_0:def 3;

          then

           A5: (L2 . v) = ( 0. GF);

          

           A6: (L1 /. v) = (L1 . v) & (L2 /. v) = (L2 . v) by A1, PARTFUN1:def 6;

           not v in ( Carrier L1) by A4, XBOOLE_0:def 3;

          then

           A7: (L1 . v) = ( 0. GF);

          

          thus (f . v) = (f /. v) by A1, A2, PARTFUN1:def 6

          .= (( 0. GF) + ( 0. GF)) by A1, A2, A5, A6, A7, VFUNCT_1:def 1

          .= ( 0. GF) by RLVECT_1: 4;

        end;

        hence thesis by A3, Def1;

      end;

    end

    theorem :: VECTSP_6:22

    

     Th22: ((L1 + L2) . v) = ((L1 . v) + (L2 . v))

    proof

      ( dom L1) = the carrier of V & ( dom L2) = the carrier of V by FUNCT_2:def 1;

      then

       A1: (L1 /. v) = (L1 . v) & (L2 /. v) = (L2 . v) by PARTFUN1:def 6;

      

       A2: ( dom (L1 + L2)) = the carrier of V by FUNCT_2:def 1;

      

      hence ((L1 + L2) . v) = ((L1 + L2) /. v) by PARTFUN1:def 6

      .= ((L1 . v) + (L2 . v)) by A1, A2, VFUNCT_1:def 1;

    end;

    theorem :: VECTSP_6:23

    

     Th23: ( Carrier (L1 + L2)) c= (( Carrier L1) \/ ( Carrier L2))

    proof

      let x be object;

      assume x in ( Carrier (L1 + L2));

      then

      consider u such that

       A1: x = u and

       A2: ((L1 + L2) . u) <> ( 0. GF);

      ((L1 + L2) . u) = ((L1 . u) + (L2 . u)) by Th22;

      then (L1 . u) <> ( 0. GF) or (L2 . u) <> ( 0. GF) by A2, RLVECT_1: 4;

      then x in { v1 : (L1 . v1) <> ( 0. GF) } or x in { v2 : (L2 . v2) <> ( 0. GF) } by A1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: VECTSP_6:24

    

     Th24: L1 is Linear_Combination of A & L2 is Linear_Combination of A implies (L1 + L2) is Linear_Combination of A

    proof

      assume L1 is Linear_Combination of A & L2 is Linear_Combination of A;

      then ( Carrier L1) c= A & ( Carrier L2) c= A by Def4;

      then

       A1: (( Carrier L1) \/ ( Carrier L2)) c= A by XBOOLE_1: 8;

      ( Carrier (L1 + L2)) c= (( Carrier L1) \/ ( Carrier L2)) by Th23;

      hence ( Carrier (L1 + L2)) c= A by A1;

    end;

    theorem :: VECTSP_6:25

    (L1 + L2) = (L2 + L1);

    theorem :: VECTSP_6:26

    (L1 + (L2 + L3)) = ((L1 + L2) + L3)

    proof

      let v;

      

      thus ((L1 + (L2 + L3)) . v) = ((L1 . v) + ((L2 + L3) . v)) by Th22

      .= ((L1 . v) + ((L2 . v) + (L3 . v))) by Th22

      .= (((L1 . v) + (L2 . v)) + (L3 . v)) by RLVECT_1:def 3

      .= (((L1 + L2) . v) + (L3 . v)) by Th22

      .= (((L1 + L2) + L3) . v) by Th22;

    end;

    theorem :: VECTSP_6:27

    (L + ( ZeroLC V)) = L & (( ZeroLC V) + L) = L

    proof

      thus (L + ( ZeroLC V)) = L

      proof

        let v;

        

        thus ((L + ( ZeroLC V)) . v) = ((L . v) + (( ZeroLC V) . v)) by Th22

        .= ((L . v) + ( 0. GF)) by Th3

        .= (L . v) by RLVECT_1: 4;

      end;

      hence thesis;

    end;

    definition

      let GF, V, a, L;

      :: VECTSP_6:def9

      func a * L -> Linear_Combination of V means

      : Def9: for v holds (it . v) = (a * (L . v));

      existence

      proof

        deffunc F( Element of V) = (a * (L . $1));

        consider f be Function of the carrier of V, the carrier of GF such that

         A1: for v be Element of V holds (f . v) = F(v) from FUNCT_2:sch 4;

        reconsider f as Element of ( Funcs (the carrier of V,the carrier of GF)) by FUNCT_2: 8;

        now

          let v;

          assume not v in ( Carrier L);

          then (L . v) = ( 0. GF);

          

          hence (f . v) = (a * ( 0. GF)) by A1

          .= ( 0. GF);

        end;

        then

        reconsider f as Linear_Combination of V by Def1;

        take f;

        let v;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let L1, L2;

        assume

         A2: for v holds (L1 . v) = (a * (L . v));

        assume

         A3: for v holds (L2 . v) = (a * (L . v));

        let v;

        

        thus (L1 . v) = (a * (L . v)) by A2

        .= (L2 . v) by A3;

      end;

    end

    theorem :: VECTSP_6:28

    

     Th28: ( Carrier (a * L)) c= ( Carrier L)

    proof

      set T = { u : ((a * L) . u) <> ( 0. GF) };

      set S = { v : (L . v) <> ( 0. GF) };

      T c= S

      proof

        let x be object;

        assume x in T;

        then

        consider u such that

         A1: x = u and

         A2: ((a * L) . u) <> ( 0. GF);

        ((a * L) . u) = (a * (L . u)) by Def9;

        then (L . u) <> ( 0. GF) by A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: VECTSP_6:29

    

     Th29: for GF be Field, V be VectSp of GF, a be Element of GF, L be Linear_Combination of V st a <> ( 0. GF) holds ( Carrier (a * L)) = ( Carrier L)

    proof

      let GF be Field, V be VectSp of GF, a be Element of GF, L be Linear_Combination of V;

      set T = { u where u be Vector of V : ((a * L) . u) <> ( 0. GF) };

      set S = { v where v be Vector of V : (L . v) <> ( 0. GF) };

      assume

       A1: a <> ( 0. GF);

      T = S

      proof

        thus T c= S

        proof

          let x be object;

          assume x in T;

          then

          consider u be Vector of V such that

           A2: x = u and

           A3: ((a * L) . u) <> ( 0. GF);

          ((a * L) . u) = (a * (L . u)) by Def9;

          then (L . u) <> ( 0. GF) by A3;

          hence thesis by A2;

        end;

        let x be object;

        assume x in S;

        then

        consider v be Vector of V such that

         A4: x = v and

         A5: (L . v) <> ( 0. GF);

        ((a * L) . v) = (a * (L . v)) by Def9;

        then ((a * L) . v) <> ( 0. GF) by A1, A5, VECTSP_1: 12;

        hence thesis by A4;

      end;

      hence thesis;

    end;

    theorem :: VECTSP_6:30

    

     Th30: (( 0. GF) * L) = ( ZeroLC V)

    proof

      let v;

      

      thus ((( 0. GF) * L) . v) = (( 0. GF) * (L . v)) by Def9

      .= ( 0. GF)

      .= (( ZeroLC V) . v) by Th3;

    end;

    theorem :: VECTSP_6:31

    

     Th31: L is Linear_Combination of A implies (a * L) is Linear_Combination of A

    proof

      assume L is Linear_Combination of A;

      then

       A1: ( Carrier L) c= A by Def4;

      ( Carrier (a * L)) c= ( Carrier L) by Th28;

      then ( Carrier (a * L)) c= A by A1;

      hence thesis by Def4;

    end;

    theorem :: VECTSP_6:32

    ((a + b) * L) = ((a * L) + (b * L))

    proof

      let v;

      

      thus (((a + b) * L) . v) = ((a + b) * (L . v)) by Def9

      .= ((a * (L . v)) + (b * (L . v))) by VECTSP_1:def 7

      .= (((a * L) . v) + (b * (L . v))) by Def9

      .= (((a * L) . v) + ((b * L) . v)) by Def9

      .= (((a * L) + (b * L)) . v) by Th22;

    end;

    theorem :: VECTSP_6:33

    (a * (L1 + L2)) = ((a * L1) + (a * L2))

    proof

      let v;

      

      thus ((a * (L1 + L2)) . v) = (a * ((L1 + L2) . v)) by Def9

      .= (a * ((L1 . v) + (L2 . v))) by Th22

      .= ((a * (L1 . v)) + (a * (L2 . v))) by VECTSP_1:def 7

      .= (((a * L1) . v) + (a * (L2 . v))) by Def9

      .= (((a * L1) . v) + ((a * L2) . v)) by Def9

      .= (((a * L1) + (a * L2)) . v) by Th22;

    end;

    theorem :: VECTSP_6:34

    

     Th34: (a * (b * L)) = ((a * b) * L)

    proof

      let v;

      

      thus ((a * (b * L)) . v) = (a * ((b * L) . v)) by Def9

      .= (a * (b * (L . v))) by Def9

      .= ((a * b) * (L . v)) by GROUP_1:def 3

      .= (((a * b) * L) . v) by Def9;

    end;

    theorem :: VECTSP_6:35

    (( 1. GF) * L) = L

    proof

      let v;

      

      thus ((( 1. GF) * L) . v) = (( 1. GF) * (L . v)) by Def9

      .= (L . v);

    end;

    definition

      let GF, V, L;

      :: VECTSP_6:def10

      func - L -> Linear_Combination of V equals (( - ( 1. GF)) * L);

      correctness ;

      involutiveness

      proof

        let L,L9 be Linear_Combination of V;

        assume

         A1: L = (( - ( 1. GF)) * L9);

        let v;

        

        thus (L9 . v) = (( 1. GF) * (L9 . v))

        .= ((( 1. GF) * ( 1. GF)) * (L9 . v))

        .= ((( - ( 1. GF)) * ( - ( 1. GF))) * (L9 . v)) by VECTSP_1: 10

        .= (((( - ( 1. GF)) * ( - ( 1. GF))) * L9) . v) by Def9

        .= ((( - ( 1. GF)) * L) . v) by A1, Th34;

      end;

    end

    

     Lm2: (( - ( 1. GF)) * a) = ( - a)

    proof

      

      thus (( - ( 1. GF)) * a) = ((( 0. GF) - ( 1. GF)) * a) by RLVECT_1: 14

      .= ((( 0. GF) * a) - (( 1. GF) * a)) by VECTSP_1: 13

      .= (( 0. GF) - (( 1. GF) * a))

      .= ( - (( 1. GF) * a)) by RLVECT_1: 14

      .= ( - a);

    end;

    theorem :: VECTSP_6:36

    

     Th36: (( - L) . v) = ( - (L . v))

    proof

      

      thus (( - L) . v) = (( - ( 1. GF)) * (L . v)) by Def9

      .= ( - (L . v)) by Lm2;

    end;

    theorem :: VECTSP_6:37

    (L1 + L2) = ( ZeroLC V) implies L2 = ( - L1)

    proof

      assume

       A1: (L1 + L2) = ( ZeroLC V);

      let v;

      ((L1 . v) + (L2 . v)) = (( ZeroLC V) . v) by A1, Th22

      .= ( 0. GF) by Th3;

      

      hence (L2 . v) = ( - (L1 . v)) by RLVECT_1: 6

      .= (( - L1) . v) by Th36;

    end;

    

     Lm3: for GF be Field holds ( - ( 1. GF)) <> ( 0. GF)

    proof

      let GF be Field;

      assume not thesis;

      then ( 1. GF) = ( - ( 0. GF)) by RLVECT_1: 17;

      hence thesis by RLVECT_1: 12;

    end;

    theorem :: VECTSP_6:38

    

     Th38: ( Carrier ( - L)) = ( Carrier L)

    proof

      ( Carrier ( - L)) c= ( Carrier L) & ( Carrier ( - ( - L))) c= ( Carrier ( - L)) by Th28;

      hence thesis;

    end;

    theorem :: VECTSP_6:39

    L is Linear_Combination of A implies ( - L) is Linear_Combination of A by Th31;

    definition

      let GF, V, L1, L2;

      :: VECTSP_6:def11

      func L1 - L2 -> Linear_Combination of V equals (L1 + ( - L2));

      coherence ;

    end

    theorem :: VECTSP_6:40

    

     Th40: ((L1 - L2) . v) = ((L1 . v) - (L2 . v))

    proof

      

      thus ((L1 - L2) . v) = ((L1 . v) + (( - L2) . v)) by Th22

      .= ((L1 . v) + ( - (L2 . v))) by Th36

      .= ((L1 . v) - (L2 . v)) by RLVECT_1:def 11;

    end;

    theorem :: VECTSP_6:41

    ( Carrier (L1 - L2)) c= (( Carrier L1) \/ ( Carrier L2))

    proof

      ( Carrier (L1 - L2)) c= (( Carrier L1) \/ ( Carrier ( - L2))) by Th23;

      hence thesis by Th38;

    end;

    theorem :: VECTSP_6:42

    L1 is Linear_Combination of A & L2 is Linear_Combination of A implies (L1 - L2) is Linear_Combination of A

    proof

      assume that

       A1: L1 is Linear_Combination of A and

       A2: L2 is Linear_Combination of A;

      ( - L2) is Linear_Combination of A by A2, Th31;

      hence thesis by A1, Th24;

    end;

    theorem :: VECTSP_6:43

    

     Th43: (L - L) = ( ZeroLC V)

    proof

      let v;

      

      thus ((L - L) . v) = ((L . v) - (L . v)) by Th40

      .= ( 0. GF) by RLVECT_1: 15

      .= (( ZeroLC V) . v) by Th3;

    end;

    theorem :: VECTSP_6:44

    

     Th44: ( Sum (L1 + L2)) = (( Sum L1) + ( Sum L2))

    proof

      set A = ((( Carrier (L1 + L2)) \/ ( Carrier L1)) \/ ( Carrier L2));

      set C1 = (A \ ( Carrier L1));

      consider p such that

       A1: ( rng p) = C1 and

       A2: p is one-to-one by FINSEQ_4: 58;

      reconsider p as FinSequence of the carrier of V by A1, FINSEQ_1:def 4;

      

       A3: A = (( Carrier L1) \/ (( Carrier (L1 + L2)) \/ ( Carrier L2))) by XBOOLE_1: 4;

      set C3 = (A \ ( Carrier (L1 + L2)));

      consider r such that

       A4: ( rng r) = C3 and

       A5: r is one-to-one by FINSEQ_4: 58;

      reconsider r as FinSequence of the carrier of V by A4, FINSEQ_1:def 4;

      

       A6: A = (( Carrier (L1 + L2)) \/ (( Carrier L1) \/ ( Carrier L2))) by XBOOLE_1: 4;

      set C2 = (A \ ( Carrier L2));

      consider q such that

       A7: ( rng q) = C2 and

       A8: q is one-to-one by FINSEQ_4: 58;

      reconsider q as FinSequence of the carrier of V by A7, FINSEQ_1:def 4;

      consider F such that

       A9: F is one-to-one and

       A10: ( rng F) = ( Carrier (L1 + L2)) and

       A11: ( Sum ((L1 + L2) (#) F)) = ( Sum (L1 + L2)) by Def6;

      set FF = (F ^ r);

      consider G such that

       A12: G is one-to-one and

       A13: ( rng G) = ( Carrier L1) and

       A14: ( Sum (L1 (#) G)) = ( Sum L1) by Def6;

      ( rng FF) = (( rng F) \/ ( rng r)) by FINSEQ_1: 31;

      then ( rng FF) = (( Carrier (L1 + L2)) \/ A) by A10, A4, XBOOLE_1: 39;

      then

       A15: ( rng FF) = A by A6, XBOOLE_1: 7, XBOOLE_1: 12;

      set GG = (G ^ p);

      ( rng GG) = (( rng G) \/ ( rng p)) by FINSEQ_1: 31;

      then ( rng GG) = (( Carrier L1) \/ A) by A13, A1, XBOOLE_1: 39;

      then

       A16: ( rng GG) = A by A3, XBOOLE_1: 7, XBOOLE_1: 12;

      ( rng F) misses ( rng r)

      proof

        set x = the Element of (( rng F) /\ ( rng r));

        assume not thesis;

        then (( rng F) /\ ( rng r)) <> {} ;

        then x in ( Carrier (L1 + L2)) & x in C3 by A10, A4, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A17: FF is one-to-one by A9, A5, FINSEQ_3: 91;

      ( rng G) misses ( rng p)

      proof

        set x = the Element of (( rng G) /\ ( rng p));

        assume not thesis;

        then (( rng G) /\ ( rng p)) <> {} ;

        then x in ( Carrier L1) & x in C1 by A13, A1, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A18: GG is one-to-one by A12, A2, FINSEQ_3: 91;

      then

       A19: ( len GG) = ( len FF) by A17, A16, A15, FINSEQ_1: 48;

      deffunc F( Nat) = (FF <- (GG . $1));

      consider P be FinSequence such that

       A20: ( len P) = ( len FF) and

       A21: for k be Nat st k in ( dom P) holds (P . k) = F(k) from FINSEQ_1:sch 2;

      

       A22: ( dom P) = ( Seg ( len FF)) by A20, FINSEQ_1:def 3;

       A23:

      now

        let x be object;

        assume

         A24: x in ( dom GG);

        then

        reconsider n = x as Element of NAT by FINSEQ_3: 23;

        (GG . n) in ( rng FF) by A16, A15, A24, FUNCT_1:def 3;

        then

         A25: FF just_once_values (GG . n) by A17, FINSEQ_4: 8;

        n in ( Seg ( len FF)) by A19, A24, FINSEQ_1:def 3;

        

        then (FF . (P . n)) = (FF . (FF <- (GG . n))) by A21, A22

        .= (GG . n) by A25, FINSEQ_4:def 3;

        hence (GG . x) = (FF . (P . x));

      end;

      

       A26: ( rng P) c= ( dom FF)

      proof

        let x be object;

        assume x in ( rng P);

        then

        consider y be object such that

         A27: y in ( dom P) and

         A28: (P . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A27, FINSEQ_3: 23;

        y in ( dom GG) by A19, A20, A27, FINSEQ_3: 29;

        then (GG . y) in ( rng FF) by A16, A15, FUNCT_1:def 3;

        then

         A29: FF just_once_values (GG . y) by A17, FINSEQ_4: 8;

        (P . y) = (FF <- (GG . y)) by A21, A27;

        hence thesis by A28, A29, FINSEQ_4:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom P) & (P . x) in ( dom FF)

        proof

          assume x in ( dom GG);

          then x in ( Seg ( len P)) by A19, A20, FINSEQ_1:def 3;

          hence x in ( dom P) by FINSEQ_1:def 3;

          then (P . x) in ( rng P) by FUNCT_1:def 3;

          hence thesis by A26;

        end;

        assume that

         A30: x in ( dom P) and (P . x) in ( dom FF);

        x in ( Seg ( len P)) by A30, FINSEQ_1:def 3;

        hence x in ( dom GG) by A19, A20, FINSEQ_1:def 3;

      end;

      then

       A31: GG = (FF * P) by A23, FUNCT_1: 10;

      ( dom FF) c= ( rng P)

      proof

        set f = ((FF " ) * GG);

        let x be object;

        assume

         A32: x in ( dom FF);

        ( dom (FF " )) = ( rng GG) by A17, A16, A15, FUNCT_1: 33;

        

        then

         A33: ( rng f) = ( rng (FF " )) by RELAT_1: 28

        .= ( dom FF) by A17, FUNCT_1: 33;

        f = (((FF " ) * FF) * P) by A31, RELAT_1: 36

        .= (( id ( dom FF)) * P) by A17, FUNCT_1: 39

        .= P by A26, RELAT_1: 53;

        hence thesis by A32, A33;

      end;

      then

       A34: ( dom FF) = ( rng P) by A26;

      

       A35: ( len r) = ( len ((L1 + L2) (#) r)) by Def5;

      now

        let k be Nat;

        assume

         A36: k in ( dom r);

        then (r /. k) = (r . k) by PARTFUN1:def 6;

        then (r /. k) in C3 by A4, A36, FUNCT_1:def 3;

        then

         A37: not (r /. k) in ( Carrier (L1 + L2)) by XBOOLE_0:def 5;

        k in ( dom ((L1 + L2) (#) r)) by A35, A36, FINSEQ_3: 29;

        then (((L1 + L2) (#) r) . k) = (((L1 + L2) . (r /. k)) * (r /. k)) by Def5;

        hence (((L1 + L2) (#) r) . k) = (( 0. GF) * (r /. k)) by A37;

      end;

      

      then

       A38: ( Sum ((L1 + L2) (#) r)) = (( 0. GF) * ( Sum r)) by A35, RLVECT_2: 67

      .= ( 0. V) by VECTSP_1: 14;

      

       A39: ( len p) = ( len (L1 (#) p)) by Def5;

      now

        let k be Nat;

        assume

         A40: k in ( dom p);

        then (p /. k) = (p . k) by PARTFUN1:def 6;

        then (p /. k) in C1 by A1, A40, FUNCT_1:def 3;

        then

         A41: not (p /. k) in ( Carrier L1) by XBOOLE_0:def 5;

        k in ( dom (L1 (#) p)) by A39, A40, FINSEQ_3: 29;

        then ((L1 (#) p) . k) = ((L1 . (p /. k)) * (p /. k)) by Def5;

        hence ((L1 (#) p) . k) = (( 0. GF) * (p /. k)) by A41;

      end;

      

      then

       A42: ( Sum (L1 (#) p)) = (( 0. GF) * ( Sum p)) by A39, RLVECT_2: 67

      .= ( 0. V) by VECTSP_1: 14;

      

       A43: ( len q) = ( len (L2 (#) q)) by Def5;

      now

        let k be Nat;

        assume

         A44: k in ( dom q);

        then (q /. k) = (q . k) by PARTFUN1:def 6;

        then (q /. k) in C2 by A7, A44, FUNCT_1:def 3;

        then

         A45: not (q /. k) in ( Carrier L2) by XBOOLE_0:def 5;

        k in ( dom (L2 (#) q)) by A43, A44, FINSEQ_3: 29;

        then ((L2 (#) q) . k) = ((L2 . (q /. k)) * (q /. k)) by Def5;

        hence ((L2 (#) q) . k) = (( 0. GF) * (q /. k)) by A45;

      end;

      

      then

       A46: ( Sum (L2 (#) q)) = (( 0. GF) * ( Sum q)) by A43, RLVECT_2: 67

      .= ( 0. V) by VECTSP_1: 14;

      set g = (L1 (#) GG);

      

       A47: ( len g) = ( len GG) by Def5;

      then

       A48: ( Seg ( len GG)) = ( dom g) by FINSEQ_1:def 3;

      set f = ((L1 + L2) (#) FF);

      consider H such that

       A49: H is one-to-one and

       A50: ( rng H) = ( Carrier L2) and

       A51: ( Sum (L2 (#) H)) = ( Sum L2) by Def6;

      set HH = (H ^ q);

      ( rng H) misses ( rng q)

      proof

        set x = the Element of (( rng H) /\ ( rng q));

        assume not thesis;

        then (( rng H) /\ ( rng q)) <> {} ;

        then x in ( Carrier L2) & x in C2 by A50, A7, XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       A52: HH is one-to-one by A49, A8, FINSEQ_3: 91;

      ( rng HH) = (( rng H) \/ ( rng q)) by FINSEQ_1: 31;

      then ( rng HH) = (( Carrier L2) \/ A) by A50, A7, XBOOLE_1: 39;

      then

       A53: ( rng HH) = A by XBOOLE_1: 7, XBOOLE_1: 12;

      then

       A54: ( len GG) = ( len HH) by A52, A18, A16, FINSEQ_1: 48;

      deffunc F( Nat) = (HH <- (GG . $1));

      consider R be FinSequence such that

       A55: ( len R) = ( len HH) and

       A56: for k be Nat st k in ( dom R) holds (R . k) = F(k) from FINSEQ_1:sch 2;

      

       A57: ( dom R) = ( Seg ( len HH)) by A55, FINSEQ_1:def 3;

       A58:

      now

        let x be object;

        assume

         A59: x in ( dom GG);

        then

        reconsider n = x as Element of NAT by FINSEQ_3: 23;

        (GG . n) in ( rng HH) by A16, A53, A59, FUNCT_1:def 3;

        then

         A60: HH just_once_values (GG . n) by A52, FINSEQ_4: 8;

        n in ( Seg ( len HH)) by A54, A59, FINSEQ_1:def 3;

        

        then (HH . (R . n)) = (HH . (HH <- (GG . n))) by A56, A57

        .= (GG . n) by A60, FINSEQ_4:def 3;

        hence (GG . x) = (HH . (R . x));

      end;

      

       A61: ( rng R) c= ( dom HH)

      proof

        let x be object;

        assume x in ( rng R);

        then

        consider y be object such that

         A62: y in ( dom R) and

         A63: (R . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A62, FINSEQ_3: 23;

        y in ( dom GG) by A54, A55, A62, FINSEQ_3: 29;

        then (GG . y) in ( rng HH) by A16, A53, FUNCT_1:def 3;

        then

         A64: HH just_once_values (GG . y) by A52, FINSEQ_4: 8;

        (R . y) = (HH <- (GG . y)) by A56, A62;

        hence thesis by A63, A64, FINSEQ_4:def 3;

      end;

      now

        let x be object;

        thus x in ( dom GG) implies x in ( dom R) & (R . x) in ( dom HH)

        proof

          assume x in ( dom GG);

          then x in ( Seg ( len R)) by A54, A55, FINSEQ_1:def 3;

          hence x in ( dom R) by FINSEQ_1:def 3;

          then (R . x) in ( rng R) by FUNCT_1:def 3;

          hence thesis by A61;

        end;

        assume that

         A65: x in ( dom R) and (R . x) in ( dom HH);

        x in ( Seg ( len R)) by A65, FINSEQ_1:def 3;

        hence x in ( dom GG) by A54, A55, FINSEQ_1:def 3;

      end;

      then

       A66: GG = (HH * R) by A58, FUNCT_1: 10;

      ( dom HH) c= ( rng R)

      proof

        set f = ((HH " ) * GG);

        let x be object;

        assume

         A67: x in ( dom HH);

        ( dom (HH " )) = ( rng GG) by A52, A16, A53, FUNCT_1: 33;

        

        then

         A68: ( rng f) = ( rng (HH " )) by RELAT_1: 28

        .= ( dom HH) by A52, FUNCT_1: 33;

        f = (((HH " ) * HH) * R) by A66, RELAT_1: 36

        .= (( id ( dom HH)) * R) by A52, FUNCT_1: 39

        .= R by A61, RELAT_1: 53;

        hence thesis by A67, A68;

      end;

      then

       A69: ( dom HH) = ( rng R) by A61;

      set h = (L2 (#) HH);

      

       A70: ( Sum h) = ( Sum ((L2 (#) H) ^ (L2 (#) q))) by Th13

      .= (( Sum (L2 (#) H)) + ( 0. V)) by A46, RLVECT_1: 41

      .= ( Sum (L2 (#) H)) by RLVECT_1: 4;

      

       A71: ( Sum g) = ( Sum ((L1 (#) G) ^ (L1 (#) p))) by Th13

      .= (( Sum (L1 (#) G)) + ( 0. V)) by A42, RLVECT_1: 41

      .= ( Sum (L1 (#) G)) by RLVECT_1: 4;

      

       A72: ( dom P) = ( dom FF) by A20, FINSEQ_3: 29;

      then

       A73: P is one-to-one by A34, FINSEQ_4: 60;

      

       A74: ( dom R) = ( dom HH) by A55, FINSEQ_3: 29;

      then

       A75: R is one-to-one by A69, FINSEQ_4: 60;

      reconsider R as Function of ( dom HH), ( dom HH) by A61, A74, FUNCT_2: 2;

      reconsider R as Permutation of ( dom HH) by A69, A75, FUNCT_2: 57;

      

       A76: ( len h) = ( len HH) by Def5;

      then ( dom h) = ( dom HH) by FINSEQ_3: 29;

      then

      reconsider R as Permutation of ( dom h);

      reconsider Hp = (h * R) as FinSequence of the carrier of V by FINSEQ_2: 47;

      

       A77: ( len Hp) = ( len GG) by A54, A76, FINSEQ_2: 44;

      reconsider P as Function of ( dom FF), ( dom FF) by A26, A72, FUNCT_2: 2;

      reconsider P as Permutation of ( dom FF) by A34, A73, FUNCT_2: 57;

      

       A78: ( len f) = ( len FF) by Def5;

      then ( dom f) = ( dom FF) by FINSEQ_3: 29;

      then

      reconsider P as Permutation of ( dom f);

      reconsider Fp = (f * P) as FinSequence of the carrier of V by FINSEQ_2: 47;

      

       A79: ( Sum f) = ( Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r))) by Th13

      .= (( Sum ((L1 + L2) (#) F)) + ( 0. V)) by A38, RLVECT_1: 41

      .= ( Sum ((L1 + L2) (#) F)) by RLVECT_1: 4;

      deffunc F( Nat) = ((g /. $1) + (Hp /. $1));

      consider I be FinSequence such that

       A80: ( len I) = ( len GG) and

       A81: for k be Nat st k in ( dom I) holds (I . k) = F(k) from FINSEQ_1:sch 2;

      

       A82: ( dom I) = ( Seg ( len GG)) by A80, FINSEQ_1:def 3;

      then

       A83: for k be Nat st k in ( Seg ( len GG)) holds (I . k) = F(k) by A81;

      ( rng I) c= the carrier of V

      proof

        let x be object;

        assume x in ( rng I);

        then

        consider y be object such that

         A84: y in ( dom I) and

         A85: (I . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A84, FINSEQ_3: 23;

        (I . y) = ((g /. y) + (Hp /. y)) by A81, A84;

        hence thesis by A85;

      end;

      then

      reconsider I as FinSequence of the carrier of V by FINSEQ_1:def 4;

      

       A86: ( len Fp) = ( len I) by A19, A78, A80, FINSEQ_2: 44;

       A87:

      now

        let x be object;

        assume

         A88: x in ( Seg ( len I));

        then

        reconsider k = x as Element of NAT ;

        

         A89: x in ( dom Hp) by A80, A77, A88, FINSEQ_1:def 3;

        

        then

         A90: (Hp /. k) = ((h * R) . k) by PARTFUN1:def 6

        .= (h . (R . k)) by A89, FUNCT_1: 12;

        set v = (GG /. k);

        x in ( dom Fp) by A86, A88, FINSEQ_1:def 3;

        then

         A91: (Fp . k) = (f . (P . k)) by FUNCT_1: 12;

        

         A92: x in ( dom HH) by A54, A80, A88, FINSEQ_1:def 3;

        then (R . k) in ( dom R) by A69, A74, FUNCT_1:def 3;

        then

        reconsider j = (R . k) as Element of NAT by FINSEQ_3: 23;

        

         A93: x in ( dom GG) by A80, A88, FINSEQ_1:def 3;

        

        then

         A94: (HH . j) = (GG . k) by A58

        .= (GG /. k) by A93, PARTFUN1:def 6;

        

         A95: ( dom FF) = ( dom GG) by A19, FINSEQ_3: 29;

        then (P . k) in ( dom P) by A34, A72, A93, FUNCT_1:def 3;

        then

        reconsider l = (P . k) as Element of NAT by FINSEQ_3: 23;

        

         A96: (FF . l) = (GG . k) by A23, A93

        .= (GG /. k) by A93, PARTFUN1:def 6;

        (R . k) in ( dom HH) by A69, A74, A92, FUNCT_1:def 3;

        then

         A97: (h . j) = ((L2 . v) * v) by A94, Th8;

        (P . k) in ( dom FF) by A34, A72, A93, A95, FUNCT_1:def 3;

        

        then

         A98: (f . l) = (((L1 + L2) . v) * v) by A96, Th8

        .= (((L1 . v) + (L2 . v)) * v) by Th22

        .= (((L1 . v) * v) + ((L2 . v) * v)) by VECTSP_1:def 15;

        

         A99: x in ( dom g) by A80, A47, A88, FINSEQ_1:def 3;

        

        then (g /. k) = (g . k) by PARTFUN1:def 6

        .= ((L1 . v) * v) by A99, Def5;

        hence (I . x) = (Fp . x) by A80, A81, A82, A88, A90, A97, A91, A98;

      end;

      ( dom I) = ( Seg ( len I)) & ( dom Fp) = ( Seg ( len I)) by A86, FINSEQ_1:def 3;

      then

       A100: I = Fp by A87;

      ( Sum Fp) = ( Sum f) & ( Sum Hp) = ( Sum h) by RLVECT_2: 7;

      hence thesis by A11, A14, A51, A71, A70, A79, A80, A83, A77, A47, A100, A48, RLVECT_2: 2;

    end;

    theorem :: VECTSP_6:45

    for GF be Field, V be VectSp of GF, L be Linear_Combination of V, a be Element of GF holds ( Sum (a * L)) = (a * ( Sum L))

    proof

      let GF be Field, V be VectSp of GF, L be Linear_Combination of V, a be Element of GF;

      per cases ;

        suppose

         A1: a <> ( 0. GF);

        set l = (a * L);

        consider F be FinSequence of the carrier of V such that

         A2: F is one-to-one and

         A3: ( rng F) = ( Carrier (a * L)) and

         A4: ( Sum (a * L)) = ( Sum ((a * L) (#) F)) by Def6;

        consider G be FinSequence of the carrier of V such that

         A5: G is one-to-one and

         A6: ( rng G) = ( Carrier L) and

         A7: ( Sum L) = ( Sum (L (#) G)) by Def6;

        

         A8: ( len G) = ( len F) by A1, A2, A3, A5, A6, Th29, FINSEQ_1: 48;

        set f = ((a * L) (#) F);

        set g = (L (#) G);

        deffunc F( Nat) = (F <- (G . $1));

        consider P be FinSequence such that

         A9: ( len P) = ( len F) and

         A10: for k be Nat st k in ( dom P) holds (P . k) = F(k) from FINSEQ_1:sch 2;

        

         A11: ( Carrier l) = ( Carrier L) by A1, Th29;

        

         A12: ( rng P) c= ( Seg ( len F))

        proof

          let x be object;

          assume x in ( rng P);

          then

          consider y be object such that

           A13: y in ( dom P) and

           A14: (P . y) = x by FUNCT_1:def 3;

          reconsider y as Element of NAT by A13, FINSEQ_3: 23;

          y in ( Seg ( len F)) by A9, A13, FINSEQ_1:def 3;

          then y in ( dom G) by A8, FINSEQ_1:def 3;

          then (G . y) in ( rng F) by A3, A6, A11, FUNCT_1:def 3;

          then

           A15: F just_once_values (G . y) by A2, FINSEQ_4: 8;

          (P . y) = (F <- (G . y)) by A10, A13;

          then (P . y) in ( dom F) by A15, FINSEQ_4:def 3;

          hence thesis by A14, FINSEQ_1:def 3;

        end;

         A16:

        now

          let x be object;

          thus x in ( dom G) implies x in ( dom P) & (P . x) in ( dom F)

          proof

            assume x in ( dom G);

            then x in ( Seg ( len P)) by A9, A8, FINSEQ_1:def 3;

            hence x in ( dom P) by FINSEQ_1:def 3;

            then (P . x) in ( rng P) by FUNCT_1:def 3;

            then (P . x) in ( Seg ( len F)) by A12;

            hence thesis by FINSEQ_1:def 3;

          end;

          assume that

           A17: x in ( dom P) and (P . x) in ( dom F);

          x in ( Seg ( len P)) by A17, FINSEQ_1:def 3;

          hence x in ( dom G) by A9, A8, FINSEQ_1:def 3;

        end;

        

         A18: ( dom P) = ( Seg ( len F)) by A9, FINSEQ_1:def 3;

        now

          let x be object;

          assume

           A19: x in ( dom G);

          then

          reconsider n = x as Element of NAT by FINSEQ_3: 23;

          (G . n) in ( rng F) by A3, A6, A11, A19, FUNCT_1:def 3;

          then

           A20: F just_once_values (G . n) by A2, FINSEQ_4: 8;

          n in ( Seg ( len F)) by A8, A19, FINSEQ_1:def 3;

          

          then (F . (P . n)) = (F . (F <- (G . n))) by A10, A18

          .= (G . n) by A20, FINSEQ_4:def 3;

          hence (G . x) = (F . (P . x));

        end;

        then

         A21: G = (F * P) by A16, FUNCT_1: 10;

        ( Seg ( len F)) c= ( rng P)

        proof

          set f = ((F " ) * G);

          let x be object;

          assume

           A22: x in ( Seg ( len F));

          ( dom (F " )) = ( rng G) by A2, A3, A6, A11, FUNCT_1: 33;

          

          then

           A23: ( rng f) = ( rng (F " )) by RELAT_1: 28

          .= ( dom F) by A2, FUNCT_1: 33;

          

           A24: ( rng P) c= ( dom F) by A12, FINSEQ_1:def 3;

          f = (((F " ) * F) * P) by A21, RELAT_1: 36

          .= (( id ( dom F)) * P) by A2, FUNCT_1: 39

          .= P by A24, RELAT_1: 53;

          hence thesis by A22, A23, FINSEQ_1:def 3;

        end;

        then

         A25: ( Seg ( len F)) = ( rng P) by A12;

        

         A26: ( dom P) = ( Seg ( len F)) by A9, FINSEQ_1:def 3;

        then

         A27: P is one-to-one by A25, FINSEQ_4: 60;

        reconsider P as Function of ( Seg ( len F)), ( Seg ( len F)) by A12, A26, FUNCT_2: 2;

        reconsider P as Permutation of ( Seg ( len F)) by A25, A27, FUNCT_2: 57;

        

         A28: ( len f) = ( len F) by Def5;

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

        then

        reconsider P as Permutation of ( dom f);

        reconsider Fp = (f * P) as FinSequence of the carrier of V by FINSEQ_2: 47;

        

         A29: ( len Fp) = ( len f) by FINSEQ_2: 44;

        then

         A30: ( len Fp) = ( len g) by A8, A28, Def5;

         A31:

        now

          let k be Nat;

          let v be Vector of V;

          assume that

           A32: k in ( dom g) and

           A33: v = (g . k);

          

           A34: k in ( Seg ( len g)) by A32, FINSEQ_1:def 3;

          then

           A35: k in ( dom P) by A9, A28, A29, A30, FINSEQ_1:def 3;

          

           A36: k in ( dom G) by A8, A28, A29, A30, A34, FINSEQ_1:def 3;

          then (G . k) in ( rng G) by FUNCT_1:def 3;

          then F just_once_values (G . k) by A2, A3, A6, A11, FINSEQ_4: 8;

          then

           A37: (F <- (G . k)) in ( dom F) by FINSEQ_4:def 3;

          then

          reconsider i = (F <- (G . k)) as Element of NAT by FINSEQ_3: 23;

          

           A38: (G /. k) = (G . k) by A36, PARTFUN1:def 6

          .= (F . (P . k)) by A21, A35, FUNCT_1: 13

          .= (F . i) by A10, A18, A28, A29, A30, A34

          .= (F /. i) by A37, PARTFUN1:def 6;

          i in ( Seg ( len f)) by A28, A37, FINSEQ_1:def 3;

          then

           A39: i in ( dom f) by FINSEQ_1:def 3;

          

          thus (Fp . k) = (f . (P . k)) by A35, FUNCT_1: 13

          .= (f . (F <- (G . k))) by A10, A18, A28, A29, A30, A34

          .= ((l . (F /. i)) * (F /. i)) by A39, Def5

          .= ((a * (L . (F /. i))) * (F /. i)) by Def9

          .= (a * ((L . (F /. i)) * (F /. i))) by VECTSP_1:def 16

          .= (a * v) by A32, A33, A38, Def5;

        end;

        ( Sum Fp) = ( Sum f) & ( dom Fp) = ( dom g) by A30, FINSEQ_3: 29, RLVECT_2: 7;

        hence thesis by A4, A7, A30, A31, RLVECT_2: 66;

      end;

        suppose

         A40: a = ( 0. GF);

        

        hence ( Sum (a * L)) = ( Sum ( ZeroLC V)) by Th30

        .= ( 0. V) by Lm1

        .= (a * ( Sum L)) by A40, VECTSP_1: 14;

      end;

    end;

    theorem :: VECTSP_6:46

    

     Th46: ( Sum ( - L)) = ( - ( Sum L))

    proof

      (( Sum L) + ( Sum ( - L))) = ( Sum (L - L)) by Th44

      .= ( Sum ( ZeroLC V)) by Th43

      .= ( 0. V) by Lm1;

      hence thesis by VECTSP_1: 16;

    end;

    theorem :: VECTSP_6:47

    ( Sum (L1 - L2)) = (( Sum L1) - ( Sum L2))

    proof

      

      thus ( Sum (L1 - L2)) = (( Sum L1) + ( Sum ( - L2))) by Th44

      .= (( Sum L1) + ( - ( Sum L2))) by Th46

      .= (( Sum L1) - ( Sum L2)) by RLVECT_1:def 11;

    end;

    theorem :: VECTSP_6:48

    (( - ( 1. GF)) * a) = ( - a) by Lm2;

    theorem :: VECTSP_6:49

    for GF be Field holds ( - ( 1. GF)) <> ( 0. GF) by Lm3;