zmodul03.miz



    begin

    reserve x,y,y1,y2 for set;

    reserve V for Z_Module;

    reserve u,v,w for Vector of V;

    reserve F,G,H,I for FinSequence of V;

    reserve W,W1,W2,W3 for Submodule of V;

    registration

      cluster non trivial for Z_Module;

      correctness

      proof

        set AG = INT.Ring ;

        set G = ModuleStr (# the carrier of AG, the addF of AG, the ZeroF of AG, ( Int-mult-left AG) #);

        

         A1: G is Z_Module by ZMODUL01: 164;

        G is non trivial;

        hence thesis by A1;

      end;

    end

    registration

      let V be Z_Module;

      cluster linearly-independent for finite Subset of V;

      correctness

      proof

        reconsider W = ( {} the carrier of V) as finite Subset of V;

        take W;

        thus W is linearly-independent;

      end;

    end

    theorem :: ZMODUL03:1

    

     Th1: for u be Vector of V holds ex l be Linear_Combination of V st (l . u) = 1 & for v be Vector of V st v <> u holds (l . v) = 0

    proof

      let u be Element of V;

      reconsider i0 = 0 as Element of INT by INT_1:def 2;

      deffunc F( Element of V) = i0;

      reconsider i1 = 1 as Element of INT by INT_1:def 2;

      ex f be Function of the carrier of V, INT st (f . u) = i1 & for v be Element of V st v <> u holds (f . v) = F(v) from FUNCT_2:sch 6;

      then

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

       A1: (f . u) = 1 and

       A2: for v be Element of V st v <> u holds (f . v) = 0 ;

      for v be Element of V holds not v in {u} implies v <> u by TARSKI:def 1;

      then

       A3: for v be Element of V holds not v in {u} implies (f . v) = ( 0. INT.Ring ) by A2;

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

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

      take f;

      thus thesis by A1, A2;

    end;

    

     Lm1: for r be Element of INT.Ring , n be Element of NAT , i be Integer st i = n holds (i * r) = (n * r)

    proof

      let r be Element of INT.Ring ;

      defpred P[ Nat] means for i be Integer st i = $1 holds (i * r) = ($1 * r);

      reconsider rr = r as Integer;

      

       A1: ( 0. INT.Ring ) = 0 ;

      

       A2: P[ 0 ] by A1, BINOM: 12;

      

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

      proof

        let n be Nat;

        assume

         A4: P[n];

        now

          let i be Integer;

          assume

           A5: i = (n + 1);

          reconsider Kn = n, K1 = 1 as Integer;

          reconsider n1 = 1 as Element of NAT ;

          

           A6: (K1 * r) = (n1 * r) by BINOM: 13;

          

          thus (i * r) = ((Kn * r) + (K1 * r)) by A5

          .= ((n * r) + (n1 * r)) by A4, A6

          .= ((n + 1) * r) by BINOM: 15;

        end;

        hence P[(n + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: ZMODUL03:2

    

     Th2: for G be Z_Module, i be Element of INT.Ring , w be Element of INT , v be Element of G st G = ModuleStr (# the carrier of INT.Ring , the addF of INT.Ring , the ZeroF of INT.Ring , ( Int-mult-left INT.Ring ) #) & v = w holds (i * v) = (i * w)

    proof

      let G be Z_Module, i be Element of INT.Ring , w be Element of INT , v be Element of G;

      assume

       A1: G = ModuleStr (# the carrier of INT.Ring , the addF of INT.Ring , the ZeroF of INT.Ring , ( Int-mult-left INT.Ring ) #) & v = w;

      reconsider r = v as Element of INT.Ring by A1;

      per cases ;

        suppose 0 <= i;

        then

        reconsider n = i as Element of NAT by INT_1: 3;

        

        thus (i * v) = (n * r) by A1, ZMODUL01:def 20

        .= (i * w) by A1, Lm1;

      end;

        suppose

         A2: not 0 <= i;

        then

        reconsider n = ( - i) as Element of NAT by INT_1: 3;

        

        thus (i * v) = (n * ( - r)) by A1, A2, ZMODUL01:def 20

        .= (( - i) * ( - r)) by Lm1

        .= (i * w) by A1;

      end;

    end;

    definition

      ::$Canceled

    end

    registration

      let V;

      cluster ( (0). V) -> free;

      coherence by MOD_3: 14;

    end

    registration

      cluster strict free for Z_Module;

      existence

      proof

        take ( (0). the Z_Module);

        thus thesis;

      end;

    end

    registration

      let V be Z_Module;

      cluster strict free for Submodule of V;

      existence

      proof

        take ( (0). V);

        thus thesis;

      end;

    end

    registration

      let V be free Z_Module;

      cluster base for Subset of V;

      existence by VECTSP_7:def 4;

    end

    definition

      let V be free Z_Module;

      mode Basis of V is base Subset of V;

      ::$Canceled

    end

    registration

      cluster -> Mult-cancelable for free Z_Module;

      coherence

      proof

        let V be free Z_Module;

        set I = the Basis of V;

        assume

         A1: not V is Mult-cancelable;

        consider a be Element of INT.Ring , v be Vector of V such that

         A2: (a * v) = ( 0. V) & a <> ( 0. INT.Ring ) & v <> ( 0. V) by A1;

        I is base;

        then I is linearly-independent & ( Lin I) = the ModuleStr of V;

        then

        consider lv be Linear_Combination of I such that

         A3: v = ( Sum lv) by STRUCT_0:def 5, ZMODUL02: 64;

        ( Carrier lv) <> {} by A2, A3, ZMODUL02: 23;

        then

         A4: ( Carrier (a * lv)) <> {} by A2, ZMODUL02: 29;

        

         A5: (a * lv) is Linear_Combination of I by ZMODUL02: 31;

        ( Sum (a * lv)) = ( 0. V) by A2, A3, ZMODUL02: 53;

        hence contradiction by A4, A5, VECTSP_7:def 3, VECTSP_7:def 1;

      end;

    end

    registration

      cluster free for non trivial Z_Module;

      correctness

      proof

        set AG = INT.Ring ;

        set G = ModuleStr (# the carrier of AG, the addF of AG, the ZeroF of AG, ( Int-mult-left AG) #);

        reconsider G as non trivial Z_Module by ZMODUL01: 164;

        reconsider iv = 1 as Vector of G;

        reconsider i1 = 1 as Element of INT by INT_1:def 2;

        set I = {iv};

        reconsider I as Subset of G;

        for a be Element of INT.Ring holds for v be Vector of G st (a * v) = ( 0. G) holds a = ( 0. INT.Ring ) or v = ( 0. G)

        proof

          let a be Element of INT.Ring , v be Vector of G;

          assume

           A1: (a * v) = ( 0. G);

          reconsider w = v as Element of INT ;

          (a * w) = 0 by A1, Th2;

          hence a = ( 0. INT.Ring ) or v = ( 0. G) by XCMPLX_1: 6;

        end;

        then G is Mult-cancelable;

        then

         A3: I is linearly-independent by ZMODUL02: 59;

        for x be object holds x in the carrier of ( Lin I) iff x in the carrier of G

        proof

          let x be object;

          hereby

            assume

             A4: x in the carrier of ( Lin I);

            the carrier of ( Lin I) c= the carrier of G by VECTSP_4:def 2;

            hence x in the carrier of G by A4;

          end;

          assume x in the carrier of G;

          then

          reconsider v0 = x as Vector of G;

          reconsider w = v0 as Element of INT.Ring ;

          reconsider a = w as Integer;

          reconsider i0 = 0 as Element of INT.Ring ;

          deffunc G( Vector of G) = ( 0. INT.Ring );

          deffunc L0( Vector of G) = w;

          consider g be Function of G, INT.Ring such that

           A5: (g . iv) = w and

           A6: for u be Vector of G st u <> iv holds (g . u) = G(u) from FUNCT_2:sch 6;

          reconsider g as Element of ( Funcs (the carrier of G,the carrier of INT.Ring )) by FUNCT_2: 8;

          now

            let u be Vector of G;

            assume not u in {iv};

            then u <> iv by TARSKI:def 1;

            hence (g . u) = ( 0. INT.Ring ) by A6;

          end;

          then

          reconsider g as Linear_Combination of G by VECTSP_6:def 1;

          ( Carrier g) c= {iv}

          proof

            let x be object;

            assume x in ( Carrier g);

            then ex u be Vector of G st x = u & (g . u) <> 0 ;

            then x = iv by A6;

            hence thesis by TARSKI:def 1;

          end;

          then

          reconsider g as Linear_Combination of {iv} by VECTSP_6:def 4;

          ( Sum g) = (w * iv) by A5, ZMODUL02: 21

          .= (w * i1) by Th2

          .= v0;

          hence x in the carrier of ( Lin I) by STRUCT_0:def 5, ZMODUL02: 64;

        end;

        then ( Lin I) = the ModuleStr of G by TARSKI: 2, ZMODUL01: 47;

        then ex I be Subset of G st I is base by A3, VECTSP_7:def 3;

        then G is free;

        hence thesis;

      end;

    end

    reserve KL1,KL2 for Linear_Combination of V;

    reserve X for Subset of V;

    theorem :: ZMODUL03:3

    

     Th3: X is linearly-independent & ( Carrier KL1) c= X & ( Carrier KL2) c= X & ( Sum KL1) = ( Sum KL2) implies KL1 = KL2

    proof

      assume

       A1: X is linearly-independent;

      assume

       A2: ( Carrier KL1) c= X;

      assume ( Carrier KL2) c= X;

      then

       A3: (( Carrier KL1) \/ ( Carrier KL2)) c= X by A2, XBOOLE_1: 8;

      assume ( Sum KL1) = ( Sum KL2);

      then (( Sum KL1) - ( Sum KL2)) = ( 0. V) by RLVECT_1: 5;

      then

       A4: (KL1 - KL2) is Linear_Combination of ( Carrier (KL1 - KL2)) & ( Sum (KL1 - KL2)) = ( 0. V) by ZMODUL02: 55, VECTSP_6:def 4;

      ( Carrier (KL1 - KL2)) c= (( Carrier KL1) \/ ( Carrier KL2)) by ZMODUL02: 40;

      then

       A5: ( Carrier (KL1 - KL2)) is linearly-independent by A1, A3, XBOOLE_1: 1, ZMODUL02: 56;

      now

        let v be Vector of V;

         not v in ( Carrier (KL1 - KL2)) by A5, A4;

        then ((KL1 - KL2) . v) = 0 ;

        then ((KL1 . v) - (KL2 . v)) = 0 by ZMODUL02: 39;

        hence (KL1 . v) = (KL2 . v);

      end;

      hence thesis;

    end;

    theorem :: ZMODUL03:4

    for V be free Z_Module, A be Subset of V st A is linearly-independent holds ex B be Subset of V st A c= B & B is linearly-independent & (for v be Vector of V holds ex a be Element of INT.Ring st (a * v) in ( Lin B))

    proof

      let V be free Z_Module, A be Subset of V such that

       A1: A is linearly-independent;

      defpred P[ set] means ex B be Subset of V st B = $1 & A c= B & B is linearly-independent;

      consider Q be set such that

       A2: for Z be set holds Z in Q iff Z in ( bool the carrier of V) & P[Z] from XFAMILY:sch 1;

       A3:

      now

        let Z be set;

        assume that

         A4: Z <> {} and

         A5: Z c= Q and

         A6: Z is c=-linear;

        set W = ( union Z);

        W c= the carrier of V

        proof

          let x be object;

          assume x in W;

          then

          consider X be set such that

           A7: x in X and

           A8: X in Z by TARSKI:def 4;

          X in ( bool the carrier of V) by A2, A5, A8;

          hence thesis by A7;

        end;

        then

        reconsider W as Subset of V;

        

         A9: W is linearly-independent

        proof

          deffunc Q( object) = { C where C be Subset of V : $1 in C & C in Z };

          let l be Linear_Combination of W;

          assume that

           A10: ( Sum l) = ( 0. V) and

           A11: ( Carrier l) <> {} ;

          consider f be Function such that

           A12: ( dom f) = ( Carrier l) and

           A13: for x be object st x in ( Carrier l) holds (f . x) = Q(x) from FUNCT_1:sch 3;

          reconsider M = ( rng f) as non empty set by A11, A12, RELAT_1: 42;

          set F = the Choice_Function of M;

          set S = ( rng F);

           A14:

          now

            assume {} in M;

            then

            consider x be object such that

             A15: x in ( dom f) and

             A16: (f . x) = {} by FUNCT_1:def 3;

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

            then

            consider X be set such that

             A17: x in X and

             A18: X in Z by A12, A15, TARSKI:def 4;

            reconsider X as Subset of V by A2, A5, A18;

            X in { C where C be Subset of V : x in C & C in Z } by A17, A18;

            hence contradiction by A12, A13, A15, A16;

          end;

          then

           A19: ( dom F) = M by RLVECT_3: 28;

          then ( dom F) is finite by A12, FINSET_1: 8;

          then

           A20: S is finite by FINSET_1: 8;

           A21:

          now

            let X be set;

            assume X in S;

            then

            consider x be object such that

             A22: x in ( dom F) and

             A23: (F . x) = X by FUNCT_1:def 3;

            consider y be object such that

             A24: y in ( dom f) & (f . y) = x by A22, FUNCT_1:def 3;

            reconsider x as set by TARSKI: 1;

            

             A25: x = Q(y) by A12, A13, A24;

            X in x by A14, A22, A23, ORDERS_1: 89;

            then ex C be Subset of V st C = X & y in C & C in Z by A25;

            hence X in Z;

          end;

           A26:

          now

            let X,Y be set;

            assume X in S & Y in S;

            then X in Z & Y in Z by A21;

            hence X c= Y or Y c= X by A6, ORDINAL1:def 8, XBOOLE_0:def 9;

          end;

          S <> {} by A19, RELAT_1: 42;

          then ( union S) in Z by A20, A21, A26, CARD_2: 62;

          then

          consider B be Subset of V such that

           A27: B = ( union S) and A c= B and

           A28: B is linearly-independent by A2, A5;

          ( Carrier l) c= ( union S)

          proof

            let x be object;

            set X = (f . x);

            assume

             A29: x in ( Carrier l);

            then

             A30: (f . x) = { C where C be Subset of V : x in C & C in Z } by A13;

            

             A31: (f . x) in M by A12, A29, FUNCT_1:def 3;

            then (F . X) in X by A14, ORDERS_1: 89;

            then

             A32: ex C be Subset of V st (F . X) = C & x in C & C in Z by A30;

            (F . X) in S by A19, A31, FUNCT_1:def 3;

            hence thesis by A32, TARSKI:def 4;

          end;

          then l is Linear_Combination of B by A27, VECTSP_6:def 4;

          hence thesis by A10, A11, A28;

        end;

        set x = the Element of Z;

        x in Q by A4, A5;

        then

         A33: ex B be Subset of V st B = x & A c= B & B is linearly-independent by A2;

        x c= W by A4, ZFMISC_1: 74;

        hence ( union Z) in Q by A2, A9, A33, XBOOLE_1: 1;

      end;

      Q <> {} by A1, A2;

      then

      consider X be set such that

       A34: X in Q and

       A35: for Z be set st Z in Q & Z <> X holds not X c= Z by A3, ORDERS_1: 67;

      consider B be Subset of V such that

       A36: B = X and

       A37: A c= B and

       A38: B is linearly-independent by A2, A34;

      take B;

      thus A c= B & B is linearly-independent by A37, A38;

      assume not for v be Vector of V holds ex a be Element of INT.Ring st (a * v) in ( Lin B);

      then

      consider v be Vector of V such that

       A39: for a be Element of INT.Ring holds not (a * v) in ( Lin B);

      

       A40: (B \/ {v}) is linearly-independent

      proof

        let l be Linear_Combination of (B \/ {v});

        assume

         A41: ( Sum l) = ( 0. V);

        now

          per cases ;

            suppose v in ( Carrier l);

            reconsider i0 = 0 as Element of INT.Ring ;

            deffunc G( Vector of V) = ( 0. INT.Ring );

            deffunc L( Vector of V) = (l . $1);

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

             A42: (f . v) = i0 and

             A43: for u be Vector of V st u <> v holds (f . u) = L(u) from FUNCT_2:sch 6;

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

            now

              let u be Vector of V;

              assume not u in (( Carrier l) \ {v});

              then not u in ( Carrier l) or u in {v} by XBOOLE_0:def 5;

              then (l . u) = 0 & u <> v or u = v by TARSKI:def 1;

              hence (f . u) = 0 by A42, A43;

            end;

            then

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

            ( Carrier f) c= B

            proof

              let x be object;

              

               A44: ( Carrier l) c= (B \/ {v}) by VECTSP_6:def 4;

              assume x in ( Carrier f);

              then

              consider u be Vector of V such that

               A45: u = x and

               A46: (f . u) <> 0 ;

              (f . u) = (l . u) by A42, A43, A46;

              then u in ( Carrier l) by A46;

              then u in B or u in {v} by A44, XBOOLE_0:def 3;

              hence thesis by A42, A45, A46, TARSKI:def 1;

            end;

            then

            reconsider f as Linear_Combination of B by VECTSP_6:def 4;

            reconsider lv = ( - (l . v)) as Element of INT.Ring ;

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

             A47: (g . v) = lv and

             A48: for u be Vector of V st u <> v holds (g . u) = G(u) from FUNCT_2:sch 6;

            reconsider g as Element of ( Funcs (the carrier of V,the carrier of INT.Ring )) by FUNCT_2: 8;

            now

              let u be Vector of V;

              assume not u in {v};

              then u <> v by TARSKI:def 1;

              hence (g . u) = ( 0. INT.Ring ) by A48;

            end;

            then

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

            ( Carrier g) c= {v}

            proof

              let x be object;

              assume x in ( Carrier g);

              then ex u be Vector of V st x = u & (g . u) <> 0 ;

              then x = v by A48;

              hence thesis by TARSKI:def 1;

            end;

            then

            reconsider g as Linear_Combination of {v} by VECTSP_6:def 4;

            

             A49: ( Sum g) = (( - (l . v)) * v) by A47, ZMODUL02: 21;

            (f - g) = l

            proof

              let u be Vector of V;

              now

                per cases ;

                  suppose

                   A50: v = u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by ZMODUL02: 39

                  .= (l . u) by A42, A47, A50;

                end;

                  suppose

                   A51: v <> u;

                  

                  thus ((f - g) . u) = ((f . u) - (g . u)) by ZMODUL02: 39

                  .= ((l . u) - (g . u)) by A43, A51

                  .= ((l . u) - ( 0. INT.Ring )) by A48, A51

                  .= (l . u);

                end;

              end;

              hence thesis;

            end;

            then ( 0. V) = (( Sum f) - ( Sum g)) by A41, ZMODUL02: 55;

            

            then ( Sum f) = (( 0. V) + ( Sum g)) by RLSUB_2: 61

            .= (( - (l . v)) * v) by A49, RLVECT_1: 4;

            hence thesis by A39, ZMODUL02: 64;

          end;

            suppose

             A52: not v in ( Carrier l);

            ( Carrier l) c= B

            proof

              let x be object;

              assume

               A53: x in ( Carrier l);

              ( Carrier l) c= (B \/ {v}) by VECTSP_6:def 4;

              then x in B or x in {v} by A53, XBOOLE_0:def 3;

              hence thesis by A52, A53, TARSKI:def 1;

            end;

            then l is Linear_Combination of B by VECTSP_6:def 4;

            hence thesis by A38, A41;

          end;

        end;

        hence thesis;

      end;

      v in {v} by TARSKI:def 1;

      then

       A54: v in (B \/ {v}) by XBOOLE_0:def 3;

       not (( 1. INT.Ring ) * v) in ( Lin B) by A39;

      then not v in ( Lin B) by VECTSP_1:def 17;

      then

       A55: not v in B by ZMODUL02: 65;

      B c= (B \/ {v}) by XBOOLE_1: 7;

      then (B \/ {v}) in Q by A2, A37, A40, XBOOLE_1: 1;

      hence contradiction by A35, A36, A54, A55, XBOOLE_1: 7;

    end;

    theorem :: ZMODUL03:5

    

     Th5: for L be Linear_Combination of V holds for F,G be FinSequence of V holds for P be Permutation of ( dom F) st G = (F * P) holds ( Sum (L (#) F)) = ( Sum (L (#) G))

    proof

      let L be Linear_Combination of V;

      let F,G be FinSequence of V;

      set p = (L (#) F), q = (L (#) G);

      let P be Permutation of ( dom F) such that

       A1: G = (F * P);

      

       A2: ( len G) = ( len F) by A1, FINSEQ_2: 44;

      ( len F) = ( len (L (#) F)) by VECTSP_6:def 5;

      then

       A3: ( dom F) = ( dom (L (#) F)) by FINSEQ_3: 29;

      then

      reconsider r = ((L (#) F) * P) as FinSequence of V by FINSEQ_2: 47;

      ( len r) = ( len (L (#) F)) by A3, FINSEQ_2: 44;

      then

       A4: ( dom r) = ( dom (L (#) F)) by FINSEQ_3: 29;

      

       A5: ( len p) = ( len F) by VECTSP_6:def 5;

      then

       A6: ( dom F) = ( dom p) by FINSEQ_3: 29;

      ( len q) = ( len G) by VECTSP_6:def 5;

      then

       A7: ( dom p) = ( dom q) by A1, A5, FINSEQ_2: 44, FINSEQ_3: 29;

      

       A8: ( dom F) = ( dom G) by A2, FINSEQ_3: 29;

      now

        let k be Nat;

        assume

         A9: k in ( dom q);

        set l = (P . k);

        ( dom P) = ( dom F) & ( rng P) = ( dom F) by FUNCT_2: 52, FUNCT_2:def 3;

        then

         A10: l in ( dom F) by A7, A6, A9, FUNCT_1:def 3;

        then

        reconsider l as Element of NAT ;

        (G /. k) = (G . k) by A7, A8, A6, A9, PARTFUN1:def 6

        .= (F . (P . k)) by A1, A7, A8, A6, A9, FUNCT_1: 12

        .= (F /. l) by A10, PARTFUN1:def 6;

        

        then (q . k) = ((L . (F /. l)) * (F /. l)) by A9, VECTSP_6:def 5

        .= ((L (#) F) . (P . k)) by A6, A10, VECTSP_6:def 5

        .= (r . k) by A7, A4, A9, FUNCT_1: 12;

        hence (q . k) = (r . k);

      end;

      hence ( Sum p) = ( Sum q) by A3, A4, A7, FINSEQ_1: 13, RLVECT_2: 7;

    end;

    theorem :: ZMODUL03:6

    

     Th6: for L be Linear_Combination of V holds for F be FinSequence of V st ( Carrier L) misses ( rng F) holds ( Sum (L (#) F)) = ( 0. V)

    proof

      let L be Linear_Combination of V;

      defpred P[ FinSequence] means for G be FinSequence of V st G = $1 holds ( Carrier L) misses ( rng G) implies ( Sum (L (#) G)) = ( 0. V);

      

       A1: for p be FinSequence, x be object st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence, x be object such that

         A2: P[p];

        let G be FinSequence of V;

        assume

         A3: G = (p ^ <*x*>);

        then

        reconsider p, x9 = <*x*> as FinSequence of V by FINSEQ_1: 36;

        x in {x} by TARSKI:def 1;

        then

         A4: x in ( rng x9) by FINSEQ_1: 38;

        reconsider x as Vector of V by A4;

        assume ( Carrier L) misses ( rng G);

        

        then

         A5: {} = (( Carrier L) /\ ( rng G)) by XBOOLE_0:def 7

        .= (( Carrier L) /\ (( rng p) \/ ( rng <*x*>))) by A3, FINSEQ_1: 31

        .= (( Carrier L) /\ (( rng p) \/ {x})) by FINSEQ_1: 38

        .= ((( Carrier L) /\ ( rng p)) \/ (( Carrier L) /\ {x})) by XBOOLE_1: 23;

        then (( Carrier L) /\ ( rng p)) = {} ;

        then

         A6: ( Sum (L (#) p)) = ( 0. V) by A2, XBOOLE_0:def 7;

        

         A7: (( Carrier L) /\ {x}) = {} by A5;

        now

          

           A8: x in {x} by TARSKI:def 1;

          assume x in ( Carrier L);

          hence contradiction by A7, A8, XBOOLE_0:def 4;

        end;

        then

         A9: (L . x) = 0 ;

        ( Sum (L (#) G)) = ( Sum ((L (#) p) ^ (L (#) x9))) by A3, ZMODUL02: 51

        .= (( Sum (L (#) p)) + ( Sum (L (#) x9))) by RLVECT_1: 41

        .= (( 0. V) + ( Sum <*((L . x) * x)*>)) by A6, ZMODUL02: 15

        .= ( Sum <*((L . x) * x)*>) by RLVECT_1: 4

        .= (( 0. INT.Ring ) * x) by A9, RLVECT_1: 44

        .= ( 0. V) by ZMODUL01: 1;

        hence thesis;

      end;

      

       A10: P[ {} ]

      proof

        let G be FinSequence of V;

        assume G = {} ;

        then

         A11: (L (#) G) = ( <*> the carrier of V) by ZMODUL02: 14;

        assume ( Carrier L) misses ( rng G);

        thus thesis by A11, RLVECT_1: 43;

      end;

      

       A12: for p be FinSequence holds P[p] from FINSEQ_1:sch 3( A10, A1);

      let F be FinSequence of V;

      assume ( Carrier L) misses ( rng F);

      hence thesis by A12;

    end;

    theorem :: ZMODUL03:7

    for F be FinSequence of V st F is one-to-one holds for L be Linear_Combination of V st ( Carrier L) c= ( rng F) holds ( Sum (L (#) F)) = ( Sum L)

    proof

      let F be FinSequence of V such that

       A1: F is one-to-one;

      ( rng F) c= ( rng F);

      then

      reconsider X = ( rng F) as Subset of ( rng F);

      let L be Linear_Combination of V such that

       A2: ( Carrier L) c= ( rng F);

      consider G be FinSequence of V such that

       A3: G is one-to-one and

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

       A5: ( Sum L) = ( Sum (L (#) G)) by VECTSP_6:def 6;

      reconsider A = ( rng G) as Subset of ( rng F) by A2, A4;

      set F1 = (F - (A ` ));

      (X \ (A ` )) = (X /\ ((A ` ) ` )) by SUBSET_1: 13

      .= A by XBOOLE_1: 28;

      then

       A6: ( rng F1) = ( rng G) by FINSEQ_3: 65;

      F1 is one-to-one by A1, FINSEQ_3: 87;

      then

       A7: ex Q be Permutation of ( dom G) st F1 = (G * Q) by A3, A6, RFINSEQ: 4, RFINSEQ: 26;

      reconsider F1, F2 = (F - A) as FinSequence of V by FINSEQ_3: 86;

      

       A8: (( rng F2) /\ ( rng G)) = ((( rng F) \ ( rng G)) /\ ( rng G)) by FINSEQ_3: 65

      .= {} by XBOOLE_0:def 7, XBOOLE_1: 79;

      ex P be Permutation of ( dom F) st ((F - (A ` )) ^ (F - A)) = (F * P) by FINSEQ_3: 115;

      

      then ( Sum (L (#) F)) = ( Sum (L (#) (F1 ^ F2))) by Th5

      .= ( Sum ((L (#) F1) ^ (L (#) F2))) by ZMODUL02: 51

      .= (( Sum (L (#) F1)) + ( Sum (L (#) F2))) by RLVECT_1: 41

      .= (( Sum (L (#) F1)) + ( 0. V)) by A4, A8, Th6, XBOOLE_0:def 7

      .= (( Sum (L (#) G)) + ( 0. V)) by A7, Th5

      .= ( Sum L) by A5, RLVECT_1: 4;

      hence thesis;

    end;

    theorem :: ZMODUL03:8

    for L be Linear_Combination of V holds for F be FinSequence of V holds ex K be Linear_Combination of V st ( Carrier K) = (( rng F) /\ ( Carrier L)) & (L (#) F) = (K (#) F)

    proof

      let L be Linear_Combination of V, F be FinSequence of V;

      defpred P[ object, object] means $1 is Vector of V implies ($1 in ( rng F) & $2 = (L . $1)) or ( not $1 in ( rng F) & $2 = 0 );

      reconsider R = ( rng F) as finite Subset of V;

      

       A1: for x be object st x in the carrier of V holds ex y be object st y in INT & P[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

           A2: x in ( rng F);

          (L . x9) in INT ;

          hence thesis by A2;

        end;

          suppose

           A3: not x in ( rng F);

          thus thesis by A3;

        end;

      end;

      ex K be Function of the carrier of V, INT st for x be object st x in the carrier of V holds P[x, (K . x)] from FUNCT_2:sch 1( A1);

      then

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

       A4: for x be object st x in the carrier of V holds P[x, (K . x)];

       A5:

      now

        let v be Vector of V;

        assume

         A6: not v in (R /\ ( Carrier L));

        per cases by A6, XBOOLE_0:def 4;

          suppose not v in R;

          hence (K . v) = 0 by A4;

        end;

          suppose not v in ( Carrier L);

          then (L . v) = 0 ;

          hence (K . v) = 0 by A4;

        end;

      end;

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

      reconsider K as Linear_Combination of V by A5, VECTSP_6:def 1;

      now

        let v be object;

        assume

         A7: v in (( rng F) /\ ( Carrier L));

        then

        reconsider v9 = v as Vector of V;

        v in ( Carrier L) by A7, XBOOLE_0:def 4;

        then

         A8: (L . v9) <> 0 by ZMODUL02: 8;

        v in R by A7, XBOOLE_0:def 4;

        then (K . v9) = (L . v9) by A4;

        hence v in ( Carrier K) by A8;

      end;

      then

       A9: (( rng F) /\ ( Carrier L)) c= ( Carrier K);

      take K;

      

       A10: (L (#) F) = (K (#) F)

      proof

        set p = (L (#) F), q = (K (#) F);

        

         A11: ( len p) = ( len F) by VECTSP_6:def 5;

        ( len q) = ( len F) by VECTSP_6:def 5;

        then

         A12: ( dom p) = ( dom q) by A11, FINSEQ_3: 29;

        

         A13: ( dom p) = ( dom F) by A11, FINSEQ_3: 29;

        now

          let k be Nat;

          set u = (F /. k);

          

           A14: P[u, (K . u)] by A4;

          assume

           A15: k in ( dom p);

          then (F /. k) = (F . k) & (p . k) = ((L . u) * u) by A13, PARTFUN1:def 6, VECTSP_6:def 5;

          hence (p . k) = (q . k) by A12, A13, A15, A14, FUNCT_1:def 3, VECTSP_6:def 5;

        end;

        hence thesis by A12, FINSEQ_1: 13;

      end;

      now

        let v be object;

        assume v in ( Carrier K);

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

        hence v in (( rng F) /\ ( Carrier L)) by A5;

      end;

      then ( Carrier K) c= (( rng F) /\ ( Carrier L));

      hence thesis by A9, A10, XBOOLE_0:def 10;

    end;

    theorem :: ZMODUL03:9

    

     Th9: for L be Linear_Combination of V holds for A be Subset of V holds for F be FinSequence of V st ( rng F) c= the carrier of ( Lin A) holds ex K be Linear_Combination of A st ( Sum (L (#) F)) = ( Sum K)

    proof

      let L be Linear_Combination of V;

      let A be Subset of V;

      defpred P[ Nat] means for F be FinSequence of V st ( rng F) c= the carrier of ( Lin A) & ( len F) = $1 holds ex K be Linear_Combination of A st ( Sum (L (#) F)) = ( Sum K);

      

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

      proof

        let n be Nat;

        assume

         A2: P[n];

        let F be FinSequence of V such that

         A3: ( rng F) c= the carrier of ( Lin A) and

         A4: ( len F) = (n + 1);

        consider G be FinSequence, x be object such that

         A5: F = (G ^ <*x*>) by A4, FINSEQ_2: 18;

        reconsider G, x9 = <*x*> as FinSequence of V by A5, FINSEQ_1: 36;

        

         A6: ( rng (G ^ <*x*>)) = (( rng G) \/ ( rng <*x*>)) by FINSEQ_1: 31

        .= (( rng G) \/ {x}) by FINSEQ_1: 38;

        then

         A7: ( rng G) c= ( rng F) by A5, XBOOLE_1: 7;

         {x} c= ( rng F) by A5, A6, XBOOLE_1: 7;

        then {x} c= the carrier of ( Lin A) by A3;

        then

         A8: x in {x} implies x in the carrier of ( Lin A);

        then

        consider LA1 be Linear_Combination of A such that

         A9: x = ( Sum LA1) by STRUCT_0:def 5, TARSKI:def 1, ZMODUL02: 64;

        x in V by A8, STRUCT_0:def 5, TARSKI:def 1, ZMODUL01: 24;

        then

        reconsider x as Vector of V;

        ( len (G ^ <*x*>)) = (( len G) + ( len <*x*>)) by FINSEQ_1: 22

        .= (( len G) + 1) by FINSEQ_1: 39;

        then

        consider LA2 be Linear_Combination of A such that

         A10: ( Sum (L (#) G)) = ( Sum LA2) by A2, A3, A4, A5, A7, XBOOLE_1: 1;

        ((L . x) * LA1) is Linear_Combination of A by ZMODUL02: 31;

        then

         A11: (LA2 + ((L . x) * LA1)) is Linear_Combination of A by ZMODUL02: 27;

        ( Sum (L (#) F)) = ( Sum ((L (#) G) ^ (L (#) x9))) by A5, ZMODUL02: 51

        .= (( Sum LA2) + ( Sum (L (#) x9))) by A10, RLVECT_1: 41

        .= (( Sum LA2) + ( Sum <*((L . x) * x)*>)) by ZMODUL02: 15

        .= (( Sum LA2) + ((L . x) * ( Sum LA1))) by A9, RLVECT_1: 44

        .= (( Sum LA2) + ( Sum ((L . x) * LA1))) by ZMODUL02: 53

        .= ( Sum (LA2 + ((L . x) * LA1))) by ZMODUL02: 52;

        hence thesis by A11;

      end;

      let F be FinSequence of V;

      assume

       A12: ( rng F) c= the carrier of ( Lin A);

      

       A13: ( len F) is Element of NAT ;

      

       A14: P[ 0 ]

      proof

        let F be FinSequence of V;

        assume that ( rng F) c= the carrier of ( Lin A) and

         A15: ( len F) = 0 ;

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

        then (L (#) F) = ( <*> the carrier of V) by ZMODUL02: 14;

        

        then

         A16: ( Sum (L (#) F)) = ( 0. V) by RLVECT_1: 43

        .= ( Sum ( ZeroLC V)) by ZMODUL02: 19;

        ( ZeroLC V) is Linear_Combination of A by ZMODUL02: 11;

        hence thesis by A16;

      end;

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

      hence thesis by A12, A13;

    end;

    theorem :: ZMODUL03:10

    

     Th10: for L be Linear_Combination of V holds for A be Subset of V st ( Carrier L) c= the carrier of ( Lin A) holds ex K be Linear_Combination of A st ( Sum L) = ( Sum K)

    proof

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

      consider F be FinSequence of V such that F is one-to-one and

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

       A2: ( Sum L) = ( Sum (L (#) F)) by VECTSP_6:def 6;

      assume ( Carrier L) c= the carrier of ( Lin A);

      then

      consider K be Linear_Combination of A such that

       A3: ( Sum (L (#) F)) = ( Sum K) by A1, Th9;

      take K;

      thus thesis by A2, A3;

    end;

    theorem :: ZMODUL03:11

    

     Th11: for L be Linear_Combination of V st ( Carrier L) c= the carrier of W holds for K be Linear_Combination of W st K = (L | the carrier of W) holds ( Carrier L) = ( Carrier K) & ( Sum L) = ( Sum K)

    proof

      let L be Linear_Combination of V such that

       A1: ( Carrier L) c= the carrier of W;

      let K be Linear_Combination of W such that

       A2: K = (L | the carrier of W);

      

       A3: ( dom K) = the carrier of W by FUNCT_2:def 1;

      now

        let x be object;

        assume x in ( Carrier K);

        then

        consider w be Vector of W such that

         A4: x = w and

         A5: (K . w) <> 0 ;

        

         A6: w is Vector of V by ZMODUL01: 25;

        (L . w) <> 0 by A2, A3, A5, FUNCT_1: 47;

        hence x in ( Carrier L) by A4, A6;

      end;

      then

       A7: ( Carrier K) c= ( Carrier L);

      consider G be FinSequence of W such that

       A8: G is one-to-one & ( rng G) = ( Carrier K) and

       A9: ( Sum K) = ( Sum (K (#) G)) by VECTSP_6:def 6;

      consider F be FinSequence of V such that

       A10: F is one-to-one and

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

       A12: ( Sum L) = ( Sum (L (#) F)) by VECTSP_6:def 6;

      now

        let x be object;

        assume

         A13: x in ( Carrier L);

        then

        consider v be Vector of V such that

         A14: x = v and

         A15: (L . v) <> 0 ;

        (K . v) <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1: 47;

        hence x in ( Carrier K) by A1, A13, A14;

      end;

      then

       A16: ( Carrier L) c= ( Carrier K);

      then

       A17: ( Carrier K) = ( Carrier L) by A7, XBOOLE_0:def 10;

      (F,G) are_fiberwise_equipotent by A7, A8, A10, A11, A16, RFINSEQ: 26, XBOOLE_0:def 10;

      then

      consider P be Permutation of ( dom G) such that

       A18: F = (G * P) by RFINSEQ: 4;

      ( len (K (#) G)) = ( len G) by VECTSP_6:def 5;

      then

       A19: ( dom (K (#) G)) = ( dom G) by FINSEQ_3: 29;

      then

      reconsider q = ((K (#) G) * P) as FinSequence of W by FINSEQ_2: 47;

      

       A20: ( len q) = ( len (K (#) G)) by A19, FINSEQ_2: 44;

      then ( len q) = ( len G) by VECTSP_6:def 5;

      then

       A21: ( dom q) = ( dom G) by FINSEQ_3: 29;

      set p = (L (#) F);

      

       A22: the carrier of W c= the carrier of V by VECTSP_4:def 2;

      ( rng q) c= the carrier of V by A22;

      then

      reconsider q9 = q as FinSequence of V by FINSEQ_1:def 4;

      consider f be Function of NAT , the carrier of W such that

       A23: ( Sum q) = (f . ( len q)) and

       A24: (f . 0 ) = ( 0. W) and

       A25: for i be Nat, w be Vector of W st i < ( len q) & w = (q . (i + 1)) holds (f . (i + 1)) = ((f . i) + w) by RLVECT_1:def 12;

      ( dom f) = NAT & ( rng f) c= the carrier of W by FUNCT_2:def 1;

      then

      reconsider f9 = f as Function of NAT , the carrier of V by A22, FUNCT_2: 2, XBOOLE_1: 1;

      

       A26: for i be Nat, v be Vector of V st i < ( len q9) & v = (q9 . (i + 1)) holds (f9 . (i + 1)) = ((f9 . i) + v)

      proof

        let i be Nat, v be Vector of V;

        assume that

         A27: i < ( len q9) and

         A28: v = (q9 . (i + 1));

        1 <= (i + 1) & (i + 1) <= ( len q) by A27, NAT_1: 11, NAT_1: 13;

        then (i + 1) in ( dom q) by FINSEQ_3: 25;

        then

        reconsider v9 = v as Vector of W by A28, FINSEQ_2: 11;

        (f . (i + 1)) = ((f . i) + v9) by A25, A27, A28;

        hence thesis by ZMODUL01: 28;

      end;

      

       A29: ( len G) = ( len F) by A18, FINSEQ_2: 44;

      then

       A30: ( dom G) = ( dom F) by FINSEQ_3: 29;

      

       A31: ( len G) = ( len (L (#) F)) by A29, VECTSP_6:def 5;

      then

       A32: ( dom p) = ( dom G) by FINSEQ_3: 29;

      

       A33: ( dom q) = ( dom (K (#) G)) by A20, FINSEQ_3: 29;

      now

        let i be Nat;

        set v = (F /. i);

        set j = (P . i);

        assume

         A34: i in ( dom p);

        then

         A35: (F /. i) = (F . i) by A30, A32, PARTFUN1:def 6;

        then v in ( rng F) by A30, A32, A34, FUNCT_1:def 3;

        then

        reconsider w = v as Vector of W by A17, A11;

        ( dom P) = ( dom G) & ( rng P) = ( dom G) by FUNCT_2: 52, FUNCT_2:def 3;

        then

         A36: j in ( dom G) by A32, A34, FUNCT_1:def 3;

        then

        reconsider j as Element of NAT ;

        

         A37: (G /. j) = (G . (P . i)) by A36, PARTFUN1:def 6

        .= v by A18, A30, A32, A34, A35, FUNCT_1: 12;

        (q . i) = ((K (#) G) . j) by A21, A32, A34, FUNCT_1: 12

        .= ((K . w) * w) by A33, A21, A36, A37, VECTSP_6:def 5

        .= ((L . v) * w) by A2, A3, FUNCT_1: 47

        .= ((L . v) * v) by ZMODUL01: 29;

        hence (p . i) = (q . i) by A34, VECTSP_6:def 5;

      end;

      then

       A38: (L (#) F) = ((K (#) G) * P) by A21, A31, FINSEQ_1: 13, FINSEQ_3: 29;

      ( len G) = ( len (K (#) G)) by VECTSP_6:def 5;

      then ( dom G) = ( dom (K (#) G)) by FINSEQ_3: 29;

      then

      reconsider P as Permutation of ( dom (K (#) G));

      q = ((K (#) G) * P);

      then

       A39: ( Sum (K (#) G)) = ( Sum q) by RLVECT_2: 7;

      

       A40: (f9 . ( len q9)) is Element of V;

      (f9 . 0 ) = ( 0. V) by A24, ZMODUL01: 26;

      hence thesis by A7, A16, A12, A9, A38, A39, A23, A26, A40, RLVECT_1:def 12, XBOOLE_0:def 10;

    end;

    theorem :: ZMODUL03:12

    

     Th12: for K be Linear_Combination of W holds ex L be Linear_Combination of V st ( Carrier K) = ( Carrier L) & ( Sum K) = ( Sum L)

    proof

      let K be Linear_Combination of W;

      defpred P[ object, object] means ($1 in W & $2 = (K . $1)) or ( not $1 in W & $2 = 0 );

      reconsider K9 = K as Function of the carrier of W, INT ;

      

       A1: the carrier of W c= the carrier of V by VECTSP_4:def 2;

      then

      reconsider C = ( Carrier K) as finite Subset of V by XBOOLE_1: 1;

      

       A2: for x be object st x in the carrier of V holds ex y be object st y in INT & P[x, y]

      proof

        let x be object;

        assume x in the carrier of V;

        then

        reconsider x as Vector of V;

        per cases ;

          suppose

           A3: x in W;

          then

          reconsider x as Vector of W;

           P[x, (K . x)] by A3;

          hence thesis;

        end;

          suppose

           A4: not x in W;

          thus thesis by A4;

        end;

      end;

      consider L be Function of the carrier of V, INT such that

       A5: for x be object st x in the carrier of V holds P[x, (L . x)] from FUNCT_2:sch 1( A2);

       A6:

      now

        let v be Vector of V;

        assume not v in C;

        then P[v, (K . v)] & not v in C & v in the carrier of W or P[v, 0 ] by STRUCT_0:def 5;

        then P[v, (K . v)] & (K . v) = 0 or P[v, 0 ];

        hence (L . v) = 0 by A5;

      end;

      L is Element of ( Funcs (the carrier of V,the carrier of INT.Ring )) by FUNCT_2: 8;

      then

      reconsider L as Linear_Combination of V by A6, VECTSP_6:def 1;

      reconsider L9 = (L | the carrier of W) as Function of the carrier of W, INT by A1, FUNCT_2: 32;

      take L;

      now

        let x be object;

        assume that

         A7: x in ( Carrier L) and

         A8: not x in the carrier of W;

        consider v be Vector of V such that

         A9: x = v and

         A10: (L . v) <> 0 by A7;

         P[v, 0 ] by A8, A9, STRUCT_0:def 5;

        hence contradiction by A5, A10;

      end;

      then

       A11: ( Carrier L) c= the carrier of W;

      now

        let x be object;

        assume

         A12: x in the carrier of W;

        then P[x, (L . x)] by A5, A1;

        hence (K9 . x) = (L9 . x) by A12, FUNCT_1: 49, STRUCT_0:def 5;

      end;

      then K9 = L9 by FUNCT_2: 12;

      hence thesis by A11, Th11;

    end;

    theorem :: ZMODUL03:13

    

     Th13: for L be Linear_Combination of V st ( Carrier L) c= the carrier of W holds ex K be Linear_Combination of W st ( Carrier K) = ( Carrier L) & ( Sum K) = ( Sum L)

    proof

      let L be Linear_Combination of V;

      assume

       A1: ( Carrier L) c= the carrier of W;

      then

      reconsider C = ( Carrier L) as finite Subset of W;

      the carrier of W c= the carrier of V by VECTSP_4:def 2;

      then

      reconsider K = (L | the carrier of W) as Function of the carrier of W, the carrier of INT.Ring by FUNCT_2: 32;

      

       A2: K is Element of ( Funcs (the carrier of W,the carrier of INT.Ring )) by FUNCT_2: 8;

      

       A3: ( dom K) = the carrier of W by FUNCT_2:def 1;

      now

        let w be Vector of W;

        

         A4: w is Vector of V by ZMODUL01: 25;

        assume not w in C;

        then (L . w) = 0 by A4;

        hence (K . w) = 0 by A3, FUNCT_1: 47;

      end;

      then

      reconsider K as Linear_Combination of W by A2, VECTSP_6:def 1;

      take K;

      thus thesis by A1, Th11;

    end;

    theorem :: ZMODUL03:14

    

     Th14: for V be free Z_Module holds for I be Basis of V, v be Vector of V holds v in ( Lin I)

    proof

      let V be free Z_Module;

      let I be Basis of V, v be Vector of V;

      

       A1: v in the ModuleStr of V;

      for I be Subset of V holds I is base iff I is linearly-independent & ( Lin I) = the ModuleStr of V;

      hence thesis by A1;

    end;

    theorem :: ZMODUL03:15

    for A be Subset of W st A is linearly-independent holds A is linearly-independent Subset of V

    proof

      let A be Subset of W;

      the carrier of W c= the carrier of V by VECTSP_4:def 2;

      then

      reconsider A9 = A as Subset of V by XBOOLE_1: 1;

      assume

       A1: A is linearly-independent;

      now

        assume A9 is linearly-dependent;

        then

        consider L be Linear_Combination of A9 such that

         A2: ( Sum L) = ( 0. V) and

         A3: ( Carrier L) <> {} ;

        ( Carrier L) c= A by VECTSP_6:def 4;

        then

        consider LW be Linear_Combination of W such that

         A4: ( Carrier LW) = ( Carrier L) and

         A5: ( Sum LW) = ( Sum L) by Th13, XBOOLE_1: 1;

        reconsider LW as Linear_Combination of A by A4, VECTSP_6:def 4;

        ( Sum LW) = ( 0. W) by A2, A5, ZMODUL01: 26;

        hence contradiction by A1, A3, A4;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL03:16

    

     Th16: for A be Subset of V st A is linearly-independent & A c= the carrier of W holds A is linearly-independent Subset of W

    proof

      let A be Subset of V such that

       A1: A is linearly-independent and

       A2: A c= the carrier of W;

      reconsider A9 = A as Subset of W by A2;

      now

        assume A9 is linearly-dependent;

        then

        consider K be Linear_Combination of A9 such that

         A3: ( Sum K) = ( 0. W) and

         A4: ( Carrier K) <> {} ;

        consider L be Linear_Combination of V such that

         A5: ( Carrier L) = ( Carrier K) and

         A6: ( Sum L) = ( Sum K) by Th12;

        reconsider L as Linear_Combination of A by A5, VECTSP_6:def 4;

        ( Sum L) = ( 0. V) by A3, A6, ZMODUL01: 26;

        hence contradiction by A1, A4, A5;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL03:17

    

     Th17: for V be Z_Module holds for A be Subset of V st A is linearly-independent holds for v be Vector of V st v in A holds for B be Subset of V st B = (A \ {v}) holds not v in ( Lin B)

    proof

      let V be Z_Module;

      let A be Subset of V such that

       A1: A is linearly-independent;

      let v be Vector of V;

      assume v in A;

      then

       A2: {v} is Subset of A by SUBSET_1: 41;

      v in {v} by TARSKI:def 1;

      then v in ( Lin {v}) by ZMODUL02: 65;

      then

      consider K be Linear_Combination of {v} such that

       A3: v = ( Sum K) by ZMODUL02: 64;

      let B be Subset of V such that

       A4: B = (A \ {v});

      B c= A by A4, XBOOLE_1: 36;

      then

       A5: (B \/ {v}) c= (A \/ A) by A2, XBOOLE_1: 13;

      assume v in ( Lin B);

      then

      consider L be Linear_Combination of B such that

       A6: v = ( Sum L) by ZMODUL02: 64;

      

       A7: ( Carrier L) c= B & ( Carrier K) c= {v} by VECTSP_6:def 4;

      then (( Carrier L) \/ ( Carrier K)) c= (B \/ {v}) by XBOOLE_1: 13;

      then ( Carrier (L - K)) c= (( Carrier L) \/ ( Carrier K)) & (( Carrier L) \/ ( Carrier K)) c= A by A5, ZMODUL02: 40;

      then

       A8: (L - K) is Linear_Combination of A by XBOOLE_1: 1, VECTSP_6:def 4;

      

       A9: for x be Vector of V holds x in ( Carrier L) implies (K . x) = 0

      proof

        let x be Vector of V;

        assume x in ( Carrier L);

        then not x in ( Carrier K) by A4, A7, XBOOLE_0:def 5;

        hence thesis;

      end;

       A10:

      now

        let x be set such that

         A11: x in ( Carrier L) and

         A12: not x in ( Carrier (L - K));

        reconsider x as Vector of V by A11;

        

         A13: (L . x) <> 0 by A11, ZMODUL02: 8;

        ((L - K) . x) = ((L . x) - (K . x)) by ZMODUL02: 39

        .= ((L . x) - ( 0. INT.Ring )) by A9, A11

        .= (L . x);

        hence contradiction by A12, A13;

      end;

      v <> ( 0. V) by A1, A2, ZMODUL02: 56;

      then ( Carrier L) is non empty by A6, ZMODUL02: 23;

      then ex w be object st w in ( Carrier L) by XBOOLE_0:def 1;

      then

       A14: ( Carrier (L - K)) is non empty by A10;

      ( 0. V) = (( Sum L) + ( - ( Sum K))) by A6, A3, RLVECT_1: 5

      .= (( Sum L) + ( Sum ( - K))) by ZMODUL02: 54

      .= ( Sum (L - K)) by ZMODUL02: 52;

      hence contradiction by A1, A8, A14;

    end;

    theorem :: ZMODUL03:18

    

     Th18: for V be free Z_Module holds for I be Basis of V holds for A be non empty Subset of V st A misses I holds for B be Subset of V st B = (I \/ A) holds B is linearly-dependent

    proof

      let V be free Z_Module;

      let I be Basis of V;

      let A be non empty Subset of V such that

       A1: A misses I;

      consider v be object such that

       A2: v in A by XBOOLE_0:def 1;

      let B be Subset of V such that

       A3: B = (I \/ A);

      

       A4: A c= B by A3, XBOOLE_1: 7;

      reconsider v as Vector of V by A2;

      reconsider Bv = (B \ {v}) as Subset of V;

      

       A5: (I \ {v}) c= (B \ {v}) by A3, XBOOLE_1: 7, XBOOLE_1: 33;

       not v in I by A1, A2, XBOOLE_0: 3;

      then I c= Bv by A5, ZFMISC_1: 57;

      then

       A6: ( Lin I) is Submodule of ( Lin Bv) by ZMODUL02: 70;

      assume

       A7: B is linearly-independent;

      v in ( Lin I) by Th14;

      hence contradiction by A7, A2, A4, A6, Th17, ZMODUL01: 23;

    end;

    theorem :: ZMODUL03:19

    for A be Subset of V st A c= the carrier of W holds ( Lin A) is Submodule of W

    proof

      let A be Subset of V;

      assume

       A1: A c= the carrier of W;

      now

        let w be object;

        assume w in the carrier of ( Lin A);

        then

        consider L be Linear_Combination of A such that

         A2: w = ( Sum L) by STRUCT_0:def 5, ZMODUL02: 64;

        ( Carrier L) c= A by VECTSP_6:def 4;

        then ex K be Linear_Combination of W st ( Carrier K) = ( Carrier L) & ( Sum L) = ( Sum K) by A1, Th13, XBOOLE_1: 1;

        hence w in the carrier of W by A2;

      end;

      hence thesis by TARSKI:def 3, ZMODUL01: 43;

    end;

    theorem :: ZMODUL03:20

    

     Th20: for A be Subset of V, B be Subset of W st A = B holds ( Lin A) = ( Lin B)

    proof

      let A be Subset of V, B be Subset of W;

      reconsider B9 = ( Lin B), V9 = V as Z_Module;

      

       A1: B9 is Submodule of V9 by ZMODUL01: 42;

      assume

       A2: A = B;

      now

        let x be object;

        assume x in the carrier of ( Lin A);

        then

        consider L be Linear_Combination of A such that

         A3: x = ( Sum L) by STRUCT_0:def 5, ZMODUL02: 64;

        ( Carrier L) c= A by VECTSP_6:def 4;

        then

        consider K be Linear_Combination of W such that

         A4: ( Carrier K) = ( Carrier L) and

         A5: ( Sum K) = ( Sum L) by A2, Th13, XBOOLE_1: 1;

        reconsider K as Linear_Combination of B by A2, A4, VECTSP_6:def 4;

        x = ( Sum K) by A3, A5;

        hence x in the carrier of ( Lin B) by STRUCT_0:def 5, ZMODUL02: 64;

      end;

      then

       A6: the carrier of ( Lin A) c= the carrier of ( Lin B);

      now

        let x be object;

        assume x in the carrier of ( Lin B);

        then

        consider K be Linear_Combination of B such that

         A7: x = ( Sum K) by STRUCT_0:def 5, ZMODUL02: 64;

        consider L be Linear_Combination of V such that

         A8: ( Carrier L) = ( Carrier K) and

         A9: ( Sum L) = ( Sum K) by Th12;

        reconsider L as Linear_Combination of A by A2, A8, VECTSP_6:def 4;

        x = ( Sum L) by A7, A9;

        hence x in the carrier of ( Lin A) by STRUCT_0:def 5, ZMODUL02: 64;

      end;

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

      hence thesis by A1, A6, XBOOLE_0:def 10, ZMODUL01: 45;

    end;

    registration

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

      cluster ( Lin A) -> free;

      correctness

      proof

        ex B be Subset of ( Lin A) st B is base

        proof

          for x be object holds x in A implies x in the carrier of ( Lin A) by STRUCT_0:def 5, ZMODUL02: 65;

          then

          reconsider B = A as linearly-independent Subset of ( Lin A) by Th16, TARSKI:def 3;

          take B;

          ( Lin B) = the ModuleStr of ( Lin A) by Th20;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let V be free Z_Module;

      cluster ( (Omega). V) -> strict free;

      coherence

      proof

        reconsider VV = ( (Omega). V) as Z_Module;

        consider A be Subset of V such that

         a1: A is base by VECTSP_7:def 4;

        

         A1: A is linearly-independent & ( Lin A) = the ModuleStr of V by a1;

        ex AA be Subset of VV st AA is linearly-independent & ( Lin AA) = the ModuleStr of VV

        proof

          consider AA be Subset of VV such that

           A2: AA = A;

          take AA;

          thus thesis by A1, A2, Th16, Th20;

        end;

        hence thesis;

      end;

    end

    begin

    definition

      let IT be free Z_Module;

      :: ZMODUL03:def3

      attr IT is finite-rank means

      : Def3: ex A be finite Subset of IT st A is Basis of IT;

    end

    registration

      let V;

      cluster ( (0). V) -> finite-rank;

      coherence

      proof

        reconsider VV = ( (0). V) as free Z_Module;

        ex A be finite Subset of VV st A is Basis of VV

        proof

          set WW = ( {} the carrier of VV);

          reconsider WW as Subset of VV;

          

           A1: ( Lin WW) = ( (0). VV) by ZMODUL02: 67

          .= VV by ZMODUL01: 51;

          reconsider WW as finite Subset of VV;

          take WW;

          thus thesis by A1, VECTSP_7:def 3;

        end;

        hence thesis;

      end;

    end

    registration

      cluster strict finite-rank for free Z_Module;

      existence

      proof

        set V = the Z_Module;

        take ( (0). V);

        thus thesis;

      end;

    end

    registration

      let V be Z_Module;

      cluster strict finite-rank for free Submodule of V;

      existence

      proof

        reconsider W = ( (0). V) as strict free Submodule of V;

        take W;

        thus thesis;

      end;

    end

    registration

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

      cluster ( Lin A) -> finite-rank;

      coherence

      proof

        ex AA be finite Subset of ( Lin A) st AA is Basis of ( Lin A)

        proof

          for x be object holds x in A implies x in the carrier of ( Lin A) by STRUCT_0:def 5, ZMODUL02: 65;

          then

          reconsider AA = A as finite linearly-independent Subset of ( Lin A) by Th16, TARSKI:def 3;

          take AA;

          ( Lin A) = ( Lin AA) by Th20;

          hence thesis by VECTSP_7:def 3;

        end;

        hence thesis;

      end;

    end

    definition

      let V be Z_Module;

      :: ZMODUL03:def4

      attr V is finitely-generated means ex A be finite Subset of V st ( Lin A) = the ModuleStr of V;

    end

    registration

      let V;

      cluster ( (0). V) -> finitely-generated;

      coherence

      proof

        set W = ( (0). V);

        reconsider W as Z_Module;

        set A = ( {} the carrier of W);

        reconsider A as Subset of W;

        ( Lin A) = ( (0). W) by ZMODUL02: 67

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

        hence thesis;

      end;

    end

    registration

      cluster strict finitely-generated free for Z_Module;

      existence

      proof

        set V = the Z_Module;

        take ( (0). V);

        thus thesis;

      end;

    end

    registration

      let V be finite-rank free Z_Module;

      cluster -> finite for Basis of V;

      coherence

      proof

        consider A be finite Subset of V such that

         A1: A is Basis of V by Def3;

        let B be Basis of V;

        consider p be FinSequence such that

         A2: ( rng p) = A by FINSEQ_1: 52;

        reconsider p as FinSequence of V by A2, FINSEQ_1:def 4;

        set Car = { ( Carrier L) where L be Linear_Combination of B : ex i be Element of NAT st i in ( dom p) & ( Sum L) = (p . i) };

        set C = ( union Car);

        

         A3: C c= B

        proof

          let x be object;

          assume x in C;

          then

          consider R be set such that

           A4: x in R and

           A5: R in Car by TARSKI:def 4;

          ex L be Linear_Combination of B st R = ( Carrier L) & ex i be Element of NAT st i in ( dom p) & ( Sum L) = (p . i) by A5;

          then R c= B by VECTSP_6:def 4;

          hence thesis by A4;

        end;

        then

        reconsider C as Subset of V by XBOOLE_1: 1;

        

         A6: for v be Vector of V holds v in ( (Omega). V) iff v in ( Lin C)

        proof

          let v be Vector of V;

          hereby

            assume v in ( (Omega). V);

            then v in ( Lin A) by A1, VECTSP_7:def 3;

            then

            consider LA be Linear_Combination of A such that

             A7: v = ( Sum LA) by ZMODUL02: 64;

            ( Carrier LA) c= the carrier of ( Lin C)

            proof

              let w be object;

              assume

               A8: w in ( Carrier LA);

              then

              reconsider w9 = w as Vector of V;

              w9 in ( Lin B) by Th14;

              then

              consider LB be Linear_Combination of B such that

               A9: w = ( Sum LB) by ZMODUL02: 64;

              ( Carrier LA) c= A by VECTSP_6:def 4;

              then ex i be object st i in ( dom p) & w = (p . i) by A2, A8, FUNCT_1:def 3;

              then

               A10: ( Carrier LB) in Car by A9;

              ( Carrier LB) c= C by A10, TARSKI:def 4;

              then LB is Linear_Combination of C by VECTSP_6:def 4;

              hence thesis by A9, STRUCT_0:def 5, ZMODUL02: 64;

            end;

            then ex LC be Linear_Combination of C st ( Sum LA) = ( Sum LC) by Th10;

            hence v in ( Lin C) by A7, ZMODUL02: 64;

          end;

          assume v in ( Lin C);

          thus thesis;

        end;

        

         A11: B is linearly-independent by VECTSP_7:def 3;

        C is linearly-independent by A3, VECTSP_7:def 3, ZMODUL02: 56;

        then

         A12: C is Basis of V by A6, VECTSP_7:def 3, ZMODUL01: 46;

        B c= C

        proof

          set D = (B \ C);

          assume not B c= C;

          then ex v be object st v in B & not v in C;

          then

          reconsider D as non empty Subset of V by XBOOLE_0:def 5;

          reconsider B as Subset of V;

          (C \/ (B \ C)) = (C \/ B) by XBOOLE_1: 39

          .= B by A3, XBOOLE_1: 12;

          then B = (C \/ D);

          hence contradiction by A11, A12, Th18, XBOOLE_1: 79;

        end;

        then

         A13: B = C by A3, XBOOLE_0:def 10;

        defpred P[ set, object] means ex L be Linear_Combination of B st $2 = ( Carrier L) & ( Sum L) = (p . $1);

        

         A14: for i be Nat st i in ( Seg ( len p)) holds ex x be object st P[i, x]

        proof

          let i be Nat;

          assume i in ( Seg ( len p));

          then i in ( dom p) by FINSEQ_1:def 3;

          then (p . i) in the carrier of V by FINSEQ_2: 11;

          then (p . i) in ( Lin B) by Th14;

          then

          consider L be Linear_Combination of B such that

           A15: (p . i) = ( Sum L) by ZMODUL02: 64;

           P[i, ( Carrier L)] by A15;

          hence thesis;

        end;

        ex q be FinSequence st ( dom q) = ( Seg ( len p)) & for i be Nat st i in ( Seg ( len p)) holds P[i, (q . i)] from FINSEQ_1:sch 1( A14);

        then

        consider q be FinSequence such that

         A16: ( dom q) = ( Seg ( len p)) and

         A17: for i be Nat st i in ( Seg ( len p)) holds P[i, (q . i)];

        

         A18: ( dom p) = ( dom q) by A16, FINSEQ_1:def 3;

        

         A19: for i be Nat, y1, y2 st i in ( Seg ( len p)) & P[i, y1] & P[i, y2] holds y1 = y2

        proof

          let i be Nat, y1, y2;

          assume that i in ( Seg ( len p)) and

           A20: P[i, y1] and

           A21: P[i, y2];

          consider L1 be Linear_Combination of B such that

           A22: y1 = ( Carrier L1) & ( Sum L1) = (p . i) by A20;

          consider L2 be Linear_Combination of B such that

           A23: y2 = ( Carrier L2) & ( Sum L2) = (p . i) by A21;

          ( Carrier L1) c= B & ( Carrier L2) c= B by VECTSP_6:def 4;

          hence thesis by A22, A23, VECTSP_7:def 3, Th3;

        end;

        now

          let x be object;

          assume x in Car;

          then

          consider L be Linear_Combination of B such that

           A24: x = ( Carrier L) and

           A25: ex i be Element of NAT st i in ( dom p) & ( Sum L) = (p . i);

          consider i be Element of NAT such that

           A26: i in ( dom p) and

           A27: ( Sum L) = (p . i) by A25;

           P[i, (q . i)] by A16, A17, A18, A26;

          then x = (q . i) by A19, A16, A18, A24, A26, A27;

          hence x in ( rng q) by A18, A26, FUNCT_1:def 3;

        end;

        then

         A28: Car c= ( rng q);

        for R be set st R in Car holds R is finite

        proof

          let R be set;

          assume R in Car;

          then ex L be Linear_Combination of B st R = ( Carrier L) & ex i be Element of NAT st i in ( dom p) & ( Sum L) = (p . i);

          hence thesis;

        end;

        hence thesis by A13, A28, FINSET_1: 7;

      end;

    end

    begin

    theorem :: ZMODUL03:21

    

     Th21: for p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, u1,u2 be Vector of V st u1 <> u2 & u1 in I & u2 in I holds ( ZMtoMQV (V,p,u1)) <> ( ZMtoMQV (V,p,u2))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, u1,u2 be Vector of V such that

       A1: u1 <> u2 & u1 in I & u2 in I;

      set uq1 = ( ZMtoMQV (V,p,u1)), uq2 = ( ZMtoMQV (V,p,u2));

      assume

       A2: uq1 = uq2;

      consider u be Vector of V such that

       A3: u in (p (*) V) & (u1 + u) = u2 by A2, ZMODUL01: 75;

      

       A4: I is linearly-independent & ( Lin I) = the ModuleStr of V by VECTSP_7:def 3;

      

       B1: u in (p * V) by A3;

      reconsider pp = p as Element of INT.Ring ;

      consider v be Vector of V such that

       A5: u = (pp * v) by B1;

      consider lv be Linear_Combination of I such that

       A6: v = ( Sum lv) by A4, STRUCT_0:def 5, ZMODUL02: 64;

      consider lu1 be Linear_Combination of V such that

       A7: (lu1 . u1) = 1 & for v be Vector of V st v <> u1 holds (lu1 . v) = 0 by Th1;

      

       A8: ( Carrier lu1) = {u1}

      proof

        for v be object holds v in ( Carrier lu1) implies v in {u1}

        proof

          assume ex v be object st v in ( Carrier lu1) & not v in {u1};

          then

          consider v be Vector of V such that

           A9: v in ( Carrier lu1) & not v in {u1};

          v <> u1 by A9, TARSKI:def 1;

          then (lu1 . v) = 0 by A7;

          hence contradiction by A9, ZMODUL02: 8;

        end;

        then

         A10: ( Carrier lu1) c= {u1};

        u1 in ( Carrier lu1) by A7;

        then {u1} c= ( Carrier lu1) by ZFMISC_1: 31;

        hence thesis by A10, XBOOLE_0:def 10;

      end;

      

      then

       A11: ( Sum lu1) = (( 1. INT.Ring ) * u1) by A7, ZMODUL02: 24

      .= u1 by VECTSP_1:def 17;

      reconsider lu1 as Linear_Combination of {u1} by A8, VECTSP_6:def 4;

      reconsider lu1 as Linear_Combination of I by A1, ZFMISC_1: 31, ZMODUL02: 10;

      consider lu2 be Linear_Combination of V such that

       A12: (lu2 . u2) = 1 & for v be Vector of V st v <> u2 holds (lu2 . v) = 0 by Th1;

      

       A13: ( Carrier lu2) = {u2}

      proof

        for v be object holds v in ( Carrier lu2) implies v in {u2}

        proof

          assume ex v be object st v in ( Carrier lu2) & not v in {u2};

          then

          consider v be Vector of V such that

           A14: v in ( Carrier lu2) & not v in {u2};

          v <> u2 by A14, TARSKI:def 1;

          then (lu2 . v) = 0 by A12;

          hence contradiction by A14, ZMODUL02: 8;

        end;

        then

         A15: ( Carrier lu2) c= {u2};

        u2 in ( Carrier lu2) by A12;

        then {u2} c= ( Carrier lu2) by ZFMISC_1: 31;

        hence thesis by A15, XBOOLE_0:def 10;

      end;

      

      then

       A16: ( Sum lu2) = (( 1. INT.Ring ) * u2) by A12, ZMODUL02: 24

      .= u2 by VECTSP_1:def 17;

      reconsider lu2 as Linear_Combination of {u2} by A13, VECTSP_6:def 4;

      reconsider lu2 as Linear_Combination of I by A1, ZFMISC_1: 31, ZMODUL02: 10;

      

       A17: u = ( Sum (p * lv)) by A5, A6, ZMODUL02: 53;

      

       A18: ((p * lv) . u1) <> ( - 1)

      proof

        assume

         A19: ((p * lv) . u1) = ( - 1);

        ( - p) < ( - 1) & 0 > ( - 1) by INT_2:def 4, XREAL_1: 24;

        then (( - 1) mod p) = (p + ( - 1)) by NAT_D: 63;

        then (((p * lv) . u1) mod p) = (p - 1) by A19;

        then

         A20: (((p * lv) . u1) mod p) <> 0 by INT_2:def 4;

        reconsider pp = p as Element of INT.Ring ;

        

         A21: ((pp * lv) . u1) = (pp * (lv . u1)) by VECTSP_6:def 9;

        pp divides (((pp * lv) . u1) - 0 ) by A21, INT_1: 60, INT_1:def 4;

        hence contradiction by A20, INT_1: 62;

      end;

      (pp * lv) is Linear_Combination of I by ZMODUL02: 31;

      then (lu1 + (pp * lv)) is Linear_Combination of I by ZMODUL02: 27;

      then

      reconsider lx = ((lu1 + (pp * lv)) - lu2) as Linear_Combination of I by ZMODUL02: 41;

      

       A22: ( 0. V) = (( Sum (lu1 + (pp * lv))) - ( Sum lu2)) by A3, A17, A11, A16, VECTSP_1: 19, ZMODUL02: 52

      .= ( Sum lx) by ZMODUL02: 55;

      

       A23: (lx . u1) = (((lu1 + (pp * lv)) . u1) - (lu2 . u1)) by ZMODUL02: 39

      .= (((lu1 . u1) + ((pp * lv) . u1)) - (lu2 . u1)) by VECTSP_6: 22

      .= ((( 1. INT.Ring ) + ((pp * lv) . u1)) - ( 0. INT.Ring )) by A1, A7, A12

      .= (( 1. INT.Ring ) + ((pp * lv) . u1));

      (lx . u1) <> 0 by A18, A23;

      then u1 in ( Carrier lx);

      hence contradiction by A22, VECTSP_7:def 3, VECTSP_7:def 1;

    end;

    theorem :: ZMODUL03:22

    

     Th22: for p be prime Element of INT.Ring , V be Z_Module, ZQ be VectSp of ( GF p), vq be Vector of ZQ st ZQ = ( Z_MQ_VectSp (V,p)) holds ex v be Vector of V st vq = ( ZMtoMQV (V,p,v))

    proof

      let p be prime Element of INT.Ring , V be Z_Module, ZQ be VectSp of ( GF p), vq be Vector of ZQ such that

       A1: ZQ = ( Z_MQ_VectSp (V,p));

      vq is Element of ( CosetSet (V,(p (*) V))) by A1, VECTSP10:def 6;

      then vq in the set of all A where A be Coset of (p (*) V);

      then

      consider vqq be Coset of (p (*) V) such that

       A2: vqq = vq;

      consider v be Vector of V such that

       A3: vq = (v + (p (*) V)) by A2, VECTSP_4:def 6;

      take v;

      thus thesis by A3;

    end;

    

     Lm2: for p be prime Element of INT.Ring , V be Z_Module, v,w be Vector of V st (( ZMtoMQV (V,p,w)) /\ ( ZMtoMQV (V,p,v))) <> {} holds ( ZMtoMQV (V,p,w)) = ( ZMtoMQV (V,p,v))

    proof

      let p be prime Element of INT.Ring , V be Z_Module, v,w be Vector of V such that

       A1: (( ZMtoMQV (V,p,w)) /\ ( ZMtoMQV (V,p,v))) <> {} ;

      consider u be object such that

       A2: u in (( ZMtoMQV (V,p,w)) /\ ( ZMtoMQV (V,p,v))) by A1, XBOOLE_0:def 1;

      

       A3: u in ( ZMtoMQV (V,p,w)) & u in ( ZMtoMQV (V,p,v)) by A2, XBOOLE_0:def 4;

      then

      reconsider u as Vector of V;

      (w + (p (*) V)) = (u + (p (*) V)) by A3, ZMODUL01: 67

      .= (v + (p (*) V)) by A3, ZMODUL01: 67;

      hence thesis;

    end;

    theorem :: ZMODUL03:23

    

     Th23: for p be prime Element of INT.Ring , V be Z_Module, I be Subset of V, lq be Linear_Combination of ( Z_MQ_VectSp (V,p)) holds ex l be Linear_Combination of I st for v be Vector of V st v in I holds ex w be Vector of V st w in I & w in ( ZMtoMQV (V,p,v)) & (l . w) = (lq . ( ZMtoMQV (V,p,v)))

    proof

      let p be prime Element of INT.Ring , V be Z_Module, I be Subset of V, lq be Linear_Combination of ( Z_MQ_VectSp (V,p));

      set ZQ = ( Z_MQ_VectSp (V,p));

      per cases ;

        suppose

         A1: I is empty;

        set l = the Linear_Combination of I;

        take l;

        thus thesis by A1;

      end;

        suppose

         A2: I is non empty;

        set X = { ( ZMtoMQV (V,p,v)) where v be Vector of V : v in I };

        now

          let x be object;

          assume x in X;

          then

          consider v be Vector of V such that

           A3: x = ( ZMtoMQV (V,p,v)) & v in I;

          thus x in the carrier of ZQ by A3;

        end;

        then

        reconsider X as Subset of ZQ by TARSKI:def 3;

        consider v0 be object such that

         A4: v0 in I by A2, XBOOLE_0:def 1;

        reconsider v0 as Vector of V by A4;

        ( ZMtoMQV (V,p,v0)) in X by A4;

        then

        reconsider X as non empty Subset of ZQ;

        defpred F0[ Element of X, Element of V] means $2 in $1 & $2 in I;

        

         A5: for x be Element of X holds ex v be Element of V st F0[x, v]

        proof

          let x be Element of X;

          x in X;

          then

          consider v be Vector of V such that

           A6: x = ( ZMtoMQV (V,p,v)) & v in I;

          thus ex v be Element of V st F0[x, v] by A6, ZMODUL01: 58;

        end;

        consider F be Function of X, the carrier of V such that

         A7: for x be Element of X holds F0[x, (F . x)] from FUNCT_2:sch 3( A5);

         A8:

        now

          let y be object;

          assume y in ( rng F);

          then

          consider x be object such that

           A9: x in X & (F . x) = y by FUNCT_2: 11;

          reconsider x as Element of X by A9;

          thus y in I by A9, A7;

        end;

        then

         A10: ( rng F) c= I;

        defpred P[ Element of V, Element of ( GF p)] means ($1 in ( rng F) implies $2 = (lq . ( ZMtoMQV (V,p,$1)))) & ( not $1 in ( rng F) implies $2 = 0 );

        

         A11: for v be Element of V holds ex y be Element of ( GF p) st P[v, y]

        proof

          let v be Element of V;

          per cases ;

            suppose

             A12: v in ( rng F);

            reconsider y = (lq . ( ZMtoMQV (V,p,v))) as Element of ( GF p);

            take y;

            thus thesis by A12;

          end;

            suppose

             A13: not v in ( rng F);

            ( 0. ( GF p)) is Element of ( GF p);

            then

            reconsider F0 = 0 as Element of ( GF p) by EC_PF_1: 11;

            take F0;

            thus thesis by A13;

          end;

        end;

        

         A14: ( Segm p) c= INT by NUMBERS: 17;

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

         A15: for v be Element of V holds P[v, (f . v)] from FUNCT_2:sch 3( A11);

        

         A16: for v be Vector of V st v in I holds ex w be Vector of V st w in I & w in ( ZMtoMQV (V,p,v)) & (f . w) = (lq . ( ZMtoMQV (V,p,v)))

        proof

          let v be Vector of V;

          assume v in I;

          then

           A17: ( ZMtoMQV (V,p,v)) in X;

          then

           A18: (F . ( ZMtoMQV (V,p,v))) in ( rng F) by FUNCT_2: 4;

          reconsider w = (F . ( ZMtoMQV (V,p,v))) as Element of V by A17, FUNCT_2: 5;

          take w;

          

           A19: (f . w) = (lq . ( ZMtoMQV (V,p,w))) by A15, A17, FUNCT_2: 4;

          thus w in I by A18, A8;

          thus w in ( ZMtoMQV (V,p,v)) by A7, A17;

          thus (f . w) = (lq . ( ZMtoMQV (V,p,v))) by A17, A19, A7, ZMODUL01: 67;

        end;

        reconsider l = f as Function of the carrier of V, INT by A14, FUNCT_2: 7;

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

        set T = { v where v be Element of V : (l . v) <> 0 };

         A20:

        now

          let v be object;

          assume v in T;

          then ex v1 be Element of V st v1 = v & (l . v1) <> 0 ;

          hence v in the carrier of V;

        end;

         A21:

        now

          let x be object;

          assume x in T;

          then

          consider v be Element of V such that

           A22: x = v & (l . v) <> 0 ;

          thus x in ( rng F) by A15, A22;

        end;

        then

         A23: T c= ( rng F);

        now

          let x be object;

          assume

           A24: x in (F " T);

          then

           A25: x in X & (F . x) in T by FUNCT_2: 38;

          then

          consider v be Element of V such that

           A26: (F . x) = v & (l . v) <> 0 ;

          

           A27: P[v, (f . v)] by A15;

          (lq . ( ZMtoMQV (V,p,v))) <> ( 0. ( GF p)) by A26, A27, EC_PF_1: 11;

          then

           A28: ( ZMtoMQV (V,p,v)) in ( Carrier lq);

          reconsider w = x as Element of X by A24;

          

           A29: (F . w) in w & (F . w) in I by A7;

          consider v1 be Vector of V such that

           A30: w = ( ZMtoMQV (V,p,v1)) & v1 in I by A25;

          v in ( ZMtoMQV (V,p,v)) by ZMODUL01: 58;

          then (( ZMtoMQV (V,p,v)) /\ ( ZMtoMQV (V,p,v1))) <> {} by A26, A29, A30, XBOOLE_0:def 4;

          hence x in ( Carrier lq) by A28, A30, Lm2;

        end;

        then (F " T) c= ( Carrier lq);

        then

        reconsider T as finite Subset of V by A20, A21, FINSET_1: 9, TARSKI:def 3;

        for v be Element of V st not v in T holds (l . v) = ( 0. INT.Ring );

        then

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

        T = ( Carrier l);

        then

        reconsider l as Linear_Combination of I by A23, A10, XBOOLE_1: 1, VECTSP_6:def 4;

        take l;

        now

          let v be Vector of V;

          assume v in I;

          then ex w be Vector of V st w in I & w in ( ZMtoMQV (V,p,v)) & (f . w) = (lq . ( ZMtoMQV (V,p,v))) by A16;

          hence ex w be Vector of V st w in I & w in ( ZMtoMQV (V,p,v)) & (l . w) = (lq . ( ZMtoMQV (V,p,v)));

        end;

        hence thesis;

      end;

    end;

    theorem :: ZMODUL03:24

    

     Th24: for p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, lq be Linear_Combination of ( Z_MQ_VectSp (V,p)) holds ex l be Linear_Combination of I st for v be Vector of V st v in I holds (l . v) = (lq . ( ZMtoMQV (V,p,v)))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, lq be Linear_Combination of ( Z_MQ_VectSp (V,p));

      consider l be Linear_Combination of I such that

       A1: for v be Vector of V st v in I holds ex w be Vector of V st w in I & w in ( ZMtoMQV (V,p,v)) & (l . w) = (lq . ( ZMtoMQV (V,p,v))) by Th23;

      take l;

      now

        let v be Vector of V;

        assume

         A2: v in I;

        then

        consider w be Vector of V such that

         A3: w in I & w in ( ZMtoMQV (V,p,v)) & (l . w) = (lq . ( ZMtoMQV (V,p,v))) by A1;

        ( ZMtoMQV (V,p,w)) = ( ZMtoMQV (V,p,v)) by A3, ZMODUL01: 67;

        hence (l . v) = (lq . ( ZMtoMQV (V,p,v))) by A2, A3, Th21;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL03:25

    

     Th25: for p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, X be non empty Subset of ( Z_MQ_VectSp (V,p)) st X = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I } holds ex F be Function of X, the carrier of V st (for u be Vector of V st u in I holds (F . ( ZMtoMQV (V,p,u))) = u) & F is one-to-one & ( dom F) = X & ( rng F) = I

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, X be non empty Subset of ( Z_MQ_VectSp (V,p));

      assume

       A1: X = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      set ZQ = ( Z_MQ_VectSp (V,p));

      defpred F0[ Element of X, Element of V] means $2 in $1 & $2 in I;

      

       A2: for x be Element of X holds ex v be Element of V st F0[x, v]

      proof

        let x be Element of X;

        x in X;

        then

        consider v be Vector of V such that

         A3: x = ( ZMtoMQV (V,p,v)) & v in I by A1;

        thus ex v be Element of V st F0[x, v] by A3, ZMODUL01: 58;

      end;

      consider F be Function of X, the carrier of V such that

       A4: for x be Element of X holds F0[x, (F . x)] from FUNCT_2:sch 3( A2);

      take F;

      thus for v be Vector of V st v in I holds (F . ( ZMtoMQV (V,p,v))) = v

      proof

        let v be Vector of V;

        assume

         A5: v in I;

        then ( ZMtoMQV (V,p,v)) in X by A1;

        then

        reconsider w = ( ZMtoMQV (V,p,v)) as Element of X;

        

         A6: (F . w) in w & (F . w) in I by A4;

        ( ZMtoMQV (V,p,(F . w))) = ( ZMtoMQV (V,p,v)) by A4, ZMODUL01: 67;

        hence thesis by A5, A6, Th21;

      end;

      now

        let x1,x2 be object;

        assume

         A7: x1 in X & x2 in X & (F . x1) = (F . x2);

        then

        reconsider x10 = x1, x20 = x2 as Element of X;

        consider v1 be Vector of V such that

         A8: x1 = ( ZMtoMQV (V,p,v1)) & v1 in I by A7, A1;

        consider v2 be Vector of V such that

         A9: x2 = ( ZMtoMQV (V,p,v2)) & v2 in I by A7, A1;

        (F . x10) in ( ZMtoMQV (V,p,v1)) & (F . x10) in ( ZMtoMQV (V,p,v2)) by A7, A8, A9, A4;

        then (F . x10) in (( ZMtoMQV (V,p,v1)) /\ ( ZMtoMQV (V,p,v2))) by XBOOLE_0:def 4;

        hence x1 = x2 by A8, A9, Lm2;

      end;

      hence F is one-to-one by FUNCT_2: 19;

      thus ( dom F) = X by FUNCT_2:def 1;

      now

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A10: x in X & (F . x) = y by FUNCT_2: 11;

        reconsider x as Element of X by A10;

        thus y in I by A10, A4;

      end;

      then

       A11: ( rng F) c= I;

      now

        let y be object;

        assume

         A12: y in I;

        then

        reconsider u = y as Vector of V;

        ( ZMtoMQV (V,p,u)) in X by A12, A1;

        then

        reconsider z = ( ZMtoMQV (V,p,u)) as Element of X;

        

         A13: (F . z) in z & (F . z) in I by A4;

        ( ZMtoMQV (V,p,(F . z))) = ( ZMtoMQV (V,p,u)) by A4, ZMODUL01: 67;

        then (F . z) = u by Th21, A13, A12;

        hence y in ( rng F) by FUNCT_2: 4;

      end;

      then I c= ( rng F);

      hence I = ( rng F) by A11, XBOOLE_0:def 10;

    end;

    theorem :: ZMODUL03:26

    

     Th26: for p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V holds ( card { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I }) = ( card I)

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V;

      set X = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      set ZQ = ( Z_MQ_VectSp (V,p));

      per cases ;

        suppose

         A1: I is empty;

        X = {}

        proof

          assume X <> {} ;

          then

          consider v0 be object such that

           A2: v0 in X by XBOOLE_0:def 1;

          consider u be Vector of V such that

           A3: v0 = ( ZMtoMQV (V,p,u)) & u in I by A2;

          thus contradiction by A3, A1;

        end;

        hence thesis by A1;

      end;

        suppose

         A4: I is non empty;

        now

          let x be object;

          assume x in X;

          then

          consider v be Vector of V such that

           A5: x = ( ZMtoMQV (V,p,v)) & v in I;

          thus x in the carrier of ZQ by A5;

        end;

        then

        reconsider X as Subset of ZQ by TARSKI:def 3;

        consider v0 be object such that

         A6: v0 in I by A4, XBOOLE_0:def 1;

        reconsider v0 as Vector of V by A6;

        ( ZMtoMQV (V,p,v0)) in X by A6;

        then

        reconsider X as non empty Subset of ZQ;

        consider F be Function of X, the carrier of V such that

         A7: (for u be Vector of V st u in I holds (F . ( ZMtoMQV (V,p,u))) = u) & F is one-to-one & ( dom F) = X & ( rng F) = I by Th25;

        thus thesis by A7, CARD_1: 5, WELLORD2:def 4;

      end;

    end;

    theorem :: ZMODUL03:27

    

     Th27: for p be prime Element of INT.Ring , V be free Z_Module holds ( ZMtoMQV (V,p,( 0. V))) = ( 0. ( Z_MQ_VectSp (V,p)))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module;

      

      thus ( 0. ( Z_MQ_VectSp (V,p))) = ( 0. ( VectQuot (V,(p (*) V))))

      .= ( zeroCoset (V,(p (*) V))) by VECTSP10:def 6

      .= ( ZMtoMQV (V,p,( 0. V))) by ZMODUL01: 59;

    end;

    theorem :: ZMODUL03:28

    

     Th28: for p be prime Element of INT.Ring , V be free Z_Module, s,t be Element of V holds (( ZMtoMQV (V,p,s)) + ( ZMtoMQV (V,p,t))) = ( ZMtoMQV (V,p,(s + t)))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, s,t be Element of V;

      set s1 = ( ZMtoMQV (V,p,s)), t1 = ( ZMtoMQV (V,p,t));

      

       A1: ( ZMtoMQV (V,p,s)) = (s + (p (*) V));

      

       A2: ( ZMtoMQV (V,p,t)) = (t + (p (*) V));

      

       A3: (s + (p (*) V)) is Element of ( CosetSet (V,(p (*) V))) by A1, VECTSP10:def 6;

      

       A4: (t + (p (*) V)) is Element of ( CosetSet (V,(p (*) V))) by A2, VECTSP10:def 6;

      

      thus (s1 + t1) = (( addCoset (V,(p (*) V))) . ((s + (p (*) V)),(t + (p (*) V)))) by VECTSP10:def 6

      .= ( ZMtoMQV (V,p,(s + t))) by A3, A4, VECTSP10:def 3;

    end;

    theorem :: ZMODUL03:29

    

     Th29: for p be prime Element of INT.Ring , V be free Z_Module, s be FinSequence of V, t be FinSequence of ( Z_MQ_VectSp (V,p)) st ( len s) = ( len t) & for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & (t . i) = ( ZMtoMQV (V,p,si)) holds ( Sum t) = ( ZMtoMQV (V,p,( Sum s)))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module;

      defpred P[ Nat] means for s be FinSequence of V, t be FinSequence of ( Z_MQ_VectSp (V,p)) st ( len s) = $1 & ( len s) = ( len t) & for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & (t . i) = ( ZMtoMQV (V,p,si)) holds ( Sum t) = ( ZMtoMQV (V,p,( Sum s)));

      

       A1: P[ 0 ]

      proof

        let s be FinSequence of V, t be FinSequence of ( Z_MQ_VectSp (V,p));

        assume that

         A2: ( len s) = 0 & ( len s) = ( len t) and for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & (t . i) = ( ZMtoMQV (V,p,si));

        s = ( <*> the carrier of V) by A2;

        then ( Sum s) = ( 0. V) by RLVECT_1: 43;

        then

         A3: ( ZMtoMQV (V,p,( Sum s))) = ( 0. ( Z_MQ_VectSp (V,p))) by Th27;

        t = ( <*> the carrier of ( Z_MQ_VectSp (V,p))) by A2;

        hence thesis by A3, RLVECT_1: 43;

      end;

      

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

      proof

        let k be Nat;

        assume

         A5: P[k];

        now

          let s be FinSequence of V, t be FinSequence of ( Z_MQ_VectSp (V,p));

          assume that

           A6: ( len s) = (k + 1) & ( len s) = ( len t) and

           A7: for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & (t . i) = ( ZMtoMQV (V,p,si));

          reconsider s1 = (s | k) as FinSequence of V;

          

           A8: ( dom s) = ( Seg (k + 1)) by A6, FINSEQ_1:def 3;

          

           A9: ( dom t) = ( Seg (k + 1)) by A6, FINSEQ_1:def 3;

          

           A10: ( len s1) = k by A6, FINSEQ_1: 59, NAT_1: 11;

          

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

          .= ( Seg k) by A6, FINSEQ_1: 59, NAT_1: 11;

          then

           A12: s1 = (s | ( dom s1)) by FINSEQ_1:def 15;

          reconsider t1 = (t | k) as FinSequence of ( Z_MQ_VectSp (V,p));

          

           A13: ( dom t1) = ( Seg ( len t1)) by FINSEQ_1:def 3

          .= ( Seg k) by A6, FINSEQ_1: 59, NAT_1: 11;

          then

           A14: t1 = (t | ( dom t1)) by FINSEQ_1:def 15;

          k in NAT by ORDINAL1:def 12;

          then

           A15: ( len t1) = k by A13, FINSEQ_1:def 3;

          (s . ( len s)) in ( rng s) by A6, A8, FINSEQ_1: 4, FUNCT_1: 3;

          then

          reconsider vs = (s . ( len s)) as Element of V;

          (t . ( len t)) in ( rng t) by A6, A9, FINSEQ_1: 4, FUNCT_1: 3;

          then

          reconsider vt = (t . ( len t)) as Element of ( Z_MQ_VectSp (V,p));

          

           A16: ( len s1) = k & ( len s1) = ( len t1) by A10, A13, FINSEQ_1:def 3;

          

           A17: for i be Element of NAT st i in ( dom s1) holds ex si be Vector of V st si = (s1 . i) & (t1 . i) = ( ZMtoMQV (V,p,si))

          proof

            let i be Element of NAT ;

            assume

             A18: i in ( dom s1);

            ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5, NAT_1: 11;

            then

            consider si be Vector of V such that

             A19: si = (s . i) & (t . i) = ( ZMtoMQV (V,p,si)) by A7, A11, A8, A18;

            take si;

            thus si = (s1 . i) by A12, A18, A19, FUNCT_1: 49;

            thus (t1 . i) = ( ZMtoMQV (V,p,si)) by A14, A11, A13, A18, A19, FUNCT_1: 49;

          end;

          

           A20: ( Sum t1) = ( ZMtoMQV (V,p,( Sum s1))) by A5, A16, A17;

          

           A21: ( len s) = (( len s1) + 1) by A6, FINSEQ_1: 59, NAT_1: 11;

          consider ssi be Vector of V such that

           A22: ssi = (s . ( len s)) & (t . ( len s)) = ( ZMtoMQV (V,p,ssi)) by A6, A7, A8, FINSEQ_1: 4;

          

          thus ( Sum t) = (( Sum t1) + vt) by A6, A14, A15, RLVECT_1: 38

          .= ( ZMtoMQV (V,p,(( Sum s1) + vs))) by A6, A20, A22, Th28

          .= ( ZMtoMQV (V,p,( Sum s))) by A12, A21, RLVECT_1: 38;

        end;

        hence P[(k + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: ZMODUL03:30

    

     Th30: for p be prime Element of INT.Ring , V be free Z_Module, s be Element of V, a be Element of INT.Ring , b be Element of ( GF p) st a = b holds (b * ( ZMtoMQV (V,p,s))) = ( ZMtoMQV (V,p,(a * s)))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, s be Element of V, a be Element of INT.Ring , b be Element of ( GF p);

      set t = ( ZMtoMQV (V,p,s));

      assume

       A1: a = b;

      

       A2: ( ZMtoMQV (V,p,s)) = (s + (p (*) V));

      reconsider t1 = t as Element of ( VectQuot (V,(p (*) V)));

      

       A3: (s + (p (*) V)) is Element of ( CosetSet (V,(p (*) V))) by A2, VECTSP10:def 6;

      reconsider i = b as Nat;

      

       A4: b = (i mod p) by NAT_1: 44, NAT_D: 24;

      i in INT by INT_1:def 2;

      then

      reconsider i as Element of INT.Ring ;

      

      thus (b * t) = ((i mod p) * t1) by A4, ZMODUL02:def 11

      .= (( lmultCoset (V,(p (*) V))) . ((i mod p),(s + (p (*) V)))) by VECTSP10:def 6

      .= ( ZMtoMQV (V,p,(a * s))) by A1, A4, A3, VECTSP10:def 5;

    end;

    theorem :: ZMODUL03:31

    

     Th31: for p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, l be Linear_Combination of I, IQ be Subset of ( Z_MQ_VectSp (V,p)), lq be Linear_Combination of IQ st IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I } & (for v be Vector of V st v in I holds (l . v) = (lq . ( ZMtoMQV (V,p,v)))) holds ( Sum lq) = ( ZMtoMQV (V,p,( Sum l)))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, l be Linear_Combination of I, IQ be Subset of ( Z_MQ_VectSp (V,p)), lq be Linear_Combination of IQ such that

       A1: IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      assume

       A2: for v be Vector of V st v in I holds (l . v) = (lq . ( ZMtoMQV (V,p,v)));

      per cases ;

        suppose

         A3: I is empty;

        IQ = {}

        proof

          assume IQ <> {} ;

          then

          consider v0 be object such that

           A4: v0 in IQ by XBOOLE_0:def 1;

          consider u be Vector of V such that

           A5: v0 = ( ZMtoMQV (V,p,u)) & u in I by A4, A1;

          thus contradiction by A5, A3;

        end;

        then IQ = ( {} the carrier of ( Z_MQ_VectSp (V,p)));

        then lq = ( ZeroLC ( Z_MQ_VectSp (V,p))) by VECTSP_6: 6;

        then

         A6: ( Sum lq) = ( 0. ( Z_MQ_VectSp (V,p))) by VECTSP_6: 15;

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

        then l = ( ZeroLC V) by ZMODUL02: 12;

        then ( Sum l) = ( 0. V) by ZMODUL02: 19;

        hence ( Sum lq) = ( ZMtoMQV (V,p,( Sum l))) by A6, Th27;

      end;

        suppose I is non empty;

        then

        consider v0 be object such that

         A7: v0 in I by XBOOLE_0:def 1;

        reconsider v0 as Vector of V by A7;

        ( ZMtoMQV (V,p,v0)) in IQ by A7, A1;

        then

        reconsider X = IQ as non empty Subset of ( Z_MQ_VectSp (V,p));

        consider F be Function of X, the carrier of V such that

         A8: (for u be Vector of V st u in I holds (F . ( ZMtoMQV (V,p,u))) = u) & F is one-to-one & ( dom F) = X & ( rng F) = I by Th25, A1;

        consider Gq be FinSequence of ( Z_MQ_VectSp (V,p)) such that

         A9: Gq is one-to-one & ( rng Gq) = ( Carrier lq) & ( Sum lq) = ( Sum (lq (#) Gq)) by VECTSP_6:def 6;

        set n = ( len Gq);

        

         A10: ( dom Gq) = ( Seg n) by FINSEQ_1:def 3;

        

         A11: ( Carrier lq) c= X by VECTSP_6:def 4;

        

         A12: ( dom (F * Gq)) = ( Seg n) by A10, A9, A8, RELAT_1: 27, VECTSP_6:def 4;

        

         A13: ( rng (F * Gq)) c= the carrier of V;

        (F * Gq) is FinSequence by A8, A9, FINSEQ_1: 16, VECTSP_6:def 4;

        then

        reconsider FGq = (F * Gq) as FinSequence of V by A13, FINSEQ_1:def 4;

        for x be object holds x in ( rng FGq) iff x in ( Carrier l)

        proof

          let x be object;

          hereby

            assume x in ( rng FGq);

            then

            consider z be object such that

             A14: z in ( dom FGq) & x = (FGq . z) by FUNCT_1:def 3;

            

             A15: x = (F . (Gq . z)) by A14, FUNCT_1: 12;

            

             A16: z in ( dom Gq) & (Gq . z) in ( dom F) by A14, FUNCT_1: 11;

            then

            consider u be Vector of V such that

             A17: (Gq . z) = ( ZMtoMQV (V,p,u)) & u in I by A1, A8;

            

             A18: (F . (Gq . z)) = u by A8, A17;

            consider w be Element of ( Z_MQ_VectSp (V,p)) such that

             A19: (Gq . z) = w & (lq . w) <> ( 0. ( GF p)) by A9, A16, FUNCT_1: 3, VECTSP_6: 1;

            (l . u) <> ( 0. ( GF p)) by A2, A17, A19;

            then (l . u) <> 0 by EC_PF_1: 11;

            hence x in ( Carrier l) by A15, A18;

          end;

          assume

           A20: x in ( Carrier l);

          then

          reconsider u = x as Vector of V;

          

           A21: (l . u) <> 0 by A20, ZMODUL02: 8;

          

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

          then (lq . ( ZMtoMQV (V,p,u))) <> 0 by A2, A21, A20;

          then (lq . ( ZMtoMQV (V,p,u))) <> ( 0. ( GF p)) by EC_PF_1: 11;

          then

           A23: ( ZMtoMQV (V,p,u)) in ( rng Gq) by A9;

          then

          consider z be object such that

           A24: z in ( dom Gq) & ( ZMtoMQV (V,p,u)) = (Gq . z) by FUNCT_1:def 3;

          

           A25: (F . (Gq . z)) = u by A20, A22, A24, A8;

          

           A26: z in ( dom FGq) by A11, A9, A24, A8, A23, FUNCT_1: 11;

          then (FGq . z) = u by A25, FUNCT_1: 12;

          hence x in ( rng FGq) by A26, FUNCT_1:def 3;

        end;

        then ( rng FGq) = ( Carrier l) by TARSKI: 2;

        then

         A27: ( Sum l) = ( Sum (l (#) FGq)) by A9, A8, VECTSP_6:def 6;

        

         A28: ( len (l (#) FGq)) = ( len FGq) by VECTSP_6:def 5;

        then

         A29: ( len (l (#) FGq)) = n by A12, FINSEQ_1:def 3;

        

         A30: ( len (lq (#) Gq)) = n by VECTSP_6:def 5;

        now

          let i be Element of NAT ;

          assume

           A31: i in ( dom (l (#) FGq));

          then i in ( Seg ( len FGq)) by A28, FINSEQ_1:def 3;

          then

           A32: i in ( dom FGq) by FINSEQ_1:def 3;

          then (FGq . i) in ( rng FGq) by FUNCT_1: 3;

          then

          reconsider v = (FGq . i) as Element of V;

          

           A33: ((l (#) FGq) . i) = ((l . v) * v) by A32, ZMODUL02: 13;

          i in ( Seg n) by A29, A31, FINSEQ_1:def 3;

          then

           A34: i in ( dom Gq) by FINSEQ_1:def 3;

          then

           A35: (Gq . i) in ( rng Gq) by FUNCT_1: 3;

          then

           A36: (Gq . i) in X by A9, A11;

          reconsider w = (Gq . i) as Element of ( Z_MQ_VectSp (V,p)) by A35;

          consider u be Vector of V such that

           A37: (Gq . i) = ( ZMtoMQV (V,p,u)) & u in I by A1, A36;

          (F . (Gq . i)) = u by A8, A37;

          then

           A38: v = u by A32, FUNCT_1: 12;

          ((lq (#) Gq) . i) = ((lq . w) * w) by A34, VECTSP_6: 8

          .= ( ZMtoMQV (V,p,((l . v) * v))) by A2, A37, A38, Th30;

          hence ex si be Vector of V st si = ((l (#) FGq) . i) & ((lq (#) Gq) . i) = ( ZMtoMQV (V,p,si)) by A33;

        end;

        hence ( Sum lq) = ( ZMtoMQV (V,p,( Sum l))) by A9, A27, A29, A30, Th29;

      end;

    end;

    theorem :: ZMODUL03:32

    

     Th32: for p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, IQ be Subset of ( Z_MQ_VectSp (V,p)) st IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I } holds IQ is linearly-independent

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, IQ be Subset of ( Z_MQ_VectSp (V,p)) such that

       A1: IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      assume not IQ is linearly-independent;

      then

      consider lq be Linear_Combination of IQ such that

       A2: ( Sum lq) = ( 0. ( Z_MQ_VectSp (V,p))) and

       A3: ( Carrier lq) <> {} ;

      consider Lq be Linear_Combination of ( Z_MQ_VectSp (V,p)) such that

       A4: Lq = lq;

      consider l be Linear_Combination of I such that

       A5: for v be Vector of V st v in I holds (l . v) = (Lq . ( ZMtoMQV (V,p,v))) by Th24;

      set vq0 = ( Sum Lq);

      set v0 = ( Sum l);

      

       A6: vq0 = ( ZMtoMQV (V,p,v0)) by A1, A5, A4, Th31;

      

       A7: vq0 = ( 0. ( VectQuot (V,(p (*) V)))) by A2, A4

      .= ( zeroCoset (V,(p (*) V))) by VECTSP10:def 6

      .= (( 0. V) + (p (*) V)) by ZMODUL01: 59;

      consider vp be Vector of V such that

       A8: vp in (p (*) V) & (v0 + vp) = ( 0. V) by A6, A7, ZMODUL01: 75;

      reconsider pp = p as Element of INT.Ring ;

      vp in the set of all (pp * v) where v be Element of V by A8;

      then

      consider vv be Element of V such that

       A9: vp = (pp * vv);

      

       A10: I is linearly-independent & ( Lin I) = the ModuleStr of V by VECTSP_7:def 3;

      consider lvv be Linear_Combination of I such that

       A11: vv = ( Sum lvv) by A10, STRUCT_0:def 5, ZMODUL02: 64;

      vp = ( Sum (p * lvv)) by A9, A11, ZMODUL02: 53;

      then

       A12: ( 0. V) = ( Sum (l + (p * lvv))) by A8, ZMODUL02: 52;

      reconsider pp = p as Element of INT.Ring ;

      (p * lvv) is Linear_Combination of I by ZMODUL02: 31;

      then (l + (pp * lvv)) is Linear_Combination of I by ZMODUL02: 27;

      then

      consider lpv be Linear_Combination of I such that

       A13: lpv = (l + (pp * lvv));

      ex vq be object st vq in ( Carrier lq) by A3, XBOOLE_0:def 1;

      then

      consider uq be Vector of ( Z_MQ_VectSp (V,p)) such that

       A14: uq in ( Carrier lq);

      uq in { v where v be Element of ( Z_MQ_VectSp (V,p)) : (lq . v) <> ( 0. ( GF p)) } by A14;

      then

      consider uuq be Vector of ( Z_MQ_VectSp (V,p)) such that

       A15: uuq = uq & (lq . uuq) <> ( 0. ( GF p));

      

       A16: (lq . uuq) <> 0 by A15;

      ( Carrier lq) c= IQ by VECTSP_6:def 4;

      then uq in IQ by A14;

      then

      consider uu be Vector of V such that

       A17: uq = ( ZMtoMQV (V,p,uu)) & uu in I by A1;

      

       A18: (lq . uuq) = (l . uu) by A4, A5, A15, A17;

      (lpv . uu) <> ( 0. INT.Ring )

      proof

        assume

         A19: (lpv . uu) = ( 0. INT.Ring );

        ((l + (pp * lvv)) . uu) = ((l . uu) + ((pp * lvv) . uu)) by VECTSP_6: 22

        .= ((l . uu) + (pp * (lvv . uu))) by VECTSP_6:def 9;

        then ( 0. INT.Ring ) = ((l . uu) + (pp * (lvv . uu))) by A13, A19;

        then (l . uu) = ( - (pp * (lvv . uu)));

        then (l . uu) = (pp * ( - (lvv . uu)));

        then pp divides (l . uu) by INT_1:def 3;

        then

         A20: ((l . uu) mod p) = 0 by INT_1: 62;

        thus contradiction by A16, A18, A20, NAT_1: 44, NAT_D: 63;

      end;

      then uu in ( Carrier lpv);

      hence contradiction by A12, A13, VECTSP_7:def 3, VECTSP_7:def 1;

    end;

    

     Lm3: for p be Prime, i be Element of INT holds (i mod p) is Element of ( GF p)

    proof

      let p be Prime, i be Element of INT ;

      (i mod p) in NAT by INT_1: 3, INT_1: 57;

      hence thesis by INT_1: 58, NAT_1: 44;

    end;

    

     Lm4: for p be prime Element of INT.Ring , V be free Z_Module, i be Element of INT.Ring , v be Element of V holds ( ZMtoMQV (V,p,((i mod p) * v))) = ( ZMtoMQV (V,p,(i * v)))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, i be Element of INT.Ring , v be Element of V;

      reconsider a = (i mod p) as Element of ( GF p) by Lm3;

      reconsider t1 = ( ZMtoMQV (V,p,v)) as Element of ( VectQuot (V,(p (*) V)));

      ( ZMtoMQV (V,p,v)) = (v + (p (*) V));

      then

       A1: (v + (p (*) V)) is Element of ( CosetSet (V,(p (*) V))) by VECTSP10:def 6;

      

      thus ( ZMtoMQV (V,p,((i mod p) * v))) = (a * ( ZMtoMQV (V,p,v))) by Th30

      .= ((i mod p) * t1) by ZMODUL02:def 11

      .= (i * t1) by ZMODUL02: 2

      .= (( lmultCoset (V,(p (*) V))) . (i,(v + (p (*) V)))) by VECTSP10:def 6

      .= ( ZMtoMQV (V,p,(i * v))) by A1, VECTSP10:def 5;

    end;

    theorem :: ZMODUL03:33

    

     Th33: for p be prime Element of INT.Ring , V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp (V,p)) st IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I } holds (for s be FinSequence of V st (for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & ( ZMtoMQV (V,p,si)) in ( Lin IQ)) holds ( ZMtoMQV (V,p,( Sum s))) in ( Lin IQ))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Subset of V, IQ be Subset of ( Z_MQ_VectSp (V,p));

      assume IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      defpred P[ Nat] means for s be FinSequence of V st ( len s) = $1 & (for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & ( ZMtoMQV (V,p,si)) in ( Lin IQ)) holds ( ZMtoMQV (V,p,( Sum s))) in ( Lin IQ);

      

       A1: P[ 0 ]

      proof

        let s be FinSequence of V;

        assume that

         A2: ( len s) = 0 and for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & ( ZMtoMQV (V,p,si)) in ( Lin IQ);

        s = ( <*> the carrier of V) by A2;

        then ( Sum s) = ( 0. V) by RLVECT_1: 43;

        then ( ZMtoMQV (V,p,( Sum s))) = ( 0. ( Z_MQ_VectSp (V,p))) by Th27;

        hence thesis by VECTSP_4: 17;

      end;

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

        now

          let s be FinSequence of V;

          assume that

           A5: ( len s) = (k + 1) and

           A6: for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & ( ZMtoMQV (V,p,si)) in ( Lin IQ);

          reconsider s1 = (s | k) as FinSequence of V;

          

           A7: ( dom s) = ( Seg (k + 1)) by A5, FINSEQ_1:def 3;

          

           A8: ( len s1) = k by A5, FINSEQ_1: 59, NAT_1: 11;

          

           A9: ( dom s1) = ( Seg ( len s1)) by FINSEQ_1:def 3

          .= ( Seg k) by A5, FINSEQ_1: 59, NAT_1: 11;

          then

           A10: s1 = (s | ( dom s1)) by FINSEQ_1:def 15;

          (s . ( len s)) in ( rng s) by A5, A7, FINSEQ_1: 4, FUNCT_1: 3;

          then

          reconsider vs = (s . ( len s)) as Element of V;

          

           A11: ( len s1) = k by A5, FINSEQ_1: 59, NAT_1: 11;

          

           A12: for i be Element of NAT st i in ( dom s1) holds ex si be Vector of V st si = (s1 . i) & ( ZMtoMQV (V,p,si)) in ( Lin IQ)

          proof

            let i be Element of NAT ;

            assume

             A13: i in ( dom s1);

            ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5, NAT_1: 11;

            then

            consider si be Vector of V such that

             A14: si = (s . i) & ( ZMtoMQV (V,p,si)) in ( Lin IQ) by A6, A9, A7, A13;

            take si;

            thus si = (s1 . i) by A10, A13, A14, FUNCT_1: 49;

            thus thesis by A14;

          end;

          

           A15: ( ZMtoMQV (V,p,( Sum s1))) in ( Lin IQ) by A4, A11, A12;

          consider ssi be Vector of V such that

           A16: ssi = (s . ( len s)) & ( ZMtoMQV (V,p,ssi)) in ( Lin IQ) by A5, A6, A7, FINSEQ_1: 4;

          ( ZMtoMQV (V,p,( Sum s))) = ( ZMtoMQV (V,p,(( Sum s1) + vs))) by A5, A10, A8, RLVECT_1: 38

          .= (( ZMtoMQV (V,p,( Sum s1))) + ( ZMtoMQV (V,p,vs))) by Th28;

          hence ( ZMtoMQV (V,p,( Sum s))) in ( Lin IQ) by A15, A16, VECTSP_4: 20;

        end;

        hence P[(k + 1)];

      end;

      

       A17: for k be Nat holds P[k] from NAT_1:sch 2( A1, A3);

      now

        let s be FinSequence of V;

        assume

         A18: for i be Element of NAT st i in ( dom s) holds ex si be Vector of V st si = (s . i) & ( ZMtoMQV (V,p,si)) in ( Lin IQ);

        ( len s) = ( len s);

        hence ( ZMtoMQV (V,p,( Sum s))) in ( Lin IQ) by A17, A18;

      end;

      hence thesis;

    end;

    theorem :: ZMODUL03:34

    

     Th34: for p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, IQ be Subset of ( Z_MQ_VectSp (V,p)), l be Linear_Combination of I st IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I } holds ( ZMtoMQV (V,p,( Sum l))) in ( Lin IQ)

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, IQ be Subset of ( Z_MQ_VectSp (V,p)), l be Linear_Combination of I;

      assume

       A1: IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      consider G be FinSequence of V such that

       A2: G is one-to-one & ( rng G) = ( Carrier l) & ( Sum l) = ( Sum (l (#) G)) by VECTSP_6:def 6;

      now

        let i be Element of NAT ;

        assume i in ( dom (l (#) G));

        then i in ( Seg ( len (l (#) G))) by FINSEQ_1:def 3;

        then i in ( Seg ( len G)) by VECTSP_6:def 5;

        then

         A3: i in ( dom G) by FINSEQ_1:def 3;

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

        then

        reconsider v = (G . i) as Element of V;

        

         A4: ((l (#) G) . i) = ((l . v) * v) by A3, ZMODUL02: 13;

        reconsider b = ((l . v) mod p) as Element of ( GF p) by Lm3;

        reconsider a = ((l . v) mod p) as Element of INT.Ring ;

        reconsider k = (l . v) as Element of INT.Ring ;

        reconsider t = ( ZMtoMQV (V,p,v)) as Element of ( Z_MQ_VectSp (V,p));

        

         A5: (b * t) = ( ZMtoMQV (V,p,(a * v))) by Th30

        .= ( ZMtoMQV (V,p,(k * v))) by Lm4;

        

         A6: v in ( Carrier l) by A3, A2, FUNCT_1: 3;

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

        then t in IQ by A1, A6;

        then (b * t) in ( Lin IQ) by VECTSP_4: 21, VECTSP_7: 8;

        hence ex si be Vector of V st si = ((l (#) G) . i) & ( ZMtoMQV (V,p,si)) in ( Lin IQ) by A5, A4;

      end;

      hence ( ZMtoMQV (V,p,( Sum l))) in ( Lin IQ) by A1, A2, Th33;

    end;

    theorem :: ZMODUL03:35

    

     Th35: for p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, IQ be Subset of ( Z_MQ_VectSp (V,p)) st IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I } holds IQ is Basis of ( Z_MQ_VectSp (V,p))

    proof

      let p be prime Element of INT.Ring , V be free Z_Module, I be Basis of V, IQ be Subset of ( Z_MQ_VectSp (V,p));

      assume

       A1: IQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in I };

      

       A2: IQ is linearly-independent by Th32, A1;

      for vq be Element of ( Z_MQ_VectSp (V,p)) holds vq in ( Lin IQ)

      proof

        let vq be Element of ( Z_MQ_VectSp (V,p));

        consider v be Vector of V such that

         A3: vq = ( ZMtoMQV (V,p,v)) by Th22;

        I is base;

        then ( Lin I) = the ModuleStr of V;

        then

        consider l be Linear_Combination of I such that

         A4: v = ( Sum l) by STRUCT_0:def 5, ZMODUL02: 64;

        thus vq in ( Lin IQ) by A1, A4, A3, Th34;

      end;

      then ( Lin IQ) = the ModuleStr of ( Z_MQ_VectSp (V,p)) by VECTSP_4: 32;

      then IQ is base by A2;

      hence thesis;

    end;

    registration

      let p be prime Element of INT.Ring , V be finite-rank free Z_Module;

      cluster ( Z_MQ_VectSp (V,p)) -> finite-dimensional;

      coherence

      proof

        set W = ( Z_MQ_VectSp (V,p));

        set A = the Basis of V;

        set AQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in A };

        now

          let x be object;

          assume x in AQ;

          then ex u be Vector of V st x = ( ZMtoMQV (V,p,u)) & u in A;

          hence x in the carrier of ( Z_MQ_VectSp (V,p));

        end;

        then

        reconsider AQ as Subset of W by TARSKI:def 3;

        ( card A) = ( card AQ) by Th26;

        then AQ is finite Subset of W;

        hence thesis by Th35, MATRLIN:def 1;

      end;

    end

    theorem :: ZMODUL03:36

    

     Th36: for V be finite-rank free Z_Module holds for A,B be Basis of V holds ( card A) = ( card B)

    proof

      let V be finite-rank free Z_Module;

      let A,B be Basis of V;

      set p = the prime Element of INT.Ring ;

      set AQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in A };

      now

        let x be object;

        assume x in AQ;

        then ex u be Vector of V st x = ( ZMtoMQV (V,p,u)) & u in A;

        hence x in the carrier of ( Z_MQ_VectSp (V,p));

      end;

      then

      reconsider AQ as Subset of ( Z_MQ_VectSp (V,p)) by TARSKI:def 3;

      set BQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in B };

      now

        let x be object;

        assume x in BQ;

        then ex u be Vector of V st x = ( ZMtoMQV (V,p,u)) & u in B;

        hence x in the carrier of ( Z_MQ_VectSp (V,p));

      end;

      then

      reconsider BQ as Subset of ( Z_MQ_VectSp (V,p)) by TARSKI:def 3;

      

       A1: ( card A) = ( card AQ) by Th26;

      

       A2: ( card B) = ( card BQ) by Th26;

      

       A3: AQ is Basis of ( Z_MQ_VectSp (V,p)) by Th35;

      BQ is Basis of ( Z_MQ_VectSp (V,p)) by Th35;

      hence ( card A) = ( card B) by A1, A2, A3, VECTSP_9: 22;

    end;

    definition

      let V be finite-rank free Z_Module;

      :: ZMODUL03:def5

      func rank (V) -> Nat means

      : Def5: for I be Basis of V holds it = ( card I);

      existence

      proof

        consider A be finite Subset of V such that

         A1: A is Basis of V by Def3;

        consider n be Nat such that

         A2: n = ( card A);

        for I be Basis of V holds ( card I) = n by A1, A2, Th36;

        hence thesis;

      end;

      uniqueness

      proof

        let n,m be Nat;

        assume that

         A3: for I be Basis of V holds ( card I) = n and

         A4: for I be Basis of V holds ( card I) = m;

        consider A be finite Subset of V such that

         A5: A is Basis of V by Def3;

        ( card A) = n by A3, A5;

        hence thesis by A4, A5;

      end;

    end

    theorem :: ZMODUL03:37

    for p be prime Element of INT.Ring , V be finite-rank free Z_Module holds ( rank V) = ( dim ( Z_MQ_VectSp (V,p)))

    proof

      let p be prime Element of INT.Ring , V be finite-rank free Z_Module;

      set W = ( Z_MQ_VectSp (V,p));

      set A = the Basis of V;

      set AQ = { ( ZMtoMQV (V,p,u)) where u be Vector of V : u in A };

      now

        let x be object;

        assume x in AQ;

        then ex u be Vector of V st x = ( ZMtoMQV (V,p,u)) & u in A;

        hence x in the carrier of ( Z_MQ_VectSp (V,p));

      end;

      then

      reconsider AQ as Subset of W by TARSKI:def 3;

      

       A1: ( card A) = ( card AQ) by Th26;

      AQ is Basis of W by Th35;

      then ( dim W) = ( card AQ) by VECTSP_9:def 1;

      hence thesis by A1, Def5;

    end;