zmodul05.miz



    begin

    reserve V,W for Z_Module;

    registration

      let V be LeftMod of INT.Ring ;

      let A be finite Subset of V;

      cluster ( Lin A) -> finitely-generated;

      correctness

      proof

        for x be object st x in A holds x in the carrier of ( Lin A)

        proof

          let x be object such that

           A1: x in A;

          x in ( Lin A) by A1, MOD_3: 5;

          hence thesis;

        end;

        then A c= the carrier of ( Lin A);

        then

        reconsider AA = A as finite Subset of ( Lin A);

        ( Lin AA) = ( Lin A) by ZMODUL03: 20;

        hence thesis;

      end;

    end

    theorem :: ZMODUL05:1

    

     RL5Th33: for V be finite-rank free Z_Module holds ( rank V) = 0 iff ( (Omega). V) = ( (0). V)

    proof

      let V be finite-rank free Z_Module;

      consider I be finite Subset of V such that

       A1: I is Basis of V by ZMODUL03:def 3;

      hereby

        consider I be finite Subset of V such that

         A2: I is Basis of V by ZMODUL03:def 3;

        assume ( rank V) = 0 ;

        then ( card I) = 0 by A2, ZMODUL03:def 5;

        then

         A3: I = ( {} the carrier of V);

        ( (Omega). V) = ( Lin I) by A2, VECTSP_7:def 3

        .= ( (0). V) by A3, ZMODUL02: 67;

        hence ( (Omega). V) = ( (0). V);

      end;

      assume ( (Omega). V) = ( (0). V);

      then ( Lin I) = ( (0). V) by A1, VECTSP_7:def 3;

      then I = {} or I = {( 0. V)} by ZMODUL02: 68;

      hence thesis by A1, VECTSP_7:def 3, ZMODUL03:def 5, CARD_1: 27;

    end;

    registration

      let V be finite-rank free Z_Module;

      cluster finite for Basis of V;

      existence

      proof

        consider A be finite Subset of V such that

         A1: A is Basis of V by ZMODUL03:def 3;

        reconsider A as Basis of V by A1;

        take A;

        thus thesis;

      end;

    end

    registration

      let V be finite-rank free Z_Module;

      cluster -> finite for Basis of V;

      correctness ;

    end

    theorem :: ZMODUL05:2

    

     RL5Th29: for V be finite-rank free Z_Module, W be Submodule of V holds ( rank W) <= ( rank V)

    proof

      let V be finite-rank free Z_Module, W be Submodule of V;

      consider I be finite Subset of V such that

       A1: I is Basis of V by ZMODUL03:def 3;

      W is finite-rank;

      then

      consider A be finite Subset of W such that

       A2: A is Basis of W;

      reconsider AA = A as linearly-independent Subset of V by A2, ZMODUL03: 15, VECTSP_7:def 3;

      ( card AA) c= ( card I) by A1, ZMODUL04: 20;

      then ( card A) c< ( card I) or ( card A) = ( card I);

      then ( card ( card A)) < ( card ( card I)) or ( card A) = ( card I) by CARD_2: 48;

      then ( card A) <= ( rank V) by A1, ZMODUL03:def 5;

      hence thesis by A2, ZMODUL03:def 5;

    end;

    theorem :: ZMODUL05:3

    

     RL5Th30: for V be Z_Module, A be finite linearly-independent Subset of V holds ( card A) = ( rank ( Lin A))

    proof

      let V be Z_Module, A be finite linearly-independent Subset of V;

      set W = ( Lin A);

      now

        let x be object;

        assume x in A;

        then x in W by ZMODUL02: 65;

        hence x in the carrier of W;

      end;

      then

      reconsider B = A as finite linearly-independent Subset of W by ZMODUL03: 16, TARSKI:def 3;

      W = ( Lin B) by ZMODUL03: 20;

      then

      reconsider B as Basis of W by VECTSP_7:def 3;

      ( card B) = ( rank W) by ZMODUL03:def 5;

      hence thesis;

    end;

    theorem :: ZMODUL05:4

    for V be finite-rank free Z_Module holds ( rank V) = ( rank ( (Omega). V))

    proof

      let V be finite-rank free Z_Module;

      consider I be finite Subset of V such that

       A1: I is Basis of V by ZMODUL03:def 3;

      

       A2: ( (Omega). V) = ( Lin I) by A1, VECTSP_7:def 3;

      ( card I) = ( rank V) & I is linearly-independent by A1, ZMODUL03:def 5, VECTSP_7:def 3;

      hence thesis by A2, RL5Th30;

    end;

    theorem :: ZMODUL05:5

    for V be finite-rank free Z_Module holds ( rank V) = 1 iff ex v be VECTOR of V st v <> ( 0. V) & ( (Omega). V) = ( Lin {v})

    proof

      let V be finite-rank free Z_Module;

      hereby

        consider I be finite Subset of V such that

         A1: I is Basis of V by ZMODUL03:def 3;

        assume ( rank V) = 1;

        then ( card I) = 1 by A1, ZMODUL03:def 5;

        then

        consider v be object such that

         A2: I = {v} by CARD_2: 42;

        v in I by A2, TARSKI:def 1;

        then

        reconsider v as VECTOR of V;

        

         A3: v <> ( 0. V) by A1, A2, VECTSP_7:def 3;

        ( Lin {v}) = the ModuleStr of V by A1, A2, VECTSP_7:def 3;

        hence ex v be VECTOR of V st v <> ( 0. V) & ( (Omega). V) = ( Lin {v}) by A3;

      end;

      given v be VECTOR of V such that

       A4: v <> ( 0. V) & ( (Omega). V) = ( Lin {v});

       {v} is linearly-independent & ( Lin {v}) = the ModuleStr of V by A4, ZMODUL02: 59;

      then

       A5: {v} is Basis of V by VECTSP_7:def 3;

      ( card {v}) = 1 by CARD_1: 30;

      hence thesis by A5, ZMODUL03:def 5;

    end;

    theorem :: ZMODUL05:6

    for V be finite-rank free Z_Module holds ( rank V) = 2 iff ex u,v be VECTOR of V st u <> v & {u, v} is linearly-independent & ( (Omega). V) = ( Lin {u, v})

    proof

      let V be finite-rank free Z_Module;

      hereby

        consider I be finite Subset of V such that

         A1: I is Basis of V by ZMODUL03:def 3;

        assume ( rank V) = 2;

        then

         A2: ( card I) = 2 by A1, ZMODUL03:def 5;

        then

        consider u be object such that

         A3: u in I by CARD_1: 27, XBOOLE_0:def 1;

        reconsider u as VECTOR of V by A3;

        now

          assume I c= {u};

          then ( card I) <= ( card {u}) by NAT_1: 43;

          then 2 <= 1 by A2, CARD_1: 30;

          hence contradiction;

        end;

        then

        consider v be object such that

         A4: v in I and

         A5: not v in {u};

        reconsider v as VECTOR of V by A4;

        

         A6: v <> u by A5, TARSKI:def 1;

         A7:

        now

          assume not I c= {u, v};

          then

          consider w be object such that

           A8: w in I and

           A9: not w in {u, v};

           {u, v, w} c= I by A3, A4, A8, ENUMSET1:def 1;

          then

           A10: ( card {u, v, w}) <= ( card I) by NAT_1: 43;

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

          then 3 <= 2 by A2, A6, A10, CARD_2: 58;

          hence contradiction;

        end;

         {u, v} c= I by A3, A4, TARSKI:def 2;

        then

         A11: I = {u, v} by A7;

        then

         A12: {u, v} is linearly-independent by A1, VECTSP_7:def 3;

        ( Lin {u, v}) = ( (Omega). V) by A1, A11, VECTSP_7:def 3;

        hence ex u,v be VECTOR of V st u <> v & {u, v} is linearly-independent & ( (Omega). V) = ( Lin {u, v}) by A6, A12;

      end;

      given u,v be VECTOR of V such that

       A13: u <> v and

       A14: {u, v} is linearly-independent and

       A15: ( (Omega). V) = ( Lin {u, v});

      

       A16: {u, v} is Basis of V by A14, A15, VECTSP_7:def 3;

      ( card {u, v}) = 2 by A13, CARD_2: 57;

      hence thesis by A16, ZMODUL03:def 5;

    end;

    

     RL5Lm2: for V be finite-rank free Z_Module, W be Submodule of V, n be Nat holds n <= ( rank V) implies ex W be strict free Submodule of V st ( rank W) = n

    proof

      let V be finite-rank free Z_Module, W be Submodule of V, n be Nat;

      consider I be finite Subset of V such that

       A1: I is Basis of V by ZMODUL03:def 3;

      assume n <= ( rank V);

      then n <= ( card I) by A1, ZMODUL03:def 5;

      then

      consider A be finite Subset of I such that

       A2: ( card A) = n by FINSEQ_4: 72;

      reconsider A as finite Subset of V by XBOOLE_1: 1;

      reconsider W = ( Lin A) as strict finite-rank free Submodule of V;

      A is linearly-independent by ZMODUL02: 56, A1, VECTSP_7:def 3;

      then ( rank W) = n by A2, RL5Th30;

      hence thesis;

    end;

    theorem :: ZMODUL05:7

    for V be finite-rank free Z_Module, W be Submodule of V, n be Nat holds n <= ( rank V) iff ex W be strict free Submodule of V st ( rank W) = n by RL5Lm2, RL5Th29;

    definition

      let V be finite-rank free Z_Module, n be Nat;

      :: ZMODUL05:def1

      func n Submodules_of V -> set means

      : RL5Def4: for x be object holds x in it iff ex W be strict free Submodule of V st W = x & ( rank W) = n;

      existence

      proof

        set S = { ( Lin A) where A be finite Subset of V : A is linearly-independent & ( card A) = n };

        take S;

        for x be object holds x in S iff ex W be strict free Submodule of V st W = x & ( rank W) = n

        proof

          let x be object;

          hereby

            assume x in S;

            then

             A1: ex A be finite Subset of V st x = ( Lin A) & A is linearly-independent & ( card A) = n;

            then

            reconsider W = x as strict free Submodule of V;

            ( rank W) = n by A1, RL5Th30;

            hence ex W be strict free Submodule of V st W = x & ( rank W) = n;

          end;

          given W be strict free Submodule of V such that

           A2: W = x and

           A3: ( rank W) = n;

          consider A be finite Subset of W such that

           A4: A is Basis of W by ZMODUL03:def 3;

          reconsider A as Subset of W;

          reconsider B = A as linearly-independent Subset of V by A4, ZMODUL03: 15, VECTSP_7:def 3;

          

           A5: x = ( Lin A) by A2, A4, VECTSP_7:def 3

          .= ( Lin B) by ZMODUL03: 20;

          then ( card B) = n by A2, A3, RL5Th30;

          hence thesis by A5;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be set;

        assume that

         A6: for x be object holds x in S1 iff ex W be strict free Submodule of V st W = x & ( rank W) = n and

         A7: for x be object holds x in S2 iff ex W be strict free Submodule of V st W = x & ( rank W) = n;

        for x be object holds x in S1 iff x in S2

        proof

          let x be object;

          hereby

            assume x in S1;

            then ex W be strict free Submodule of V st W = x & ( rank W) = n by A6;

            hence x in S2 by A7;

          end;

          assume x in S2;

          then ex W be strict free Submodule of V st W = x & ( rank W) = n by A7;

          hence thesis by A6;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: ZMODUL05:8

    for V be finite-rank free Z_Module, n be Nat holds n <= ( rank V) implies (n Submodules_of V) is non empty

    proof

      let V be finite-rank free Z_Module, n be Nat;

      assume n <= ( rank V);

      then ex W be strict free Submodule of V st ( rank W) = n by RL5Lm2;

      hence thesis by RL5Def4;

    end;

    theorem :: ZMODUL05:9

    for V be finite-rank free Z_Module, n be Nat holds ( rank V) < n implies (n Submodules_of V) = {}

    proof

      let V be finite-rank free Z_Module, n be Nat;

      assume that

       A1: ( rank V) < n and

       A2: (n Submodules_of V) <> {} ;

      consider x be object such that

       A3: x in (n Submodules_of V) by A2, XBOOLE_0:def 1;

      ex W be strict free Submodule of V st W = x & ( rank W) = n by A3, RL5Def4;

      hence contradiction by A1, RL5Th29;

    end;

    theorem :: ZMODUL05:10

    for V be finite-rank free Z_Module, W be Submodule of V, n be Nat holds (n Submodules_of W) c= (n Submodules_of V)

    proof

      let V be finite-rank free Z_Module, W be Submodule of V, n be Nat;

      let x be object;

      assume x in (n Submodules_of W);

      then

      consider W1 be strict free Submodule of W such that

       A1: W1 = x and

       A2: ( rank W1) = n by RL5Def4;

      reconsider W1 as strict free Submodule of V by ZMODUL01: 42;

      W1 in (n Submodules_of V) by A2, RL5Def4;

      hence thesis by A1;

    end;

    theorem :: ZMODUL05:11

    for F,G be FinSequence of INT , v be Integer holds ( len F) = (( len G) + 1) & G = (F | ( dom G)) & v = (F . ( len F)) implies ( Sum F) = (( Sum G) + v)

    proof

      let F,G be FinSequence of INT , v be Integer;

      assume that

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

       A2: G = (F | ( dom G)) and

       A3: v = (F . ( len F));

      reconsider Fr = F, Gr = G as real-valued FinSequence;

      reconsider vr = v as Real;

      set k = ( len G);

      ( dom G) = ( Seg k) by FINSEQ_1:def 3;

      then Fr = (Gr ^ <*vr*>) by A1, A2, A3, FINSEQ_3: 55;

      hence thesis by RVSUM_1: 74;

    end;

    theorem :: ZMODUL05:12

    

     RLVECT142: for F,G be FinSequence of INT st ( rng F) = ( rng G) & F is one-to-one & G is one-to-one holds ( Sum F) = ( Sum G)

    proof

      let F,G be FinSequence of INT ;

      assume

       A1: ( rng F) = ( rng G) & F is one-to-one & G is one-to-one;

      

      thus ( Sum F) = ( addint $$ F) by GR_CY_1: 2

      .= ( addint $$ G) by A1, FINSOP_1: 8

      .= ( Sum G) by GR_CY_1: 2;

    end;

    definition

      let T be finite Subset of the carrier of INT.Ring ;

      :: ZMODUL05:def2

      func Sum T -> Element of INT.Ring means ex F be FinSequence of INT st ( rng F) = T & F is one-to-one & it = ( Sum F);

      existence

      proof

        consider p be FinSequence such that

         A1: ( rng p) = T and

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

        reconsider p as FinSequence of the carrier of INT.Ring by A1, FINSEQ_1:def 4;

         INT = the carrier of INT.Ring by INT_3:def 3;

        then

        reconsider F = p as FinSequence of INT ;

        reconsider Sp = ( Sum F) as Element of INT.Ring by INT_3:def 3;

        take Sp, F;

        thus ( rng F) = T & F is one-to-one & ( Sum F) = Sp by A1, A2;

      end;

      uniqueness by RLVECT142;

    end

    theorem :: ZMODUL05:13

    

     RF9: for K be Ring holds for R1,R2 be FinSequence of K st (R1,R2) are_fiberwise_equipotent holds ( Sum R1) = ( Sum R2)

    proof

      let K be Ring;

      let R1,R2 be FinSequence of K;

      defpred P[ Nat] means for f,g be FinSequence of K st (f,g) are_fiberwise_equipotent & ( len f) = $1 holds ( Sum f) = ( Sum g);

      assume

       A1: (R1,R2) are_fiberwise_equipotent ;

      

       A2: ( len R1) = ( len R1);

      

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

      proof

        let n be Nat;

        assume

         A4: P[n];

        let f,g be FinSequence of K;

        assume that

         A5: (f,g) are_fiberwise_equipotent and

         A6: ( len f) = (n + 1);

        set a = (f /. (n + 1));

        

         A7: ( rng f) = ( rng g) by A5, CLASSES1: 75;

        ( 0 qua Nat + 1) <= (n + 1) by NAT_1: 13;

        then

         Z: (n + 1) in ( dom f) by A6, FINSEQ_3: 25;

        then

         X: a = (f . (n + 1)) by PARTFUN1:def 6;

        then a in ( rng g) by A7, FUNCT_1:def 3, Z;

        then

        consider m be Nat such that

         A8: m in ( dom g) and

         A9: (g . m) = a by FINSEQ_2: 10;

        set gg = (g /^ m), gm = (g | m);

        m <= ( len g) by A8, FINSEQ_3: 25;

        then

         A10: ( len gm) = m by FINSEQ_1: 59;

        

         A11: 1 <= m by A8, FINSEQ_3: 25;

        then ( max ( 0 ,(m - 1))) = (m - 1) by FINSEQ_2: 4;

        then

        reconsider m1 = (m - 1) as Element of NAT by FINSEQ_2: 5;

        

         A12: m = (m1 + 1);

        then

         A13: ( Seg m1) c= ( Seg m) by FINSEQ_1: 5, NAT_1: 11;

        m in ( Seg m) by A11;

        then (gm . m) = a by A8, A9, RFINSEQ: 6;

        then

         A14: gm = ((gm | m1) ^ <*a*>) by A10, A12, RFINSEQ: 7;

        set fn = (f | n);

        

         A15: g = ((g | m) ^ (g /^ m)) by RFINSEQ: 8;

        

         A16: (gm | m1) = (gm | ( Seg m1))

        .= ((g | ( Seg m)) | ( Seg m1))

        .= (g | (( Seg m) /\ ( Seg m1))) by RELAT_1: 71

        .= (g | ( Seg m1)) by A13, XBOOLE_1: 28

        .= (g | m1);

        

         A17: f = (fn ^ <*a*>) by A6, RFINSEQ: 7, X;

        now

          let x be object;

          ( card ( Coim (f,x))) = ( card ( Coim (g,x))) by A5;

          

          then (( card (fn " {x})) + ( card ( <*a*> " {x}))) = ( card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x})) by A15, A14, A16, A17, FINSEQ_3: 57

          .= (( card (((g | m1) ^ <*a*>) " {x})) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ( <*a*> " {x}))) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ((g /^ m) " {x}))) + ( card ( <*a*> " {x})))

          .= (( card (((g | m1) ^ (g /^ m)) " {x})) + ( card ( <*a*> " {x}))) by FINSEQ_3: 57;

          hence ( card ( Coim (fn,x))) = ( card ( Coim (((g | m1) ^ (g /^ m)),x)));

        end;

        then

         A18: (fn,((g | m1) ^ (g /^ m))) are_fiberwise_equipotent ;

        ( len fn) = n by A6, FINSEQ_1: 59, NAT_1: 11;

        then ( Sum fn) = ( Sum ((g | m1) ^ gg)) by A4, A18;

        

        hence ( Sum f) = (( Sum ((g | m1) ^ gg)) + ( Sum <*a*>)) by A17, RLVECT_1: 41

        .= ((( Sum (g | m1)) + ( Sum gg)) + ( Sum <*a*>)) by RLVECT_1: 41

        .= (( Sum (g | m1)) + (( Sum gg) + ( Sum <*a*>))) by RLVECT_1:def 3

        .= (( Sum (g | m1)) + (( Sum <*a*>) + ( Sum gg)))

        .= ((( Sum (g | m1)) + ( Sum <*a*>)) + ( Sum gg)) by RLVECT_1:def 3

        .= (( Sum gm) + ( Sum gg)) by A14, A16, RLVECT_1: 41

        .= ( Sum g) by A15, RLVECT_1: 41;

      end;

      

       A19: P[ 0 ]

      proof

        let f,g be FinSequence of K;

        assume (f,g) are_fiberwise_equipotent & ( len f) = 0 ;

        then

         A20: ( len g) = 0 & f = ( <*> the carrier of INT.Ring ) by RFINSEQ: 3;

        then g = ( <*> the carrier of INT.Ring );

        hence thesis by A20;

      end;

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

      hence thesis by A1, A2;

    end;

    ::$Canceled

    definition

      ::$Canceled

    end

    theorem :: ZMODUL05:16

    

     MATRLIN16: for R be Ring holds for V1,V2 be LeftMod of R holds for f be Function of V1, V2 holds for p be FinSequence of V1 st f is additive homogeneous holds (f . ( Sum p)) = ( Sum (f * p))

    proof

      let R be Ring;

      let V1,V2 be LeftMod of R, f be Function of V1, V2;

      let p be FinSequence of V1;

      defpred P[ FinSequence of V1] means (f . ( Sum $1)) = ( Sum (f * $1));

      assume

       A1: f is additive homogeneous;

      

       A2: for p be FinSequence of V1 holds for w be Element of V1 st P[p] holds P[(p ^ <*w*>)]

      proof

        let p be FinSequence of V1;

        let w be Element of V1 such that

         A3: (f . ( Sum p)) = ( Sum (f * p));

        

        thus (f . ( Sum (p ^ <*w*>))) = (f . (( Sum p) + ( Sum <*w*>))) by RLVECT_1: 41

        .= (( Sum (f * p)) + (f . ( Sum <*w*>))) by A1, A3

        .= (( Sum (f * p)) + (f . w)) by RLVECT_1: 44

        .= (( Sum (f * p)) + ( Sum <*(f . w)*>)) by RLVECT_1: 44

        .= ( Sum ((f * p) ^ <*(f . w)*>)) by RLVECT_1: 41

        .= ( Sum (f * (p ^ <*w*>))) by FINSEQOP: 8;

      end;

      (f . ( Sum ( <*> the carrier of V1))) = (f . ( 0. V1)) by RLVECT_1: 43

      .= (f . (( 0. R) * ( 0. V1))) by VECTSP_1: 14

      .= (( 0. R) * (f . ( 0. V1))) by A1

      .= ( 0. V2) by VECTSP_1: 14

      .= ( Sum ( <*> the carrier of V2)) by RLVECT_1: 43

      .= ( Sum (f * ( <*> the carrier of V1)));

      then

       A4: P[( <*> the carrier of V1)];

      for p be FinSequence of V1 holds P[p] from FINSEQ_2:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: ZMODUL05:17

    for V be free Z_Module st ( [#] V) is finite holds ( (Omega). V) = ( (0). V)

    proof

      let V be free Z_Module;

      assume

       A1: ( [#] V) is finite;

      assume

       A2: ( (Omega). V) <> ( (0). V);

      consider A be Subset of V such that

       a3: A is base by VECTSP_7:def 4;

      per cases ;

        suppose A = {} ;

        

        then ( Lin A) = ( Lin ( {} the carrier of V))

        .= ( (0). V) by VECTSP_7: 9;

        hence contradiction by A2, a3;

      end;

        suppose A <> {} ;

        then

        consider v be object such that

         A4: v in A by XBOOLE_0:def 1;

        reconsider v as VECTOR of V by A4;

         {v} is linearly-independent by a3, A4, ZFMISC_1: 31, ZMODUL02: 56;

        then

         A5: v <> ( 0. V);

        deffunc F( Element of INT.Ring ) = ($1 * v);

        consider f be Function of the carrier of INT.Ring , the carrier of V such that

         A6: for x be Element of INT.Ring holds (f . x) = F(x) from FUNCT_2:sch 4;

        

         A7: ( dom f) = the carrier of INT.Ring & ( rng f) c= the carrier of V by FUNCT_2:def 1;

        for x1,x2 be object st x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & (f . x1) = (f . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume

           A8: x1 in the carrier of INT.Ring & x2 in the carrier of INT.Ring & (f . x1) = (f . x2);

          then

          reconsider a1 = x1, a2 = x2 as Element of INT.Ring ;

          (a1 * v) = (f . a2) by A6, A8

          .= (a2 * v) by A6;

          then ((a1 * v) - (a2 * v)) = ( 0. V) by RLVECT_1: 5;

          then ((a1 - a2) * v) = ( 0. V) by ZMODUL01: 9;

          then (a1 - a2) = ( 0. INT.Ring ) by A5, ZMODUL01:def 7;

          hence x1 = x2 by INT_3:def 3;

        end;

        then f is one-to-one by FUNCT_2: 19;

        then ( card the carrier of INT.Ring ) c= ( card the carrier of V) by A7, CARD_1: 10;

        hence contradiction by A1;

      end;

    end;

    begin

    reserve T for linear-transformation of V, W;

    theorem :: ZMODUL05:18

    for F be Ring, V,W be VectSp of F, T be linear-transformation of V, W holds for x,y be Element of V holds ((T . x) - (T . y)) = (T . (x - y)) by RANKNULL: 8;

    theorem :: ZMODUL05:19

    (T . ( 0. V)) = ( 0. W) by RANKNULL: 9;

    theorem :: ZMODUL05:20

    for x be Element of V holds x in ( ker T) iff (T . x) = ( 0. W) by RANKNULL: 10;

    theorem :: ZMODUL05:21

    ( 0. V) in ( ker T) by RANKNULL: 11;

    theorem :: ZMODUL05:22

    for X be Subset of V holds (T .: X) is Subset of ( im T) by RANKNULL: 12;

    theorem :: ZMODUL05:23

    for y be Element of W holds y in ( im T) iff ex x be Element of V st y = (T . x) by RANKNULL: 13;

    theorem :: ZMODUL05:24

    for x be Element of ( ker T) holds (T . x) = ( 0. W) by RANKNULL: 14;

    theorem :: ZMODUL05:25

    T is one-to-one implies ( ker T) = ( (0). V) by RANKNULL: 15;

    theorem :: ZMODUL05:26

    for V be finite-rank free Z_Module holds ( rank ( (0). V)) = 0

    proof

      let V be finite-rank free Z_Module;

      ( (Omega). ( (0). V)) = ( (0). ( (0). V)) by ZMODUL01: 51;

      hence thesis by RL5Th33;

    end;

    theorem :: ZMODUL05:27

    

     Th17: for x,y be Element of V st (T . x) = (T . y) holds (x - y) in ( ker T) by RANKNULL: 17;

    theorem :: ZMODUL05:28

    

     Th18: for A be Subset of V, x,y be Element of V st (x - y) in ( Lin A) holds x in ( Lin (A \/ {y})) by RANKNULL: 18;

    begin

    theorem :: ZMODUL05:29

    for X be Subset of V st V is Submodule of W holds X is Subset of W

    proof

      let X be Subset of V;

      assume V is Submodule of W;

      then

       A1: ( [#] V) c= ( [#] W) by VECTSP_4:def 2;

      X c= ( [#] W) by A1;

      hence thesis;

    end;

    theorem :: ZMODUL05:30

    

     ThLin4: for R be Ring holds for V be LeftMod of R, A be Subset of V holds A is Subset of ( Lin A)

    proof

      let R be Ring;

      let V be LeftMod of R;

      let A be Subset of V;

      for x be object st x in A holds x in the carrier of ( Lin A)

      proof

        let x be object such that

         A1: x in A;

        x in ( Lin A) by A1, MOD_3: 5;

        hence thesis;

      end;

      then A c= the carrier of ( Lin A);

      hence thesis;

    end;

    theorem :: ZMODUL05:31

    

     ThLin7: for V be LeftMod of INT.Ring , A be linearly-independent Subset of V holds A is Basis of ( Lin A)

    proof

      let V be LeftMod of INT.Ring , A be linearly-independent Subset of V;

      reconsider AA = A as Subset of ( Lin A) by ThLin4;

      ( (Omega). ( Lin A)) = ( Lin AA) by ZMODUL03: 20;

      hence thesis by ZMODUL03: 16, VECTSP_7:def 3;

    end;

    theorem :: ZMODUL05:32

    

     Th21: for V be finite-rank free Z_Module, A be Subset of V, x be Element of V st x in ( Lin A) & not x in A holds (A \/ {x}) is linearly-dependent

    proof

      let V be finite-rank free Z_Module, A be Subset of V, x be Element of V such that

       A1: x in ( Lin A) and

       A2: not x in A;

      per cases ;

        suppose

         A3: A is linearly-independent;

        reconsider X = {x} as Subset of ( Lin A) by A1, SUBSET_1: 41;

        reconsider A9 = A as Basis of ( Lin A) by A3, ThLin7;

        reconsider B = (A9 \/ X) as Subset of ( Lin A);

        X misses A9

        proof

          assume X meets A9;

          then ex y be object st y in X & y in A9 by XBOOLE_0: 3;

          hence contradiction by A2, TARSKI:def 1;

        end;

        then B is linearly-dependent by ZMODUL03: 18;

        hence thesis by ZMODUL03: 16;

      end;

        suppose A is linearly-dependent;

        hence thesis by ZMODUL02: 56, XBOOLE_1: 7;

      end;

    end;

    registration

      let V be finite-rank free Z_Module, W be Z_Module;

      let T be linear-transformation of V, W;

      cluster ( ker T) -> finite-rank free;

      correctness ;

    end

    reserve T for linear-transformation of V, W;

    theorem :: ZMODUL05:33

    

     Th22: for V be finite-rank free Z_Module, A be Subset of V, B be Basis of V, T be linear-transformation of V, W st A is Basis of ( ker T) & A c= B holds (T | (B \ A)) is one-to-one

    proof

      let V be finite-rank free Z_Module, A be Subset of V, B be Basis of V, T be linear-transformation of V, W such that

       A1: A is Basis of ( ker T) and

       A2: A c= B;

      reconsider A9 = A as Subset of V;

      set f = (T | (B \ A));

      let x1,x2 be object such that

       A3: x1 in ( dom f) and

       A4: x2 in ( dom f) and

       A5: (f . x1) = (f . x2) and

       A6: x1 <> x2;

      x2 in ( dom T) by A4, RELAT_1: 57;

      then

      reconsider x2 as Element of V;

      x1 in ( dom T) by A3, RELAT_1: 57;

      then

      reconsider x1 as Element of V;

      

       A7: not x1 in (A9 \/ {x2})

      proof

        assume

         A8: x1 in (A9 \/ {x2});

        per cases by A8, XBOOLE_0:def 3;

          suppose x1 in A9;

          hence contradiction by A3, XBOOLE_0:def 5;

        end;

          suppose x1 in {x2};

          hence contradiction by A6, TARSKI:def 1;

        end;

      end;

      

       A9: (f . x2) = (T . x2) by A4, FUNCT_1: 49;

      reconsider A as Subset of ( ker T) by A1;

      reconsider A as Basis of ( ker T) by A1;

      

       A10: ( ker T) = ( Lin A) by VECTSP_7:def 3;

      (f . x1) = (T . x1) by A3, FUNCT_1: 49;

      then (x1 - x2) in ( ker T) by A5, A9, Th17;

      then (x1 - x2) in ( Lin A9) by A10, ZMODUL03: 20;

      then

       A11: x1 in ( Lin (A9 \/ {x2})) by Th18;

      ( {x2} \/ {x1}) = {x1, x2} by ENUMSET1: 1;

      then

       A12: ((A9 \/ {x2}) \/ {x1}) = (A9 \/ {x1, x2}) by XBOOLE_1: 4;

       {x1, x2} c= B

      proof

        let z be object such that

         A13: z in {x1, x2};

        per cases by A13, TARSKI:def 2;

          suppose z = x1;

          hence thesis by A3, XBOOLE_0:def 5;

        end;

          suppose z = x2;

          hence thesis by A4, XBOOLE_0:def 5;

        end;

      end;

      then

       A14: (A9 \/ {x1, x2}) c= B by A2, XBOOLE_1: 8;

      B is linearly-independent by VECTSP_7:def 3;

      hence thesis by A7, A11, A12, A14, Th21, ZMODUL02: 56;

    end;

    theorem :: ZMODUL05:34

    for R be Ring, V be LeftMod of R holds for A be Subset of V, l be Linear_Combination of A, x be Element of V, a be Element of R holds (l +* (x,a)) is Linear_Combination of (A \/ {x})

    proof

      let R be Ring, V be LeftMod of R;

      let A be Subset of V, l be Linear_Combination of A, x be Element of V, a be Element of R;

      set m = (l +* (x,a));

      

       A1: ( dom m) = ( dom l) by FUNCT_7: 30

      .= ( [#] V) by FUNCT_2:def 1;

      ( rng m) c= the carrier of R;

      then

      reconsider m as Element of ( Funcs (( [#] V),the carrier of R)) by A1, FUNCT_2:def 2;

      set T = (( Carrier l) \/ {x});

      for v be Element of V st not v in T holds (m . v) = ( 0. R)

      proof

        let v be Element of V such that

         A7: not v in T;

         not v in {x} by A7, XBOOLE_0:def 3;

        then v <> x by TARSKI:def 1;

        then

         A8: (m . v) = (l . v) by FUNCT_7: 32;

         not v in ( Carrier l) by A7, XBOOLE_0:def 3;

        hence thesis by A8;

      end;

      then

      reconsider m as Linear_Combination of V by VECTSP_6:def 1;

      

       A9: ( Carrier m) c= T

      proof

        let y be object;

        assume y in ( Carrier m);

        then

        consider z be Element of V such that

         A10: y = z and

         A11: (m . z) <> ( 0. R);

        per cases ;

          suppose

           A12: z = x;

          x in {x} & {x} c= T by TARSKI:def 1, XBOOLE_1: 7;

          hence thesis by A10, A12;

        end;

          suppose z <> x;

          then (m . z) = (l . z) by FUNCT_7: 32;

          then

           A13: z in ( Carrier l) by A11;

          ( Carrier l) c= T by XBOOLE_1: 7;

          hence thesis by A10, A13;

        end;

      end;

      T c= (A \/ {x}) by XBOOLE_1: 9, VECTSP_6:def 4;

      then ( Carrier m) c= (A \/ {x}) by A9;

      hence thesis by VECTSP_6:def 4;

    end;

    reserve l for Linear_Combination of V;

    registration

      let R be non degenerated Ring, V be LeftMod of R;

      cluster linearly-dependent for Subset of V;

      existence

      proof

        reconsider S = {( 0. V)} as Subset of V;

        take S;

        thus thesis;

      end;

    end

    definition

      let R be Ring;

      let V be LeftMod of R, l be Linear_Combination of V, A be Subset of V;

      :: ZMODUL05:def6

      func l ! A -> Linear_Combination of A equals ((l | A) +* ((A ` ) --> ( 0. R)));

      coherence

      proof

        set f = ((l | A) +* ((A ` ) --> ( 0. R)));

        

         A1: ( dom f) = (( dom (l | A)) \/ ( dom ((A ` ) --> ( 0. R)))) by FUNCT_4:def 1;

        ( dom l) = ( [#] V) by FUNCT_2: 92;

        then ( dom (l | A)) = A by RELAT_1: 62;

        then

         A4: ( dom f) = ( [#] V) by A1, XBOOLE_1: 45;

        ( rng f) c= (( rng (l | A)) \/ ( rng ((A ` ) --> ( 0. R)))) & (( rng (l | A)) \/ ( rng ((A ` ) --> ( 0. R)))) c= ( [#] R) by FUNCT_4: 17;

        then ( rng f) c= the carrier of R;

        then

        reconsider f as Element of ( Funcs (( [#] V),the carrier of R)) by A4, FUNCT_2:def 2;

        ex T be finite Subset of V st for v be Element of V st not v in T holds (f . v) = ( 0. R)

        proof

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

          D c= ( [#] V)

          proof

            let x be object;

            assume x in D;

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

            hence thesis;

          end;

          then

          reconsider D as Subset of V;

          set C = ( Carrier l);

          D c= C

          proof

            let x be object;

            assume x in D;

            then

            consider v be Element of V such that

             A10: x = v and

             A11: (f . v) <> ( 0. R);

             A13:

            now

              assume

               A14: v in (A ` );

              

              then (f . v) = (((A ` ) --> ( 0. R)) . v) by A1, A4, FUNCT_4:def 1

              .= ( 0. R) by A14, FUNCOP_1: 7;

              hence contradiction by A11;

            end;

            then v in A by XBOOLE_0:def 5;

            then

             A15: ((l | A) . v) = (l . v) by FUNCT_1: 49;

             not v in ( dom ((A ` ) --> ( 0. R))) by A13;

            then (f . v) = ((l | A) . v) by FUNCT_4: 11;

            hence thesis by A10, A11, A15;

          end;

          then

          reconsider D as finite Subset of V;

          take D;

          thus thesis;

        end;

        then

        reconsider f as Linear_Combination of V by VECTSP_6:def 1;

        ( Carrier f) c= A

        proof

          let x be object such that

           A16: x in ( Carrier f);

          reconsider x as Element of V by A16;

          now

            assume not x in A;

            then

             A17: x in (A ` ) by XBOOLE_0:def 5;

            then x in (( dom (l | A)) \/ ( dom ((A ` ) --> ( 0. R)))) by XBOOLE_0:def 3;

            then (f . x) = (((A ` ) --> ( 0. R)) . x) by A17, FUNCT_4:def 1;

            hence contradiction by A16, A17, FUNCOP_1: 7, VECTSP_6: 2;

          end;

          hence thesis;

        end;

        hence thesis by VECTSP_6:def 4;

      end;

    end

    theorem :: ZMODUL05:35

    

     Th24: for R be Ring holds for V be LeftMod of R, l be Linear_Combination of V holds l = (l ! ( Carrier l))

    proof

      let R be Ring;

      let V be LeftMod of R, l be Linear_Combination of V;

      set f = (l | ( Carrier l));

      set g = ((( Carrier l) ` ) --> ( 0. R));

      set m = (f +* g);

      

       A2: ( dom l) = ( [#] V) by FUNCT_2: 92;

      then ( dom f) = ( Carrier l) by RELAT_1: 62;

      then

       A3: (( dom f) \/ ( dom g)) = ( [#] V) by XBOOLE_1: 45;

      for x be object st x in ( dom l) holds (l . x) = (m . x)

      proof

        let x be object;

        assume x in ( dom l);

        then

        reconsider x as Element of V;

        per cases ;

          suppose

           A5: x in ( Carrier l);

          then not x in ( dom g) by XBOOLE_0:def 5;

          then (m . x) = (f . x) by A3, FUNCT_4:def 1;

          hence thesis by A5, FUNCT_1: 49;

        end;

          suppose

           A6: not x in ( Carrier l);

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

          then (m . x) = (g . x) & (g . x) = ( 0. R) by A3, FUNCOP_1: 7, FUNCT_4:def 1;

          hence thesis by A6;

        end;

      end;

      hence thesis by A2;

    end;

    

     Lm1: for R be Ring holds for V be LeftMod of R holds for l be Linear_Combination of V holds for X be Subset of V holds (l .: X) is finite

    proof

      let R be Ring;

      let V be LeftMod of R;

      let l be Linear_Combination of V;

      let X be Subset of V;

      

       A1: l = (l ! ( Carrier l)) by Th24;

      (( rng (l | ( Carrier l))) \/ ( rng ((( Carrier l) ` ) --> ( 0. R)))) is finite;

      then ( rng l) is finite by A1, FINSET_1: 1, FUNCT_4: 17;

      hence thesis by FINSET_1: 1, RELAT_1: 111;

    end;

    theorem :: ZMODUL05:36

    

     Th25: for R be Ring holds for V be LeftMod of R holds for l be Linear_Combination of V holds for A be Subset of V, v be Element of V st v in A holds ((l ! A) . v) = (l . v)

    proof

      let R be Ring;

      let V be LeftMod of R;

      let l be Linear_Combination of V;

      let A be Subset of V, v be Element of V such that

       A1: v in A;

      ( dom (l ! A)) = ( [#] V) by FUNCT_2: 92;

      then

       A2: (( dom (l | A)) \/ ( dom ((A ` ) --> ( 0. R)))) = ( [#] V) by FUNCT_4:def 1;

       not v in ( dom ((A ` ) --> ( 0. R))) by A1, XBOOLE_0:def 5;

      

      then ((l ! A) . v) = ((l | A) . v) by A2, FUNCT_4:def 1

      .= (l . v) by A1, FUNCT_1: 49;

      hence thesis;

    end;

    theorem :: ZMODUL05:37

    

     Th26: for R be Ring, V be LeftMod of R holds for l be Linear_Combination of V holds for A be Subset of V, v be Element of V st not v in A holds ((l ! A) . v) = ( 0. R)

    proof

      let R be Ring, V be LeftMod of R;

      let l be Linear_Combination of V;

      let A be Subset of V, v be Element of V;

      assume not v in A;

      then

       A1: v in (A ` ) by XBOOLE_0:def 5;

      

       A2: ( dom (l ! A)) = ( [#] V) by FUNCT_2: 92;

      ( dom ((A ` ) --> ( 0. R))) = (A ` ) & ( dom (l ! A)) = (( dom (l | A)) \/ ( dom ((A ` ) --> ( 0. R)))) by FUNCT_4:def 1;

      

      then ((l ! A) . v) = (((A ` ) --> ( 0. R)) . v) by A1, A2, FUNCT_4:def 1

      .= ( 0. R) by A1, FUNCOP_1: 7;

      hence thesis;

    end;

    theorem :: ZMODUL05:38

    

     Th27: for R be Ring, V be LeftMod of R holds for A,B be Subset of V, l be Linear_Combination of B st A c= B holds l = ((l ! A) + (l ! (B \ A)))

    proof

      let R be Ring, V be LeftMod of R;

      let A,B be Subset of V, l be Linear_Combination of B such that

       A1: A c= B;

      set r = ((l ! A) + (l ! (B \ A)));

      let v be Element of V;

      

       A2: v in B implies (v in A or v in (B \ A))

      proof

        assume

         A3: v in B;

        B = (A \/ (B \ A)) by A1, XBOOLE_1: 45;

        hence thesis by A3, XBOOLE_0:def 3;

      end;

      per cases by A2;

        suppose

         A4: v in A;

        then not v in (B \ A) by XBOOLE_0:def 5;

        then

         A5: ((l ! (B \ A)) . v) = ( 0. R) by Th26;

        ((l ! A) . v) = (l . v) by A4, Th25;

        

        then (r . v) = ((l . v) + ( 0. R)) by A5, VECTSP_6: 22

        .= (l . v);

        hence (l . v) = (r . v);

      end;

        suppose

         A6: v in (B \ A);

        then not v in A by XBOOLE_0:def 5;

        then

         A7: ((l ! A) . v) = ( 0. R) by Th26;

        ((l ! (B \ A)) . v) = (l . v) by A6, Th25;

        

        then (r . v) = (( 0. R) + (l . v)) by A7, VECTSP_6: 22

        .= (l . v);

        hence (l . v) = (r . v);

      end;

        suppose

         A8: not v in B;

        ( Carrier l) c= B by VECTSP_6:def 4;

        then

         A9: not v in ( Carrier l) by A8;

         not v in (B \ A) by A8, XBOOLE_0:def 5;

        then

         A10: ((l ! (B \ A)) . v) = ( 0. R) by Th26;

        ((l ! A) . v) = ( 0. R) by A1, A8, Th26;

        

        then (r . v) = (( 0. R) + ( 0. R)) by A10, VECTSP_6: 22

        .= ( 0. R);

        hence (l . v) = (r . v) by A9;

      end;

    end;

    registration

      let R be Ring, V be LeftMod of R, l be Linear_Combination of V, X be Subset of V;

      cluster (l .: X) -> finite;

      coherence by Lm1;

    end

    theorem :: ZMODUL05:39

    

     Th28: for R be Ring, V be LeftMod of R, l be Linear_Combination of V holds for X be Subset of V st X misses ( Carrier l) holds (l .: X) c= {( 0. R)}

    proof

      let R be Ring, V be LeftMod of R, l be Linear_Combination of V;

      let X be Subset of V such that

       A1: X misses ( Carrier l);

      set M = (l .: X);

      for y be object st y in (l .: X) holds y in {( 0. R)}

      proof

        let y be object;

        assume y in M;

        then

        consider x be object such that x in ( dom l) and

         A2: x in X and

         A3: y = (l . x) by FUNCT_1:def 6;

        reconsider x as Element of V by A2;

        now

          assume (l . x) <> ( 0. R);

          then x in ( Carrier l);

          hence contradiction by A1, A2, XBOOLE_0:def 4;

        end;

        hence thesis by A3, TARSKI:def 1;

      end;

      hence (l .: X) c= {( 0. R)};

    end;

    definition

      let K be Ring;

      let V,W be VectSp of K, l be Linear_Combination of V, T be linear-transformation of V, W;

      let w be Element of W;

      :: ZMODUL05:def7

      func lCFST (l,T,w) -> the carrier of K -valued FinSequence equals (l * ( canFS ((T " {w}) /\ ( Carrier l))));

      correctness

      proof

        set p = (l * ( canFS ((T " {w}) /\ ( Carrier l))));

        set f = ( canFS ((T " {w}) /\ ( Carrier l)));

        ( dom l) = the carrier of V by FUNCT_2:def 1;

        then ( rng f) c= ( dom l) by XBOOLE_1: 1;

        hence thesis by FINSEQ_1: 16;

      end;

    end

    reserve V,W for Z_Module;

    reserve l for Linear_Combination of V;

    reserve T for linear-transformation of V, W;

    theorem :: ZMODUL05:40

    

     ThTF3C0: for V,W be non empty set, f be FinSequence, l be Function of V, W st ( rng f) c= V holds (l * f) is W -valued FinSequence-like

    proof

      let V,W be non empty set, f be FinSequence, l be Function of V, W;

      assume ( rng f) c= V;

      then ( rng f) c= ( dom l) by FUNCT_2:def 1;

      hence thesis by FINSEQ_1: 16;

    end;

    registration

      let V,W be non empty set, f be V -valued FinSequence, l be Function of V, W;

      cluster (l * f) -> W -valued FinSequence-like;

      coherence

      proof

        ( rng f) c= V;

        hence (l * f) is W -valued FinSequence-like by ThTF3C0;

      end;

    end

    

     ThTF3C1: for V,W be non empty set, A be finite Subset of V, l be Function of V, W holds (l * ( canFS A)) is W -valued FinSequence-like

    proof

      let V,W be non empty set, A be finite Subset of V, l be Function of V, W;

      set p = (l * ( canFS A));

      set f = ( canFS A);

      ( dom l) = V by FUNCT_2:def 1;

      then ( rng f) c= ( dom l) by XBOOLE_1: 1;

      hence thesis by FINSEQ_1: 16;

    end;

    registration

      let V,W be non empty set, A be finite Subset of V, l be Function of V, W;

      cluster (l * ( canFS A)) -> W -valued FinSequence-like;

      coherence by ThTF3C1;

    end

    registration

      let R be Ring;

      let V be LeftMod of R, A be finite Subset of V, l be Linear_Combination of V;

      cluster (l * ( canFS A)) -> the carrier of R -valued FinSequence-like;

      coherence ;

    end

    theorem :: ZMODUL05:41

    

     ThTF3C3: for V,W be non empty set, f,g be V -valued FinSequence, l be Function of V, W holds (l * (f ^ g)) = ((l * f) ^ (l * g))

    proof

      let V,W be non empty set, f,g be V -valued FinSequence, l be Function of V, W;

      

       A1: ( dom l) = V by FUNCT_2:def 1;

      

       A2: ( rng f) c= V;

      

       A3: ( rng g) c= V;

      

       A4: ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by FINSEQ_1: 31;

      

       A5: ( dom (l * f)) = ( dom f) by A1, A2, RELAT_1: 27

      .= ( Seg ( len f)) by FINSEQ_1:def 3;

      then

       A6: ( len (l * f)) = ( len f) by FINSEQ_1:def 3;

      ( dom (l * g)) = ( dom g) by A1, A3, RELAT_1: 27

      .= ( Seg ( len g)) by FINSEQ_1:def 3;

      then

       A7: ( len (l * g)) = ( len g) by FINSEQ_1:def 3;

      

       A8: ( dom (f ^ g)) = ( Seg ( len (f ^ g))) by FINSEQ_1:def 3

      .= ( Seg (( len f) + ( len g))) by FINSEQ_1: 22;

      

       A9: ( len ((l * f) ^ (l * g))) = (( len (l * f)) + ( len (l * g))) by FINSEQ_1: 22

      .= (( len f) + ( len g)) by A5, A7, FINSEQ_1:def 3;

      

       A10: ( dom ((l * f) ^ (l * g))) = ( Seg (( len f) + ( len g))) by A9, FINSEQ_1:def 3;

      now

        let k be object;

        assume

         A11: k in ( dom (l * (f ^ g)));

        then

        reconsider i = k as Nat;

        

         A12: i in ( dom (f ^ g)) by A1, A4, A11, RELAT_1: 27;

        per cases by A12, FINSEQ_1: 25;

          suppose

           A13: i in ( dom f);

          then

           A14: i in ( dom (l * f)) by A1, A2, RELAT_1: 27;

          

          thus ((l * (f ^ g)) . k) = (l . ((f ^ g) . i)) by A11, FUNCT_1: 12

          .= (l . (f . i)) by A13, FINSEQ_1:def 7

          .= ((l * f) . i) by A13, FUNCT_1: 13

          .= (((l * f) ^ (l * g)) . k) by A14, FINSEQ_1:def 7;

        end;

          suppose ex n be Nat st n in ( dom g) & i = (( len f) + n);

          then

          consider n be Nat such that

           A15: n in ( dom g) & i = (( len f) + n);

          

           A16: n in ( dom (l * g)) by A1, A3, A15, RELAT_1: 27;

          

          thus ((l * (f ^ g)) . k) = (l . ((f ^ g) . i)) by A11, FUNCT_1: 12

          .= (l . (g . n)) by A15, FINSEQ_1:def 7

          .= ((l * g) . n) by A15, FUNCT_1: 13

          .= (((l * f) ^ (l * g)) . k) by A6, A15, A16, FINSEQ_1:def 7;

        end;

      end;

      hence thesis by A1, A4, A8, A10, FUNCT_1: 2, RELAT_1: 27;

    end;

    theorem :: ZMODUL05:42

    

     ThTF3C2: for R be Ring holds for V be LeftMod of R, A,B be finite Subset of V, l be Linear_Combination of V, l0,l1,l2 be FinSequence of R st (A /\ B) = {} & l0 = (l * ( canFS (A \/ B))) & l1 = (l * ( canFS A)) & l2 = (l * ( canFS B)) holds ( Sum l0) = (( Sum l1) + ( Sum l2))

    proof

      let R be Ring;

      let V be LeftMod of R, A,B be finite Subset of V, l be Linear_Combination of V, l0,l1,l2 be FinSequence of R;

      assume

       A1: (A /\ B) = {} ;

      assume

       TT: l0 = (l * ( canFS (A \/ B))) & l1 = (l * ( canFS A)) & l2 = (l * ( canFS B));

      per cases ;

        suppose

         A2: (A \/ B) = {} ;

        then

         A3: A = {} ;

        

         a3: B = {} by A2;

        ( rng (l * ( canFS B))) c= the carrier of R;

        then

        reconsider lC = (l * ( canFS B)) as FinSequence of R by FINSEQ_1:def 4;

        lC = ( <*> the carrier of R) by a3;

        

        then ( Sum lC) = ( 0. R) by RLVECT_1: 43

        .= ( 0. R);

        hence ( Sum l0) = (( Sum l1) + ( Sum l2)) by A2, A3, TT;

      end;

        suppose

         A5: (A \/ B) <> {} ;

        ( rng ( canFS A)) = A by FUNCT_2:def 3;

        then

        reconsider ca = ( canFS A) as the carrier of V -valued FinSequence by RELAT_1:def 19;

        ( rng ( canFS B)) = B by FUNCT_2:def 3;

        then

        reconsider cb = ( canFS B) as the carrier of V -valued FinSequence by RELAT_1:def 19;

        set la = ( len ( canFS A));

        set lb = ( len ( canFS B));

        set lab = ( len (( canFS A) ^ ( canFS B)));

        set lavb = ( len ( canFS (A \/ B)));

        set F = (l * ( canFS (A \/ B)));

        set G = (l1 ^ l2);

        set H = ((( canFS (A \/ B)) " ) * (( canFS A) ^ ( canFS B)));

        

         A6: la = ( card A) by FINSEQ_1: 93;

        

         A7: lavb = ( card (A \/ B)) by FINSEQ_1: 93

        .= (( card A) + ( card B)) by A1, CARD_2: 40, XBOOLE_0:def 7

        .= (la + lb) by A6, FINSEQ_1: 93;

        

         A8: lab = (la + lb) by FINSEQ_1: 22;

        then

         A9: ( dom (( canFS A) ^ ( canFS B))) = ( Seg (la + lb)) by FINSEQ_1:def 3;

        

         A10: ( rng (( canFS A) ^ ( canFS B))) = (( rng ( canFS A)) \/ ( rng ( canFS B))) by FINSEQ_1: 31

        .= (A \/ ( rng ( canFS B))) by FUNCT_2:def 3

        .= (A \/ B) by FUNCT_2:def 3;

        reconsider AB = (( canFS A) ^ ( canFS B)) as Function of ( Seg (la + lb)), (A \/ B) by A9, A10, FUNCT_2: 1;

        

         A11: ( rng ( canFS (A \/ B))) = (A \/ B) by FUNCT_2:def 3;

        reconsider INVAB = (( canFS (A \/ B)) " ) as Function of (A \/ B), ( Seg ( card (A \/ B))) by FINSEQ_1: 95;

        

         A12: (INVAB * ( canFS (A \/ B))) = ( id ( dom ( canFS (A \/ B)))) & (( canFS (A \/ B)) * INVAB) = ( id ( rng ( canFS (A \/ B)))) by FUNCT_1: 39;

        

         A13: ( dom ( canFS (A \/ B))) = ( Seg ( len ( canFS (A \/ B)))) by FINSEQ_1:def 3

        .= ( Seg ( card (A \/ B))) by FINSEQ_1: 93;

        then

         A14: ( canFS (A \/ B)) is Function of ( Seg ( card (A \/ B))), (A \/ B) by A11, FUNCT_2: 1;

        

         A15: ( dom INVAB) = (A \/ B) by A5, FUNCT_2:def 1;

        

         A16: ( rng INVAB) = ( Seg ( card (A \/ B))) by A12, A13, A14, FUNCT_2: 18

        .= ( Seg (( card A) + ( card B))) by A1, CARD_2: 40, XBOOLE_0:def 7

        .= ( Seg (la + lb)) by A6, FINSEQ_1: 93;

        

         A17: ( dom H) = ( dom (( canFS A) ^ ( canFS B))) by A10, A15, RELAT_1: 27

        .= ( Seg (la + lb)) by A8, FINSEQ_1:def 3;

        

         A18: ( rng H) = ( Seg (la + lb)) by A10, A15, A16, RELAT_1: 28;

        

         A19: the carrier of V = ( dom l) by FUNCT_2:def 1;

        

         A20: ( dom F) = ( dom ( canFS (A \/ B))) by A11, A19, RELAT_1: 27

        .= ( Seg (la + lb)) by A7, FINSEQ_1:def 3;

        ( rng ( canFS A)) = A by FUNCT_2:def 3;

        

        then ( dom (l * ( canFS A))) = ( dom ( canFS A)) by A19, RELAT_1: 27

        .= ( Seg la) by FINSEQ_1:def 3;

        then

         A21: ( len (l * ( canFS A))) = la by FINSEQ_1:def 3;

        

         A22: ( rng ( canFS B)) = B by FUNCT_2:def 3;

        

        then ( dom (l * ( canFS B))) = ( dom ( canFS B)) by A19, RELAT_1: 27

        .= ( Seg lb) by FINSEQ_1:def 3;

        then

         A23: ( len (l * ( canFS B))) = lb by FINSEQ_1:def 3;

        set G = ((l * ( canFS A)) ^ (l * ( canFS B)));

        

         A24: ( len G) = (la + lb) by A21, A23, FINSEQ_1: 22;

        ( rng ( canFS A)) misses ( rng ( canFS B)) by A1, A22, FUNCT_2:def 3;

        then

         A25: (( canFS A) ^ ( canFS B)) is one-to-one by FINSEQ_3: 91;

        

         A26: ( dom H) = ( dom G) by A17, A24, FINSEQ_1:def 3;

        

         A27: (F * H) = (((l * ( canFS (A \/ B))) * (( canFS (A \/ B)) " )) * (( canFS A) ^ ( canFS B))) by RELAT_1: 36

        .= ((l * (( canFS (A \/ B)) * (( canFS (A \/ B)) " ))) * (( canFS A) ^ ( canFS B))) by RELAT_1: 36

        .= ((l * ( id ( rng ( canFS (A \/ B))))) * (( canFS A) ^ ( canFS B))) by FUNCT_1: 39

        .= ((l * ( id (A \/ B))) * (( canFS A) ^ ( canFS B))) by FUNCT_2:def 3

        .= (l * (( id (A \/ B)) * AB)) by RELAT_1: 36

        .= (l * (( canFS A) ^ ( canFS B))) by FUNCT_2: 17

        .= ((l * ca) ^ (l * cb)) by ThTF3C3

        .= G;

        

         Z2: ( rng G) = (( rng (l * ( canFS A))) \/ ( rng (l * ( canFS B)))) by FINSEQ_1: 31;

        ( rng F) c= the carrier of R;

        then

        reconsider FR = F as FinSequence of R by FINSEQ_1:def 4;

        reconsider GR = G as FinSequence of R by Z2, FINSEQ_1:def 4;

        

        thus ( Sum l0) = ( Sum FR) by TT

        .= ( Sum GR) by A18, A20, A25, A26, A27, CLASSES1: 77, RF9

        .= ( Sum (l1 ^ l2)) by TT

        .= (( Sum (l * ( canFS A))) + ( Sum (l * ( canFS B)))) by TT, RLVECT_1: 41

        .= (( Sum l1) + ( Sum l2)) by TT;

      end;

    end;

    theorem :: ZMODUL05:43

    

     ThTF3C3: for R be Ring holds for V be LeftMod of R, A be finite Subset of V, l,l0 be Linear_Combination of V st (l | ( Carrier l0)) = (l0 | ( Carrier l0)) & ( Carrier l0) c= ( Carrier l) & A c= ( Carrier l0) holds ( Sum (l * ( canFS A))) = ( Sum (l0 * ( canFS A)))

    proof

      let R be Ring;

      let V be LeftMod of R, A be finite Subset of V, l,l0 be Linear_Combination of V;

      assume

       A1: (l | ( Carrier l0)) = (l0 | ( Carrier l0)) & ( Carrier l0) c= ( Carrier l) & A c= ( Carrier l0);

      ( dom l0) = the carrier of V by FUNCT_2:def 1;

      then ( dom (l0 | ( Carrier l0))) = ( Carrier l0) by RELAT_1: 62;

      then

       A2: ( rng ( canFS A)) c= ( dom (l0 | ( Carrier l0))) by A1;

      then (l * ( canFS A)) = ((l0 | ( Carrier l0)) * ( canFS A)) by A1, RELAT_1: 165;

      hence thesis by A2, RELAT_1: 165;

    end;

    definition

      let R be Ring;

      let V,W be LeftMod of R, l be Linear_Combination of V, T be linear-transformation of V, W;

      :: ZMODUL05:def8

      func T @* l -> Linear_Combination of W means

      : LDef5: ( Carrier it ) c= (T .: ( Carrier l)) & for w be Element of W holds (it . w) = ( Sum ( lCFST (l,T,w)));

      existence

      proof

        defpred P[ object, object] means ex w be Element of W st $1 = w & $2 = ( Sum ( lCFST (l,T,w)));

        

         A1: for x be object st x in ( [#] W) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in ( [#] W);

          then

          reconsider x as Element of W;

          take ( Sum ( lCFST (l,T,x)));

          thus thesis;

        end;

        consider f be Function such that

         A2: ( dom f) = ( [#] W) and

         A3: for x be object st x in ( [#] W) holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        

         A4: ( rng f) c= the carrier of R

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A5: x in ( dom f) and

           A6: (f . x) = y by FUNCT_1:def 3;

          consider w be Element of W such that

           A7: x = w & (f . x) = ( Sum ( lCFST (l,T,w))) by A2, A3, A5;

          thus thesis by A6, A7;

        end;

        

         A8: for w be Element of W holds (f . w) = ( Sum ( lCFST (l,T,w)))

        proof

          let w be Element of W;

          ex w9 be Element of W st w = w9 & (f . w) = ( Sum ( lCFST (l,T,w9))) by A3;

          hence thesis;

        end;

        reconsider f as Element of ( Funcs (( [#] W),the carrier of R)) by A2, A4, FUNCT_2:def 2;

        set X = { w where w be Element of W : (f . w) <> ( 0. R) };

        X c= ( [#] W)

        proof

          let x be object;

          assume x in X;

          then ex w be Element of W st x = w & (f . w) <> ( 0. R);

          hence thesis;

        end;

        then

        reconsider X as Subset of W;

        set C = ( Carrier l);

        reconsider TC = (T .: C) as Subset of W;

        

         A9: X c= TC

        proof

          let x be object;

          assume x in X;

          then

          consider w be Element of W such that

           A10: x = w and

           A11: (f . w) <> ( 0. R);

          (T " {w}) meets ( Carrier l)

          proof

            assume (T " {w}) misses ( Carrier l);

            then ( lCFST (l,T,w)) = ( <*> the carrier of R);

            then ( Sum ( lCFST (l,T,w))) = ( 0. R) by RLVECT_1: 43;

            hence contradiction by A8, A11;

          end;

          then

          consider y be object such that

           A13: y in (T " {w}) and

           A14: y in ( Carrier l) by XBOOLE_0: 3;

          

           A15: ( dom T) = ( [#] V) by RANKNULL: 7;

          reconsider y as Element of V by A14;

          (T . y) in {w} by A13, FUNCT_1:def 7;

          then (T . y) = w by TARSKI:def 1;

          hence thesis by A10, A14, A15, FUNCT_1:def 6;

        end;

        then

        reconsider X as finite Subset of W;

        ex T be finite Subset of W st for w be Element of W st not w in T holds (f . w) = ( 0. R)

        proof

          take X;

          thus thesis;

        end;

        then

        reconsider f as Linear_Combination of W by VECTSP_6:def 1;

        take f;

        for w be Element of W holds (f . w) = ( Sum ( lCFST (l,T,w)))

        proof

          let w be Element of W;

          ex w9 be Element of W st w = w9 & (f . w) = ( Sum ( lCFST (l,T,w9))) by A3;

          hence thesis;

        end;

        hence thesis by A9;

      end;

      uniqueness

      proof

        let f,g be Linear_Combination of W such that

         A16: ( Carrier f) c= (T .: ( Carrier l)) & for w be Element of W holds (f . w) = ( Sum ( lCFST (l,T,w))) and

         A17: ( Carrier g) c= (T .: ( Carrier l)) & for w be Element of W holds (g . w) = ( Sum ( lCFST (l,T,w)));

        

         A18: for x be object st x in ( dom f) holds (f . x) = (g . x)

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider x as Element of W;

          (f . x) = ( Sum ( lCFST (l,T,x))) by A16;

          hence thesis by A17;

        end;

        ( dom f) = ( [#] W) & ( dom g) = ( [#] W) by FUNCT_2: 92;

        hence thesis by A18;

      end;

    end

    theorem :: ZMODUL05:44

    

     LTh29: for R be Ring holds for V,W be LeftMod of R, l be Linear_Combination of V, T be linear-transformation of V, W holds (T @* l) is Linear_Combination of (T .: ( Carrier l))

    proof

      let R be Ring;

      let V,W be LeftMod of R;

      let l be Linear_Combination of V, T be linear-transformation of V, W;

      ( Carrier (T @* l)) c= (T .: ( Carrier l)) by LDef5;

      hence thesis by VECTSP_6:def 4;

    end;

    theorem :: ZMODUL05:45

    

     ThTF3B2: for K be Ring holds for V,W be LeftMod of K, T be linear-transformation of V, W, s be Vector of W holds (for A be Subset of V, l be Linear_Combination of A st (for v be Vector of V st v in ( Carrier l) holds (T . v) = s) holds (T . ( Sum l)) = (( Sum ( lCFST (l,T,s))) * s))

    proof

      let K be Ring;

      let V,W be LeftMod of K, T be linear-transformation of V, W, s be Vector of W;

      

       A1: T is additive;

      defpred P[ Nat] means for A be Subset of V, l be Linear_Combination of A st ( card ( Carrier l)) = $1 & (for v be Vector of V st v in ( Carrier l) holds (T . v) = s) holds (T . ( Sum l)) = (( Sum ( lCFST (l,T,s))) * s);

      reconsider SZ0 = {( 0. K)} as finite Subset of K;

      

       A2: P[ 0 ]

      proof

        let A be Subset of V, l be Linear_Combination of A;

        assume ( card ( Carrier l)) = 0 & for v be Vector of V st v in ( Carrier l) holds (T . v) = s;

        then

         A3: ( Carrier l) = {} ;

        

        then

         A4: (T . ( Sum l)) = (T . ( 0. V)) by VECTSP_6: 19

        .= (T . (( 0. K) * ( 0. V))) by VECTSP_1: 14

        .= (( 0. K) * (T . ( 0. V))) by MOD_2:def 2

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

        set g = ( canFS ((T " {s}) /\ ( Carrier l)));

        ( lCFST (l,T,s)) = ( <*> the carrier of K) by A3;

        then ( Sum ( lCFST (l,T,s))) = ( 0. K) by RLVECT_1: 43;

        hence (T . ( Sum l)) = (( Sum ( lCFST (l,T,s))) * s) by A4, VECTSP_1: 14;

      end;

      

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

      proof

        let n be Nat;

        assume

         A6: P[n];

        let A be Subset of V, l be Linear_Combination of A;

        assume

         A7: ( card ( Carrier l)) = (n + 1) & (for v be Vector of V st v in ( Carrier l) holds (T . v) = s);

        then ( Carrier l) <> {} ;

        then

        consider w be object such that

         A8: w in ( Carrier l) by XBOOLE_0:def 1;

        reconsider w as Element of the carrier of V by A8;

        

         A9: ( card (( Carrier l) \ {w})) = (( card ( Carrier l)) - ( card {w})) by A8, CARD_2: 44, ZFMISC_1: 31

        .= ((n + 1) - 1) by A7, CARD_2: 42

        .= n;

        reconsider A0 = (( Carrier l) \ {w}) as finite Subset of V;

        reconsider B0 = {w} as finite Subset of V;

        defpred PA0[ object, object] means $1 is Vector of V implies ($1 in A0 & $2 = (l . $1)) or ( not $1 in A0 & $2 = ( 0. K));

        

         A10: for x be object st x in the carrier of V holds ex y be object st y in the carrier of K & PA0[x, y]

        proof

          let x be object;

          assume x in the carrier of V;

          then

          reconsider x9 = x as Vector of V;

          per cases ;

            suppose

             A11: x in A0;

            (l . x9) in the carrier of K;

            hence thesis by A11;

          end;

            suppose not x in A0;

            hence thesis;

          end;

        end;

        consider l0 be Function of the carrier of V, the carrier of K such that

         A13: for x be object st x in the carrier of V holds PA0[x, (l0 . x)] from FUNCT_2:sch 1( A10);

        

         A14: for v be Vector of V st not v in A0 holds (l0 . v) = ( 0. K) by A13;

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

        reconsider l0 as Linear_Combination of V by A14, VECTSP_6:def 1;

        

         A15: for x be object holds x in A0 iff x in ( Carrier l0)

        proof

          let x be object;

          hereby

            assume

             A16: x in A0;

            then

            reconsider v = x as Vector of V;

            

             A17: (l0 . v) = (l . v) by A13, A16;

            v in ( Carrier l) by A16, XBOOLE_0:def 5;

            then (l0 . v) <> ( 0. K) by A17, VECTSP_6: 2;

            hence x in ( Carrier l0);

          end;

          assume

           A18: x in ( Carrier l0);

          then

          reconsider v = x as Vector of V;

          ex v9 be Vector of V st v9 = v & (l0 . v9) <> ( 0. K) by A18;

          hence x in A0 by A13;

        end;

        then

         A19: ( Carrier l0) = A0 by TARSKI: 2;

        then

        reconsider l0 as Linear_Combination of A0 by VECTSP_6:def 4;

        

         A20: (l0 | ( Carrier l0)) = (l | ( Carrier l0))

        proof

          reconsider L0 = l0 as Function of V, K;

          reconsider L1 = l as Function of V, K;

          reconsider L00 = (L0 | ( Carrier l0)) as Function of ( Carrier l0), the carrier of K by FUNCT_2: 32;

          reconsider L11 = (L1 | ( Carrier l0)) as Function of ( Carrier l0), the carrier of K by FUNCT_2: 32;

          now

            let x be object;

            assume

             A21: x in ( Carrier l0);

            then

            reconsider v = x as Vector of V;

            

            thus (L00 . x) = (l0 . v) by A21, FUNCT_1: 49

            .= (l . v) by A13, A19, A21

            .= (L11 . x) by A21, FUNCT_1: 49;

          end;

          hence thesis by FUNCT_2: 12;

        end;

        defpred PB0[ object, object] means $1 is Vector of V implies ($1 in B0 & $2 = (l . $1)) or ( not $1 in B0 & $2 = ( 0. K));

        

         A22: for x be object st x in the carrier of V holds ex y be object st y in the carrier of K & PB0[x, y]

        proof

          let x be object;

          assume x in the carrier of V;

          then

          reconsider x9 = x as Vector of V;

          per cases ;

            suppose

             A23: x in B0;

            (l . x9) in the carrier of K;

            hence thesis by A23;

          end;

            suppose not x in B0;

            hence thesis;

          end;

        end;

        consider l1 be Function of V, K such that

         A25: for x be object st x in the carrier of V holds PB0[x, (l1 . x)] from FUNCT_2:sch 1( A22);

        

         A26: for v be Vector of V st not v in B0 holds (l1 . v) = ( 0. K) by A25;

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

        reconsider l1 as Linear_Combination of V by A26, VECTSP_6:def 1;

        for x be object holds x in B0 iff x in ( Carrier l1)

        proof

          let x be object;

          hereby

            assume

             A27: x in B0;

            then

             A28: x = w by TARSKI:def 1;

            then

             A29: (l1 . w) = (l . w) by A25, A27;

            (l . w) <> ( 0. K) by A8, VECTSP_6: 2;

            hence x in ( Carrier l1) by A28, A29;

          end;

          assume

           A30: x in ( Carrier l1);

          then

          reconsider v = x as Vector of V;

          ex v9 be Vector of V st v9 = v & (l1 . v9) <> ( 0. K) by A30;

          hence x in B0 by A25;

        end;

        then ( Carrier l1) = B0 by TARSKI: 2;

        then

        reconsider l1 as Linear_Combination of B0 by VECTSP_6:def 4;

        for v be Element of V holds (l . v) = ((l0 + l1) . v)

        proof

          let v be Element of V;

          per cases ;

            suppose

             A31: not v in ( Carrier l);

            then

             A32: (l . v) = ( 0. K);

             not v in A0 by A31, XBOOLE_0:def 5;

            then (l0 . v) = ( 0. K) by A13;

            then (l . v) = ((l0 . v) + (l1 . v)) by A25, A32;

            hence thesis by VECTSP_6: 22;

          end;

            suppose

             A34: v in ( Carrier l);

            per cases ;

              suppose

               A35: v in {w};

              then not v in A0 by XBOOLE_0:def 5;

              then (l0 . v) = ( 0. K) by A13;

              then (l . v) = ((l0 . v) + (l1 . v)) by A25, A35;

              hence thesis by VECTSP_6: 22;

            end;

              suppose

               A37: not v in {w};

              then

               A38: v in A0 by A34, XBOOLE_0:def 5;

              (l1 . v) = ( 0. K) by A25, A37;

              then (l . v) = ((l0 . v) + (l1 . v)) by A13, A38;

              hence thesis by VECTSP_6: 22;

            end;

          end;

        end;

        then l = (l0 + l1);

        then

         A39: ( Sum l) = (( Sum l0) + ( Sum l1)) by VECTSP_6: 44;

        for v be Vector of V st v in ( Carrier l0) holds (T . v) = s

        proof

          let v be Vector of V;

          assume v in ( Carrier l0);

          then v in ( Carrier l) by A19, XBOOLE_0:def 5;

          hence thesis by A7;

        end;

        then

         A40: (T . ( Sum l0)) = (( Sum ( lCFST (l0,T,s))) * s) by A6, A9, A19;

        

         A41: (A0 \/ B0) = (( Carrier l) \/ B0) by XBOOLE_1: 39

        .= ( Carrier l) by A8, XBOOLE_1: 12, ZFMISC_1: 31;

        

         A42: w in B0 by TARSKI:def 1;

        

         A43: (T . ( Sum l1)) = (T . ((l1 . w) * w)) by VECTSP_6: 17

        .= ((l1 . w) * (T . w)) by MOD_2:def 2

        .= ((l1 . w) * s) by A7, A8

        .= ((l . w) * s) by A25, A42

        .= (( Sum <*(l . w)*>) * s) by RLVECT_1: 44;

        set WW = (( lCFST (l0,T,s)) ^ <*(l /. w)*>);

        ( rng WW) = (( rng ( lCFST (l0,T,s))) \/ ( rng <*(l /. w)*>)) by FINSEQ_1: 31;

        then

        reconsider WW as FinSequence of K by FINSEQ_1:def 4;

        reconsider L = ( Sum WW) as Element of K;

        

         A44: ((T " {s}) /\ ( Carrier l)) = (((T " {s}) /\ A0) \/ ((T " {s}) /\ B0)) by A41, XBOOLE_1: 23

        .= (((T " {s}) /\ ( Carrier l0)) \/ ((T " {s}) /\ B0)) by A15, TARSKI: 2;

        reconsider S1 = ((T " {s}) /\ ( Carrier l0)) as finite Subset of V;

        now

          let z be object;

          assume

           A45: z in B0;

          (T . w) = s by A7, A8;

          then

           A46: (T . w) in {s} by TARSKI:def 1;

          w in (T " {s}) by A46, FUNCT_2: 38;

          hence z in (T " {s}) by A45, TARSKI:def 1;

        end;

        then B0 c= (T " {s});

        then

         A47: ((T " {s}) /\ B0) = {w} by XBOOLE_1: 28;

        reconsider S2 = ((T " {s}) /\ B0) as finite Subset of the carrier of V;

        

         A48: ((( Carrier l) \ {w}) /\ B0) = ((B0 /\ ( Carrier l)) \ B0) by XBOOLE_1: 49

        .= {} by XBOOLE_1: 17, XBOOLE_1: 37;

        

         A49: (S1 /\ S2) = ((((T " {s}) /\ ( Carrier l0)) /\ B0) /\ (T " {s})) by XBOOLE_1: 16

        .= ((((T " {s}) /\ (( Carrier l) \ {w})) /\ B0) /\ (T " {s})) by A15, TARSKI: 2

        .= (((T " {s}) /\ {} ) /\ (T " {s})) by A48, XBOOLE_1: 16

        .= {} ;

        

         A50: ( Carrier l0) c= ( Carrier l) by A19, XBOOLE_1: 36;

        reconsider ll = l as Function of the carrier of V, the carrier of K;

        

         A51: (l * ( canFS S2)) = (ll * <*w*>) by A47, FINSEQ_1: 94

        .= <*(ll . w)*> by FINSEQ_2: 35;

        ( rng (l * ( canFS S1))) c= the carrier of K;

        then

        reconsider l1 = (l * ( canFS S1)) as FinSequence of K by FINSEQ_1:def 4;

        reconsider l2 = (l * ( canFS S2)) as FinSequence of K by A51;

        ( rng ( lCFST (l,T,s))) c= the carrier of K;

        then

        reconsider ll0 = ( lCFST (l,T,s)) as FinSequence of K by FINSEQ_1:def 4;

        

         A52: ( Sum ll0) = (( Sum l1) + ( Sum l2)) by A44, A49, ThTF3C2

        .= (( Sum ( lCFST (l0,T,s))) + ( Sum <*(l . w)*>)) by A20, A50, A51, ThTF3C3, XBOOLE_1: 17;

        

        thus (T . ( Sum l)) = ((( Sum ( lCFST (l0,T,s))) * s) + (( Sum <*(l . w)*>) * s)) by A1, A39, A40, A43

        .= (( Sum ( lCFST (l,T,s))) * s) by A52, VECTSP_1:def 15;

      end;

      

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

      let A be Subset of V, l be Linear_Combination of A;

      assume

       A54: for v be Vector of V st v in ( Carrier l) holds (T . v) = s;

      ( card ( Carrier l)) is Nat;

      hence thesis by A53, A54;

    end;

    theorem :: ZMODUL05:46

    for K be Ring holds for V,W be LeftMod of K, T be linear-transformation of V, W, A be Subset of V, l be Linear_Combination of A, Tl be Linear_Combination of (T .: ( Carrier l)) st Tl = (T @* l) holds (T . ( Sum l)) = ( Sum Tl)

    proof

      let K be Ring;

      let V,W be LeftMod of K, T be linear-transformation of V, W;

      

       A1: T is additive;

      

       A2: ( dom T) = the carrier of V by FUNCT_2:def 1;

      defpred P[ Nat] means for A be Subset of V, l be Linear_Combination of A, Tl be Linear_Combination of (T .: ( Carrier l)) st Tl = (T @* l) & ( card (T .: ( Carrier l))) = $1 holds (T . ( Sum l)) = ( Sum Tl);

      

       A3: P[ 0 ]

      proof

        let A be Subset of V, l be Linear_Combination of A, Tl be Linear_Combination of (T .: ( Carrier l));

        assume

         P1: Tl = (T @* l) & ( card (T .: ( Carrier l))) = 0 ;

        

         A4: (T .: ( Carrier l)) = {} by P1;

        ( Carrier l) = {} or not ( Carrier l) c= ( dom T) by P1;

        

        then

         A5: (T . ( Sum l)) = (T . ( 0. V)) by A2, VECTSP_6: 19

        .= (T . (( 0. K) * ( 0. V))) by VECTSP_1: 14

        .= (( 0. K) * (T . ( 0. V))) by MOD_2:def 2

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

        ( Carrier (T @* l)) c= {} by A4, LDef5;

        then ( Carrier (T @* l)) = {} ;

        hence (T . ( Sum l)) = ( Sum Tl) by A5, P1, VECTSP_6: 19;

      end;

      

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

      proof

        let n be Nat;

        assume

         A21: P[n];

        let A be Subset of V, l be Linear_Combination of A, Tl be Linear_Combination of (T .: ( Carrier l));

        assume

         A7: Tl = (T @* l) & ( card (T .: ( Carrier l))) = (n + 1);

        then (T .: ( Carrier l)) <> {} ;

        then

        consider w be object such that

         A8: w in (T .: ( Carrier l)) by XBOOLE_0:def 1;

        reconsider w as Element of the carrier of W by A8;

        

         A9: ( card ((T .: ( Carrier l)) \ {w})) = (( card (T .: ( Carrier l))) - ( card {w})) by A8, CARD_2: 44, ZFMISC_1: 31

        .= ((n + 1) - 1) by A7, CARD_2: 42

        .= n;

        reconsider A0 = (( Carrier l) \ (T " {w})) as finite Subset of V;

        reconsider B0 = ((T " {w}) /\ ( Carrier l)) as Subset of V;

        reconsider B0 as finite Subset of V;

        defpred PA0[ object, object] means $1 is Vector of V implies ($1 in A0 & $2 = (l . $1)) or ( not $1 in A0 & $2 = ( 0. K));

        

         A10: for x be object st x in the carrier of V holds ex y be object st y in the carrier of K & PA0[x, y]

        proof

          let x be object;

          assume x in the carrier of V;

          then

          reconsider x9 = x as Vector of V;

          per cases ;

            suppose

             A11: x in A0;

            (l . x9) in the carrier of K;

            hence thesis by A11;

          end;

            suppose not x in A0;

            hence thesis;

          end;

        end;

        consider l0 be Function of the carrier of V, the carrier of K such that

         A13: for x be object st x in the carrier of V holds PA0[x, (l0 . x)] from FUNCT_2:sch 1( A10);

        

         A14: for v be Vector of V st not v in A0 holds (l0 . v) = ( 0. K) by A13;

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

        reconsider l0 as Linear_Combination of V by A14, VECTSP_6:def 1;

        

         A15: for x be object holds x in A0 iff x in ( Carrier l0)

        proof

          let x be object;

          hereby

            assume

             A16: x in A0;

            then

            reconsider v = x as Vector of V;

            

             A17: (l0 . v) = (l . v) by A13, A16;

            v in ( Carrier l) by A16, XBOOLE_0:def 5;

            then (l0 . v) <> ( 0. K) by A17, VECTSP_6: 2;

            hence x in ( Carrier l0);

          end;

          assume

           A18: x in ( Carrier l0);

          then

          reconsider v = x as Vector of V;

          ex v9 be Vector of V st v9 = v & (l0 . v9) <> ( 0. K) by A18;

          hence x in A0 by A13;

        end;

        then

         A19: ( Carrier l0) = A0 by TARSKI: 2;

        then

        reconsider l0 as Linear_Combination of A0 by VECTSP_6:def 4;

        

         A20: (l0 | ( Carrier l0)) = (l | ( Carrier l0))

        proof

          set L0 = l0;

          set L1 = l;

          reconsider L00 = (L0 | ( Carrier l0)) as Function of ( Carrier l0), the carrier of K by FUNCT_2: 32;

          reconsider L11 = (L1 | ( Carrier l0)) as Function of ( Carrier l0), the carrier of K by FUNCT_2: 32;

          now

            let x be object;

            assume

             A21: x in ( Carrier l0);

            then

            reconsider v = x as Vector of V;

            

            thus (L00 . x) = (L0 . x) by A21, FUNCT_1: 49

            .= (l . v) by A13, A19, A21

            .= (L11 . x) by A21, FUNCT_1: 49;

          end;

          hence thesis by FUNCT_2: 12;

        end;

        defpred PB0[ object, object] means $1 is Vector of V implies ($1 in B0 & $2 = (l . $1)) or ( not $1 in B0 & $2 = ( 0. K));

        

         A22: for x be object st x in the carrier of V holds ex y be object st y in the carrier of K & PB0[x, y]

        proof

          let x be object;

          assume x in the carrier of V;

          then

          reconsider x9 = x as Vector of V;

          per cases ;

            suppose

             A23: x in B0;

            (l . x9) in the carrier of K;

            hence thesis by A23;

          end;

            suppose not x in B0;

            hence thesis;

          end;

        end;

        consider l1 be Function of the carrier of V, the carrier of K such that

         A25: for x be object st x in the carrier of V holds PB0[x, (l1 . x)] from FUNCT_2:sch 1( A22);

        

         A26: for v be Vector of V st not v in B0 holds (l1 . v) = ( 0. K) by A25;

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

        reconsider l1 as Linear_Combination of V by A26, VECTSP_6:def 1;

        

         A27: for x be object holds x in B0 iff x in ( Carrier l1)

        proof

          let x be object;

          hereby

            assume

             A28: x in B0;

            then

            reconsider v = x as Vector of V;

            

             A29: (l1 . v) = (l . v) by A25, A28;

            v in ( Carrier l) by A28, XBOOLE_0:def 4;

            then (l1 . v) <> ( 0. K) by A29, VECTSP_6: 2;

            hence x in ( Carrier l1);

          end;

          assume

           X1: x in ( Carrier l1);

          then

          reconsider v = x as Vector of V;

          ex v9 be Vector of V st v9 = v & (l1 . v9) <> ( 0. K) by X1;

          hence x in B0 by A25;

        end;

        then

         A30: ( Carrier l1) = B0 by TARSKI: 2;

        then

        reconsider l1 as Linear_Combination of B0 by VECTSP_6:def 4;

        

         A31: (l1 | ( Carrier l1)) = (l | ( Carrier l1))

        proof

          reconsider L0 = l1 as Function of V, K;

          reconsider L1 = l as Function of V, K;

          reconsider L00 = (L0 | ( Carrier l1)) as Function of ( Carrier l1), the carrier of K by FUNCT_2: 32;

          reconsider L11 = (L1 | ( Carrier l1)) as Function of ( Carrier l1), the carrier of K by FUNCT_2: 32;

          now

            let x be object;

            assume

             A32: x in ( Carrier l1);

            then

            reconsider v = x as Vector of V;

            

            thus (L00 . x) = (L0 . x) by A32, FUNCT_1: 49

            .= (l . v) by A25, A30, A32

            .= (L11 . x) by A32, FUNCT_1: 49;

          end;

          hence thesis by FUNCT_2: 12;

        end;

        

         A33: for v be Element of V holds (l . v) = ((l0 + l1) . v)

        proof

          let v be Element of V;

          per cases ;

            suppose

             A34: not v in ( Carrier l);

            then

             A35: (l . v) = ( 0. K);

             not v in A0 by A34, XBOOLE_0:def 5;

            then

             A36: (l0 . v) = ( 0. K) by A13;

            (l . v) = ((l1 . v) + (l0 . v)) by A25, A35, A36;

            hence (l . v) = ((l0 + l1) . v) by VECTSP_6: 22;

          end;

            suppose

             A37: v in ( Carrier l);

            per cases ;

              suppose

               A38: v in (T " {w});

              then not v in A0 by XBOOLE_0:def 5;

              then

               A39: (l0 . v) = ( 0. K) by A13;

              v in B0 by A37, A38, XBOOLE_0:def 4;

              then (l . v) = ((l1 . v) + (l0 . v)) by A25, A39;

              hence (l . v) = ((l0 + l1) . v) by VECTSP_6: 22;

            end;

              suppose

               A40: not v in (T " {w});

              then

               A41: v in A0 by A37, XBOOLE_0:def 5;

               not v in B0 by A40, XBOOLE_0:def 4;

              then (l1 . v) = ( 0. K) by A25;

              then (l . v) = ((l1 . v) + (l0 . v)) by A13, A41;

              hence (l . v) = ((l0 + l1) . v) by VECTSP_6: 22;

            end;

          end;

        end;

        then

         A42: l = (l0 + l1);

        reconsider Tl0 = (T @* l0) as Linear_Combination of (T .: ( Carrier l0)) by LTh29;

        reconsider Tl1 = (T @* l1) as Linear_Combination of (T .: ( Carrier l1)) by LTh29;

        

         A43: ((T .: ( Carrier l0)) /\ (T .: ( Carrier l1))) = {}

        proof

          assume ((T .: ( Carrier l0)) /\ (T .: ( Carrier l1))) <> {} ;

          then

          consider y be object such that

           A44: y in ((T .: ( Carrier l0)) /\ (T .: ( Carrier l1))) by XBOOLE_0:def 1;

          

           A45: y in (T .: ( Carrier l0)) & y in (T .: ( Carrier l1)) by A44, XBOOLE_0:def 4;

          then

          consider x be object such that

           A46: x in the carrier of V & x in ( Carrier l0) & y = (T . x) by FUNCT_2: 64;

          consider z be object such that

           A47: z in the carrier of V & z in ( Carrier l1) & y = (T . z) by A45, FUNCT_2: 64;

          x in (( Carrier l) \ (T " {w})) by A15, A46;

          then not x in (T " {w}) by XBOOLE_0:def 5;

          then

           A48: not y in {w} by A46, FUNCT_2: 38;

          z in ((T " {w}) /\ ( Carrier l)) by A27, A47;

          then z in (T " {w}) by XBOOLE_0:def 4;

          hence contradiction by A47, A48, FUNCT_2: 38;

        end;

        

         A49: (T .: ( Carrier l)) c= (T .: (( Carrier l1) \/ ( Carrier l0))) by A42, RELAT_1: 123, VECTSP_6: 23;

        

         A50: for w be Vector of W st w in (T .: ( Carrier l0)) holds (Tl . w) = (Tl0 . w)

        proof

          let v be Vector of W;

          assume v in (T .: ( Carrier l0));

          then

          consider x be object such that

           A51: x in the carrier of V & x in ( Carrier l0) & v = (T . x) by FUNCT_2: 64;

          reconsider x as Vector of V by A51;

          

           A52: (Tl0 . v) = ( Sum ( lCFST (l0,T,v))) by LDef5;

          

           A53: (Tl . v) = ( Sum ( lCFST (l,T,v))) by A7, LDef5;

          

           A54: ( Carrier l0) c= ( Carrier l) by A19, XBOOLE_1: 36;

          now

            let s be object;

            assume s in ((T " {v}) /\ ( Carrier l));

            then

             A55: s in (T " {v}) & s in ( Carrier l) by XBOOLE_0:def 4;

            then s in the carrier of V & (T . s) in {v} by FUNCT_2: 38;

            then

             A56: (T . s) = (T . x) by A51, TARSKI:def 1;

             not s in (T " {w})

            proof

              assume s in (T " {w});

              then (T . x) in {w} by A56, FUNCT_2: 38;

              then x in (T " {w}) by FUNCT_2: 38;

              hence contradiction by A19, A51, XBOOLE_0:def 5;

            end;

            then s in ( Carrier l0) by A19, A55, XBOOLE_0:def 5;

            hence s in ((T " {v}) /\ ( Carrier l0)) by A55, XBOOLE_0:def 4;

          end;

          then ((T " {v}) /\ ( Carrier l)) c= ((T " {v}) /\ ( Carrier l0));

          then

           A57: ((T " {v}) /\ ( Carrier l0)) = ((T " {v}) /\ ( Carrier l)) by A19, XBOOLE_1: 26, XBOOLE_1: 36;

          reconsider XX = ((T " {v}) /\ ( Carrier l0)) as finite Subset of V;

          thus thesis by A20, A52, A53, A54, A57, ThTF3C3, XBOOLE_1: 17;

        end;

        

         A58: for w be Vector of W st w in (T .: ( Carrier l1)) holds (Tl . w) = (Tl1 . w)

        proof

          let v be Vector of W;

          assume v in (T .: ( Carrier l1));

          then

          consider x be object such that

           A59: x in the carrier of V & x in ( Carrier l1) & v = (T . x) by FUNCT_2: 64;

          reconsider x as Vector of V by A59;

          

           A60: (Tl1 . v) = ( Sum ( lCFST (l1,T,v))) by LDef5;

          

           A61: (Tl . v) = ( Sum ( lCFST (l,T,v))) by A7, LDef5;

          

           A62: ( Carrier l1) c= ( Carrier l) by A30, XBOOLE_1: 17;

          now

            let s be object;

            assume

             A63: s in ((T " {v}) /\ ( Carrier l));

            then

             A64: s in (T " {v}) & s in ( Carrier l) by XBOOLE_0:def 4;

            then s in the carrier of V & (T . s) in {v} by FUNCT_2: 38;

            then

             A65: (T . s) = (T . x) by A59, TARSKI:def 1;

            x in (T " {w}) by A30, A59, XBOOLE_0:def 4;

            then (T . s) in {w} by A65, FUNCT_2: 38;

            then s in (T " {w}) by A63, FUNCT_2: 38;

            then s in ( Carrier l1) by A30, A64, XBOOLE_0:def 4;

            hence s in ((T " {v}) /\ ( Carrier l1)) by A64, XBOOLE_0:def 4;

          end;

          then ((T " {v}) /\ ( Carrier l)) c= ((T " {v}) /\ ( Carrier l1));

          then

           A66: ((T " {v}) /\ ( Carrier l1)) = ((T " {v}) /\ ( Carrier l)) by A30, XBOOLE_1: 17, XBOOLE_1: 26;

          reconsider XX = ((T " {v}) /\ ( Carrier l1)) as finite Subset of V;

          thus thesis by A31, A60, A61, A62, A66, ThTF3C3, XBOOLE_1: 17;

        end;

        

         A67: for x be object st x in ( Carrier Tl0) holds x in ( Carrier Tl)

        proof

          let x be object;

          assume

           A68: x in ( Carrier Tl0);

          then

          reconsider v = x as Vector of W;

          

           A69: v in (T .: ( Carrier l0)) by A68, LDef5, TARSKI:def 3;

          (Tl0 . v) <> ( 0. K) by A68, VECTSP_6: 2;

          then (Tl . v) <> ( 0. K) by A50, A69;

          hence x in ( Carrier Tl);

        end;

        

         A70: for x be object st x in ( Carrier Tl1) holds x in ( Carrier Tl)

        proof

          let x be object;

          assume

           A71: x in ( Carrier Tl1);

          then

          reconsider v = x as Vector of W;

          

           A72: v in (T .: ( Carrier l1)) by A71, LDef5, TARSKI:def 3;

          (Tl1 . v) <> ( 0. K) by A71, VECTSP_6: 2;

          then (Tl . v) <> ( 0. K) by A58, A72;

          hence x in ( Carrier Tl);

        end;

        

         A73: (T .: ( Carrier l0)) = (T .: (( Carrier l) \ (T " {w}))) by A15, TARSKI: 2;

        then

         A74: ((T .: ( Carrier l)) \ (T .: (T " {w}))) c= (T .: ( Carrier l0)) by RELAT_1: 122;

        

         A75: (T .: ( Carrier l)) c= (T .: ( dom T)) by RELAT_1: 114;

        

         A76: (T .: ( Carrier l)) c= ( rng T) by A75, RELAT_1: 113;

        for x be object st x in (T .: ( Carrier l0)) holds x in ((T .: ( Carrier l)) \ {w})

        proof

          let x be object;

          assume x in (T .: ( Carrier l0));

          then

          consider z be object such that

           A77: z in the carrier of V & z in (( Carrier l) \ (T " {w})) & x = (T . z) by A73, FUNCT_2: 64;

          z in ( Carrier l) by A77, XBOOLE_0:def 5;

          then

           A78: x in (T .: ( Carrier l)) by A77, FUNCT_2: 35;

           not x in {w}

          proof

            assume

             A79: x in {w};

            z in ( dom T) by A77, FUNCT_2:def 1;

            then z in (T " {w}) by A77, A79, FUNCT_1:def 7;

            hence contradiction by A77, XBOOLE_0:def 5;

          end;

          hence x in ((T .: ( Carrier l)) \ {w}) by A78, XBOOLE_0:def 5;

        end;

        then (T .: ( Carrier l0)) c= ((T .: ( Carrier l)) \ {w});

        then

         A80: (T .: ( Carrier l0)) = ((T .: ( Carrier l)) \ {w}) by A8, A74, A76, FUNCT_1: 77, ZFMISC_1: 31;

        for y be object st y in ( Carrier Tl1) holds y in {w}

        proof

          let y be object;

          assume

           A81: y in ( Carrier Tl1);

          then

          reconsider v = y as Vector of W;

          

           A83: (Tl1 . v) = ( Sum ( lCFST (l1,T,v))) by LDef5;

          y = w

          proof

            assume

             A84: y <> w;

            

             A85: ((T " {v}) /\ (T " {w})) = {}

            proof

              assume ((T " {v}) /\ (T " {w})) <> {} ;

              then

              consider x be object such that

               A86: x in ((T " {v}) /\ (T " {w})) by XBOOLE_0:def 1;

              x in (T " {v}) & x in (T " {w}) by A86, XBOOLE_0:def 4;

              then (T . x) in {v} & (T . x) in {w} by FUNCT_1:def 7;

              then (T . x) = v & (T . x) = w by TARSKI:def 1;

              hence contradiction by A84;

            end;

            set g = ( canFS ((T " {v}) /\ ( Carrier l1)));

            ((T " {v}) /\ ( Carrier l1)) = ((T " {v}) /\ ((T " {w}) /\ ( Carrier l))) by A27, TARSKI: 2

            .= ( {} /\ ( Carrier l)) by A85, XBOOLE_1: 16

            .= {} ;

            then ( lCFST (l1,T,v)) = ( <*> the carrier of K);

            hence contradiction by A81, A83, RLVECT_1: 43, VECTSP_6: 2;

          end;

          hence y in {w} by TARSKI:def 1;

        end;

        then

         A87: ( Carrier Tl1) c= {w};

        

         A88: (T . ( Sum l1)) = ( Sum Tl1)

        proof

          

           A89: (Tl1 . w) = ( Sum ( lCFST (l1,T,w))) by LDef5;

          reconsider w as Vector of W;

          

           A90: for v be Vector of V st v in ( Carrier l1) holds (T . v) = w

          proof

            let v be Vector of V;

            assume v in ( Carrier l1);

            then v in ((T " {w}) /\ ( Carrier l)) by A27;

            then v in (T " {w}) by XBOOLE_0:def 4;

            then (T . v) in {w} by FUNCT_1:def 7;

            hence (T . v) = w by TARSKI:def 1;

          end;

          per cases ;

            suppose

             A91: ( Sum ( lCFST (l1,T,w))) = ( 0. K);

            then

             A92: not w in ( Carrier Tl1) by A89, VECTSP_6: 2;

            

             A93: ( Carrier Tl1) = {}

            proof

              assume ( Carrier Tl1) <> {} ;

              then

              consider x be object such that

               A94: x in ( Carrier Tl1) by XBOOLE_0:def 1;

              thus contradiction by A87, A92, A94, TARSKI:def 1;

            end;

            (T . ( Sum l1)) = (( 0. K) * w) by A90, A91, ThTF3B2

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

            hence (T . ( Sum l1)) = ( Sum Tl1) by A93, VECTSP_6: 19;

          end;

            suppose ( Sum ( lCFST (l1,T,w))) <> ( 0. K);

            then w in ( Carrier Tl1) by A89;

            then

             A95: {w} = ( Carrier Tl1) by A87, ZFMISC_1: 31;

            ( Sum Tl1) = (( Sum ( lCFST (l1,T,w))) * w) by A89, A95, VECTSP_6: 20

            .= (T . ( Sum l1)) by A90, ThTF3B2;

            hence (T . ( Sum l1)) = ( Sum Tl1);

          end;

        end;

        for w be Element of W holds (Tl . w) = ((Tl0 + Tl1) . w)

        proof

          let w be Element of W;

          per cases ;

            suppose

             A96: not w in ( Carrier Tl);

            then

             A97: (Tl . w) = ( 0. K);

             not w in ( Carrier Tl0) by A67, A96;

            then

             A98: (Tl0 . w) = ( 0. K);

             not w in ( Carrier Tl1) by A70, A96;

            then (Tl . w) = ((Tl1 . w) + (Tl0 . w)) by A97, A98;

            hence (Tl . w) = ((Tl0 + Tl1) . w) by VECTSP_6: 22;

          end;

            suppose w in ( Carrier Tl);

            then w in (T .: ( Carrier l)) by TARSKI:def 3, VECTSP_6:def 4;

            then w in (T .: (( Carrier l0) \/ ( Carrier l1))) by A49;

            then

             A99: w in ((T .: ( Carrier l0)) \/ (T .: ( Carrier l1))) by RELAT_1: 120;

            thus (Tl . w) = ((Tl0 + Tl1) . w)

            proof

              per cases by A99, XBOOLE_0:def 3;

                suppose

                 A100: w in (T .: ( Carrier l1));

                 not w in (T .: ( Carrier l0)) by A43, A100, XBOOLE_0:def 4;

                then not w in ( Carrier Tl0) by LDef5, TARSKI:def 3;

                then (Tl0 . w) = ( 0. K);

                then (Tl . w) = ((Tl1 . w) + (Tl0 . w)) by A58, A100;

                hence (Tl . w) = ((Tl0 + Tl1) . w) by VECTSP_6: 22;

              end;

                suppose

                 A101: w in (T .: ( Carrier l0));

                 not w in (T .: ( Carrier l1)) by A43, A101, XBOOLE_0:def 4;

                then not w in ( Carrier Tl1) by LDef5, TARSKI:def 3;

                then (Tl1 . w) = ( 0. K);

                then (Tl . w) = ((Tl1 . w) + (Tl0 . w)) by A50, A101;

                hence (Tl . w) = ((Tl0 + Tl1) . w) by VECTSP_6: 22;

              end;

            end;

          end;

        end;

        then

         A102: Tl = (Tl0 + Tl1);

        l = (l0 + l1) by A33;

        

        hence (T . ( Sum l)) = (T . (( Sum l0) + ( Sum l1))) by VECTSP_6: 44

        .= ((T . ( Sum l0)) + (T . ( Sum l1))) by A1

        .= (( Sum Tl0) + ( Sum Tl1)) by A9, A21, A80, A88

        .= ( Sum Tl) by A102, VECTSP_6: 44;

      end;

      

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

      let A be Subset of V, l be Linear_Combination of A, Tl be Linear_Combination of (T .: ( Carrier l));

      assume

       A104: Tl = (T @* l);

      ( card (T .: ( Carrier l))) is Nat;

      hence thesis by A103, A104;

    end;

    theorem :: ZMODUL05:47

    

     Th31: for R be Ring holds for V be LeftMod of R holds for l,m be Linear_Combination of V st ( Carrier l) misses ( Carrier m) holds ( Carrier (l + m)) = (( Carrier l) \/ ( Carrier m))

    proof

      let R be Ring;

      let V be LeftMod of R;

      let l,m be Linear_Combination of V such that

       A1: ( Carrier l) misses ( Carrier m);

      thus ( Carrier (l + m)) c= (( Carrier l) \/ ( Carrier m)) by VECTSP_6: 23;

      thus (( Carrier l) \/ ( Carrier m)) c= ( Carrier (l + m))

      proof

        let v be object such that

         A2: v in (( Carrier l) \/ ( Carrier m));

        per cases by A2, XBOOLE_0:def 3;

          suppose

           A3: v in ( Carrier l);

          then

          reconsider v as Element of V;

           not v in ( Carrier m) by A1, A2, A3, XBOOLE_0: 5;

          then

           A4: ((l + m) . v) = ((l . v) + (m . v)) & (m . v) = ( 0. R) by VECTSP_6: 22;

          (l . v) <> ( 0. R) by A3, VECTSP_6: 2;

          hence thesis by A4;

        end;

          suppose

           A5: v in ( Carrier m);

          then

          reconsider v as Element of V;

           not v in ( Carrier l) by A1, A2, A5, XBOOLE_0: 5;

          then

           A6: ((l + m) . v) = ((l . v) + (m . v)) & (l . v) = ( 0. R) by VECTSP_6: 22;

          (m . v) <> ( 0. R) by A5, VECTSP_6: 2;

          hence thesis by A6;

        end;

      end;

    end;

    theorem :: ZMODUL05:48

    

     Th32: for R be Ring holds for V be LeftMod of R holds for l,m be Linear_Combination of V st ( Carrier l) misses ( Carrier m) holds ( Carrier (l - m)) = (( Carrier l) \/ ( Carrier m))

    proof

      let R be Ring;

      let V be LeftMod of R;

      let l,m be Linear_Combination of V such that

       A1: ( Carrier l) misses ( Carrier m);

      ( Carrier ( - m)) = ( Carrier m) by VECTSP_6: 38;

      hence thesis by A1, Th31;

    end;

    theorem :: ZMODUL05:49

    for R be Ring holds for V be LeftMod of R, A be Subset of V, l1,l2 be Linear_Combination of A st ( Carrier l1) misses ( Carrier l2) holds ( Carrier (l1 - l2)) = (( Carrier l1) \/ ( Carrier l2))

    proof

      let R be Ring;

      let V be LeftMod of R;

      let A be Subset of V, l1,l2 be Linear_Combination of A such that

       A1: ( Carrier l1) misses ( Carrier l2);

      

       A2: ( Carrier l1) misses ( Carrier ( - l2)) by A1, VECTSP_6: 38;

      

      thus ( Carrier (l1 - l2)) = ( Carrier (l1 + ( - l2)))

      .= (( Carrier l1) \/ ( Carrier ( - l2))) by A2, Th31

      .= (( Carrier l1) \/ ( Carrier l2)) by VECTSP_6: 38;

    end;

    theorem :: ZMODUL05:50

    for V be free Z_Module, A,B be Subset of V st A c= B & B is Basis of V holds V is_the_direct_sum_of (( Lin A),( Lin (B \ A)))

    proof

      let V be free Z_Module, A,B be Subset of V such that

       A1: A c= B and

       A2: B is Basis of V;

      

       A3: (( Lin A) /\ ( Lin (B \ A))) = ( (0). V)

      proof

        set U = (( Lin A) /\ ( Lin (B \ A)));

        reconsider W = ( (0). V) as strict Submodule of U by ZMODUL01: 54;

        for v be Element of U holds v in W

        proof

          let v be Element of U;

          

           A4: B is linearly-independent by A2, VECTSP_7:def 3;

          

           A5: v in U;

          then v in ( Lin A) by ZMODUL01: 94;

          then

          consider l be Linear_Combination of A such that

           A6: v = ( Sum l) by ZMODUL02: 64;

          v in ( Lin (B \ A)) by A5, ZMODUL01: 94;

          then

          consider m be Linear_Combination of (B \ A) such that

           A7: v = ( Sum m) by ZMODUL02: 64;

          

           A8: ( 0. V) = (( Sum l) - ( Sum m)) by A6, A7, VECTSP_1: 19

          .= ( Sum (l - m)) by ZMODUL02: 55;

          

           A9: ( Carrier (l - m)) c= (( Carrier l) \/ ( Carrier m)) & (A \/ (B \ A)) = B by A1, XBOOLE_1: 45, ZMODUL02: 40;

          

           A10: ( Carrier l) c= A & ( Carrier m) c= (B \ A) by VECTSP_6:def 4;

          then (( Carrier l) \/ ( Carrier m)) c= (A \/ (B \ A)) by XBOOLE_1: 13;

          then ( Carrier (l - m)) c= B by A9;

          then

          reconsider n = (l - m) as Linear_Combination of B by VECTSP_6:def 4;

          A misses (B \ A) by XBOOLE_1: 79;

          then ( Carrier n) = (( Carrier l) \/ ( Carrier m)) by A10, Th32, XBOOLE_1: 64;

          then ( Carrier l) = {} by A4, A8;

          then l = ( ZeroLC V) by VECTSP_6:def 3;

          then ( Sum l) = ( 0. V) by ZMODUL02: 19;

          hence thesis by A6, ZMODUL02: 66;

        end;

        hence thesis by ZMODUL01: 149;

      end;

      ( (Omega). V) = (( Lin A) + ( Lin (B \ A)))

      proof

        set U = (( Lin A) + ( Lin (B \ A)));

        

         A11: ( [#] V) c= ( [#] U)

        proof

          let v be object;

          assume v in ( [#] V);

          then

          reconsider v as Element of V;

          v in ( Lin B) by A2, ZMODUL03: 14;

          then

          consider l be Linear_Combination of B such that

           A12: v = ( Sum l) by ZMODUL02: 64;

          set n = (l ! (B \ A));

          set m = (l ! A);

          

           A13: l = (m + n) by A1, Th27;

          ex v1,v2 be Element of V st v1 in ( Lin A) & v2 in ( Lin (B \ A)) & v = (v1 + v2)

          proof

            take ( Sum m), ( Sum n);

            thus thesis by A12, A13, ZMODUL02: 52, ZMODUL02: 64;

          end;

          then v in (( Lin A) + ( Lin (B \ A))) by ZMODUL01: 92;

          hence thesis;

        end;

        ( [#] U) = ( [#] V) by A11, VECTSP_4:def 2;

        hence thesis by ZMODUL01: 45;

      end;

      hence thesis by A3, VECTSP_5:def 4;

    end;

    theorem :: ZMODUL05:51

    for R be Ring holds for V,W be LeftMod of R holds for A be Subset of V, l be Linear_Combination of A, T be linear-transformation of V, W, v be Element of V st (T | A) is one-to-one & v in A holds ex X be Subset of V st X misses A & (T " {(T . v)}) = ( {v} \/ X)

    proof

      let R be Ring;

      let V,W be LeftMod of R;

      let A be Subset of V, l be Linear_Combination of A, T be linear-transformation of V, W, v be Element of V such that

       A1: (T | A) is one-to-one and

       A2: v in A;

      set X = ((T " {(T . v)}) \ {v});

      

       A3: X misses A

      proof

        ( dom T) = ( [#] V) by RANKNULL: 7;

        then

         A4: ( dom (T | A)) = A by RELAT_1: 62;

        assume X meets A;

        then

        consider x be object such that

         A5: x in X and

         A6: x in A by XBOOLE_0: 3;

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

        then

         A7: x <> v by TARSKI:def 1;

        x in (T " {(T . v)}) by A5, XBOOLE_0:def 5;

        then (T . x) in {(T . v)} by FUNCT_1:def 7;

        then

         A8: (T . x) = (T . v) by TARSKI:def 1;

        (T . x) = ((T | A) . x) by A6, FUNCT_1: 49;

        then ((T | A) . v) = ((T | A) . x) by A2, A8, FUNCT_1: 49;

        hence contradiction by A1, A2, A4, A6, A7, FUNCT_1:def 4;

      end;

      take X;

       {v} c= (T " {(T . v)})

      proof

        let x be object;

        assume x in {v};

        then

         A9: x = v by TARSKI:def 1;

        ( dom T) = ( [#] V) & (T . v) in {(T . v)} by TARSKI:def 1, RANKNULL: 7;

        hence thesis by A9, FUNCT_1:def 7;

      end;

      hence thesis by A3, XBOOLE_1: 45;

    end;

    theorem :: ZMODUL05:52

    for R be Ring holds for V be LeftMod of R, A be Subset of V, l be Linear_Combination of A holds for X be Subset of V st X misses ( Carrier l) & X <> {} holds (l .: X) = {( 0. R)}

    proof

      let R be Ring;

      let V be LeftMod of R, A be Subset of V;

      let l be Linear_Combination of A;

      let X be Subset of V such that

       A1: X misses ( Carrier l) and

       A2: X <> {} ;

      ( dom l) = ( [#] V) by FUNCT_2: 92;

      hence thesis by A1, A2, Th28, ZFMISC_1: 33;

    end;

    theorem :: ZMODUL05:53

    

     Th36: for R be Ring holds for V,W be LeftMod of R holds for l be Linear_Combination of V, T be linear-transformation of V, W holds for w be Element of W st w in ( Carrier (T @* l)) holds (T " {w}) meets ( Carrier l)

    proof

      let R be Ring;

      let V,W be LeftMod of R;

      let l be Linear_Combination of V, T be linear-transformation of V, W;

      let w be Element of W;

      assume w in ( Carrier (T @* l));

      then

       A1: ((T @* l) . w) <> ( 0. R) by ZMODUL02: 8;

      assume (T " {w}) misses ( Carrier l);

      then ( lCFST (l,T,w)) = ( <*> the carrier of R);

      then ( Sum ( lCFST (l,T,w))) = ( 0. R) by RLVECT_1: 43;

      hence thesis by A1, LDef5;

    end;

    theorem :: ZMODUL05:54

    

     Th37: for R be Ring holds for V,W be LeftMod of R holds for l be Linear_Combination of V, T be linear-transformation of V, W holds for v be Element of V st (T | ( Carrier l)) is one-to-one & v in ( Carrier l) holds ((T @* l) . (T . v)) = (l . v)

    proof

      let R be Ring;

      let V,W be LeftMod of R;

      let l be Linear_Combination of V, T be linear-transformation of V, W;

      let v be Element of V such that

       A1: (T | ( Carrier l)) is one-to-one and

       A2: v in ( Carrier l);

      v in the carrier of V;

      then

       A3: v in ( dom l) by FUNCT_2:def 1;

      

       A4: ( dom T) = the carrier of V by FUNCT_2:def 1;

      for x be object holds x in ((T " {(T . v)}) /\ ( Carrier l)) iff x in {v}

      proof

        let x be object;

        hereby

          assume x in ((T " {(T . v)}) /\ ( Carrier l));

          then

           A5: x in (T " {(T . v)}) & x in ( Carrier l) by XBOOLE_0:def 4;

          then

           A6: x in the carrier of V & (T . x) in {(T . v)} by FUNCT_2: 38;

          

           A7: ((T | ( Carrier l)) . x) = (T . x) by A5, FUNCT_1: 49

          .= (T . v) by A6, TARSKI:def 1

          .= ((T | ( Carrier l)) . v) by A2, FUNCT_1: 49;

          

           A8: x in ( dom (T | ( Carrier l))) by A4, A5, RELAT_1: 57;

          v in ( dom (T | ( Carrier l))) by A2, A4, RELAT_1: 57;

          then x = v by A1, A7, A8, FUNCT_1:def 4;

          hence x in {v} by TARSKI:def 1;

        end;

        assume x in {v};

        then

         A9: x = v by TARSKI:def 1;

        x in the carrier of V & (T . x) in {(T . v)} by A9, TARSKI:def 1;

        then x in (T " {(T . v)}) by FUNCT_2: 38;

        hence thesis by A2, A9, XBOOLE_0:def 4;

      end;

      then ((T " {(T . v)}) /\ ( Carrier l)) = {v} by TARSKI: 2;

      then ( canFS ((T " {(T . v)}) /\ ( Carrier l))) = <*v*> by FINSEQ_1: 94;

      then ( lCFST (l,T,(T . v))) = <*(l . v)*> by A3, FINSEQ_2: 34;

      then ( Sum ( lCFST (l,T,(T . v)))) = (l . v) by RLVECT_1: 44;

      hence thesis by LDef5;

    end;

    theorem :: ZMODUL05:55

    

     Th38: for R be Ring holds for V,W be LeftMod of R holds for l be Linear_Combination of V, T be linear-transformation of V, W holds for G be FinSequence of V st ( rng G) = ( Carrier l) & (T | ( Carrier l)) is one-to-one holds (T * (l (#) G)) = ((T @* l) (#) (T * G))

    proof

      let R be Ring;

      let V,W be LeftMod of R;

      let l be Linear_Combination of V, T be linear-transformation of V, W;

      let G be FinSequence of V such that

       A1: ( rng G) = ( Carrier l) and

       A2: (T | ( Carrier l)) is one-to-one;

      reconsider R = ((T @* l) (#) (T * G)) as FinSequence of W;

      reconsider L = (T * (l (#) G)) as FinSequence of W;

      

       A3: ( len R) = ( len (T * G)) by VECTSP_6:def 5

      .= ( len G) by FINSEQ_2: 33;

      

       A4: ( len L) = ( len (l (#) G)) by FINSEQ_2: 33

      .= ( len G) by VECTSP_6:def 5;

      for k be Nat st 1 <= k & k <= ( len L) holds (L . k) = (R . k)

      proof

        

         A5: ( dom R) = ( Seg ( len G)) by A3, FINSEQ_1:def 3;

        let k be Nat such that

         A6: 1 <= k & k <= ( len L);

        reconsider gk = (G /. k) as Element of V;

        ( len (l (#) G)) = ( len G) by VECTSP_6:def 5;

        then

         A7: ( dom (l (#) G)) = ( Seg ( len G)) by FINSEQ_1:def 3;

        

         A8: k in ( dom (l (#) G)) by A4, A6, A7;

        then

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

        then

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

        then

        reconsider Gk = (G . k) as Element of V;

        ((T * G) . k) = (T . Gk) by A9, FUNCT_1: 13;

        then

        reconsider TGk = ((T * G) . k) as Element of W;

        ((l (#) G) . k) = ((l . gk) * gk) by A8, VECTSP_6:def 5;

        

        then

         A11: (L . k) = (T . ((l . gk) * gk)) by A8, FUNCT_1: 13

        .= ((l . gk) * (T . gk)) by MOD_2:def 2

        .= ((l . Gk) * TGk) by A9, A10, FUNCT_1: 13;

        (G . k) in ( rng G) & ((T * G) . k) = (T . (G . k)) by A9, FUNCT_1: 3, FUNCT_1: 13;

        then

         A12: ((T @* l) . ((T * G) . k)) = (l . (G . k)) by A1, A2, Th37;

        ( dom T) = ( [#] V) by RANKNULL: 7;

        then ( dom (T * G)) = ( dom G) by A1, RELAT_1: 27;

        then ((T * G) /. k) = ((T * G) . k) by A9, PARTFUN1:def 6;

        hence thesis by A5, A7, A8, A11, A12, VECTSP_6:def 5;

      end;

      hence thesis by A3, A4;

    end;

    theorem :: ZMODUL05:56

    

     Th39: for R be Ring holds for V,W be LeftMod of R holds for l be Linear_Combination of V, T be linear-transformation of V, W holds (T | ( Carrier l)) is one-to-one implies (T .: ( Carrier l)) = ( Carrier (T @* l))

    proof

      let R be Ring;

      let V,W be LeftMod of R;

      let l be Linear_Combination of V, T be linear-transformation of V, W;

      assume

       A1: (T | ( Carrier l)) is one-to-one;

      

       A2: (T .: ( Carrier l)) c= ( Carrier (T @* l))

      proof

        let w be object;

        assume w in (T .: ( Carrier l));

        then

        consider v be object such that

         A3: v in ( dom T) and

         A4: v in ( Carrier l) and

         A5: (T . v) = w by FUNCT_1:def 6;

        reconsider v as Element of V by A3;

        ((T @* l) . (T . v)) = (l . v) & (l . v) <> ( 0. R) by A1, A4, Th37, ZMODUL02: 8;

        hence thesis by A5;

      end;

      thus thesis by LDef5, A2;

    end;

    theorem :: ZMODUL05:57

    for V be finite-rank free Z_Module, A be Subset of V, B be Basis of V, T be linear-transformation of V, W, l be Linear_Combination of (B \ A) st A is Basis of ( ker T) & A c= B holds (T . ( Sum l)) = ( Sum (T @* l))

    proof

      let V be finite-rank free Z_Module, A be Subset of V, B be Basis of V, T be linear-transformation of V, W, l be Linear_Combination of (B \ A);

      assume A is Basis of ( ker T) & A c= B;

      then

       A1: (T | (B \ A)) is one-to-one by Th22;

      

       A2: ((T | (B \ A)) | ( Carrier l)) = (T | ( Carrier l)) by RELAT_1: 74, VECTSP_6:def 4;

      then

       A3: (T | ( Carrier l)) is one-to-one by A1, FUNCT_1: 52;

      consider G be FinSequence of V such that

       A4: G is one-to-one and

       A5: ( rng G) = ( Carrier l) and

       A6: ( Sum l) = ( Sum (l (#) G)) by VECTSP_6:def 6;

      set H = (T * G);

      reconsider H as FinSequence of W;

      

       A7: ( rng H) = (T .: ( Carrier l)) by A5, RELAT_1: 127

      .= ( Carrier (T @* l)) by A3, Th39;

      ( dom T) = ( [#] V) by RANKNULL: 7;

      then H is one-to-one by A1, A2, A4, A5, FUNCT_1: 52, RANKNULL: 1;

      then

       A8: ( Sum (T @* l)) = ( Sum ((T @* l) (#) H)) by A7, VECTSP_6:def 6;

      (T * (l (#) G)) = ((T @* l) (#) H) by A3, A5, Th38;

      hence thesis by A6, A8, MATRLIN16;

    end;

    theorem :: ZMODUL05:58

    for X be Subset of V st X is linearly-dependent holds ex l be Linear_Combination of X st ( Carrier l) <> {} & ( Sum l) = ( 0. V);

    definition

      let R be Ring;

      let V,W be LeftMod of R, X be Subset of V, T be linear-transformation of V, W, l be Linear_Combination of (T .: X);

      assume

       A1: (T | X) is one-to-one;

      :: ZMODUL05:def9

      func T # l -> Linear_Combination of X equals

      : Def6: ((l * T) +* ((X ` ) --> ( 0. R)));

      coherence

      proof

        reconsider SZ0 = {( 0. R)} as finite Subset of R;

        ( dom l) = ( [#] W) by FUNCT_2: 92;

        then ( rng T) c= ( dom l);

        then

         A3: ( dom (l * T)) = ( dom T) by RELAT_1: 27;

        set f = ((l * T) +* ((X ` ) --> ( 0. R)));

        

         A4: ( dom ((X ` ) --> ( 0. R))) = (X ` );

        ( rng f) c= (( rng (l * T)) \/ ( rng ((X ` ) --> ( 0. R)))) & (( rng (l * T)) \/ ( rng ((X ` ) --> ( 0. R)))) c= the carrier of R by FUNCT_4: 17;

        then

         A5: ( rng f) c= the carrier of R;

        ( dom T) = ( [#] V) & (( [#] V) \/ (( [#] V) \ X)) = ( [#] V) by RANKNULL: 7, XBOOLE_1: 12;

        then ( dom f) = ( [#] V) by A3, A4, FUNCT_4:def 1;

        then

        reconsider f as Element of ( Funcs (( [#] V),the carrier of R)) by A5, FUNCT_2:def 2;

        ex T be finite Subset of V st for v be Element of V st not v in T holds (f . v) = ( 0. R)

        proof

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

          C c= ( [#] V)

          proof

            let x be object;

            assume x in C;

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

            hence thesis;

          end;

          then

          reconsider C as Subset of V;

          ex g be Function st g is one-to-one & ( dom g) = C & ( rng g) c= ( Carrier l)

          proof

            set S = ((T " ( Carrier l)) /\ X);

            set g = (T | S);

            take g;

            

             A6: C c= S

            proof

              let x be object such that

               A7: x in C;

              

               A8: ex v be Element of V st v = x & (f . v) <> ( 0. R) by A7;

              reconsider x as Element of V by A7;

               A9:

              now

                assume not x in X;

                then

                 A10: x in (X ` ) by XBOOLE_0:def 5;

                then x in ( dom ((X ` ) --> ( 0. R)));

                then (f . x) = (((X ` ) --> ( 0. R)) . x) by FUNCT_4: 13;

                hence contradiction by A8, A10, FUNCOP_1: 7;

              end;

              then not x in (X ` ) by XBOOLE_0:def 5;

              then

               A11: (f . x) = ((l * T) . x) by A4, FUNCT_4: 11;

              

               A12: ( dom T) = ( [#] V) by RANKNULL: 7;

              then ((l * T) . x) = (l . (T . x)) by FUNCT_1: 13;

              then (T . x) in ( Carrier l) by A8, A11;

              then x in (T " ( Carrier l)) by A12, FUNCT_1:def 7;

              hence thesis by A9, XBOOLE_0:def 4;

            end;

            

             A13: ( dom T) = ( [#] V) by RANKNULL: 7;

            

             A14: ( rng g) c= ( Carrier l)

            proof

              let y be object;

              assume y in ( rng g);

              then

              consider x be object such that

               A15: x in ( dom g) and

               A16: y = (g . x) by FUNCT_1:def 3;

              x in (T " ( Carrier l)) by A15, XBOOLE_0:def 4;

              then (T . x) in ( Carrier l) by FUNCT_1:def 7;

              hence thesis by A15, A16, FUNCT_1: 49;

            end;

            S c= C

            proof

              let x be object such that

               A17: x in S;

              

               A18: x in X by A17, XBOOLE_0:def 4;

              

               A19: x in (T " ( Carrier l)) by A17, XBOOLE_0:def 4;

              then

               A20: x in ( dom T) by FUNCT_1:def 7;

              

               A21: (T . x) in ( Carrier l) by A19, FUNCT_1:def 7;

              reconsider x as Element of V by A17;

              

               A22: (l . (T . x)) <> ( 0. R) by A21, ZMODUL02: 8;

               not x in ( dom ((X ` ) --> ( 0. R))) by A18, XBOOLE_0:def 5;

              then

               A23: (f . x) = ((l * T) . x) by FUNCT_4: 11;

              ((l * T) . x) = (l . (T . x)) by A20, FUNCT_1: 13;

              hence thesis by A22, A23;

            end;

            hence thesis by A1, A6, A13, A14, RANKNULL: 2, RELAT_1: 62, XBOOLE_1: 17;

          end;

          then ( card C) c= ( card ( Carrier l)) by CARD_1: 10;

          then

          reconsider C as finite Subset of V;

          take C;

          thus thesis;

        end;

        then

        reconsider f as Linear_Combination of V by VECTSP_6:def 1;

        ( Carrier f) c= X

        proof

          let x be object such that

           A24: x in ( Carrier f);

          reconsider x as Element of V by A24;

          now

            assume not x in X;

            then

             A25: x in (X ` ) by XBOOLE_0:def 5;

            

            then (f . x) = (((X ` ) --> ( 0. R)) . x) by A4, FUNCT_4: 13

            .= ( 0. R) by A25, FUNCOP_1: 7;

            hence contradiction by A24, ZMODUL02: 8;

          end;

          hence thesis;

        end;

        hence thesis by VECTSP_6:def 4;

      end;

    end

    theorem :: ZMODUL05:59

    

     Th42: for R be Ring holds for V,W be LeftMod of R, X be Subset of V, T be linear-transformation of V, W holds for X be Subset of V, l be Linear_Combination of (T .: X), v be Element of V st v in X & (T | X) is one-to-one holds ((T # l) . v) = (l . (T . v))

    proof

      let R be Ring;

      let V,W be LeftMod of R, X be Subset of V, T be linear-transformation of V, W;

      let X be Subset of V, l be Linear_Combination of (T .: X);

      let v be Element of V;

      assume v in X & (T | X) is one-to-one;

      then not v in ( dom ((X ` ) --> ( 0. R))) & (T # l) = ((l * T) +* ((X ` ) --> ( 0. R))) by Def6, XBOOLE_0:def 5;

      then

       A1: ((T # l) . v) = ((l * T) . v) by FUNCT_4: 11;

      ( dom T) = ( [#] V) by RANKNULL: 7;

      hence thesis by A1, FUNCT_1: 13;

    end;

    theorem :: ZMODUL05:60

    for R be Ring holds for V,W be LeftMod of R, X be Subset of V, T be linear-transformation of V, W, X be Subset of V, l be Linear_Combination of (T .: X) st (T | X) is one-to-one holds (T @* (T # l)) = l

    proof

      let R be Ring;

      let V,W be LeftMod of R, X be Subset of V, T be linear-transformation of V, W;

      let X be Subset of V, l be Linear_Combination of (T .: X) such that

       A1: (T | X) is one-to-one;

      let w be Element of W;

      set m = (T @* (T # l));

      reconsider SZ0 = {( 0. R)} as finite Subset of R;

      per cases ;

        suppose

         A2: w in ( Carrier l);

        ( Carrier l) c= (T .: X) by VECTSP_6:def 4;

        then

        consider v be object such that

         A3: v in ( dom T) and

         A4: v in X and

         A5: w = (T . v) by A2, FUNCT_1:def 6;

        reconsider v as Element of V by A3;

        w in the carrier of W;

        then

         A6: w in ( dom l) by FUNCT_2:def 1;

        

         A7: v in the carrier of V;

        for x be object holds x in ((T " {w}) /\ ( Carrier (T # l))) iff x in ( {v} /\ ( Carrier (T # l)))

        proof

          let x be object;

          hereby

            assume

             A8: x in ((T " {w}) /\ ( Carrier (T # l)));

            then

             A9: x in (T " {w}) & x in ( Carrier (T # l)) by XBOOLE_0:def 4;

            then

             A10: x in X by TARSKI:def 3, VECTSP_6:def 4;

            x in the carrier of V by A8;

            then

             A11: x in ( dom T) by FUNCT_2:def 1;

            

             A12: x in the carrier of V & (T . x) in {w} by A9, FUNCT_2: 38;

            

             A13: ((T | X) . x) = (T . x) by A10, FUNCT_1: 49

            .= (T . v) by A5, A12, TARSKI:def 1

            .= ((T | X) . v) by A4, FUNCT_1: 49;

            

             A14: x in ( dom (T | X)) by A10, A11, RELAT_1: 57;

            v in ( dom (T | X)) by A3, A4, RELAT_1: 57;

            then x = v by A1, A13, A14, FUNCT_1:def 4;

            then x in {v} by TARSKI:def 1;

            hence x in ( {v} /\ ( Carrier (T # l))) by A9, XBOOLE_0:def 4;

          end;

          assume x in ( {v} /\ ( Carrier (T # l)));

          then

           A15: x in {v} & x in ( Carrier (T # l)) by XBOOLE_0:def 4;

          then

           A16: x = v by TARSKI:def 1;

          x in the carrier of V & (T . x) in {w} by A5, A16, TARSKI:def 1;

          then x in (T " {w}) by FUNCT_2: 38;

          hence x in ((T " {w}) /\ ( Carrier (T # l))) by A15, XBOOLE_0:def 4;

        end;

        then

         A17: ((T " {w}) /\ ( Carrier (T # l))) = ( {v} /\ ( Carrier (T # l))) by TARSKI: 2;

        per cases ;

          suppose

           A18: not v in ( Carrier (T # l));

          ( {v} /\ ( Carrier (T # l))) = {}

          proof

            assume ( {v} /\ ( Carrier (T # l))) <> {} ;

            then

            consider x be object such that

             A19: x in ( {v} /\ ( Carrier (T # l))) by XBOOLE_0:def 1;

            

             A20: x in {v} by A19, XBOOLE_0:def 4;

            x in ( Carrier (T # l)) by A19, XBOOLE_0:def 4;

            hence contradiction by A18, A20, TARSKI:def 1;

          end;

          then

           b1: ( lCFST ((T # l),T,w)) = ( <*> the carrier of R) by A17;

          ((T @* (T # l)) . w) = ( Sum ( lCFST ((T # l),T,w))) by LDef5;

          then

           A21: ((T @* (T # l)) . w) = ( 0. R) by RLVECT_1: 43, b1;

          

           A22: ((T # l) . v) = ( 0. R) by A18;

          

           A23: not v in ( dom ((X ` ) --> ( 0. R))) by A4, XBOOLE_0:def 5;

          (T # l) = ((l * T) +* ((X ` ) --> ( 0. R))) by A1, Def6;

          then ((T # l) . v) = ((l * T) . v) by A23, FUNCT_4: 11;

          hence ((T @* (T # l)) . w) = (l . w) by A3, A5, A21, A22, FUNCT_1: 13;

        end;

          suppose v in ( Carrier (T # l));

          then ((T " {w}) /\ ( Carrier (T # l))) = {v} by A17, XBOOLE_1: 28, ZFMISC_1: 31;

          then

           A24: ( canFS ((T " {w}) /\ ( Carrier (T # l)))) = <*v*> by FINSEQ_1: 94;

          

           A25: not v in ( dom ((X ` ) --> ( 0. R))) by A4, XBOOLE_0:def 5;

          

           A26: (T # l) = ((l * T) +* ((X ` ) --> ( 0. R))) by A1, Def6;

          

           A27: v in ( dom (T # l)) by A7, FUNCT_2:def 1;

          

           A28: v in ( dom (l * T)) by A7, FUNCT_2:def 1;

          ((T # l) * <*v*>) = <*((T # l) . v)*> by A27, FINSEQ_2: 34

          .= <*((l * T) . v)*> by A25, A26, FUNCT_4: 11

          .= ((l * T) * <*v*>) by A28, FINSEQ_2: 34

          .= (l * (T * <*v*>)) by RELAT_1: 36

          .= (l * <*(T . v)*>) by A3, FINSEQ_2: 34

          .= <*(l . w)*> by A5, A6, FINSEQ_2: 34;

          then ( Sum ( lCFST ((T # l),T,w))) = (l . w) by A24, RLVECT_1: 44;

          hence (m . w) = (l . w) by LDef5;

        end;

      end;

        suppose

         A29: not w in ( Carrier l);

        then

         A30: (l . w) = ( 0. R);

        now

          assume

           A31: (m . w) <> ( 0. R);

          then w in ( Carrier m);

          then

          consider v be Element of V such that

           A32: v in (T " {w}) and

           A33: v in ( Carrier (T # l)) by RANKNULL: 3, Th36;

          (T . v) in {w} by A32, FUNCT_1:def 7;

          then

           A34: (T . v) = w by TARSKI:def 1;

          

           A35: ( Carrier (T # l)) c= X by VECTSP_6:def 4;

          (T | ( Carrier (T # l))) is one-to-one by A1, RANKNULL: 2, VECTSP_6:def 4;

          

          then (m . w) = ((T # l) . v) by A33, A34, Th37

          .= ( 0. R) by A1, A30, A33, A34, A35, Th42;

          hence contradiction by A31;

        end;

        hence thesis by A29;

      end;

    end;