zmatrlin.miz



    begin

    reserve x,y,z for object,

i,j,k,l,n,m for Nat,

D,E for non empty set;

    reserve M for Matrix of D;

    reserve L for Matrix of E;

    theorem :: ZMATRLIN:1

    

     EQ2: for i,j be Nat st M = L & [i, j] in ( Indices M) holds (M * (i,j)) = (L * (i,j))

    proof

      let i,j be Nat;

      assume

       AS1: M = L & [i, j] in ( Indices M);

      then

      consider p be FinSequence of D such that

       A1: p = (M . i) & (M * (i,j)) = (p . j) by MATRIX_0:def 5;

      consider q be FinSequence of E such that

       A2: q = (L . i) & (L * (i,j)) = (q . j) by MATRIX_0:def 5, AS1;

      thus (M * (i,j)) = (L * (i,j)) by AS1, A1, A2;

    end;

    theorem :: ZMATRLIN:2

    for i be Nat st M = L & i in ( dom M) holds ( Line (M,i)) = ( Line (L,i))

    proof

      let i be Nat;

      assume

       AS1: M = L & i in ( dom M);

      

       A1: ( len ( Line (M,i))) = ( width M) & for j st j in ( Seg ( width M)) holds (( Line (M,i)) . j) = (M * (i,j)) by MATRIX_0:def 7;

      

       A2: ( len ( Line (L,i))) = ( width L) & for j st j in ( Seg ( width L)) holds (( Line (L,i)) . j) = (L * (i,j)) by MATRIX_0:def 7;

      

       A3: ( dom ( Line (M,i))) = ( Seg ( width M)) by A1, FINSEQ_1:def 3

      .= ( dom ( Line (L,i))) by AS1, A2, FINSEQ_1:def 3;

      for j st j in ( dom ( Line (M,i))) holds (( Line (M,i)) . j) = (( Line (L,i)) . j)

      proof

        let j;

        assume j in ( dom ( Line (M,i)));

        then

         A4: j in ( Seg ( width M)) by FINSEQ_1:def 3, A1;

        then [i, j] in ( Indices M) by AS1, ZFMISC_1: 87;

        then

         A5: (M * (i,j)) = (L * (i,j)) by AS1, EQ2;

        

        thus (( Line (M,i)) . j) = (M * (i,j)) by A4, MATRIX_0:def 7

        .= (( Line (L,i)) . j) by AS1, A4, A5, MATRIX_0:def 7;

      end;

      hence thesis by A3;

    end;

    theorem :: ZMATRLIN:3

    for i be Nat st M = L & i in ( Seg ( width M)) holds ( Col (M,i)) = ( Col (L,i))

    proof

      let i be Nat;

      assume

       AS1: M = L & i in ( Seg ( width M));

      

       A1: ( len ( Col (M,i))) = ( len M) & for j st j in ( dom M) holds (( Col (M,i)) . j) = (M * (j,i)) by MATRIX_0:def 8;

      

       A2: ( len ( Col (L,i))) = ( len L) & for j st j in ( dom L) holds (( Col (L,i)) . j) = (L * (j,i)) by MATRIX_0:def 8;

      

       A3: ( dom ( Col (M,i))) = ( Seg ( len M)) by A1, FINSEQ_1:def 3

      .= ( dom ( Col (L,i))) by AS1, A2, FINSEQ_1:def 3;

      for j st j in ( dom ( Col (M,i))) holds (( Col (M,i)) . j) = (( Col (L,i)) . j)

      proof

        let j;

        assume j in ( dom ( Col (M,i)));

        then j in ( Seg ( len M)) by FINSEQ_1:def 3, A1;

        then

         A4: j in ( dom M) by FINSEQ_1:def 3;

        then [j, i] in ( Indices M) by AS1, ZFMISC_1: 87;

        then

         A5: (M * (j,i)) = (L * (j,i)) by AS1, EQ2;

        

        thus (( Col (M,i)) . j) = (M * (j,i)) by A4, MATRIX_0:def 8

        .= (( Col (L,i)) . j) by AS1, A4, A5, MATRIX_0:def 8;

      end;

      hence thesis by A3;

    end;

    theorem :: ZMATRLIN:4

    

     EQ40: ( len M) = ( len L) & ( width M) = ( width L) & (for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) = (L * (i,j))) implies M = L

    proof

      assume that

       A1: ( len M) = ( len L) and

       A2: ( width M) = ( width L) and

       A3: for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) = (L * (i,j));

      M is Matrix of E

      proof

        consider n be Nat such that

         A0: for x be object st x in ( rng M) holds ex p be FinSequence of D st x = p & ( len p) = n by MATRIX_0: 9;

        per cases ;

          suppose ( len M) = 0 ;

          then M = {} ;

          then ( rng M) c= (E * );

          hence thesis by FINSEQ_1:def 4;

        end;

          suppose

           I0: ( len M) <> 0 ;

          for x be object st x in ( rng M) holds ex p be FinSequence of E st x = p & ( len p) = n

          proof

            let x be object;

            assume

             S1: x in ( rng M);

            then

            consider p be FinSequence of D such that

             S3: x = p & ( len p) = n by A0;

            

             X1: ( width M) = n by S1, S3, MATRIX_0:def 3, I0;

            for z be object st z in ( rng p) holds z in E

            proof

              let z be object;

              assume z in ( rng p);

              then

              consider j1 be object such that

               S4: j1 in ( dom p) & z = (p . j1) by FUNCT_1:def 3;

              

               S5: j1 in ( Seg n) by S3, S4, FINSEQ_1:def 3;

              reconsider j1 as Nat by S4;

              consider i1 be object such that

               S6: i1 in ( dom M) & x = (M . i1) by S1, FUNCT_1:def 3;

              reconsider i1 as Nat by S6;

              

               S8: [i1, j1] in ( Indices M) by S6, S5, X1, ZFMISC_1: 87;

              then

              consider q be FinSequence of D such that

               S9: q = (M . i1) & (M * (i1,j1)) = (q . j1) by MATRIX_0:def 5;

              (M * (i1,j1)) = (L * (i1,j1)) by A3, S8;

              hence z in E by S3, S4, S6, S9;

            end;

            then ( rng p) c= E;

            then

            reconsider p as FinSequence of E by FINSEQ_1:def 4;

            take p;

            thus x = p & ( len p) = n by S3;

          end;

          hence M is Matrix of E by MATRIX_0: 9;

        end;

      end;

      then

      reconsider L0 = M as Matrix of E;

      for i,j be Nat st [i, j] in ( Indices L0) holds (L0 * (i,j)) = (L * (i,j))

      proof

        let i,j be Nat;

        assume

         X3: [i, j] in ( Indices L0);

        then

        consider q be FinSequence of D such that

         S9: q = (M . i) & (M * (i,j)) = (q . j) by MATRIX_0:def 5;

        consider p be FinSequence of E such that

         T9: p = (L0 . i) & (L0 * (i,j)) = (p . j) by MATRIX_0:def 5, X3;

        thus (L0 * (i,j)) = (L * (i,j)) by A3, S9, T9, X3;

      end;

      hence thesis by A1, A2, MATRIX_0: 21;

    end;

    theorem :: ZMATRLIN:5

    

     REALTOINT: for M be Matrix of D st for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) in E holds M is Matrix of E

    proof

      let M be Matrix of D;

      assume

       AS: for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) in E;

      consider n be Nat such that

       A0: for x be object st x in ( rng M) holds ex p be FinSequence of D st x = p & ( len p) = n by MATRIX_0: 9;

      per cases ;

        suppose ( len M) = 0 ;

        then M = {} ;

        then ( rng M) c= (E * );

        hence thesis by FINSEQ_1:def 4;

      end;

        suppose

         I0: ( len M) <> 0 ;

        for x be object st x in ( rng M) holds ex p be FinSequence of E st x = p & ( len p) = n

        proof

          let x be object;

          assume

           S1: x in ( rng M);

          then

          consider p be FinSequence of D such that

           S3: x = p & ( len p) = n by A0;

          

           X1: ( width M) = n by S1, S3, MATRIX_0:def 3, I0;

          for z be object st z in ( rng p) holds z in E

          proof

            let z be object;

            assume z in ( rng p);

            then

            consider j1 be object such that

             S4: j1 in ( dom p) & z = (p . j1) by FUNCT_1:def 3;

            

             S5: j1 in ( Seg n) by S3, S4, FINSEQ_1:def 3;

            reconsider j1 as Nat by S4;

            consider i1 be object such that

             S6: i1 in ( dom M) & x = (M . i1) by S1, FUNCT_1:def 3;

            reconsider i1 as Nat by S6;

            

             S8: [i1, j1] in ( Indices M) by S6, S5, X1, ZFMISC_1: 87;

            then

            consider q be FinSequence of D such that

             S9: q = (M . i1) & (M * (i1,j1)) = (q . j1) by MATRIX_0:def 5;

            thus z in E by AS, S3, S4, S6, S8, S9;

          end;

          then ( rng p) c= E;

          then

          reconsider p as FinSequence of E by FINSEQ_1:def 4;

          take p;

          thus x = p & ( len p) = n by S3;

        end;

        hence M is Matrix of E by MATRIX_0: 9;

      end;

    end;

    theorem :: ZMATRLIN:6

    M = L implies (M @ ) = (L @ )

    proof

      assume

       AS: M = L;

      for i,j be Nat st [i, j] in ( Indices (M @ )) holds ((M @ ) * (i,j)) in E

      proof

        let i,j be Nat;

        assume [i, j] in ( Indices (M @ ));

        then

         A2: [j, i] in ( Indices M) by MATRIX_0:def 6;

        

        then ((M @ ) * (i,j)) = (M * (j,i)) by MATRIX_0:def 6

        .= (L * (j,i)) by AS, A2, EQ2;

        hence ((M @ ) * (i,j)) in E;

      end;

      then

      reconsider M1 = (M @ ) as Matrix of E by REALTOINT;

      

       P1: ( len M1) = ( width L) by AS, MATRIX_0:def 6;

      

       P2: for i,j be Nat holds [i, j] in ( Indices M1) iff [j, i] in ( Indices L) by AS, MATRIX_0:def 6;

      for i,j be Nat st [j, i] in ( Indices L) holds (M1 * (i,j)) = (L * (j,i))

      proof

        let i,j be Nat;

        assume

         A2: [j, i] in ( Indices L);

        then [i, j] in ( Indices (M @ )) by AS, MATRIX_0:def 6;

        

        then (M1 * (i,j)) = ((M @ ) * (i,j)) by EQ2

        .= (M * (j,i)) by AS, A2, MATRIX_0:def 6;

        hence (M1 * (i,j)) = (L * (j,i)) by AS, A2, EQ2;

      end;

      hence thesis by P1, P2, MATRIX_0:def 6;

    end;

    theorem :: ZMATRLIN:7

    

     INTTOREAL: for M be Matrix of INT holds M is Matrix of REAL

    proof

      let M be Matrix of INT ;

      ( INT * ) c= ( REAL * ) by NUMBERS: 15, FINSEQ_1: 62;

      then ( rng M) c= ( REAL * );

      hence thesis by FINSEQ_1:def 4;

    end;

    definition

      let M be Matrix of INT ;

      :: ZMATRLIN:def1

      func inttorealM (M) -> Matrix of REAL equals M;

      correctness by INTTOREAL;

    end

    definition

      let n,m be Nat;

      let M be Matrix of n, m, INT ;

      :: original: inttorealM

      redefine

      func inttorealM (M) -> Matrix of n, m, REAL ;

      correctness

      proof

        

         B2: ( len M) = n by MATRIX_0: 25;

        per cases ;

          suppose

           X11: not 0 < n;

          then

           X1: n = 0 ;

          M = {} by B2, X11;

          hence ( inttorealM M) is Matrix of n, m, REAL by X1, MATRIX_0: 13;

        end;

          suppose

           X2: 0 < n;

          then ( width M) = m by B2, MATRIX_0: 20;

          hence ( inttorealM M) is Matrix of n, m, REAL by X2, B2, MATRIX_0: 20;

        end;

      end;

    end

    definition

      let n be Nat;

      let M be Matrix of n, INT ;

      :: original: inttorealM

      redefine

      func inttorealM (M) -> Matrix of n, REAL ;

      correctness

      proof

        ( inttorealM M) is Matrix of n, n, REAL ;

        hence thesis;

      end;

    end

    definition

      let M be Matrix of REAL ;

      :: ZMATRLIN:def2

      attr M is integer means M is Matrix of INT ;

    end

    registration

      cluster integer for Matrix of REAL ;

      correctness

      proof

        set M = the Matrix of INT ;

        reconsider L = ( inttorealM M) as Matrix of REAL ;

        take L;

        thus L is Matrix of INT ;

      end;

    end

    registration

      let n,m be Nat;

      cluster integer for Matrix of n, m, REAL ;

      correctness

      proof

        set M = the Matrix of n, m, INT ;

        reconsider L = ( inttorealM M) as Matrix of n, m, REAL ;

        take L;

        thus thesis;

      end;

    end

    definition

      let M be integer Matrix of REAL ;

      :: ZMATRLIN:def3

      func realtointM (M) -> Matrix of INT equals M;

      correctness

      proof

        M is integer;

        then

        reconsider L = M as Matrix of INT ;

        L = M;

        hence thesis;

      end;

    end

    definition

      let n,m be Nat;

      let M be integer Matrix of n, m, REAL ;

      :: original: realtointM

      redefine

      func realtointM (M) -> Matrix of n, m, INT ;

      correctness

      proof

        

         B2: ( len M) = n by MATRIX_0: 25;

        per cases ;

          suppose

           X11: not 0 < n;

          then

           X1: n = 0 ;

          M = {} by B2, X11;

          hence ( realtointM M) is Matrix of n, m, INT by X1, MATRIX_0: 13;

        end;

          suppose

           X2: 0 < n;

          then ( width M) = m by B2, MATRIX_0: 20;

          hence ( realtointM M) is Matrix of n, m, INT by X2, B2, MATRIX_0: 20;

        end;

      end;

    end

    definition

      let n be Nat;

      let M be integer Matrix of n, REAL ;

      :: original: realtointM

      redefine

      func realtointM (M) -> Matrix of n, INT ;

      correctness

      proof

        ( realtointM M) is Matrix of n, n, INT ;

        hence thesis;

      end;

    end

    definition

      let n,m be Nat;

      :: ZMATRLIN:def4

      func 0. (n,m) -> Matrix of n, m, INT.Ring equals (n |-> (m |-> ( 0. INT.Ring )));

      correctness by MATRIX_0: 10;

    end

    begin

    reserve k,t,i,j,m,n for Nat,

D for non empty set;

    reserve V for free Z_Module;

    reserve a for Element of INT.Ring ,

W for Element of V;

    reserve KL1,KL2,KL3 for Linear_Combination of V,

X for Subset of V;

    

     Th5: X is linearly-independent & ( Carrier KL1) c= X & ( Carrier KL2) c= X & ( Sum KL1) = ( Sum KL2) implies KL1 = KL2 by ZMODUL03: 3;

    theorem :: ZMATRLIN:8

    

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

    proof

      assume that

       A1: X is linearly-independent & ( Carrier KL1) c= X and

       A2: ( Carrier KL2) c= X & ( Carrier KL3) c= X and

       A3: ( Sum KL1) = (( Sum KL2) + ( Sum KL3));

      ( Carrier (KL2 + KL3)) c= (( Carrier KL2) \/ ( Carrier KL3)) & (( Carrier KL2) \/ ( Carrier KL3)) c= X by A2, ZMODUL02: 26, XBOOLE_1: 8;

      then

       A4: ( Carrier (KL2 + KL3)) c= X;

      ( Sum KL1) = ( Sum (KL2 + KL3)) by A3, ZMODUL02: 52;

      hence thesis by A1, A4, Th5;

    end;

    theorem :: ZMATRLIN:9

    

     Th7: X is linearly-independent & ( Carrier KL1) c= X & ( Carrier KL2) c= X & a <> ( 0. INT.Ring ) & ( Sum KL1) = (a * ( Sum KL2)) implies KL1 = (a * KL2)

    proof

      assume that

       A1: X is linearly-independent & ( Carrier KL1) c= X and

       A2: ( Carrier KL2) c= X & a <> ( 0. INT.Ring ) & ( Sum KL1) = (a * ( Sum KL2));

      ( Carrier (a * KL2)) c= X & ( Sum KL1) = ( Sum (a * KL2)) by A2, ZMODUL02: 29, ZMODUL02: 53;

      hence thesis by A1, Th5;

    end;

    reserve V for finite-rank free Z_Module,

W for Element of V;

    reserve KL1,KL2,KL3 for Linear_Combination of V,

X for Subset of V;

    theorem :: ZMATRLIN:10

    

     Th8: for b2 be Basis of V holds ex KL be Linear_Combination of V st W = ( Sum KL) & ( Carrier KL) c= b2

    proof

      let b2 be Basis of V;

      W in the ModuleStr of V;

      then W in ( Lin b2) by VECTSP_7:def 3;

      then

      consider KL1 be Linear_Combination of b2 such that

       A1: W = ( Sum KL1) by ZMODUL02: 64;

      take KL = KL1;

      thus W = ( Sum KL) by A1;

      thus thesis by VECTSP_6:def 4;

    end;

    definition

      let V be finite-rank free Z_Module;

      :: ZMATRLIN:def5

      mode OrdBasis of V -> FinSequence of V means

      : defOrdBasis: it is one-to-one & ( rng it ) is Basis of V;

      existence

      proof

        consider A be finite Subset of V such that

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

        consider p be FinSequence such that

         A2: ( rng p) = A and

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

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

        take f = p;

        thus f is one-to-one by A3;

        thus thesis by A1, A2;

      end;

    end

    reserve s for FinSequence,

V1,V2,V3 for finite-rank free Z_Module,

f,f1,f2 for Function of V1, V2,

g for Function of V2, V3,

b1 for OrdBasis of V1,

b2 for OrdBasis of V2,

b3 for OrdBasis of V3,

v1,v2 for Vector of V2,

v,w for Element of V1;

    reserve p2,F for FinSequence of V1,

p1,d for FinSequence of INT.Ring ,

KL for Linear_Combination of V1;

    theorem :: ZMATRLIN:11

    

     Th9: for a be Element of V1, F be FinSequence of V1, G be FinSequence of INT.Ring st ( len F) = ( len G) & for k holds for v be Element of INT.Ring st k in ( dom F) & v = (G . k) holds (F . k) = (v * a) holds ( Sum F) = (( Sum G) * a)

    proof

      let a be Element of V1;

      let F be FinSequence of V1;

      let G be FinSequence of INT.Ring ;

      defpred P[ Nat] means for H be FinSequence of V1, I be FinSequence of INT.Ring st ( len H) = ( len I) & ( len H) = $1 & (for k holds for v be Element of INT.Ring st k in ( dom H) & v = (I . k) holds (H . k) = (v * a)) holds ( Sum H) = (( Sum I) * a);

      

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

      proof

        let n;

        assume

         A2: for H be FinSequence of V1, I be FinSequence of INT.Ring st ( len H) = ( len I) & ( len H) = n & (for k holds for v be Element of INT.Ring st k in ( dom H) & v = (I . k) holds (H . k) = (v * a)) holds ( Sum H) = (( Sum I) * a);

        let H be FinSequence of V1, I be FinSequence of INT.Ring ;

        assume that

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

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

         A5: for k holds for v be Element of INT.Ring st k in ( dom H) & v = (I . k) holds (H . k) = (v * a);

        reconsider q = (I | ( Seg n)) as FinSequence of INT.Ring by FINSEQ_1: 18;

        reconsider p = (H | ( Seg n)) as FinSequence of V1 by FINSEQ_1: 18;

        

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

        then

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

        

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

        

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

        

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

         A11:

        now

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

          then

           A12: ( dom p) c= ( dom H) by FINSEQ_3: 30;

          let k;

          let v be Element of INT.Ring ;

          assume that

           A13: k in ( dom p) and

           A14: v = (q . k);

          (I . k) = (q . k) by A8, A10, A13, FUNCT_1: 47;

          then (H . k) = (v * a) by A5, A13, A14, A12;

          hence (p . k) = (v * a) by A13, FUNCT_1: 47;

        end;

        reconsider n as Element of NAT by ORDINAL1:def 12;

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

        then

         A15: (n + 1) in ( dom H) by A4, FINSEQ_1:def 3;

        then

        reconsider v1 = (H . (n + 1)) as Element of V1 by FINSEQ_2: 11;

        reconsider v2 = (I . (n + 1)) as Element of INT.Ring by INT_1:def 2;

        

         A16: v1 = (v2 * a) by A5, A15;

        

         A17: I = (q ^ <*v2*>) by FINSEQ_3: 55, A3, A4;

        

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

        .= ((( Sum q) * a) + (v2 * a)) by A2, A7, A9, A11, A16

        .= ((( Sum q) + v2) * a) by VECTSP_1:def 15

        .= (( Sum I) * a) by A17, FVSUM_1: 71;

      end;

      

       A17: P[ 0 ]

      proof

        let H be FinSequence of V1, I be FinSequence of INT.Ring ;

        assume that

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

         A19: ( len H) = 0 and for k holds for v be Element of INT.Ring st k in ( dom H) & v = (I . k) holds (H . k) = (v * a);

        H = ( <*> the carrier of V1) by A19;

        then

         A20: ( Sum H) = ( 0. V1) by RLVECT_1: 43;

        I = ( <*> the carrier of INT.Ring ) by A18, A19;

        then ( Sum I) = ( 0. INT.Ring ) by RLVECT_1: 43;

        then (( Sum I) * a) = ( 0. V1) by VECTSP_1: 14;

        hence thesis by A20;

      end;

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

      hence thesis;

    end;

    theorem :: ZMATRLIN:12

    

     Th10: for a be Element of V1, F be FinSequence of INT.Ring , G be FinSequence of V1 st ( len F) = ( len G) & for k st k in ( dom F) holds (G . k) = ((F /. k) * a) holds ( Sum G) = (( Sum F) * a)

    proof

      let a be Element of V1;

      let F be FinSequence of INT.Ring ;

      let G be FinSequence of V1;

      assume that

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

       A2: for k st k in ( dom F) holds (G . k) = ((F /. k) * a);

      now

        let k;

        let v be Element of INT.Ring ;

        assume that

         A3: k in ( dom G) and

         A4: v = (F . k);

        

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

        then v = (F /. k) by A4, PARTFUN1:def 6;

        hence (G . k) = (v * a) by A2, A5;

      end;

      hence thesis by A1, Th9;

    end;

    definition

      let V1, p1, p2;

      :: ZMATRLIN:def6

      func lmlt (p1,p2) -> FinSequence of V1 equals (the lmult of V1 .: (p1,p2));

      coherence ;

    end

    theorem :: ZMATRLIN:13

    

     Th12: ( dom p1) = ( dom p2) implies ( dom ( lmlt (p1,p2))) = ( dom p1)

    proof

      assume

       A1: ( dom p1) = ( dom p2);

      

       A2: [:( rng p1), ( rng p2):] c= [: INT , the carrier of V1:] by ZFMISC_1: 96;

      

       A3: ( rng <:p1, p2:>) c= [:( rng p1), ( rng p2):] & [: INT , the carrier of V1:] = ( dom the lmult of V1) by FUNCT_2:def 1, FUNCT_3: 51;

      

      thus ( dom ( lmlt (p1,p2))) = ( dom (the lmult of V1 * <:p1, p2:>)) by FUNCOP_1:def 3

      .= ( dom <:p1, p2:>) by A2, A3, RELAT_1: 27, XBOOLE_1: 1

      .= (( dom p1) /\ ( dom p2)) by FUNCT_3:def 7

      .= ( dom p1) by A1;

    end;

    theorem :: ZMATRLIN:14

    

     Th13: for M be Matrix of the carrier of V1 st ( len M) = 0 holds ( Sum ( Sum M)) = ( 0. V1)

    proof

      let M be Matrix of the carrier of V1;

      assume ( len M) = 0 ;

      then ( len ( Sum M)) = 0 by MATRLIN:def 6;

      then ( Sum M) = ( <*> the carrier of V1);

      hence thesis by RLVECT_1: 43;

    end;

    theorem :: ZMATRLIN:15

    

     Th14: for M be Matrix of (m + 1), 0 , the carrier of V1 holds ( Sum ( Sum M)) = ( 0. V1)

    proof

      let M be Matrix of (m + 1), 0 , the carrier of V1;

      for k st k in ( dom ( Sum M)) holds (( Sum M) /. k) = ( 0. V1)

      proof

        let k such that

         A1: k in ( dom ( Sum M));

        reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

        ( len M) = ( len ( Sum M)) by MATRLIN:def 6;

        then ( dom M) = ( dom ( Sum M)) by FINSEQ_3: 29;

        then (M /. k1) in ( rng M) by A1, PARTFUN2: 2;

        then ( len (M /. k)) = 0 by MATRIX_0:def 2;

        then

         A2: (M /. k) = ( <*> the carrier of V1);

        

        thus (( Sum M) /. k) = ( Sum (M /. k)) by A1, MATRLIN:def 6

        .= ( 0. V1) by A2, RLVECT_1: 43;

      end;

      hence thesis by MATRLIN: 11;

    end;

    theorem :: ZMATRLIN:16

    

     Th16: for V1,V2 be Z_Module, f be Function of V1, V2, p be FinSequence of V1 st f is additive homogeneous holds (f . ( Sum p)) = ( Sum (f * p))

    proof

      let V1,V2 be Z_Module, f be Function of V1, V2;

      let p be FinSequence of V1;

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

      assume

       A1: f is additive homogeneous;

      

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

      proof

        let p be FinSequence of V1;

        let w be Element of V1 such that

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

        

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

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

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

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

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

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

      end;

      set I0 = ( 0. INT.Ring );

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

      .= (f . (I0 * ( 0. V1))) by ZMODUL01: 1

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

      .= ( 0. V2) by ZMODUL01: 1

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

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

      then

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

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

      hence thesis;

    end;

    theorem :: ZMATRLIN:17

    

     Th17: for a be FinSequence of INT.Ring , p be FinSequence of V1 st ( len p) = ( len a) holds f is additive homogeneous implies (f * ( lmlt (a,p))) = ( lmlt (a,(f * p)))

    proof

      let a be FinSequence of INT.Ring , p be FinSequence of V1;

      assume ( len p) = ( len a);

      then

       A1: ( dom p) = ( dom a) by FINSEQ_3: 29;

      ( dom f) = the carrier of V1 by FUNCT_2:def 1;

      then ( rng p) c= ( dom f);

      then

       A2: ( dom p) = ( dom (f * p)) by RELAT_1: 27;

      assume

       A3: f is additive homogeneous;

       A4:

      now

        set P = (f * p);

        let k be Nat;

        assume

         A5: k in ( dom (f * ( lmlt (a,p))));

        

         A6: ( dom (f * ( lmlt (a,p)))) c= ( dom ( lmlt (a,p))) by RELAT_1: 25;

        then k in ( dom ( lmlt (a,p))) by A5;

        then

         A7: k in ( dom p) by A1, Th12;

        then

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

        

         A9: k in ( dom ( lmlt (a,(f * p)))) by A1, A2, A7, Th12;

        

         A10: (a /. k) = (a . k) by A1, A7, PARTFUN1:def 6;

        

         A11: (P /. k) = ((f * p) . k) by A2, A7, PARTFUN1:def 6;

        

        thus ((f * ( lmlt (a,p))) . k) = (f . (( lmlt (a,p)) . k)) by A5, FUNCT_1: 12

        .= (f . ((a /. k) * (p /. k))) by A10, A8, A5, A6, FUNCOP_1: 22

        .= ((a /. k) * (f . (p /. k))) by A3

        .= ((a /. k) * (P /. k)) by A7, A8, A11, FUNCT_1: 13

        .= (( lmlt (a,(f * p))) . k) by A9, A10, A11, FUNCOP_1: 22;

      end;

      ( dom ( lmlt (a,p))) = ( dom p) by A1, Th12

      .= ( dom ( lmlt (a,(f * p)))) by A1, A2, Th12;

      then ( len ( lmlt (a,p))) = ( len ( lmlt (a,(f * p)))) by FINSEQ_3: 29;

      then ( len (f * ( lmlt (a,p)))) = ( len ( lmlt (a,(f * p)))) by FINSEQ_2: 33;

      hence thesis by A4, FINSEQ_2: 9;

    end;

    theorem :: ZMATRLIN:18

    

     Th18: for a be FinSequence of INT.Ring st ( len a) = ( len b2) & g is additive homogeneous holds (g . ( Sum ( lmlt (a,b2)))) = ( Sum ( lmlt (a,(g * b2))))

    proof

      let a be FinSequence of INT.Ring such that

       A1: ( len a) = ( len b2) and

       A2: g is additive homogeneous;

      

      thus (g . ( Sum ( lmlt (a,b2)))) = ( Sum (g * ( lmlt (a,b2)))) by A2, Th16

      .= ( Sum ( lmlt (a,(g * b2)))) by A1, A2, Th17;

    end;

    theorem :: ZMATRLIN:19

    

     Th19: for F,F1 be FinSequence of V1, KL be Linear_Combination of V1, p be Permutation of ( dom F) st F1 = (F * p) holds (KL (#) F1) = ((KL (#) F) * p)

    proof

      let F,F1 be FinSequence of V1;

      let KL be Linear_Combination of V1;

      let p be Permutation of ( dom F) such that

       A1: F1 = (F * p);

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

      then ( dom F) = ( Seg ( len (KL (#) F))) by VECTSP_6:def 5;

      then

       A2: ( dom F) = ( dom (KL (#) F)) by FINSEQ_1:def 3;

      then

      reconsider F2 = ((KL (#) F) * p) as FinSequence of V1 by FINSEQ_2: 47;

      

       A31: ( len (KL (#) F1)) = ( len F1) by VECTSP_6:def 5

      .= ( len F) by A1, FINSEQ_2: 44

      .= ( len (KL (#) F)) by VECTSP_6:def 5

      .= ( len F2) by A2, FINSEQ_2: 44;

      then

       A3: ( dom (KL (#) F1)) = ( dom ((KL (#) F) * p)) by FINSEQ_3: 29;

      ( len (KL (#) F1)) = ( len F1) by VECTSP_6:def 5;

      then

       A4: ( dom (KL (#) F1)) = ( dom F1) by FINSEQ_3: 29;

      now

        let k be Nat;

        reconsider k0 = k as Element of NAT by ORDINAL1:def 12;

        assume

         A5: k in ( dom (KL (#) F1));

        then k in ( dom p) by A3, FUNCT_1: 11;

        then

         A6: (p . k) in ( rng p) by FUNCT_1:def 3;

        then (p . k) in ( dom F);

        then

        reconsider k1 = (p . k0) as Element of NAT ;

        (F1 /. k) = (F1 . k) by A4, A5, PARTFUN1:def 6

        .= (F . (p . k)) by A1, A4, A5, FUNCT_1: 12

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

        

        hence ((KL (#) F1) . k) = ((KL . (F /. k1)) * (F /. k1)) by A5, VECTSP_6:def 5

        .= ((KL (#) F) . k1) by A2, A6, VECTSP_6:def 5

        .= (F2 . k) by A3, A5, FUNCT_1: 12;

      end;

      hence thesis by A31, FINSEQ_3: 29;

    end;

    theorem :: ZMATRLIN:20

    

     Th20: F is one-to-one & ( Carrier KL) c= ( rng F) implies ( Sum (KL (#) F)) = ( Sum KL)

    proof

      assume

       A1: F is one-to-one;

      assume

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

      then

      reconsider A = ( Carrier KL) as Subset of ( rng F);

      consider p1 be Permutation of ( dom F) such that

       A3: ((F - (A ` )) ^ (F - A)) = (F * p1) by FINSEQ_3: 115;

      reconsider G1 = (F - (A ` )), G2 = (F - A) as FinSequence of V1 by FINSEQ_3: 86;

      

       A4: G1 is one-to-one by A1, FINSEQ_3: 87;

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

      then ( dom (KL (#) F)) = ( dom F) by FINSEQ_3: 29;

      then

      reconsider p1 as Permutation of ( dom (KL (#) F));

      

       A5: ( rng G1) = (( rng F) \ (A ` )) by FINSEQ_3: 65

      .= (( rng F) /\ ( Carrier KL)) by XBOOLE_1: 48

      .= ( Carrier KL) by A2, XBOOLE_1: 28;

      for k st k in ( dom (KL (#) G2)) holds ((KL (#) G2) /. k) = ( 0. V1)

      proof

        let k such that

         A6: k in ( dom (KL (#) G2));

        ( len (KL (#) G2)) = ( len G2) by VECTSP_6:def 5;

        then

         A7: ( dom (KL (#) G2)) = ( dom G2) by FINSEQ_3: 29;

        then (G2 . k) in ( rng G2) by A6, FUNCT_1:def 3;

        then (G2 . k) in (( rng F) \ ( Carrier KL)) by FINSEQ_3: 65;

        then not (G2 . k) in ( Carrier KL) by XBOOLE_0:def 5;

        then

         A8: not (G2 /. k) in ( Carrier KL) by A6, A7, PARTFUN1:def 6;

        reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

        

        thus ((KL (#) G2) /. k) = ((KL (#) G2) . k) by A6, PARTFUN1:def 6

        .= ((KL . (G2 /. k1)) * (G2 /. k1)) by A6, VECTSP_6:def 5

        .= (( 0. INT.Ring ) * (G2 /. k)) by A8

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

      end;

      then

       A9: ( Sum (KL (#) G2)) = ( 0. V1) by MATRLIN: 11;

      (KL (#) (G1 ^ G2)) = ((KL (#) F) * p1) by A3, Th19;

      

      hence ( Sum (KL (#) F)) = ( Sum (KL (#) (G1 ^ G2))) by RLVECT_2: 7

      .= ( Sum ((KL (#) G1) ^ (KL (#) G2))) by ZMODUL02: 51

      .= (( Sum (KL (#) G1)) + ( Sum (KL (#) G2))) by RLVECT_1: 41

      .= ( Sum KL) by A4, A5, A9, VECTSP_6:def 6;

    end;

    theorem :: ZMATRLIN:21

    

     Th21: for A be set, p be FinSequence of V1 st ( rng p) c= A holds f1 is additive homogeneous & f2 is additive homogeneous & (for v st v in A holds (f1 . v) = (f2 . v)) implies (f1 . ( Sum p)) = (f2 . ( Sum p))

    proof

      let A be set;

      let p be FinSequence of V1 such that

       A1: ( rng p) c= A;

      defpred P[ FinSequence of V1] means ( rng $1) c= A implies (f1 . ( Sum $1)) = (f2 . ( Sum $1));

      assume that

       A2: f1 is additive homogeneous and

       A3: f2 is additive homogeneous;

      assume

       A4: for v st v in A holds (f1 . v) = (f2 . v);

      

       A5: for p be FinSequence of V1, x be Element of V1 st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence of V1, x be Element of V1 such that

         A6: ( rng p) c= A implies (f1 . ( Sum p)) = (f2 . ( Sum p));

        

         A7: ( rng p) c= (( rng p) \/ ( rng <*x*>)) by XBOOLE_1: 7;

        assume ( rng (p ^ <*x*>)) c= A;

        then

         A8: (( rng p) \/ ( rng <*x*>)) c= A by FINSEQ_1: 31;

        ( rng <*x*>) c= (( rng p) \/ ( rng <*x*>)) by XBOOLE_1: 7;

        then ( rng <*x*>) c= A by A8;

        then

         A9: {x} c= A by FINSEQ_1: 39;

        

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

        .= ((f2 . ( Sum p)) + (f1 . ( Sum <*x*>))) by A2, A6, A8, A7

        .= ((f2 . ( Sum p)) + (f1 . x)) by RLVECT_1: 44

        .= ((f2 . ( Sum p)) + (f2 . x)) by A4, A9, ZFMISC_1: 31

        .= ((f2 . ( Sum p)) + (f2 . ( Sum <*x*>))) by RLVECT_1: 44

        .= (f2 . (( Sum p) + ( Sum <*x*>))) by A3

        .= (f2 . ( Sum (p ^ <*x*>))) by RLVECT_1: 41;

      end;

      

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

      proof

        assume ( rng ( <*> the carrier of V1)) c= A;

        set I0 = ( 0. INT.Ring );

        

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

        .= (f1 . (I0 * ( 0. V1))) by ZMODUL01: 1

        .= (I0 * (f1 . ( 0. V1))) by A2

        .= ( 0. V2) by ZMODUL01: 1

        .= (I0 * (f2 . ( 0. V1))) by ZMODUL01: 1

        .= (f2 . (I0 * ( 0. V1))) by A3

        .= (f2 . ( 0. V1)) by ZMODUL01: 1

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

      end;

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

      hence thesis by A1;

    end;

    theorem :: ZMATRLIN:22

    

     Th22: f1 is additive homogeneous & f2 is additive homogeneous implies for b1 be OrdBasis of V1 st ( len b1) > 0 holds (f1 * b1) = (f2 * b1) implies f1 = f2

    proof

      assume that

       A1: f1 is additive homogeneous and

       A2: f2 is additive homogeneous;

      let b1 be OrdBasis of V1 such that

       A3: ( len b1) > 0 ;

      reconsider b = ( rng b1) as Basis of V1 by defOrdBasis;

      assume

       A4: (f1 * b1) = (f2 * b1);

      now

        ( len b1) in ( Seg ( len b1)) by A3, FINSEQ_1: 3;

        then

        reconsider D = ( dom b1) as non empty set by FINSEQ_1:def 3;

        let v be Element of V1;

        ( Lin b) = the ModuleStr of V1 by VECTSP_7:def 3;

        then v in ( Lin b);

        then

        consider KL be Linear_Combination of b such that

         A5: v = ( Sum KL) by ZMODUL02: 64;

        set p = (KL (#) b1);

        set A = the set of all ((KL . (b1 /. i)) * (b1 /. i)) where i be Element of D;

        

         A6: ( rng p) c= A

        proof

          let x be object;

          assume x in ( rng p);

          then

          consider i be Nat such that

           A7: i in ( dom p) and

           A8: (p . i) = x by FINSEQ_2: 10;

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

          then i in ( Seg ( len b1)) by A7, VECTSP_6:def 5;

          then

           A9: i in ( dom b1) by FINSEQ_1:def 3;

          ((KL (#) b1) . i) = ((KL . (b1 /. i)) * (b1 /. i)) by A7, VECTSP_6:def 5;

          hence thesis by A8, A9;

        end;

        

         A10: for w st w in A holds (f1 . w) = (f2 . w)

        proof

          let w;

          assume w in A;

          then

          consider i be Element of D such that

           A11: w = ((KL . (b1 /. i)) * (b1 /. i));

          (f1 . (b1 /. i)) = (f1 . (b1 . i)) by PARTFUN1:def 6

          .= ((f2 * b1) . i) by A4, FUNCT_1: 13

          .= (f2 . (b1 . i)) by FUNCT_1: 13

          .= (f2 . (b1 /. i)) by PARTFUN1:def 6;

          

          then (f1 . ((KL . (b1 /. i)) * (b1 /. i))) = ((KL . (b1 /. i)) * (f2 . (b1 /. i))) by A1

          .= (f2 . ((KL . (b1 /. i)) * (b1 /. i))) by A2;

          hence thesis by A11;

        end;

        

         A12: b1 is one-to-one & ( Carrier KL) c= ( rng b1) by defOrdBasis, VECTSP_6:def 4;

        

        hence (f1 . v) = (f1 . ( Sum (KL (#) b1))) by A5, Th20

        .= (f2 . ( Sum p)) by A1, A2, A6, A10, Th21

        .= (f2 . v) by A5, A12, Th20;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:23

    

     Th27: for M1 be Matrix of n, k, the carrier of V, M2 be Matrix of m, k, the carrier of V holds ( Sum (M1 ^ M2)) = (( Sum M1) ^ ( Sum M2))

    proof

      let M1 be Matrix of n, k, the carrier of V;

      let M2 be Matrix of m, k, the carrier of V;

      

       A1: ( dom ( Sum (M1 ^ M2))) = ( Seg ( len ( Sum (M1 ^ M2)))) by FINSEQ_1:def 3;

       A2:

      now

        let i be Nat;

        assume

         A3: i in ( dom ( Sum (M1 ^ M2)));

        then i in ( Seg ( len (M1 ^ M2))) by A1, MATRLIN:def 6;

        then

         A4: i in ( dom (M1 ^ M2)) by FINSEQ_1:def 3;

        now

          per cases by A4, FINSEQ_1: 25;

            suppose

             A5: i in ( dom M1);

            ( len M1) = ( len ( Sum M1)) by MATRLIN:def 6;

            then

             A6: ( dom M1) = ( dom ( Sum M1)) by FINSEQ_3: 29;

            

            thus (( Sum (M1 ^ M2)) . i) = (( Sum (M1 ^ M2)) /. i) by A3, PARTFUN1:def 6

            .= ( Sum ((M1 ^ M2) /. i)) by A3, MATRLIN:def 6

            .= ( Sum (M1 /. i)) by A5, FINSEQ_4: 68

            .= (( Sum M1) /. i) by A5, A6, MATRLIN:def 6

            .= (( Sum M1) . i) by A5, A6, PARTFUN1:def 6

            .= ((( Sum M1) ^ ( Sum M2)) . i) by A5, A6, FINSEQ_1:def 7;

          end;

            suppose

             A7: ex n be Nat st n in ( dom M2) & i = (( len M1) + n);

            

             A8: ( len M1) = ( len ( Sum M1)) by MATRLIN:def 6;

            ( len M2) = ( len ( Sum M2)) by MATRLIN:def 6;

            then

             A9: ( dom M2) = ( dom ( Sum M2)) by FINSEQ_3: 29;

            consider n be Nat such that

             A10: n in ( dom M2) and

             A11: i = (( len M1) + n) by A7;

            

            thus (( Sum (M1 ^ M2)) . i) = (( Sum (M1 ^ M2)) /. i) by A3, PARTFUN1:def 6

            .= ( Sum ((M1 ^ M2) /. i)) by A3, MATRLIN:def 6

            .= ( Sum (M2 /. n)) by A10, A11, FINSEQ_4: 69

            .= (( Sum M2) /. n) by A10, A9, MATRLIN:def 6

            .= (( Sum M2) . n) by A10, A9, PARTFUN1:def 6

            .= ((( Sum M1) ^ ( Sum M2)) . i) by A10, A11, A8, A9, FINSEQ_1:def 7;

          end;

        end;

        hence (( Sum (M1 ^ M2)) . i) = ((( Sum M1) ^ ( Sum M2)) . i);

      end;

      ( len ( Sum (M1 ^ M2))) = ( len (M1 ^ M2)) by MATRLIN:def 6

      .= (( len M1) + ( len M2)) by FINSEQ_1: 22

      .= (( len ( Sum M1)) + ( len M2)) by MATRLIN:def 6

      .= (( len ( Sum M1)) + ( len ( Sum M2))) by MATRLIN:def 6

      .= ( len (( Sum M1) ^ ( Sum M2))) by FINSEQ_1: 22;

      hence thesis by A2, FINSEQ_2: 9;

    end;

    theorem :: ZMATRLIN:24

    

     Th29: for M1,M2 be Matrix of the carrier of V1 holds (( Sum M1) + ( Sum M2)) = ( Sum (M1 ^^ M2))

    proof

      let M1,M2 be Matrix of the carrier of V1;

      reconsider m = ( min (( len M1),( len M2))) as Element of NAT by ORDINAL1:def 12;

      

       A1: ( Seg m) = (( Seg ( len M1)) /\ ( Seg ( len M2))) by FINSEQ_2: 2

      .= (( Seg ( len M1)) /\ ( dom M2)) by FINSEQ_1:def 3

      .= (( dom M1) /\ ( dom M2)) by FINSEQ_1:def 3

      .= ( dom (M1 ^^ M2)) by PRE_POLY:def 4

      .= ( Seg ( len (M1 ^^ M2))) by FINSEQ_1:def 3;

      

       A2: ( len (( Sum M1) + ( Sum M2))) = ( min (( len ( Sum M1)),( len ( Sum M2)))) by FINSEQ_2: 71

      .= ( min (( len M1),( len ( Sum M2)))) by MATRLIN:def 6

      .= ( min (( len M1),( len M2))) by MATRLIN:def 6

      .= ( len (M1 ^^ M2)) by A1, FINSEQ_1: 6

      .= ( len ( Sum (M1 ^^ M2))) by MATRLIN:def 6;

      

       A3: ( dom (( Sum M1) + ( Sum M2))) = ( Seg ( len (( Sum M1) + ( Sum M2)))) by FINSEQ_1:def 3;

      now

        let i be Nat;

        assume

         A4: i in ( dom (( Sum M1) + ( Sum M2)));

        then

         A5: i in ( dom ( Sum (M1 ^^ M2))) by A2, A3, FINSEQ_1:def 3;

        i in ( Seg ( len (M1 ^^ M2))) by A2, A3, A4, MATRLIN:def 6;

        then

         A6: i in ( dom (M1 ^^ M2)) by FINSEQ_1:def 3;

        then

         A7: i in (( dom M1) /\ ( dom M2)) by PRE_POLY:def 4;

        then

         A8: i in ( dom M1) by XBOOLE_0:def 4;

        

         A9: i in ( dom M2) by A7, XBOOLE_0:def 4;

        reconsider m1 = (M1 . i), m2 = (M2 . i) as FinSequence;

        

         A10: ((M1 /. i) ^ (M2 /. i)) = (m1 ^ (M2 /. i)) by A8, PARTFUN1:def 6

        .= (m1 ^ m2) by A9, PARTFUN1:def 6

        .= ((M1 ^^ M2) . i) by A6, PRE_POLY:def 4

        .= ((M1 ^^ M2) /. i) by A6, PARTFUN1:def 6;

        i in ( Seg ( len M2)) by A9, FINSEQ_1:def 3;

        then i in ( Seg ( len ( Sum M2))) by MATRLIN:def 6;

        then

         A11: i in ( dom ( Sum M2)) by FINSEQ_1:def 3;

        then

         A12: (( Sum M2) /. i) = (( Sum M2) . i) by PARTFUN1:def 6;

        i in ( Seg ( len M1)) by A8, FINSEQ_1:def 3;

        then i in ( Seg ( len ( Sum M1))) by MATRLIN:def 6;

        then

         A13: i in ( dom ( Sum M1)) by FINSEQ_1:def 3;

        then (( Sum M1) /. i) = (( Sum M1) . i) by PARTFUN1:def 6;

        

        hence ((( Sum M1) + ( Sum M2)) . i) = ((( Sum M1) /. i) + (( Sum M2) /. i)) by A4, A12, FUNCOP_1: 22

        .= (( Sum (M1 /. i)) + (( Sum M2) /. i)) by A13, MATRLIN:def 6

        .= (( Sum (M1 /. i)) + ( Sum (M2 /. i))) by A11, MATRLIN:def 6

        .= ( Sum ((M1 ^^ M2) /. i)) by A10, RLVECT_1: 41

        .= (( Sum (M1 ^^ M2)) /. i) by A5, MATRLIN:def 6

        .= (( Sum (M1 ^^ M2)) . i) by A5, PARTFUN1:def 6;

      end;

      hence thesis by A2, FINSEQ_2: 9;

    end;

    theorem :: ZMATRLIN:25

    

     Th30: for P1,P2 be FinSequence of V1 st ( len P1) = ( len P2) holds ( Sum (P1 + P2)) = (( Sum P1) + ( Sum P2))

    proof

      let P1,P2 be FinSequence of V1;

      assume ( len P1) = ( len P2);

      then

      reconsider R1 = P1, R2 = P2 as Element of (( len P1) -tuples_on the carrier of V1) by FINSEQ_2: 92;

      

      thus ( Sum (P1 + P2)) = ( Sum (R1 + R2))

      .= (( Sum P1) + ( Sum P2)) by FVSUM_1: 76;

    end;

    theorem :: ZMATRLIN:26

    

     Th31: for M1,M2 be Matrix of the carrier of V1 st ( len M1) = ( len M2) holds (( Sum ( Sum M1)) + ( Sum ( Sum M2))) = ( Sum ( Sum (M1 ^^ M2)))

    proof

      let M1,M2 be Matrix of the carrier of V1 such that

       A1: ( len M1) = ( len M2);

      ( len ( Sum M1)) = ( len M1) by MATRLIN:def 6

      .= ( len ( Sum M2)) by A1, MATRLIN:def 6;

      

      hence (( Sum ( Sum M1)) + ( Sum ( Sum M2))) = ( Sum (( Sum M1) + ( Sum M2))) by Th30

      .= ( Sum ( Sum (M1 ^^ M2))) by Th29;

    end;

    theorem :: ZMATRLIN:27

    

     Th32: for M be Matrix of the carrier of V1 holds ( Sum ( Sum M)) = ( Sum ( Sum (M @ )))

    proof

      defpred X[ Nat] means for M be Matrix of the carrier of V1 st ( len M) = $1 holds ( Sum ( Sum M)) = ( Sum ( Sum (M @ )));

      let M be Matrix of the carrier of V1;

      

       A1: for P be FinSequence of V1 holds ( Sum ( Sum <*P*>)) = ( Sum ( Sum ( <*P*> @ )))

      proof

        defpred X[ FinSequence of V1] means ( Sum ( Sum <*$1*>)) = ( Sum ( Sum ( <*$1*> @ )));

        let P be FinSequence of V1;

        ( len <*( <*> the carrier of V1)*>) = 1 by MATRIX_0:def 2;

        then ( width <*( <*> the carrier of V1)*>) = 0 by MATRIX_0: 20;

        then

         A2: ( len ( <*( <*> the carrier of V1)*> @ )) = 0 by MATRIX_0:def 6;

        

         A3: for P be FinSequence of V1, x be Element of V1 st X[P] holds X[(P ^ <*x*>)]

        proof

          let P be FinSequence of V1, x be Element of V1 such that

           A4: ( Sum ( Sum <*P*>)) = ( Sum ( Sum ( <*P*> @ )));

          ( Seg ( len ( <*P*> ^^ <* <*x*>*>))) = ( dom ( <*P*> ^^ <* <*x*>*>)) by FINSEQ_1:def 3

          .= (( dom <*P*>) /\ ( dom <* <*x*>*>)) by PRE_POLY:def 4

          .= (( Seg 1) /\ ( dom <* <*x*>*>)) by FINSEQ_1: 38

          .= (( Seg 1) /\ ( Seg 1)) by FINSEQ_1: 38

          .= ( Seg 1);

          

          then

           A5: ( len ( <*P*> ^^ <* <*x*>*>)) = 1 by FINSEQ_1: 6

          .= ( len <*(P ^ <*x*>)*>) by FINSEQ_1: 39;

          then

           A6: ( dom ( <*P*> ^^ <* <*x*>*>)) = ( Seg ( len <*(P ^ <*x*>)*>)) by FINSEQ_1:def 3;

           A7:

          now

            let i be Nat;

            assume

             A8: i in ( dom ( <*P*> ^^ <* <*x*>*>));

            then i in {1} by A6, FINSEQ_1: 2, FINSEQ_1: 40;

            then

             A9: i = 1 by TARSKI:def 1;

            reconsider m1 = ( <*P*> . i), m2 = ( <* <*x*>*> . i) as FinSequence;

            

            thus (( <*P*> ^^ <* <*x*>*>) . i) = (m1 ^ m2) by A8, PRE_POLY:def 4

            .= (P ^ m2) by A9, FINSEQ_1: 40

            .= (P ^ <*x*>) by A9, FINSEQ_1: 40

            .= ( <*(P ^ <*x*>)*> . i) by A9, FINSEQ_1: 40;

          end;

          per cases ;

            suppose ( len P) = 0 ;

            then

             A10: P = {} ;

            

            hence ( Sum ( Sum <*(P ^ <*x*>)*>)) = ( Sum ( Sum <* <*x*>*>)) by FINSEQ_1: 34

            .= ( Sum ( Sum ( <* <*x*>*> @ ))) by MATRLIN: 15

            .= ( Sum ( Sum ( <*(P ^ <*x*>)*> @ ))) by A10, FINSEQ_1: 34;

          end;

            suppose

             A11: ( len P) <> 0 ;

            

             A12: ( len <* <*x*>*>) = 1 by FINSEQ_1: 40;

            

            then

             A13: ( width <* <*x*>*>) = ( len <*x*>) by MATRIX_0: 20

            .= 1 by FINSEQ_1: 40;

            then

             A14: ( len ( <* <*x*>*> @ )) = 1 by MATRIX_0:def 6;

            

             A15: ( len <*P*>) = 1 by FINSEQ_1: 40;

            then

             A16: ( width <*P*>) = ( len P) by MATRIX_0: 20;

            then

             A17: ( len ( <*P*> @ )) = ( len P) by MATRIX_0:def 6;

            ( width ( <*P*> @ )) = 1 by A11, A15, A16, MATRIX_0: 54;

            then

            reconsider d1 = ( <*P*> @ ) as Matrix of ( len P), 1, the carrier of V1 by A11, A17, MATRIX_0: 20;

            

             A18: ( len <*(P ^ <*x*>)*>) = 1 by FINSEQ_1: 40;

            

            then

             A19: ( width <*(P ^ <*x*>)*>) = ( len (P ^ <*x*>)) by MATRIX_0: 20

            .= (( len P) + ( len <*x*>)) by FINSEQ_1: 22

            .= (( len P) + 1) by FINSEQ_1: 40;

            

             A20: (( <* <*x*>*> @ ) @ ) = <* <*x*>*> by A12, A13, MATRIX_0: 57;

            

             A21: ( width ( <*P*> @ )) = ( len <*P*>) by A11, A16, MATRIX_0: 54

            .= ( width ( <* <*x*>*> @ )) by A15, A12, A13, MATRIX_0: 54;

            then ( width ( <* <*x*>*> @ )) = 1 by A11, A15, A16, MATRIX_0: 54;

            then

            reconsider d2 = ( <* <*x*>*> @ ) as Matrix of 1, 1, the carrier of V1 by A14, MATRIX_0: 20;

            

             A22: ((d1 ^ d2) @ ) = ((( <*P*> @ ) @ ) ^^ (( <* <*x*>*> @ ) @ )) by A21, MATRLIN: 28

            .= ( <*P*> ^^ <* <*x*>*>) by A11, A15, A16, A20, MATRIX_0: 57

            .= <*(P ^ <*x*>)*> by A5, A7, FINSEQ_2: 9

            .= (( <*(P ^ <*x*>)*> @ ) @ ) by A18, A19, MATRIX_0: 57;

            

             A23: ( len (( <*P*> @ ) ^ ( <* <*x*>*> @ ))) = (( len ( <*P*> @ )) + ( len ( <* <*x*>*> @ ))) by FINSEQ_1: 22

            .= (( width <*P*>) + ( len ( <* <*x*>*> @ ))) by MATRIX_0:def 6

            .= (( width <*P*>) + ( width <* <*x*>*>)) by MATRIX_0:def 6

            .= ( len ( <*(P ^ <*x*>)*> @ )) by A16, A13, A19, MATRIX_0:def 6;

            

            thus ( Sum ( Sum <*(P ^ <*x*>)*>)) = ( Sum ( Sum ( <*P*> ^^ <* <*x*>*>))) by A5, A7, FINSEQ_2: 9

            .= (( Sum ( Sum ( <*P*> @ ))) + ( Sum ( Sum <* <*x*>*>))) by A4, A15, A12, Th31

            .= (( Sum ( Sum ( <*P*> @ ))) + ( Sum ( Sum ( <* <*x*>*> @ )))) by MATRLIN: 15

            .= ( Sum (( Sum d1) ^ ( Sum d2))) by RLVECT_1: 41

            .= ( Sum ( Sum (d1 ^ d2))) by Th27

            .= ( Sum ( Sum ( <*(P ^ <*x*>)*> @ ))) by A23, A22, MATRIX_0: 53;

          end;

        end;

         <*( <*> the carrier of V1)*> is Matrix of ( 0 + 1), 0 , the carrier of V1;

        

        then ( Sum ( Sum <*( <*> the carrier of V1)*>)) = ( 0. V1) by Th14

        .= ( Sum ( Sum ( <*( <*> the carrier of V1)*> @ ))) by A2, Th13;

        then

         A24: X[( <*> the carrier of V1)];

        for P be FinSequence of V1 holds X[P] from FINSEQ_2:sch 2( A24, A3);

        hence thesis;

      end;

      

       A25: for n st X[n] holds X[(n + 1)]

      proof

        let n such that

         A26: for M be Matrix of the carrier of V1 st ( len M) = n holds ( Sum ( Sum M)) = ( Sum ( Sum (M @ )));

        thus for M be Matrix of the carrier of V1 st ( len M) = (n + 1) holds ( Sum ( Sum M)) = ( Sum ( Sum (M @ )))

        proof

          let M be Matrix of the carrier of V1 such that

           A27: ( len M) = (n + 1);

          

           A28: M <> {} by A27;

          

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

          per cases ;

            suppose

             A30: n = 0 ;

            then (M . 1) = ( Line (M,1)) by A27, A29, FINSEQ_1: 4, MATRIX_0: 60;

            then

            reconsider G = (M . 1) as FinSequence of V1;

            M = <*G*> by A27, A30, FINSEQ_1: 40;

            hence thesis by A1;

          end;

            suppose

             A31: n > 0 ;

            

             A32: (M . (n + 1)) = ( Line (M,(n + 1))) by A27, A29, FINSEQ_1: 4, MATRIX_0: 60;

            then

            reconsider M1 = (M . (n + 1)) as FinSequence of V1;

            ( len M1) = ( width M) by A32, MATRIX_0:def 7;

            then

            reconsider R = <*M1*> as Matrix of 1, ( width M), the carrier of V1;

            reconsider M9 = M as Matrix of (n + 1), ( width M), the carrier of V1 by A27, MATRIX_0: 20;

            reconsider W = ( Del (M9,(n + 1))) as Matrix of n, ( width M), the carrier of V1 by MATRLIN: 3;

            

             A33: ( width W) = ( width M9) by A31, MATRLIN: 2

            .= ( width R) by MATRLIN: 2;

            

             A34: ( len (W @ )) = ( width W) by MATRIX_0:def 6

            .= ( len (R @ )) by A33, MATRIX_0:def 6;

            

             A35: ( len ( Del (M,(n + 1)))) = n by A27, PRE_POLY: 12;

            

            thus ( Sum ( Sum M)) = ( Sum ( Sum (W ^ R))) by A28, PRE_POLY: 13, A27

            .= ( Sum (( Sum W) ^ ( Sum R))) by Th27

            .= (( Sum ( Sum ( Del (M,(n + 1))))) + ( Sum ( Sum R))) by RLVECT_1: 41

            .= (( Sum ( Sum (( Del (M,(n + 1))) @ ))) + ( Sum ( Sum R))) by A26, A35

            .= (( Sum ( Sum (( Del (M,(n + 1))) @ ))) + ( Sum ( Sum (R @ )))) by A1

            .= ( Sum ( Sum ((W @ ) ^^ (R @ )))) by A34, Th31

            .= ( Sum ( Sum ((W ^ R) @ ))) by A33, MATRLIN: 28

            .= ( Sum ( Sum (M @ ))) by A28, PRE_POLY: 13, A27;

          end;

        end;

      end;

      

       A36: X[ 0 ]

      proof

        let M be Matrix of the carrier of V1;

        assume

         A37: ( len M) = 0 ;

        then ( width M) = 0 by MATRIX_0:def 3;

        then

         A38: ( len (M @ )) = 0 by MATRIX_0:def 6;

        

        thus ( Sum ( Sum M)) = ( 0. V1) by A37, Th13

        .= ( Sum ( Sum (M @ ))) by A38, Th13;

      end;

      for n holds X[n] from NAT_1:sch 2( A36, A25);

      then X[( len M)];

      hence thesis;

    end;

    theorem :: ZMATRLIN:28

    

     Th33: for M be Matrix of n, m, INT.Ring st n > 0 & m > 0 holds for p,d be FinSequence of INT.Ring st ( len p) = n & ( len d) = m & for j st j in ( dom d) holds (d /. j) = ( Sum ( mlt (p,( Col (M,j))))) holds for b,c be FinSequence of V1 st ( len b) = m & ( len c) = n & for i st i in ( dom c) holds (c /. i) = ( Sum ( lmlt (( Line (M,i)),b))) holds ( Sum ( lmlt (p,c))) = ( Sum ( lmlt (d,b)))

    proof

      let M be Matrix of n, m, INT.Ring such that

       A1: n > 0 and

       A2: m > 0 ;

      

       A3: ( len M) = n by A1, MATRIX_0: 23;

      reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;

      let p,d be FinSequence of INT.Ring such that

       A4: ( len p) = n and

       A5: ( len d) = m and

       A6: for j st j in ( dom d) holds (d /. j) = ( Sum ( mlt (p,( Col (M,j)))));

      let b,c be FinSequence of V1 such that

       A7: ( len b) = m and

       A8: ( len c) = n and

       A9: for i st i in ( dom c) holds (c /. i) = ( Sum ( lmlt (( Line (M,i)),b)));

      deffunc V( Nat, Nat) = (((p /. $1) * (M * ($1,$2))) * (b /. $2));

      consider M1 be Matrix of n1, m1, the carrier of V1 such that

       A10: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = V(i,j) from MATRIX_0:sch 1;

      

       A11: ( width M1) = ( len (M1 @ )) by MATRIX_0:def 6

      .= ( len ( Sum (M1 @ ))) by MATRLIN:def 6;

      

       A12: ( dom d) = ( dom b) by A5, A7, FINSEQ_3: 29;

      then

       A13: ( dom ( lmlt (d,b))) = ( dom b) by Th12;

      

      then

       A14: ( len ( lmlt (d,b))) = ( len b) by FINSEQ_3: 29

      .= ( len ( Sum (M1 @ ))) by A1, A7, A11, MATRIX_0: 23;

      then

       A15: ( dom ( lmlt (d,b))) = ( Seg ( len ( Sum (M1 @ )))) by FINSEQ_1:def 3;

      

       A16: ( width M1) = m by A1, MATRIX_0: 23;

      

       A17: ( len M1) = n by A1, MATRIX_0: 23;

       A19:

      now

        

         A20: ( Seg ( len ( Sum (M1 @ )))) = ( dom ( Sum (M1 @ ))) by FINSEQ_1:def 3;

        let j be Nat such that

         A21: j in ( dom ( lmlt (d,b)));

        

         A22: j in ( dom ( Sum (M1 @ ))) by A15, A21, FINSEQ_1:def 3;

        

         A23: j in ( dom d) by A12, A21, Th12;

        

         A24: (d /. j) = (d . j) & (b /. j) = (b . j) by A12, A13, A21, PARTFUN1:def 6;

        ( len ( Sum (M1 @ ))) = ( len (M1 @ )) by MATRLIN:def 6;

        then

         A25: ( dom ( Sum (M1 @ ))) = ( dom (M1 @ )) by FINSEQ_3: 29;

        

        then

         A26: ((M1 @ ) /. j) = ((M1 @ ) . j) by A22, PARTFUN1:def 6

        .= ( Line ((M1 @ ),j)) by A22, A25, MATRIX_0: 60;

        reconsider H = ( mlt (p,( Col (M,j)))) as FinSequence of INT.Ring ;

        deffunc V( Nat) = ((H /. $1) * (b /. j));

        consider G be FinSequence of V1 such that

         A27: ( len G) = ( len p) & for i be Nat st i in ( dom G) holds (G . i) = V(i) from FINSEQ_2:sch 1;

        

         A28: ( len p) = ( len ( Col (M,j))) by A4, A3, MATRIX_0:def 8;

        then

         A29: ( len (the multF of INT.Ring .: (p,( Col (M,j))))) = ( len p) by FINSEQ_2: 72;

        then

         A30: ( dom H) = ( dom G) by A27, FINSEQ_3: 29;

        

         A31: ( dom p) = ( dom G) by A27, FINSEQ_3: 29;

        

         A32: ( len ( Line ((M1 @ ),j))) = ( width (M1 @ )) by MATRIX_0:def 7

        .= ( len ((M1 @ ) @ )) by MATRIX_0:def 6

        .= ( len G) by A1, A2, A4, A17, A16, A27, MATRIX_0: 57;

        then

         A33: ( dom ( Line ((M1 @ ),j))) = ( Seg ( len G)) by FINSEQ_1:def 3;

        

         A34: ( dom G) = ( Seg ( len p)) by A27, FINSEQ_1:def 3;

         A35:

        now

          let i be Nat;

          

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

          assume

           A37: i in ( dom ( Line ((M1 @ ),j)));

          then

           A38: i in ( Seg ( len (the multF of INT.Ring .: (p,( Col (M,j)))))) by A27, A28, A33, FINSEQ_2: 72;

          then

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

          

           A40: i in ( dom ( multint .: (p,( Col (M,j))))) by A38, FINSEQ_1:def 3;

          

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

          then (p /. i) = (p . i) by A31, A33, A37, PARTFUN1:def 6;

          

          then

           A42: ((p /. i) * (M * (i,j))) = ( multint . ((p . i),(( Col (M,j)) . i))) by A4, A3, A27, A33, A37, A36, MATRIX_0:def 8

          .= (( multint .: (p,( Col (M,j)))) . i) by A40, FUNCOP_1: 22

          .= (H /. i) by A39, PARTFUN1:def 6;

          ( dom M1) = ( dom G) by A4, A17, A27, FINSEQ_3: 29;

          then

           A43: [i, j] in ( Indices M1) by A11, A15, A21, A33, A37, A41, ZFMISC_1: 87;

          i in ( Seg ( width (M1 @ ))) by A32, A33, A37, MATRIX_0:def 7;

          

          hence (( Line ((M1 @ ),j)) . i) = ((M1 @ ) * (j,i)) by MATRIX_0:def 7

          .= (M1 * (i,j)) by A43, MATRIX_0:def 6

          .= ((H /. i) * (b /. j)) by A10, A43, A42

          .= (G . i) by A27, A34, A33, A37;

        end;

        

        thus (( lmlt (d,b)) . j) = (the lmult of V1 . ((d . j),(b . j))) by A21, FUNCOP_1: 22

        .= (( Sum H) * (b /. j)) by A6, A23, A24

        .= ( Sum G) by A27, A29, A30, Th10

        .= ( Sum ((M1 @ ) /. j)) by A32, A35, A26, FINSEQ_2: 9

        .= (( Sum (M1 @ )) /. j) by A22, MATRLIN:def 6

        .= (( Sum (M1 @ )) . j) by A15, A21, A20, PARTFUN1:def 6;

      end;

      

       A44: ( dom p) = ( dom c) by A4, A8, FINSEQ_3: 29;

      then

       A45: ( dom ( lmlt (p,c))) = ( dom p) by Th12;

      

      then

       A46: ( len ( lmlt (p,c))) = ( len p) by FINSEQ_3: 29

      .= ( len M1) by A4, MATRIX_0:def 2

      .= ( len ( Sum M1)) by MATRLIN:def 6;

      now

        let i be Nat such that

         A47: i in ( dom ( Sum M1));

        

         A48: i in ( dom c) by A44, A45, A46, A47, FINSEQ_3: 29;

        then

         A49: (c . i) = (c /. i) & (p . i) = (p /. i) by A44, PARTFUN1:def 6;

        i in ( Seg ( len ( Sum M1))) by A47, FINSEQ_1:def 3;

        then i in ( Seg ( len M1)) by MATRLIN:def 6;

        then

         A50: i in ( dom M1) by FINSEQ_1:def 3;

        

        then

         A51: (M1 /. i) = (M1 . i) by PARTFUN1:def 6

        .= ( Line (M1,i)) by A50, MATRIX_0: 60;

        deffunc V( Nat) = ((p /. i) * (( lmlt (( Line (M,i)),b)) /. $1));

        consider F be FinSequence of V1 such that

         A52: ( len F) = ( len b) & for j be Nat st j in ( dom F) holds (F . j) = V(j) from FINSEQ_2:sch 1;

        

         A53: ( len F) = ( width M) by A1, A7, A52, MATRIX_0: 23;

        

         A54: ( dom ( Line (M,i))) = ( Seg ( len ( Line (M,i)))) by FINSEQ_1:def 3

        .= ( dom b) by A52, A53, FINSEQ_1:def 3, MATRIX_0:def 7;

        then ( dom ( lmlt (( Line (M,i)),b))) = ( dom b) by Th12;

        then

         A55: ( len F) = ( len ( lmlt (( Line (M,i)),b))) & ( dom F) = ( dom ( lmlt (( Line (M,i)),b))) by A52, FINSEQ_3: 29;

        

         A56: ( len F) = ( width M1) by A1, A7, A52, MATRIX_0: 23;

        then

         A57: ( len ( Line (M1,i))) = ( len F) by MATRIX_0:def 7;

        then

         A58: ( dom (M1 /. i)) = ( Seg ( len F)) by A51, FINSEQ_1:def 3;

        

         A59: ( dom F) = ( Seg ( len b)) by A52, FINSEQ_1:def 3;

         A60:

        now

          let j be Nat;

          assume

           A61: j in ( dom (M1 /. i));

          then

           A62: (( Line (M,i)) . j) = (M * (i,j)) by A53, A58, MATRIX_0:def 7;

          

           A63: [i, j] in ( Indices M1) by A56, A50, A58, A61, ZFMISC_1: 87;

          

           A64: j in ( dom b) by A52, A58, A61, FINSEQ_1:def 3;

          then

           A65: (b . j) = (b /. j) by PARTFUN1:def 6;

          

           A66: j in ( dom ( lmlt (( Line (M,i)),b))) by A54, A64, Th12;

          

          then

           A67: (( lmlt (( Line (M,i)),b)) /. j) = (( lmlt (( Line (M,i)),b)) . j) by PARTFUN1:def 6

          .= ((M * (i,j)) * (b /. j)) by A65, A62, A66, FUNCOP_1: 22;

          

          thus ((M1 /. i) . j) = (M1 * (i,j)) by A56, A51, A58, A61, MATRIX_0:def 7

          .= (((p /. i) * (M * (i,j))) * (b /. j)) by A10, A63

          .= ((p /. i) * (( lmlt (( Line (M,i)),b)) /. j)) by A67, VECTSP_1:def 16

          .= (F . j) by A52, A59, A58, A61;

        end;

        

         A68: for j be Nat, v be Vector of V1 st j in ( dom F) & v = (( lmlt (( Line (M,i)),b)) . j) holds (F . j) = ((p /. i) * v)

        proof

          let j be Nat, v be Vector of V1;

          assume

           A681: j in ( dom F) & v = (( lmlt (( Line (M,i)),b)) . j);

          

          thus (F . j) = ((p /. i) * (( lmlt (( Line (M,i)),b)) /. j)) by A52, A681

          .= ((p /. i) * v) by A55, A681, PARTFUN1:def 6;

        end;

        i in ( dom (the lmult of V1 .: (p,c))) by A46, A47, FINSEQ_3: 29;

        

        hence (( lmlt (p,c)) . i) = (the lmult of V1 . ((p . i),(c . i))) by FUNCOP_1: 22

        .= ((p /. i) * ( Sum ( lmlt (( Line (M,i)),b)))) by A9, A48, A49

        .= ( Sum F) by A55, A68, ZMODUL01: 12

        .= ( Sum (M1 /. i)) by A57, A51, A60, FINSEQ_2: 9

        .= (( Sum M1) /. i) by A47, MATRLIN:def 6

        .= (( Sum M1) . i) by A47, PARTFUN1:def 6;

      end;

      

      hence ( Sum ( lmlt (p,c))) = ( Sum ( Sum M1)) by A46, FINSEQ_2: 9

      .= ( Sum ( Sum (M1 @ ))) by Th32

      .= ( Sum ( lmlt (d,b))) by A14, A19, FINSEQ_2: 9;

    end;

    begin

    definition

      let V be finite-rank free Z_Module;

      let b1 be OrdBasis of V;

      let W be Element of V;

      :: ZMATRLIN:def7

      func W |-- b1 -> FinSequence of INT.Ring means

      : Def7: ( len it ) = ( len b1) & ex KL be Linear_Combination of V st W = ( Sum KL) & ( Carrier KL) c= ( rng b1) & for k st 1 <= k & k <= ( len it ) holds (it /. k) = (KL . (b1 /. k));

      existence

      proof

        reconsider b2 = ( rng b1) as Basis of V by defOrdBasis;

        consider KL be Linear_Combination of V such that

         A1: W = ( Sum KL) and

         A2: ( Carrier KL) c= b2 by Th8;

        deffunc V( Nat) = (KL . (b1 /. $1));

        consider A be FinSequence of INT.Ring such that

         A3: ( len A) = ( len b1) and

         A4: for k be Nat st k in ( dom A) holds (A . k) = V(k) from FINSEQ_2:sch 1;

        take A;

        thus ( len A) = ( len b1) by A3;

        take KL;

        thus W = ( Sum KL) by A1;

        thus ( Carrier KL) c= ( rng b1) by A2;

        let k;

        

         A5: ( dom A) = ( Seg ( len b1)) by A3, FINSEQ_1:def 3;

        assume

         A6: 1 <= k & k <= ( len A);

        then k in ( Seg ( len b1)) by A3, FINSEQ_1: 1;

        then k in ( dom A) by A3, FINSEQ_1:def 3;

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

        hence thesis by A3, A4, A5, A6, FINSEQ_1: 1;

      end;

      uniqueness

      proof

        reconsider b = ( rng b1) as Basis of V by defOrdBasis;

        let F1,F2 be FinSequence of INT.Ring ;

        assume

         A7: ( len F1) = ( len b1);

        given KL1 be Linear_Combination of V such that

         A8: W = ( Sum KL1) & ( Carrier KL1) c= ( rng b1) and

         A9: for k st 1 <= k & k <= ( len F1) holds (F1 /. k) = (KL1 . (b1 /. k));

        assume

         A10: ( len F2) = ( len b1);

        given KL2 be Linear_Combination of V such that

         A11: W = ( Sum KL2) & ( Carrier KL2) c= ( rng b1) and

         A12: for k st 1 <= k & k <= ( len F2) holds (F2 /. k) = (KL2 . (b1 /. k));

        

         A13: b is linearly-independent by VECTSP_7:def 3;

        for k be Nat st 1 <= k & k <= ( len F1) holds (F1 . k) = (F2 . k)

        proof

          let k be Nat;

          assume

           A14: 1 <= k & k <= ( len F1);

          then

           A15: k in ( dom F2) by A7, A10, FINSEQ_3: 25;

          k in ( dom F1) by A14, FINSEQ_3: 25;

          

          hence (F1 . k) = (F1 /. k) by PARTFUN1:def 6

          .= (KL1 . (b1 /. k)) by A9, A14

          .= (KL2 . (b1 /. k)) by A8, A11, A13, Th5

          .= (F2 /. k) by A7, A10, A12, A14

          .= (F2 . k) by A15, PARTFUN1:def 6;

        end;

        hence thesis by A7, A10, FINSEQ_1: 14;

      end;

    end

    

     Lm1: for V be finite-rank free Z_Module holds for b be OrdBasis of V holds for W be Element of V holds ( dom (W |-- b)) = ( dom b)

    proof

      let V be finite-rank free Z_Module, b be OrdBasis of V, W be Element of V;

      ( len (W |-- b)) = ( len b) by Def7;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: ZMATRLIN:29

    

     Th34: (v1 |-- b2) = (v2 |-- b2) implies v1 = v2

    proof

      consider KL1 be Linear_Combination of V2 such that

       A1: v1 = ( Sum KL1) and

       A2: ( Carrier KL1) c= ( rng b2) and

       A3: for t st 1 <= t & t <= ( len (v1 |-- b2)) holds ((v1 |-- b2) /. t) = (KL1 . (b2 /. t)) by Def7;

      consider KL2 be Linear_Combination of V2 such that

       A4: v2 = ( Sum KL2) and

       A5: ( Carrier KL2) c= ( rng b2) and

       A6: for t st 1 <= t & t <= ( len (v2 |-- b2)) holds ((v2 |-- b2) /. t) = (KL2 . (b2 /. t)) by Def7;

      assume

       A7: (v1 |-- b2) = (v2 |-- b2);

       A8:

      now

        let t be Nat;

        assume

         A9: 1 <= t & t <= ( len (v1 |-- b2));

        

        hence (KL1 . (b2 /. t)) = ((v2 |-- b2) /. t) by A7, A3

        .= (KL2 . (b2 /. t)) by A7, A6, A9;

      end;

      

       A10: (( Carrier KL1) \/ ( Carrier KL2)) c= ( rng b2) by A2, A5, XBOOLE_1: 8;

      now

        let v be Vector of V2;

        per cases ;

          suppose

           A11: not v in (( Carrier KL1) \/ ( Carrier KL2));

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

          then

           A12: (KL2 . v) = 0 ;

           not v in ( Carrier KL1) by A11, XBOOLE_0:def 3;

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

        end;

          suppose v in (( Carrier KL1) \/ ( Carrier KL2));

          then

          consider x be object such that

           A13: x in ( dom b2) and

           A14: v = (b2 . x) by A10, FUNCT_1:def 3;

          reconsider x as Nat by A13;

          x <= ( len b2) by A13, FINSEQ_3: 25;

          then

           A15: x <= ( len (v1 |-- b2)) by Def7;

          v = (b2 /. x) & 1 <= x by A13, A14, FINSEQ_3: 25, PARTFUN1:def 6;

          hence (KL1 . v) = (KL2 . v) by A8, A15;

        end;

      end;

      hence thesis by A1, A4, VECTSP_6:def 7;

    end;

    theorem :: ZMATRLIN:30

    

     Th35: v = ( Sum ( lmlt ((v |-- b1),b1)))

    proof

      consider KL be Linear_Combination of V1 such that

       A1: v = ( Sum KL) & ( Carrier KL) c= ( rng b1) and

       A2: for k st 1 <= k & k <= ( len (v |-- b1)) holds ((v |-- b1) /. k) = (KL . (b1 /. k)) by Def7;

      ( len (v |-- b1)) = ( len b1) by Def7;

      then

       A3: ( dom (v |-- b1)) = ( dom b1) by FINSEQ_3: 29;

      then

       A4: ( dom b1) = ( dom ( lmlt ((v |-- b1),b1))) by Th12;

      

       A51: ( len (KL (#) b1)) = ( len b1) by VECTSP_6:def 5

      .= ( len ( lmlt ((v |-- b1),b1))) by A4, FINSEQ_3: 29;

      then

       A5: ( dom (KL (#) b1)) = ( dom ( lmlt ((v |-- b1),b1))) by FINSEQ_3: 29;

       A6:

      now

        let t be Nat;

        assume

         A7: t in ( dom ( lmlt ((v |-- b1),b1)));

        then

         A8: (b1 /. t) = (b1 . t) by A4, PARTFUN1:def 6;

        t in ( dom (v |-- b1)) by A3, A7, Th12;

        then

         A9: t <= ( len (v |-- b1)) by FINSEQ_3: 25;

        

         A10: 1 <= t by A7, FINSEQ_3: 25;

        then

         A11: ((v |-- b1) /. t) = ((v |-- b1) . t) by A9, FINSEQ_4: 15;

        t in ( dom (KL (#) b1)) by A51, A7, FINSEQ_3: 29;

        

        hence ((KL (#) b1) . t) = ((KL . (b1 /. t)) * (b1 /. t)) by VECTSP_6:def 5

        .= (((v |-- b1) /. t) * (b1 /. t)) by A2, A10, A9

        .= (( lmlt ((v |-- b1),b1)) . t) by A7, A8, A11, FUNCOP_1: 22;

      end;

      

      thus v = ( Sum (KL (#) b1)) by A1, defOrdBasis, Th20

      .= ( Sum ( lmlt ((v |-- b1),b1))) by A5, A6, FINSEQ_1: 13;

    end;

    theorem :: ZMATRLIN:31

    

     Th36: ( len d) = ( len b1) implies d = (( Sum ( lmlt (d,b1))) |-- b1)

    proof

      reconsider T = ( rng b1) as finite Subset of V1;

      defpred X[ Element of V1, Element of INT.Ring ] means ($1 in ( rng b1) implies (for k st k in ( dom b1) & (b1 /. k) = $1 holds $2 = (d /. k))) & ( not $1 in ( rng b1) implies $2 = ( 0. INT.Ring ));

      

       A1: for v holds ex u be Element of INT.Ring st X[v, u]

      proof

        let v be Element of V1;

        per cases ;

          suppose

           A2: v in ( rng b1);

          then

          consider k be Element of NAT such that

           A3: k in ( dom b1) and

           A4: (b1 /. k) = v by PARTFUN2: 2;

          take u = (d /. k);

          now

            

             A5: b1 is one-to-one by defOrdBasis;

            let i;

            assume that

             A6: i in ( dom b1) and

             A7: (b1 /. i) = v;

            (b1 . i) = (b1 /. k) by A4, A6, A7, PARTFUN1:def 6

            .= (b1 . k) by A3, PARTFUN1:def 6;

            hence u = (d /. i) by A3, A6, A5;

          end;

          hence thesis by A2;

        end;

          suppose

           A8: not v in ( rng b1);

          reconsider I0 = ( 0. INT.Ring ) as Element of INT.Ring ;

          take I0;

          thus thesis by A8;

        end;

      end;

      consider KL be Function of V1, the carrier of INT.Ring such that

       A9: for v holds X[v, (KL . v)] from FUNCT_2:sch 3( A1);

      now

        take f = KL;

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

      end;

      then KL in ( Funcs (the carrier of V1,the carrier of INT.Ring )) by FUNCT_2:def 2;

      then

      reconsider KL1 = KL as Linear_Combination of V1 by A9, VECTSP_6:def 1;

      assume

       A11: ( len d) = ( len b1);

      now

        take KL1;

        thus

         A13: for k st 1 <= k & k <= ( len d) holds (d /. k) = (KL1 . (b1 /. k))

        proof

          let k;

          assume

           A141: 1 <= k & k <= ( len d);

          then

           A14: k in ( dom b1) by A11, FINSEQ_3: 25;

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

          then (b1 /. k) in ( rng b1) by A14, FUNCT_1:def 3;

          hence thesis by A9, A11, A141, FINSEQ_3: 25;

        end;

        for x be object holds x in ( Carrier KL1) implies x in ( rng b1)

        proof

          let x be object;

          assume x in ( Carrier KL1);

          then

           A15: ex v st x = v & (KL1 . v) <> 0 ;

          assume not x in ( rng b1);

          hence contradiction by A9, A15;

        end;

        hence

         A16: ( Carrier KL1) c= ( rng b1);

        

         A17: ( dom d) = ( dom b1) by A11, FINSEQ_3: 29;

        then

         A18: ( dom ( lmlt (d,b1))) = ( dom b1) by Th12;

        

        then

         A19: ( len ( lmlt (d,b1))) = ( len b1) by FINSEQ_3: 29

        .= ( len (KL1 (#) b1)) by VECTSP_6:def 5;

        now

          let k be Nat;

          assume

           A20: k in ( dom ( lmlt (d,b1)));

          then

           A21: k in ( dom (KL1 (#) b1)) by A19, FINSEQ_3: 29;

          

           A22: 1 <= k & k <= ( len d) by A11, A18, A20, FINSEQ_3: 25;

          

           A23: (d /. k) = (d . k) & (b1 /. k) = (b1 . k) by A17, A18, A20, PARTFUN1:def 6;

          

          thus (( lmlt (d,b1)) . k) = (the lmult of V1 . ((d . k),(b1 . k))) by A20, FUNCOP_1: 22

          .= ((KL1 . (b1 /. k)) * (b1 /. k)) by A13, A22, A23

          .= ((KL1 (#) b1) . k) by A21, VECTSP_6:def 5;

        end;

        

        hence ( Sum ( lmlt (d,b1))) = ( Sum (KL1 (#) b1)) by A19, FINSEQ_2: 9

        .= ( Sum KL1) by A16, defOrdBasis, Th20;

      end;

      hence thesis by A11, Def7;

    end;

    

     Lm2: for p be FinSequence, k be set st k in ( dom p) holds ( len p) > 0

    proof

      let p be FinSequence, k be set;

      assume k in ( dom p);

      then p <> {} ;

      hence thesis;

    end;

    theorem :: ZMATRLIN:32

    

     Th37: for a,d be FinSequence of INT.Ring st ( len a) = ( len b1) holds for j be Nat st j in ( dom b2) & ( len d) = ( len b1) & for k st k in ( dom b1) holds (d . k) = (((f . (b1 /. k)) |-- b2) /. j) holds ( len b1) > 0 implies ((( Sum ( lmlt (a,(f * b1)))) |-- b2) /. j) = ( Sum ( mlt (a,d)))

    proof

      let a,d be FinSequence of INT.Ring such that

       A1: ( len a) = ( len b1);

      reconsider B3 = (f * b1) as FinSequence of V2;

      deffunc V( Nat, Nat) = (((B3 /. $1) |-- b2) /. $2);

      consider M be Matrix of ( len b1), ( len b2), INT.Ring such that

       A2: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = V(i,j) from MATRIX_0:sch 1;

      deffunc W( Nat) = ( Sum ( mlt (a,( Col (M,$1)))));

      consider dd be FinSequence of INT.Ring such that

       A3: ( len dd) = ( len b2) & for j be Nat st j in ( dom dd) holds (dd /. j) = W(j) from FINSEQ_4:sch 2;

      let j be Nat such that

       A4: j in ( dom b2);

      

       A5: j in ( dom dd) by A4, A3, FINSEQ_3: 29;

      assume that

       A6: ( len d) = ( len b1) and

       A7: for k st k in ( dom b1) holds (d . k) = (((f . (b1 /. k)) |-- b2) /. j);

      

       A8: ( len ( Col (M,j))) = ( len M) by MATRIX_0:def 8

      .= ( len d) by A6, MATRIX_0:def 2;

      ( len M) = ( len b1) by MATRIX_0:def 2;

      then

       A9: ( dom M) = ( dom b1) by FINSEQ_3: 29;

      

       A10: ( len b1) = ( len B3) by FINSEQ_2: 33;

      then

       A11: ( dom b1) = ( dom B3) by FINSEQ_3: 29;

      assume

       A12: ( len b1) > 0 ;

      then

       A13: ( width M) = ( len b2) by MATRIX_0: 23;

       A14:

      now

        let i such that

         A15: i in ( dom B3);

         A16:

        now

          let j be Nat;

          assume

           A17: j in ( dom ((B3 /. i) |-- b2));

          then j in ( Seg ( len ((B3 /. i) |-- b2))) by FINSEQ_1:def 3;

          then

           A18: j in ( Seg ( width M)) by A13, Def7;

          then

           A19: [i, j] in ( Indices M) by A9, A11, A15, ZFMISC_1: 87;

          

          thus (( Line (M,i)) . j) = (M * (i,j)) by A18, MATRIX_0:def 7

          .= (((B3 /. i) |-- b2) /. j) by A2, A19

          .= (((B3 /. i) |-- b2) . j) by A17, PARTFUN1:def 6;

        end;

        

         A20: ( len ( Line (M,i))) = ( width M) by MATRIX_0:def 7

        .= ( len ((B3 /. i) |-- b2)) by A13, Def7;

        

        thus (B3 /. i) = ( Sum ( lmlt (((B3 /. i) |-- b2),b2))) by Th35

        .= ( Sum ( lmlt (( Line (M,i)),b2))) by A20, A16, FINSEQ_2: 9;

      end;

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

      then

       A21: j in ( Seg ( width M)) by A4, A12, MATRIX_0: 23;

       A22:

      now

        let i be Nat;

        assume i in ( dom d);

        then

         A23: i in ( dom b1) by A6, FINSEQ_3: 29;

        

        then

         A24: (B3 /. i) = (B3 . i) by A11, PARTFUN1:def 6

        .= (f . (b1 . i)) by A23, FUNCT_1: 13

        .= (f . (b1 /. i)) by A23, PARTFUN1:def 6;

        

         A25: [i, j] in ( Indices M) by A9, A21, A23, ZFMISC_1: 87;

        

        thus (( Col (M,j)) . i) = (M * (i,j)) by A9, A23, MATRIX_0:def 8

        .= (((f . (b1 /. i)) |-- b2) /. j) by A2, A24, A25

        .= (d . i) by A7, A23;

      end;

      ( len b2) > 0 by A4, Lm2;

      

      hence ((( Sum ( lmlt (a,(f * b1)))) |-- b2) /. j) = ((( Sum ( lmlt (dd,b2))) |-- b2) /. j) by A1, A12, A3, A10, A14, Th33

      .= (dd /. j) by A3, Th36

      .= ( Sum ( mlt (a,( Col (M,j))))) by A3, A5

      .= ( Sum ( mlt (a,d))) by A8, A22, FINSEQ_2: 9;

    end;

    begin

    definition

      let V1,V2 be finite-rank free Z_Module;

      let f be Function of V1, V2;

      let b1 be FinSequence of V1;

      let b2 be OrdBasis of V2;

      :: ZMATRLIN:def8

      func AutMt (f,b1,b2) -> Matrix of INT.Ring means

      : Def8: ( len it ) = ( len b1) & for k st k in ( dom b1) holds (it /. k) = ((f . (b1 /. k)) |-- b2);

      existence

      proof

        deffunc V( Nat) = ((f . (b1 /. $1)) |-- b2);

        consider M be FinSequence such that

         A1: ( len M) = ( len b1) and

         A2: for k be Nat st k in ( dom M) holds (M . k) = V(k) from FINSEQ_1:sch 2;

        

         A3: ( dom M) = ( Seg ( len b1)) by A1, FINSEQ_1:def 3;

        ex n be Nat st for x st x in ( rng M) holds ex s st s = x & ( len s) = n

        proof

          take n = ( len ((f . (b1 /. 1)) |-- b2));

          let x be object;

          assume x in ( rng M);

          then

          consider y be object such that

           A4: y in ( dom M) and

           A5: x = (M . y) by FUNCT_1:def 3;

          reconsider y as Nat by A4;

          (M . y) = ((f . (b1 /. y)) |-- b2) by A2, A4;

          then

          reconsider s = (M . y) as FinSequence;

          take s;

          thus s = x by A5;

          

          thus ( len s) = ( len ((f . (b1 /. y)) |-- b2)) by A2, A4

          .= ( len b2) by Def7

          .= n by Def7;

        end;

        then

        reconsider M as tabular FinSequence by MATRIX_0:def 1;

        now

          let x be object;

          assume x in ( rng M);

          then

          consider y be object such that

           A6: y in ( dom M) and

           A7: x = (M . y) by FUNCT_1:def 3;

          reconsider y as Nat by A6;

          (M . y) = ((f . (b1 /. y)) |-- b2) by A2, A6;

          then

          reconsider s = (M . y) as FinSequence of INT ;

          s = x by A7;

          hence x in ( INT * ) by FINSEQ_1:def 11;

        end;

        then ( rng M) c= (the carrier of INT.Ring * );

        then

        reconsider M as Matrix of INT.Ring by FINSEQ_1:def 4;

        take M1 = M;

        for k st k in ( dom b1) holds (M1 /. k) = ((f . (b1 /. k)) |-- b2)

        proof

          let k be Nat;

          assume

           A8: k in ( dom b1);

          then

           A9: k in ( Seg ( len b1)) by FINSEQ_1:def 3;

          ( dom M1) = ( dom b1) by A1, FINSEQ_3: 29;

          

          hence (M1 /. k) = (M1 . k) by A8, PARTFUN1:def 6

          .= ((f . (b1 /. k)) |-- b2) by A2, A3, A9;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let K1,K2 be Matrix of INT.Ring such that

         A10: ( len K1) = ( len b1) and

         A11: for k st k in ( dom b1) holds (K1 /. k) = ((f . (b1 /. k)) |-- b2) and

         A12: ( len K2) = ( len b1) and

         A13: for k st k in ( dom b1) holds (K2 /. k) = ((f . (b1 /. k)) |-- b2);

        for k be Nat st 1 <= k & k <= ( len K1) holds (K1 . k) = (K2 . k)

        proof

          let k be Nat;

          assume

           A14: 1 <= k & k <= ( len K1);

          

           A16: k in ( dom K2) by A10, A12, A14, FINSEQ_3: 25;

          k in ( dom K1) by A14, FINSEQ_3: 25;

          

          hence (K1 . k) = (K1 /. k) by PARTFUN1:def 6

          .= ((f . (b1 /. k)) |-- b2) by A10, A11, A14, FINSEQ_3: 25

          .= (K2 /. k) by A10, A13, A14, FINSEQ_3: 25

          .= (K2 . k) by A16, PARTFUN1:def 6;

        end;

        hence thesis by A10, A12, FINSEQ_1: 14;

      end;

    end

    

     Lm3: ( dom ( AutMt (f,b1,b2))) = ( dom b1)

    proof

      ( len ( AutMt (f,b1,b2))) = ( len b1) by Def8;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: ZMATRLIN:33

    

     Th38: ( len b1) = 0 implies ( AutMt (f,b1,b2)) = {}

    proof

      assume ( len b1) = 0 ;

      then ( len ( AutMt (f,b1,b2))) = 0 by Def8;

      hence thesis;

    end;

    theorem :: ZMATRLIN:34

    

     Th39: ( len b1) > 0 implies ( width ( AutMt (f,b1,b2))) = ( len b2)

    proof

      assume ( len b1) > 0 ;

      then ( len ( AutMt (f,b1,b2))) > 0 by Def8;

      then

      consider s be FinSequence such that

       A1: s in ( rng ( AutMt (f,b1,b2))) and

       A2: ( len s) = ( width ( AutMt (f,b1,b2))) by MATRIX_0:def 3;

      consider i be Nat such that

       A3: i in ( dom ( AutMt (f,b1,b2))) and

       A4: (( AutMt (f,b1,b2)) . i) = s by A1, FINSEQ_2: 10;

      ( len ( AutMt (f,b1,b2))) = ( len b1) by Def8;

      then

       A5: i in ( dom b1) by A3, FINSEQ_3: 29;

      s = (( AutMt (f,b1,b2)) /. i) by A3, A4, PARTFUN1:def 6

      .= ((f . (b1 /. i)) |-- b2) by A5, Def8;

      hence thesis by A2, Def7;

    end;

    theorem :: ZMATRLIN:35

    f1 is additive homogeneous & f2 is additive homogeneous & ( AutMt (f1,b1,b2)) = ( AutMt (f2,b1,b2)) & ( len b1) > 0 implies f1 = f2

    proof

      assume that

       A1: f1 is additive homogeneous & f2 is additive homogeneous and

       A2: ( AutMt (f1,b1,b2)) = ( AutMt (f2,b1,b2)) and

       A3: ( len b1) > 0 ;

      

       A4: ( rng b1) c= the carrier of V1;

      then

       A5: ( rng b1) c= ( dom f2) by FUNCT_2:def 1;

      ( rng b1) c= ( dom f1) by A4, FUNCT_2:def 1;

      

      then

       A6: ( dom (f1 * b1)) = ( dom b1) by RELAT_1: 27

      .= ( dom (f2 * b1)) by A5, RELAT_1: 27;

      now

        let x be object;

        assume

         A7: x in ( dom (f1 * b1));

        then

        reconsider k = x as Nat;

        

         A8: ( dom (f1 * b1)) c= ( dom b1) by RELAT_1: 25;

        

        then

         A9: ((f1 . (b1 /. k)) |-- b2) = (( AutMt (f2,b1,b2)) /. k) by A2, A7, Def8

        .= ((f2 . (b1 /. k)) |-- b2) by A7, A8, Def8;

        

        thus ((f1 * b1) . x) = (f1 . (b1 . x)) by A7, FUNCT_1: 12

        .= (f1 . (b1 /. x)) by A7, A8, PARTFUN1:def 6

        .= (f2 . (b1 /. x)) by A9, Th34

        .= (f2 . (b1 . x)) by A7, A8, PARTFUN1:def 6

        .= ((f2 * b1) . x) by A6, A7, FUNCT_1: 12;

      end;

      hence thesis by A1, A3, A6, Th22, FUNCT_1: 2;

    end;

    theorem :: ZMATRLIN:36

    

     LmSign1X: for F be FinSequence of F_Real , G be FinSequence of INT.Ring st F = G holds ( Sum F) = ( Sum G)

    proof

      defpred P[ Nat] means for F be FinSequence of F_Real , G be FinSequence of INT.Ring st ( len F) = $1 & F = G holds ( Sum F) = ( Sum G);

      

       P1: P[ 0 ]

      proof

        let F be FinSequence of F_Real , G be FinSequence of INT.Ring ;

        assume

         AS1: ( len F) = 0 & F = G;

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

        

        then

         P1: ( Sum F) = ( 0. F_Real ) by RLVECT_1: 43

        .= 0 ;

        G = ( <*> REAL ) by AS1;

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

        then ( Sum G) = ( 0. INT.Ring ) by RLVECT_1: 43;

        hence thesis by P1;

      end;

      

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

      proof

        let n be Nat;

        assume

         AS1: P[n];

        let F be FinSequence of F_Real , G be FinSequence of INT.Ring ;

        assume

         AS2: ( len F) = (n + 1) & F = G;

        reconsider F0 = (F | n) as FinSequence of F_Real ;

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

        then (n + 1) in ( dom F) by AS2, FINSEQ_1:def 3;

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

        then

        reconsider af = (F . (n + 1)) as Element of F_Real ;

        

         P1: ( len F0) = n by FINSEQ_1: 59, AS2, NAT_1: 11;

        then

         P4: ( dom F0) = ( Seg n) by FINSEQ_1:def 3;

        

         A9: ( len F) = (( len F0) + 1) by AS2, FINSEQ_1: 59, NAT_1: 11;

        F0 = (F | ( dom F0)) by P4, FINSEQ_1:def 15;

        then

         P3: ( Sum F) = (( Sum F0) + af) by AS2, A9, RLVECT_1: 38;

        reconsider G0 = (G | n) as FinSequence of INT.Ring ;

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

        then (n + 1) in ( dom G) by AS2, FINSEQ_1:def 3;

        then (G . (n + 1)) in ( rng G) by FUNCT_1: 3;

        then

        reconsider bf = (G . (n + 1)) as Element of INT.Ring ;

        ( len G) = (n + 1) & G0 = (G | ( Seg n)) by AS2, FINSEQ_1:def 15;

        then G = (G0 ^ <*bf*>) by FINSEQ_3: 55;

        then ( Sum G) = (( Sum G0) + bf) by FVSUM_1: 71;

        hence ( Sum F) = ( Sum G) by AS1, AS2, P1, P3;

      end;

      

       X1: for n be Nat holds P[n] from NAT_1:sch 2( P1, P2);

      let F be FinSequence of F_Real , G be FinSequence of INT.Ring ;

      assume

       X2: F = G;

      ( len F) is Nat;

      hence thesis by X1, X2;

    end;

    

     LMEQ5: for f,g,h be Function st (f | ( dom g)) = g & ( rng h) c= ( dom g) & ( rng h) c= ( dom f) holds (f * h) = (g * h)

    proof

      let f,g,h be Function;

      assume

       AS: (f | ( dom g)) = g & ( rng h) c= ( dom g) & ( rng h) c= ( dom f);

      

       P1: ( dom (f * h)) = ( dom h) by AS, RELAT_1: 27;

      

       P2: ( dom (g * h)) = ( dom h) by AS, RELAT_1: 27;

      for x be object st x in ( dom (f * h)) holds ((f * h) . x) = ((g * h) . x)

      proof

        let x be object;

        assume

         AS1: x in ( dom (f * h));

        then x in ( dom h) by AS, RELAT_1: 27;

        then

         P3: (h . x) in ( rng h) by FUNCT_1: 3;

        

        thus ((f * h) . x) = (f . (h . x)) by FUNCT_1: 12, AS1

        .= ((f | ( dom g)) . (h . x)) by AS, P3, FUNCT_1: 49

        .= ((g * h) . x) by AS, AS1, P1, P2, FUNCT_1: 12;

      end;

      hence thesis by AS, P1, RELAT_1: 27;

    end;

    

     LMLT12: multint = ( multreal | [: INT , INT :])

    proof

      set ad = ( multreal | [: INT , INT :]);

       [: INT , INT :] c= [: REAL , REAL :] by NUMBERS: 15, ZFMISC_1: 96;

      then

       A1: [: INT , INT :] c= ( dom multreal ) by FUNCT_2:def 1;

      then

       A2: ( dom ad) = [: INT , INT :] by RELAT_1: 62;

      

       A3: ( dom multint ) = [: INT , INT :] by FUNCT_2:def 1;

      for z be object st z in ( dom ad) holds (ad . z) = ( multint . z)

      proof

        let z be object;

        assume

         A4: z in ( dom ad);

        then

        consider x,y be object such that

         A5: x in INT & y in INT & z = [x, y] by A2, ZFMISC_1:def 2;

        reconsider x1 = x, y1 = y as Integer by A5;

        

        thus (ad . z) = ( multreal . (x1,y1)) by A4, A5, A2, FUNCT_1: 49

        .= (x1 * y1) by BINOP_2:def 11

        .= ( multint . (x1,y1)) by BINOP_2:def 22

        .= ( multint . z) by A5;

      end;

      hence thesis by A1, A3, FUNCT_1: 2, RELAT_1: 62;

    end;

    theorem :: ZMATRLIN:37

    for p,q be FinSequence of INT.Ring , p1,q1 be FinSequence of F_Real st p = p1 & q = q1 holds (p "*" q) = (p1 "*" q1)

    proof

      let p,q be FinSequence of INT.Ring , p1,q1 be FinSequence of F_Real ;

      assume

       AS: p = p1 & q = q1;

      

       A2: [:( rng p), ( rng q):] c= [: INT , INT :] by ZFMISC_1: 96;

      

       A3: ( rng <:p, q:>) c= [:( rng p), ( rng q):] by FUNCT_3: 51;

      

       B1: ( dom multreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

       [: INT , INT :] c= [: REAL , REAL :] by NUMBERS: 15, ZFMISC_1: 96;

      then

       B2: ( rng <:p, q:>) c= ( dom multreal ) by A2, A3, B1;

       [: INT , INT :] = ( dom multint ) by FUNCT_2:def 1;

      then

       B3: ( rng <:p, q:>) c= ( dom multint ) by A2, A3;

      ( multreal | ( dom multint )) = multint by LMLT12, FUNCT_2:def 1;

      then

       A6: ( multint * <:p, q:>) = ( multreal * <:p, q:>) by LMEQ5, B3, B2;

      ( mlt (p,q)) = ( multint * <:p1, q1:>) by AS, FUNCOP_1:def 3

      .= ( mlt (p1,q1)) by AS, A6, FUNCOP_1:def 3;

      hence thesis by LmSign1X;

    end;

    theorem :: ZMATRLIN:38

    

     ThComp1: g is additive homogeneous & ( len b1) > 0 & ( len b2) > 0 implies ( AutMt ((g * f),b1,b3)) = (( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3)))

    proof

      assume

       A1: g is additive homogeneous;

      assume that

       A2: ( len b1) > 0 and

       A3: ( len b2) > 0 ;

      

       A4: ( width ( AutMt (f,b1,b2))) = ( len b2) by A2, Th39

      .= ( len ( AutMt (g,b2,b3))) by Def8;

      

       A5: ( width ( AutMt ((g * f),b1,b3))) = ( len b3) by A2, Th39

      .= ( width ( AutMt (g,b2,b3))) by A3, Th39;

      

       A6: ( width ( AutMt ((g * f),b1,b3))) = ( width (( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3)))) by A5, A4, MATRIX_3:def 4;

      

       A7: ( len ( AutMt ((g * f),b1,b3))) = ( len b1) by Def8

      .= ( len ( AutMt (f,b1,b2))) by Def8

      .= ( len (( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3)))) by A4, MATRIX_3:def 4;

      for i, j st [i, j] in ( Indices ( AutMt ((g * f),b1,b3))) holds (( AutMt ((g * f),b1,b3)) * (i,j)) = ((( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3))) * (i,j))

      proof

        let i, j;

        deffunc V( Nat) = (((g . (b2 /. $1)) |-- b3) /. j);

        consider d be FinSequence of INT.Ring such that

         A9: ( len d) = ( len b2) & for k be Nat st k in ( dom d) holds (d . k) = V(k) from FINSEQ_2:sch 1;

        assume

         A10: [i, j] in ( Indices ( AutMt ((g * f),b1,b3)));

        then

         A12: j in ( Seg ( width ( AutMt ((g * f),b1,b3)))) by ZFMISC_1: 87;

        

         A13: ( len ( Col (( AutMt (g,b2,b3)),j))) = ( len ( AutMt (g,b2,b3))) by MATRIX_0:def 8

        .= ( len d) by A9, Def8;

        

         A14: ( dom d) = ( Seg ( len b2)) by A9, FINSEQ_1:def 3;

        

         A15: [i, j] in ( Indices (( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3)))) by A6, A7, A10, FINSEQ_3: 29;

        

         A16: i in ( dom ( AutMt ((g * f),b1,b3))) by A10, ZFMISC_1: 87;

        

         A17: ( width ( AutMt ((g * f),b1,b3))) <> {} by A10;

        ( len b1) = ( len ( AutMt ((g * f),b1,b3))) by Def8;

        then ( len b1) > 0 by A17, MATRIX_0:def 3;

        then

         A18: j in ( Seg ( len b3)) by A12, Th39;

        then

         A19: j in ( dom b3) by FINSEQ_1:def 3;

         A20:

        now

          let k be Nat;

          assume

           A21: 1 <= k & k <= ( len d);

          

           A23: k in ( dom b2) by A9, A21, FINSEQ_3: 25;

          

           A24: ( len ( AutMt (g,b2,b3))) = ( len b2) by Def8;

          then

           A25: k in ( dom ( AutMt (g,b2,b3))) by A9, A21, FINSEQ_3: 25;

          j in ( Seg ( width ( AutMt (g,b2,b3)))) by A5, A10, ZFMISC_1: 87;

          then [k, j] in ( Indices ( AutMt (g,b2,b3))) by A25, ZFMISC_1: 87;

          then

          consider p2 be FinSequence of INT such that

           A26: p2 = (( AutMt (g,b2,b3)) . k) and

           A27: (( AutMt (g,b2,b3)) * (k,j)) = (p2 . j) by MATRIX_0:def 5;

          

           A28: p2 = (( AutMt (g,b2,b3)) /. k) by A25, A26, PARTFUN1:def 6

          .= ((g . (b2 /. k)) |-- b3) by A23, Def8;

          then j in ( Seg ( len p2)) by A18, Def7;

          then

           A29: j in ( dom p2) by FINSEQ_1:def 3;

          k in ( dom ( AutMt (g,b2,b3))) by A9, A21, A24, FINSEQ_3: 25;

          

          hence (( Col (( AutMt (g,b2,b3)),j)) . k) = (p2 . j) by A27, MATRIX_0:def 8

          .= (((g . (b2 /. k)) |-- b3) /. j) by A28, A29, PARTFUN1:def 6

          .= (d . k) by A9, A21, FINSEQ_3: 25;

        end;

        (b1 /. i) in the carrier of V1;

        then

         A30: (b1 /. i) in ( dom f) by FUNCT_2:def 1;

        consider p1 be FinSequence of INT such that

         A31: p1 = (( AutMt ((g * f),b1,b3)) . i) and

         A32: (( AutMt ((g * f),b1,b3)) * (i,j)) = (p1 . j) by A10, MATRIX_0:def 5;

        

         A33: ( len ((f . (b1 /. i)) |-- b2)) = ( len b2) by Def7;

        

         A34: ( len ( AutMt ((g * f),b1,b3))) = ( len b1) by Def8;

        then

         A35: i in ( dom b1) by A16, FINSEQ_3: 29;

        

         A36: p1 = (( AutMt ((g * f),b1,b3)) /. i) by A16, A31, PARTFUN1:def 6

        .= (((g * f) . (b1 /. i)) |-- b3) by A35, Def8;

        ( len ( AutMt (f,b1,b2))) = ( len b1) by Def8;

        then

         A37: i in ( dom ( AutMt (f,b1,b2))) by A16, A34, FINSEQ_3: 29;

        

        then

         A38: ( Line (( AutMt (f,b1,b2)),i)) = (( AutMt (f,b1,b2)) . i) by MATRIX_0: 60

        .= (( AutMt (f,b1,b2)) /. i) by A37, PARTFUN1:def 6

        .= ((f . (b1 /. i)) |-- b2) by A35, Def8;

        

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

        j in ( Seg ( len (((g * f) . (b1 /. i)) |-- b3))) by A18, Def7;

        then

         A40: j in ( dom p1) by A36, FINSEQ_1:def 3;

        

        thus (( AutMt ((g * f),b1,b3)) * (i,j)) = ((((g * f) . (b1 /. i)) |-- b3) /. j) by A32, A36, A40, PARTFUN1:def 6

        .= (((g . (f . (b1 /. i))) |-- b3) /. j) by A30, FUNCT_1: 13

        .= (((g . ( Sum ( lmlt (((f . (b1 /. i)) |-- b2),b2)))) |-- b3) /. j) by Th35

        .= ((( Sum ( lmlt (((f . (b1 /. i)) |-- b2),(g * b2)))) |-- b3) /. j) by A1, A33, Th18

        .= ( Sum ( mlt (((f . (b1 /. i)) |-- b2),d))) by A3, A19, A9, A14, A39, A33, Th37

        .= (( Line (( AutMt (f,b1,b2)),i)) "*" ( Col (( AutMt (g,b2,b3)),j))) by A38, A13, A20, FINSEQ_1: 14

        .= ((( AutMt (f,b1,b2)) * ( AutMt (g,b2,b3))) * (i,j)) by A4, A15, MATRIX_3:def 4;

      end;

      hence thesis by A7, A6, MATRIX_0: 21;

    end;

    theorem :: ZMATRLIN:39

    ( AutMt ((f1 + f2),b1,b2)) = (( AutMt (f1,b1,b2)) + ( AutMt (f2,b1,b2)))

    proof

      

       A1: ( len ( AutMt ((f1 + f2),b1,b2))) = ( len b1) by Def8

      .= ( len ( AutMt (f1,b1,b2))) by Def8;

      

       A3: ( width ( AutMt (f1,b1,b2))) = ( width ( AutMt (f2,b1,b2)))

      proof

        per cases ;

          suppose

           A4: ( len b1) = 0 ;

          

          then ( AutMt (f1,b1,b2)) = {} by Th38

          .= ( AutMt (f2,b1,b2)) by A4, Th38;

          hence thesis;

        end;

          suppose

           A5: ( len b1) > 0 ;

          

          hence ( width ( AutMt (f1,b1,b2))) = ( len b2) by Th39

          .= ( width ( AutMt (f2,b1,b2))) by A5, Th39;

        end;

      end;

      

       A6: ( width ( AutMt ((f1 + f2),b1,b2))) = ( width ( AutMt (f1,b1,b2)))

      proof

        per cases ;

          suppose

           A7: ( len b1) = 0 ;

          

          then ( AutMt ((f1 + f2),b1,b2)) = {} by Th38

          .= ( AutMt (f1,b1,b2)) by A7, Th38;

          hence thesis;

        end;

          suppose

           A8: ( len b1) > 0 ;

          

          hence ( width ( AutMt ((f1 + f2),b1,b2))) = ( len b2) by Th39

          .= ( width ( AutMt (f1,b1,b2))) by A8, Th39;

        end;

      end;

      then

       A9: ( width ( AutMt ((f1 + f2),b1,b2))) = ( width (( AutMt (f1,b1,b2)) + ( AutMt (f2,b1,b2)))) by MATRIX_3:def 3;

      

       AX10: ( len ( AutMt (f1,b1,b2))) = ( len b1) by Def8

      .= ( len ( AutMt (f2,b1,b2))) by Def8;

      

       A11: for i, j st [i, j] in ( Indices ( AutMt ((f1 + f2),b1,b2))) holds (( AutMt ((f1 + f2),b1,b2)) * (i,j)) = ((( AutMt (f1,b1,b2)) + ( AutMt (f2,b1,b2))) * (i,j))

      proof

        let i, j;

        assume

         A12: [i, j] in ( Indices ( AutMt ((f1 + f2),b1,b2)));

        then

         A14: [i, j] in ( Indices ( AutMt (f1,b1,b2))) by A1, A6, FINSEQ_3: 29;

        

         A15: [i, j] in ( Indices ( AutMt (f2,b1,b2))) by A1, A3, A6, AX10, A12, FINSEQ_3: 29;

        

         A15A: (( AutMt ((f1 + f2),b1,b2)) * (i,j)) = ((( AutMt (f1,b1,b2)) * (i,j)) + (( AutMt (f2,b1,b2)) * (i,j)))

        proof

          consider KL3 be Linear_Combination of V2 such that

           A16: (f2 . (b1 /. i)) = ( Sum KL3) & ( Carrier KL3) c= ( rng b2) and

           A17: for t st 1 <= t & t <= ( len ((f2 . (b1 /. i)) |-- b2)) holds (((f2 . (b1 /. i)) |-- b2) /. t) = (KL3 . (b2 /. t)) by Def7;

          consider KL2 be Linear_Combination of V2 such that

           A18: (f1 . (b1 /. i)) = ( Sum KL2) & ( Carrier KL2) c= ( rng b2) and

           A19: for t st 1 <= t & t <= ( len ((f1 . (b1 /. i)) |-- b2)) holds (((f1 . (b1 /. i)) |-- b2) /. t) = (KL2 . (b2 /. t)) by Def7;

          

           A20: i in ( dom ( AutMt ((f1 + f2),b1,b2))) by A12, ZFMISC_1: 87;

          then

           A21: i in ( dom b1) by Lm3;

          reconsider b4 = ( rng b2) as Basis of V2 by defOrdBasis;

          consider p1 be FinSequence of INT.Ring such that

           A22: p1 = (( AutMt ((f1 + f2),b1,b2)) . i) and

           A23: (( AutMt ((f1 + f2),b1,b2)) * (i,j)) = (p1 . j) by A12, MATRIX_0:def 5;

          consider KL1 be Linear_Combination of V2 such that

           A24: ((f1 + f2) . (b1 /. i)) = ( Sum KL1) & ( Carrier KL1) c= ( rng b2) and

           A25: for t st 1 <= t & t <= ( len (((f1 + f2) . (b1 /. i)) |-- b2)) holds ((((f1 + f2) . (b1 /. i)) |-- b2) /. t) = (KL1 . (b2 /. t)) by Def7;

          

           Z: b4 is linearly-independent by VECTSP_7:def 3;

          ((f1 + f2) . (b1 /. i)) = ((f1 . (b1 /. i)) + (f2 . (b1 /. i))) by MATRLIN:def 3;

          

          then

           A26: (KL1 . (b2 /. j)) = ((KL2 + KL3) . (b2 /. j)) by A24, A18, A16, Th6, Z

          .= ((KL2 . (b2 /. j)) + (KL3 . (b2 /. j))) by VECTSP_6: 22;

          

           A27: p1 = (( AutMt ((f1 + f2),b1,b2)) /. i) by A22, A20, PARTFUN1:def 6

          .= (((f1 + f2) . (b1 /. i)) |-- b2) by A21, Def8;

          consider p3 be FinSequence of INT.Ring such that

           A28: p3 = (( AutMt (f2,b1,b2)) . i) and

           A29: (( AutMt (f2,b1,b2)) * (i,j)) = (p3 . j) by A15, MATRIX_0:def 5;

          consider p2 be FinSequence of INT.Ring such that

           A30: p2 = (( AutMt (f1,b1,b2)) . i) and

           A31: (( AutMt (f1,b1,b2)) * (i,j)) = (p2 . j) by A14, MATRIX_0:def 5;

          

           A32: j in ( Seg ( width ( AutMt ((f1 + f2),b1,b2)))) by A12, ZFMISC_1: 87;

          then

           A33: 1 <= j by FINSEQ_1: 1;

          ( len b1) = ( len ( AutMt ((f1 + f2),b1,b2))) by Def8;

          then ( dom b1) = ( dom ( AutMt ((f1 + f2),b1,b2))) by FINSEQ_3: 29;

          then ( dom b1) <> {} by A12;

          then ( Seg ( len b1)) <> {} by FINSEQ_1:def 3;

          then ( len b1) > 0 ;

          then

           A34: j in ( Seg ( len b2)) by A32, Th39;

          then

           A35: j <= ( len b2) by FINSEQ_1: 1;

          then j <= ( len (((f1 + f2) . (b1 /. i)) |-- b2)) by Def7;

          then

           A36: (p1 /. j) = (KL1 . (b2 /. j)) by A33, A27, A25;

          

           A37: j in ( dom b2) by A34, FINSEQ_1:def 3;

          i in ( dom ( AutMt (f2,b1,b2))) by A21, Lm3;

          

          then

           A38: p3 = (( AutMt (f2,b1,b2)) /. i) by A28, PARTFUN1:def 6

          .= ((f2 . (b1 /. i)) |-- b2) by A21, Def8;

          then j in ( dom p3) by A37, Lm1;

          then

           A39: (( AutMt (f2,b1,b2)) * (i,j)) = (p3 /. j) by A29, PARTFUN1:def 6;

          i in ( dom ( AutMt (f1,b1,b2))) by A21, Lm3;

          

          then

           A40: p2 = (( AutMt (f1,b1,b2)) /. i) by A30, PARTFUN1:def 6

          .= ((f1 . (b1 /. i)) |-- b2) by A21, Def8;

          then j in ( dom p2) by A37, Lm1;

          then

           A41: (( AutMt (f1,b1,b2)) * (i,j)) = (p2 /. j) by A31, PARTFUN1:def 6;

          j <= ( len ((f2 . (b1 /. i)) |-- b2)) by A35, Def7;

          then

           A42: (p3 /. j) = (KL3 . (b2 /. j)) by A33, A38, A17;

          j <= ( len ((f1 . (b1 /. i)) |-- b2)) by A35, Def7;

          then

           A43: (p2 /. j) = (KL2 . (b2 /. j)) by A33, A40, A19;

          j in ( dom p1) by A37, A27, Lm1;

          hence thesis by A23, A41, A39, A36, A43, A42, A26, PARTFUN1:def 6;

        end;

        

        thus (( AutMt ((f1 + f2),b1,b2)) * (i,j)) = ((( AutMt (f1,b1,b2)) * (i,j)) + (( AutMt (f2,b1,b2)) * (i,j))) by A15A

        .= ((( AutMt (f1,b1,b2)) + ( AutMt (f2,b1,b2))) * (i,j)) by A14, MATRIX_3:def 3;

      end;

      ( len ( AutMt ((f1 + f2),b1,b2))) = ( len (( AutMt (f1,b1,b2)) + ( AutMt (f2,b1,b2)))) by A1, MATRIX_3:def 3;

      hence thesis by A9, A11, MATRIX_0: 21;

    end;

    theorem :: ZMATRLIN:40

    a <> ( 0. INT.Ring ) implies ( AutMt ((a * f),b1,b2)) = (a * ( AutMt (f,b1,b2)))

    proof

      assume

       A1: a <> ( 0. INT.Ring );

      

       A2: ( width ( AutMt ((a * f),b1,b2))) = ( width ( AutMt (f,b1,b2)))

      proof

        per cases ;

          suppose

           A3: ( len b1) = 0 ;

          

          then ( AutMt ((a * f),b1,b2)) = {} by Th38

          .= ( AutMt (f,b1,b2)) by A3, Th38;

          hence thesis;

        end;

          suppose

           A4: ( len b1) > 0 ;

          

          hence ( width ( AutMt ((a * f),b1,b2))) = ( len b2) by Th39

          .= ( width ( AutMt (f,b1,b2))) by A4, Th39;

        end;

      end;

      

       A5: ( width ( AutMt ((a * f),b1,b2))) = ( width (a * ( AutMt (f,b1,b2)))) by A2, MATRIX_3:def 5;

      

       A6: ( len ( AutMt ((a * f),b1,b2))) = ( len b1) by Def8

      .= ( len ( AutMt (f,b1,b2))) by Def8;

      

       A8: for i, j st [i, j] in ( Indices ( AutMt ((a * f),b1,b2))) holds (( AutMt ((a * f),b1,b2)) * (i,j)) = ((a * ( AutMt (f,b1,b2))) * (i,j))

      proof

        let i, j;

        assume

         A9: [i, j] in ( Indices ( AutMt ((a * f),b1,b2)));

        then

         A11: [i, j] in ( Indices ( AutMt (f,b1,b2))) by A2, A6, FINSEQ_3: 29;

        

         A11A: (( AutMt ((a * f),b1,b2)) * (i,j)) = (a * (( AutMt (f,b1,b2)) * (i,j)))

        proof

          consider p2 be FinSequence of INT such that

           A12: p2 = (( AutMt (f,b1,b2)) . i) and

           A13: (( AutMt (f,b1,b2)) * (i,j)) = (p2 . j) by A11, MATRIX_0:def 5;

          

           A14: i in ( dom ( AutMt ((a * f),b1,b2))) by A9, ZFMISC_1: 87;

          then

           A15: i in ( dom b1) by Lm3;

          then i in ( dom ( AutMt (f,b1,b2))) by Lm3;

          

          then

           A16: p2 = (( AutMt (f,b1,b2)) /. i) by A12, PARTFUN1:def 6

          .= ((f . (b1 /. i)) |-- b2) by A15, Def8;

          reconsider b4 = ( rng b2) as Basis of V2 by defOrdBasis;

          consider p1 be FinSequence of INT such that

           A17: p1 = (( AutMt ((a * f),b1,b2)) . i) and

           A18: (( AutMt ((a * f),b1,b2)) * (i,j)) = (p1 . j) by A9, MATRIX_0:def 5;

          consider KL1 be Linear_Combination of V2 such that

           A19: ((a * f) . (b1 /. i)) = ( Sum KL1) & ( Carrier KL1) c= ( rng b2) and

           A20: for t st 1 <= t & t <= ( len (((a * f) . (b1 /. i)) |-- b2)) holds ((((a * f) . (b1 /. i)) |-- b2) /. t) = (KL1 . (b2 /. t)) by Def7;

          consider KL2 be Linear_Combination of V2 such that

           A21: (f . (b1 /. i)) = ( Sum KL2) & ( Carrier KL2) c= ( rng b2) and

           A22: for t st 1 <= t & t <= ( len ((f . (b1 /. i)) |-- b2)) holds (((f . (b1 /. i)) |-- b2) /. t) = (KL2 . (b2 /. t)) by Def7;

          b4 is linearly-independent & ((a * f) . (b1 /. i)) = (a * (f . (b1 /. i))) by VECTSP_7:def 3, MATRLIN:def 4;

          

          then

           A23: (KL1 . (b2 /. j)) = ((a * KL2) . (b2 /. j)) by A1, A19, A21, Th7

          .= (a * (KL2 . (b2 /. j))) by VECTSP_6:def 9;

          

           A24: j in ( Seg ( width ( AutMt ((a * f),b1,b2)))) by A9, ZFMISC_1: 87;

          then

           A25: 1 <= j by FINSEQ_1: 1;

          ( len b1) = ( len ( AutMt ((a * f),b1,b2))) by Def8;

          then ( dom b1) = ( dom ( AutMt ((a * f),b1,b2))) by FINSEQ_3: 29;

          then ( dom b1) <> {} by A9;

          then ( Seg ( len b1)) <> {} by FINSEQ_1:def 3;

          then ( len b1) > 0 ;

          then

           A26: j in ( Seg ( len b2)) by A24, Th39;

          then

           A27: j <= ( len b2) by FINSEQ_1: 1;

          then j <= ( len ((f . (b1 /. i)) |-- b2)) by Def7;

          then

           A28: (p2 /. j) = (KL2 . (b2 /. j)) by A25, A16, A22;

          

           A29: j in ( dom b2) by A26, FINSEQ_1:def 3;

          then j in ( dom ((f . (b1 /. i)) |-- b2)) by Lm1;

          then

           A30: (( AutMt (f,b1,b2)) * (i,j)) = (p2 /. j) by A13, A16, PARTFUN1:def 6;

          

           A31: p1 = (( AutMt ((a * f),b1,b2)) /. i) by A17, A14, PARTFUN1:def 6

          .= (((a * f) . (b1 /. i)) |-- b2) by A15, Def8;

          then

           A32: j in ( dom p1) by A29, Lm1;

          j <= ( len (((a * f) . (b1 /. i)) |-- b2)) by A27, Def7;

          then (p1 /. j) = (KL1 . (b2 /. j)) by A25, A31, A20;

          hence thesis by A18, A32, A30, A28, A23, PARTFUN1:def 6;

        end;

        

         A110: [i, j] in ( Indices ( AutMt (f,b1,b2))) by A2, A6, A9, FINSEQ_3: 29;

        (( AutMt ((a * f),b1,b2)) * (i,j)) = ((a * ( AutMt (f,b1,b2))) * (i,j)) by A11A, A110, MATRIX_3:def 5;

        hence thesis;

      end;

      ( len ( AutMt ((a * f),b1,b2))) = ( len ( AutMt ((a * f),b1,b2))) = ( len (a * ( AutMt (f,b1,b2)))) by A6, MATRIX_3:def 5;

      hence thesis by A5, A8, MATRIX_0: 21;

    end;

    theorem :: ZMATRLIN:41

    

     LmSign1B: for D,E be non empty set, n,m,i,j be Nat, M be Matrix of n, m, D st 0 < n & M is Matrix of n, m, E & [i, j] in ( Indices M) holds (M * (i,j)) is Element of E

    proof

      let D,E be non empty set, n,m,i,j be Nat, M be Matrix of n, m, D;

      assume that

       A1: 0 < n and

       A2: M is Matrix of n, m, E and

       A3: [i, j] in ( Indices M);

      consider m1 be Nat such that

       A4: for x be object st x in ( rng M) holds ex q be FinSequence of E st x = q & ( len q) = m1 by MATRIX_0: 9, A2;

      consider p be FinSequence of D such that

       A5: p = (M . i) & (M * (i,j)) = (p . j) by A3, MATRIX_0:def 5;

      

       A6: i in ( dom M) & j in ( Seg ( width M)) by A3, ZFMISC_1: 87;

      then

       A7: p in ( rng M) by FUNCT_1: 3, A5;

      ex q be FinSequence of E st p = q & ( len q) = m1 by A4, A5, A6, FUNCT_1: 3;

      then

       A50: ( rng p) c= E by FINSEQ_1:def 4;

      ( len p) = m by A7, MATRIX_0:def 2;

      then ( len p) = ( width M) by A1, MATRIX_0: 23;

      then j in ( dom p) by FINSEQ_1:def 3, A6;

      hence thesis by A5, A50, FUNCT_1: 3;

    end;

    theorem :: ZMATRLIN:42

    

     LmSign1C: for F be FinSequence of F_Real st for i be Nat st i in ( dom F) holds (F . i) in INT holds ( Sum F) in INT

    proof

      defpred P[ Nat] means for F be FinSequence of F_Real st ( len F) = $1 & for i be Nat st i in ( dom F) holds (F . i) in INT holds ( Sum F) in INT ;

      

       P1: P[ 0 ]

      proof

        let F be FinSequence of F_Real ;

        assume

         AS1: ( len F) = 0 & for i be Nat st i in ( dom F) holds (F . i) in INT ;

        F = ( <*> the carrier of F_Real ) by AS1;

        

        then ( Sum F) = ( 0. F_Real ) by RLVECT_1: 43

        .= 0 ;

        hence ( Sum F) in INT by INT_1:def 2;

      end;

      

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

      proof

        let n be Nat;

        assume

         AS1: P[n];

        let F be FinSequence of F_Real ;

        assume

         AS2: ( len F) = (n + 1) & for i be Nat st i in ( dom F) holds (F . i) in INT ;

        reconsider F0 = (F | n) as FinSequence of F_Real ;

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

        then

         A70: (n + 1) in ( dom F) by AS2, FINSEQ_1:def 3;

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

        then

        reconsider af = (F . (n + 1)) as Element of F_Real ;

        

         P1: ( len F0) = n by FINSEQ_1: 59, AS2, NAT_1: 11;

        then

         P4: ( dom F0) = ( Seg n) by FINSEQ_1:def 3;

        

         A9: ( len F) = (( len F0) + 1) by AS2, FINSEQ_1: 59, NAT_1: 11;

        

         A11: F0 = (F | ( dom F0)) by P4, FINSEQ_1:def 15;

        then

         P3: ( Sum F) = (( Sum F0) + af) by AS2, A9, RLVECT_1: 38;

        for i be Nat st i in ( dom F0) holds (F0 . i) in INT

        proof

          let i be Nat;

          assume

           P40: i in ( dom F0);

          ( dom F) = ( Seg (n + 1)) by AS2, FINSEQ_1:def 3;

          then ( dom F0) c= ( dom F) by P4, FINSEQ_1: 5, NAT_1: 11;

          then (F . i) in INT by AS2, P40;

          hence thesis by A11, P40, FUNCT_1: 47;

        end;

        then ( Sum F0) in INT by P1, AS1;

        then

        reconsider i1 = ( Sum F0) as Integer;

        (F . (n + 1)) in INT by A70, AS2;

        then

        reconsider i2 = af as Integer;

        ( Sum F) = (i1 + i2) by P3;

        hence ( Sum F) in INT by INT_1:def 2;

      end;

      

       X1: for n be Nat holds P[n] from NAT_1:sch 2( P1, P2);

      let F be FinSequence of F_Real ;

      assume

       X2: for i be Nat st i in ( dom F) holds (F . i) in INT ;

      ( len F) is Nat;

      hence ( Sum F) in INT by X1, X2;

    end;

    theorem :: ZMATRLIN:43

    

     LmSign1D: for i be Nat, j be Element of F_Real st j in INT holds ((( power F_Real ) . (( - ( 1_ F_Real )),i)) * j) in INT

    proof

      let i be Nat, j be Element of F_Real ;

      assume

       AS: j in INT ;

      defpred P[ Nat] means ((( power F_Real ) . (( - ( 1_ F_Real )),$1)) * j) in INT ;

      

       P1: P[ 0 ]

      proof

        ((( power F_Real ) . (( - ( 1_ F_Real )), 0 )) * j) = (( 1_ F_Real ) * j) by GROUP_1:def 7

        .= j;

        hence thesis by AS;

      end;

      

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

      proof

        let n be Nat;

        assume

         AS1: P[n];

        

         P3: ((( power F_Real ) . (( - ( 1_ F_Real )),(n + 1))) * j) = (((( power F_Real ) . (( - ( 1_ F_Real )),n)) * ( - ( 1_ F_Real ))) * j) by GROUP_1:def 7

        .= (( - ( 1_ F_Real )) * ((( power F_Real ) . (( - ( 1_ F_Real )),n)) * j));

        reconsider mi = ( - ( 1_ F_Real )) as Integer;

        reconsider m0 = ((( power F_Real ) . (( - ( 1_ F_Real )),n)) * j) as Integer by AS1;

        ((( power F_Real ) . (( - ( 1_ F_Real )),(n + 1))) * j) = ( - m0) by P3;

        hence ((( power F_Real ) . (( - ( 1_ F_Real )),(n + 1))) * j) in INT by INT_1:def 2;

      end;

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

      hence thesis;

    end;

    theorem :: ZMATRLIN:44

    

     LmSign1F: for n,i,j,k,m be Nat, M be Matrix of (n + 1), F_Real st 0 < n & M is Matrix of (n + 1), INT & [i, j] in ( Indices M) & [k, m] in ( Indices ( Delete (M,i,j))) holds (( Delete (M,i,j)) * (k,m)) is Element of INT

    proof

      let n,i,j,k,m be Nat, M be Matrix of (n + 1), F_Real ;

      assume that 0 < n and

       A2: M is Matrix of (n + 1), INT and

       A3: [i, j] in ( Indices M) and

       A4: [k, m] in ( Indices ( Delete (M,i,j)));

       [i, j] in [:( Seg (n + 1)), ( Seg (n + 1)):] by A3, MATRIX_0: 24;

      then

       A5: i in ( Seg (n + 1)) & j in ( Seg (n + 1)) by ZFMISC_1: 87;

      set M0 = ( Delete (M,i,j));

      ((n + 1) -' 1) = n by NAT_D: 34;

      then ( len M0) = n & ( width M0) = n & ( Indices M0) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      then

       D5: k in ( Seg n) & m in ( Seg n) by A4, ZFMISC_1: 87;

      then

       D3: k in ( Seg ((n + 1) -' 1)) & m in ( Seg ((n + 1) -' 1)) by NAT_D: 34;

      

       FC0: 1 <= k & k <= n & 1 <= m & m <= n by FINSEQ_1: 1, D5;

      then 1 <= k & (k + 0 ) <= (n + 1) & 1 <= m & (m + 0 ) <= (n + 1) by XREAL_1: 7;

      then

       FC1: k in ( Seg (n + 1)) & m in ( Seg (n + 1)) by FINSEQ_1: 1;

      (1 + 0 ) <= (k + 1) & (k + 1) <= (n + 1) & (1 + 0 ) <= (m + 1) & (m + 1) <= (n + 1) by FC0, XREAL_1: 6;

      then

       FC3: (k + 1) in ( Seg (n + 1)) & (m + 1) in ( Seg (n + 1)) by FINSEQ_1: 1;

      per cases ;

        suppose k < i & m < j;

        then

         F11: (( Delete (M,i,j)) * (k,m)) = (M * (k,m)) by LAPLACE: 13, A5, D3;

         [k, m] in [:( Seg (n + 1)), ( Seg (n + 1)):] by FC1, ZFMISC_1: 87;

        then [k, m] in ( Indices M) by MATRIX_0: 24;

        hence thesis by A2, F11, LmSign1B;

      end;

        suppose k < i & m >= j;

        then

         F21: (( Delete (M,i,j)) * (k,m)) = (M * (k,(m + 1))) by LAPLACE: 13, A5, D3;

         [k, (m + 1)] in [:( Seg (n + 1)), ( Seg (n + 1)):] by FC1, FC3, ZFMISC_1: 87;

        then [k, (m + 1)] in ( Indices M) by MATRIX_0: 24;

        hence thesis by A2, F21, LmSign1B;

      end;

        suppose k >= i & m < j;

        then

         F31: (( Delete (M,i,j)) * (k,m)) = (M * ((k + 1),m)) by LAPLACE: 13, A5, D3;

         [(k + 1), m] in [:( Seg (n + 1)), ( Seg (n + 1)):] by FC1, FC3, ZFMISC_1: 87;

        then [(k + 1), m] in ( Indices M) by MATRIX_0: 24;

        hence thesis by A2, F31, LmSign1B;

      end;

        suppose k >= i & m >= j;

        then

         F41: (( Delete (M,i,j)) * (k,m)) = (M * ((k + 1),(m + 1))) by LAPLACE: 13, A5, D3;

         [(k + 1), (m + 1)] in [:( Seg (n + 1)), ( Seg (n + 1)):] by FC3, ZFMISC_1: 87;

        then [(k + 1), (m + 1)] in ( Indices M) by MATRIX_0: 24;

        hence thesis by A2, F41, LmSign1B;

      end;

    end;

    theorem :: ZMATRLIN:45

    

     LmSign1E: for n,i,j be Nat, M be Matrix of (n + 1), F_Real st 0 < n & M is Matrix of (n + 1), INT & [i, j] in ( Indices M) holds ( Delete (M,i,j)) is Matrix of n, INT

    proof

      let n,i,j be Nat, M be Matrix of (n + 1), F_Real ;

      assume that

       A1: 0 < n and

       A2: M is Matrix of (n + 1), INT and

       A3: [i, j] in ( Indices M);

      set M0 = ( Delete (M,i,j));

      

       X39: ((n + 1) -' 1) = n by NAT_D: 34;

      then

       D2: ( len M0) = n & ( width M0) = n & ( Indices M0) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for x be object st x in ( rng M0) holds ex p be FinSequence of INT st x = p & ( len p) = n

      proof

        let x be object;

        assume

         S1: x in ( rng M0);

        then

        reconsider p = x as FinSequence of the carrier of F_Real by FINSEQ_2:def 3;

        

         S3: ( len p) = n by S1, X39, MATRIX_0:def 2;

        for z be object st z in ( rng p) holds z in INT

        proof

          let z be object;

          assume z in ( rng p);

          then

          consider j1 be object such that

           S4: j1 in ( dom p) & z = (p . j1) by FUNCT_1:def 3;

          

           S5: j1 in ( Seg n) by S3, S4, FINSEQ_1:def 3;

          reconsider j1 as Nat by S4;

          consider i1 be object such that

           S6: i1 in ( dom M0) & x = (M0 . i1) by S1, FUNCT_1:def 3;

          reconsider i1 as Nat by S6;

          

           S8: [i1, j1] in ( Indices M0) by D2, S5, S6, ZFMISC_1: 87;

          then

          consider q be FinSequence of F_Real such that

           S9: q = (M0 . i1) & (M0 * (i1,j1)) = (q . j1) by MATRIX_0:def 5;

          (M0 * (i1,j1)) is Element of INT by A1, A2, A3, S8, LmSign1F;

          hence z in INT by S4, S6, S9;

        end;

        then ( rng p) c= INT ;

        then p is FinSequence of INT by FINSEQ_1:def 4;

        hence thesis by S3;

      end;

      hence thesis by A1, D2, MATRIX_0: 9, MATRIX_0: 20;

    end;

    theorem :: ZMATRLIN:46

    

     LmSign1A: for n be Nat, M be Matrix of n, F_Real st M is Matrix of n, INT holds ( Det M) in INT

    proof

      defpred P[ Nat] means for M be Matrix of $1, F_Real st M is Matrix of $1, INT holds ( Det M) in INT ;

      

       P0: P[ 0 ]

      proof

        let M be Matrix of 0 , F_Real ;

        assume M is Matrix of 0 , INT ;

        ( Det M) = ( 1. F_Real ) by MATRIXR2: 41

        .= 1;

        hence ( Det M) in INT by INT_1:def 2;

      end;

      

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

      proof

        let n be Nat;

        assume

         P10: P[n];

        let M be Matrix of (n + 1), F_Real ;

        assume

         AS1: M is Matrix of (n + 1), INT ;

        reconsider j = 1 as Nat;

        

         X0: 1 <= 1 & 1 <= (n + 1) by NAT_1: 14;

        then j in ( Seg (n + 1)) by FINSEQ_1: 1;

        then

         X1: ( Det M) = ( Sum ( LaplaceExpC (M,j))) by LAPLACE: 27;

        set L = ( LaplaceExpC (M,j));

        

         X2: ( len L) = (n + 1) & for i be Nat st i in ( dom L) holds (L . i) = ((M * (i,j)) * ( Cofactor (M,i,j))) by LAPLACE:def 8;

        for i be Nat st i in ( dom L) holds (L . i) in INT

        proof

          let i be Nat;

          assume

           X30: i in ( dom L);

          then

           X31: (L . i) = ((M * (i,j)) * ( Cofactor (M,i,j))) by LAPLACE:def 8;

          i in ( Seg (n + 1)) & j in ( Seg (n + 1)) by X0, X2, X30, FINSEQ_1:def 3, FINSEQ_1: 1;

          then [i, j] in [:( Seg (n + 1)), ( Seg (n + 1)):] by ZFMISC_1: 87;

          then

           X41: [i, j] in ( Indices M) by MATRIX_0: 24;

          then

           X32: (M * (i,j)) is Element of INT by AS1, LmSign1B;

          ((n + 1) -' 1) = n by NAT_D: 34;

          then

          reconsider DD = ( Delete (M,i,j)) as Matrix of n, F_Real ;

          ( Det DD) in INT

          proof

            per cases ;

              suppose 0 < n;

              then DD is Matrix of n, INT by LmSign1E, AS1, X41;

              hence ( Det DD) in INT by P10;

            end;

              suppose not 0 < n;

              then n = 0 ;

              

              then ( Det DD) = ( 1. F_Real ) by MATRIXR2: 41

              .= 1;

              hence ( Det DD) in INT by INT_1:def 2;

            end;

          end;

          then ( Minor (M,i,j)) in INT by NAT_D: 34;

          then ( Cofactor (M,i,j)) in INT by LmSign1D;

          hence (L . i) in INT by X32, X31, INT_1:def 2;

        end;

        hence thesis by X1, LmSign1C;

      end;

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

      hence thesis;

    end;

    theorem :: ZMATRLIN:47

    for n be Nat, M be Matrix of n, F_Real st M is Matrix of n, INT.Ring holds ( Det M) in INT by LmSign1A;

    theorem :: ZMATRLIN:48

    for V be finite-rank free Z_Module, I be Basis of V holds ex J be OrdBasis of V st ( rng J) = I

    proof

      let V be finite-rank free Z_Module, I be Basis of V;

      consider p be FinSequence such that

       A2: ( rng p) = I and

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

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

      take f = p;

      thus f is one-to-one by A3;

      thus thesis by A2;

    end;

    registration

      let V be Z_Module;

      cluster ( id V) -> additive homogeneous;

      correctness ;

    end

    theorem :: ZMATRLIN:49

    

     ThRank1: for V be finite-rank free Z_Module, b be OrdBasis of V holds ( len b) = ( rank V)

    proof

      let V be finite-rank free Z_Module, b be OrdBasis of V;

      reconsider R = ( rng b) as Basis of V by defOrdBasis;

      

       A1: b is one-to-one by defOrdBasis;

      

      thus ( len b) = ( card ( Seg ( len b))) by FINSEQ_1: 57

      .= ( card ( dom b)) by FINSEQ_1:def 3

      .= ( card R) by A1, CARD_1: 70

      .= ( rank V) by ZMODUL03:def 5;

    end;

    theorem :: ZMATRLIN:50

    

     LMThMBF3: for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V holds ( AutMt (( id V),b1,b2)) is Matrix of ( rank V), INT.Ring

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V;

      set n = ( rank V);

      

       A1: ( len b1) = ( rank V) by ThRank1;

      

       A2: ( len b2) = ( rank V) by ThRank1;

      

       P0: ( len ( AutMt (( id V),b1,b2))) = ( len b1) by Def8;

      per cases ;

        suppose

         X1: ( len b1) = 0 ;

        then ( len ( AutMt (( id V),b1,b2))) = 0 by Def8;

        then ( AutMt (( id V),b1,b2)) = {} ;

        hence thesis by A1, X1, MATRIX_0: 13;

      end;

        suppose

         P1: 0 < ( len b1);

        then ( width ( AutMt (( id V),b1,b2))) = ( len b2) by Th39;

        hence thesis by P0, P1, A1, A2, MATRIX_0: 20;

      end;

    end;

    theorem :: ZMATRLIN:51

    for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, M be Matrix of ( rank V), F_Real st M = ( AutMt (( id V),b1,b2)) holds ( Det M) in INT

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, M be Matrix of ( rank V), F_Real ;

      assume

       A2: M = ( AutMt (( id V),b1,b2));

      per cases ;

        suppose not 0 < ( rank V);

        then ( rank V) = 0 ;

        then ( Det M) = ( 1. F_Real ) by MATRIXR2: 41;

        hence ( Det M) in INT ;

      end;

        suppose

         A3: 0 < ( rank V);

        ( len M) = ( rank V) & ( width M) = ( rank V) by MATRIX_0: 24;

        then M is Matrix of ( rank V), INT by A2, A3, MATRIX_0: 20;

        hence thesis by LmSign1A;

      end;

    end;

    theorem :: ZMATRLIN:52

    

     LmSign31X: for V1 be finite-rank free Z_Module, b1 be OrdBasis of V1 holds for i,j be Nat st i in ( dom b1) & j in ( dom b1) holds (i = j implies (((b1 /. i) |-- b1) . j) = 1) & (i <> j implies (((b1 /. i) |-- b1) . j) = 0 )

    proof

      let V1 be finite-rank free Z_Module, b1 be OrdBasis of V1;

      let i,j be Nat;

      assume that

       A5: i in ( dom b1) and

       A18: j in ( dom b1);

      set bb = ((b1 /. i) |-- b1);

      consider KL be Linear_Combination of V1 such that

       A1: (b1 /. i) = ( Sum KL) & ( Carrier KL) c= ( rng b1) and

       A2: for k st 1 <= k & k <= ( len bb) holds (bb /. k) = (KL . (b1 /. k)) by Def7;

      reconsider rb1 = ( rng b1) as Basis of V1 by defOrdBasis;

      (b1 /. i) in {(b1 /. i)} by TARSKI:def 1;

      then (b1 /. i) in ( Lin {(b1 /. i)}) by ZMODUL02: 65;

      then

      consider Lb be Linear_Combination of {(b1 /. i)} such that

       A4: (b1 /. i) = ( Sum Lb) by ZMODUL02: 64;

      

       A6: (b1 . i) = (b1 /. i) by A5, PARTFUN1:def 6;

      then

       A7: ( Carrier Lb) c= {(b1 . i)} by VECTSP_6:def 4;

      

       A8: (b1 . i) in rb1 by A5, FUNCT_1:def 3;

      then {(b1 . i)} c= rb1 by ZFMISC_1: 31;

      then ( Carrier Lb) c= rb1 by A7;

      then

       A9: Lb = KL by A4, A1, Th5, VECTSP_7:def 3;

      

       A12: ( len b1) = ( len bb) by Def7;

      

       A13: (b1 /. i) <> ( 0. V1) by A6, A8, ZMODUL02: 57, VECTSP_7:def 3;

      j in ( Seg ( len b1)) by A18, FINSEQ_1:def 3;

      then

       A15: 1 <= j & j <= ( len bb) by FINSEQ_1: 1, A12;

      

       A19: ( dom bb) = ( dom b1) by A12, FINSEQ_3: 29;

      set One = ( 1. INT.Ring );

      reconsider KLi = (KL . (b1 /. i)) as Element of INT.Ring ;

      now

        assume

         A20: i = j;

        (KLi * (b1 /. i)) = (b1 /. i) by A4, A9, ZMODUL02: 21

        .= (One * (b1 /. i)) by VECTSP_1:def 17;

        then KLi = One by A13, ZMODUL01: 11;

        

        hence 1 = (bb /. j) by A2, A15, A20

        .= (bb . j) by A18, A19, PARTFUN1:def 6;

      end;

      hence i = j implies (((b1 /. i) |-- b1) . j) = 1;

      now

        assume

         A22: i <> j;

        b1 is one-to-one by defOrdBasis;

        then (b1 . i) <> (b1 . j) by A5, A18, A22;

        then

         A23: not (b1 . j) in ( Carrier Lb) by A7, TARSKI:def 1;

        (b1 . j) = (b1 /. j) by A18, PARTFUN1:def 6;

        

        hence 0 = (KL . (b1 /. j)) by A9, A23

        .= (bb /. j) by A2, A15

        .= (bb . j) by A18, A19, PARTFUN1:def 6;

      end;

      hence i <> j implies (((b1 /. i) |-- b1) . j) = 0 ;

    end;

    theorem :: ZMATRLIN:53

    

     LmSign31: for V be finite-rank free Z_Module, b1 be OrdBasis of V st ( rank V) > 0 holds ( AutMt (( id V),b1,b1)) = ( 1. ( INT.Ring ,( rank V)))

    proof

      let V be finite-rank free Z_Module, b1 be OrdBasis of V;

      assume

       AS: ( rank V) > 0 ;

      

       B0: ( len b1) = ( rank V) by ThRank1;

      

       B1: ( len ( AutMt (( id V),b1,b1))) = ( rank V) by B0, Def8;

      

       B3: ( width ( AutMt (( id V),b1,b1))) = ( rank V) by AS, B0, Th39;

      

       P1: ( len ( AutMt (( id V),b1,b1))) = ( len ( 1. ( INT.Ring ,( rank V)))) by B1, MATRIX_0: 24;

      

       P4: ( dom ( AutMt (( id V),b1,b1))) = ( Seg ( len ( AutMt (( id V),b1,b1)))) by FINSEQ_1:def 3

      .= ( dom ( 1. ( INT.Ring ,( rank V)))) by P1, FINSEQ_1:def 3;

      

       P2: ( width ( AutMt (( id V),b1,b1))) = ( width ( 1. ( INT.Ring ,( rank V)))) by B3, MATRIX_0: 24;

      

       P5: ( Indices ( AutMt (( id V),b1,b1))) = ( Indices ( 1. ( INT.Ring ,( rank V)))) by B3, P4, MATRIX_0: 24;

       X2:

      now

        let i,j be Nat;

        assume

         X20: [i, j] in ( Indices ( AutMt (( id V),b1,b1)));

        then

         X21: i in ( dom ( AutMt (( id V),b1,b1))) & j in ( Seg ( width ( AutMt (( id V),b1,b1)))) by ZFMISC_1: 87;

        ( dom ( AutMt (( id V),b1,b1))) = ( Seg ( len ( AutMt (( id V),b1,b1)))) by FINSEQ_1:def 3

        .= ( Seg ( len b1)) by Def8

        .= ( dom b1) by FINSEQ_1:def 3;

        then

         X23: i in ( dom b1) by X20, ZFMISC_1: 87;

        ( width ( AutMt (( id V),b1,b1))) = ( len b1) by Th39, AS, B0;

        then

         Y23: j in ( dom b1) by X21, FINSEQ_1:def 3;

        

         X25: (( AutMt (( id V),b1,b1)) /. i) = ((( id V) . (b1 /. i)) |-- b1) by Def8, X23;

        consider q be FinSequence of INT such that

         X26: q = (( AutMt (( id V),b1,b1)) . i) & (( AutMt (( id V),b1,b1)) * (i,j)) = (q . j) by MATRIX_0:def 5, X20;

        

         X27: (( AutMt (( id V),b1,b1)) * (i,j)) = (((b1 /. i) |-- b1) . j) by X21, X25, X26, PARTFUN1:def 6;

        thus i <> j implies (( AutMt (( id V),b1,b1)) * (i,j)) = 0 by X23, X27, Y23, LmSign31X;

        thus i = j implies (( AutMt (( id V),b1,b1)) * (i,j)) = 1 by X23, X27, LmSign31X;

      end;

      for i,j be Nat st [i, j] in ( Indices ( AutMt (( id V),b1,b1))) holds (( AutMt (( id V),b1,b1)) * (i,j)) = (( 1. ( INT.Ring ,( rank V))) * (i,j))

      proof

        let i,j be Nat;

        assume

         P6: [i, j] in ( Indices ( AutMt (( id V),b1,b1)));

        per cases ;

          suppose

           P8: i <> j;

          then (( 1. ( INT.Ring ,( rank V))) * (i,j)) = ( 0. INT.Ring ) by P5, P6, MATRIX_1:def 3;

          hence (( AutMt (( id V),b1,b1)) * (i,j)) = (( 1. ( INT.Ring ,( rank V))) * (i,j)) by P6, P8, X2;

        end;

          suppose

           P10: i = j;

          then (( 1. ( INT.Ring ,( rank V))) * (i,j)) = ( 1. INT.Ring ) by P5, P6, MATRIX_1:def 3;

          hence (( AutMt (( id V),b1,b1)) * (i,j)) = (( 1. ( INT.Ring ,( rank V))) * (i,j)) by P6, P10, X2;

        end;

      end;

      hence thesis by P1, P2, EQ40;

    end;

    theorem :: ZMATRLIN:54

    

     LmSign3: for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V st ( rank V) > 0 holds (( AutMt (( id V),b1,b2)) * ( AutMt (( id V),b2,b1))) = ( 1. ( INT.Ring ,( rank V)))

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V;

      assume

       AS: ( rank V) > 0 ;

      then

       A1: ( len b1) > 0 & ( len b2) > 0 by ThRank1;

      

      thus (( AutMt (( id V),b1,b2)) * ( AutMt (( id V),b2,b1))) = ( AutMt ((( id V) * ( id V)),b1,b1)) by A1, ThComp1

      .= ( AutMt (( id V),b1,b1)) by FUNCT_2: 17

      .= ( 1. ( INT.Ring ,( rank V))) by AS, LmSign31;

    end;

    theorem :: ZMATRLIN:55

    

     ThSign1: for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, M be Matrix of ( rank V), INT.Ring st M = ( AutMt (( id V),b1,b2)) holds |.( Det M).| = 1

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, M be Matrix of ( rank V), INT.Ring ;

      assume

       AS1: M = ( AutMt (( id V),b1,b2));

      per cases ;

        suppose ( rank V) = 0 ;

        then ( Det M) = ( 1. INT.Ring ) by MATRIXR2: 41;

        hence thesis by ABSVALUE:def 1;

      end;

        suppose

         AS2: ( rank V) > 0 ;

        then

         as2: ( rank V) >= (1 + 0 ) by NAT_1: 13;

        

         B0: ( len b1) = ( rank V) by ThRank1;

        

         B1: ( len ( AutMt (( id V),b2,b1))) = ( len b2) by Def8

        .= ( rank V) by ThRank1;

        ( len b2) = ( rank V) by ThRank1;

        then ( width ( AutMt (( id V),b2,b1))) = ( len b1) by AS2, Th39;

        then

        reconsider M2 = ( AutMt (( id V),b2,b1)) as Matrix of ( rank V), INT.Ring by AS2, B0, B1, MATRIX_0: 20;

        M = ( AutMt (( id V),b1,b2)) by AS1;

        then

         A1: (M * M2) = ( 1. ( INT.Ring ,( rank V))) by AS2, LmSign3;

        reconsider MM2 = (M * M2) as Matrix of ( rank V), INT.Ring ;

        

         A2: (( Det M) * ( Det M2)) = ( Det MM2) by MATRIX11: 62, AS2

        .= ( 1_ INT.Ring ) by A1, MATRIX_7: 16, as2

        .= ( 1. INT.Ring );

        reconsider i = ( Det M) as Integer;

        reconsider j = ( Det M2) as Integer;

        (i * j) = 1 by A2;

        then i = 1 & j = 1 or i = ( - 1) & j = ( - 1) by INT_1: 9;

        then |.i.| = 1 or |.i.| = ( - ( - 1)) by ABSVALUE:def 1;

        hence thesis;

      end;

    end;

    begin

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster additive homogeneous 0-preserving for Functional of V;

      existence

      proof

        take ( 0Functional V);

        thus thesis;

      end;

    end

    definition

      let V be non empty ModuleStr over INT.Ring ;

      mode linear-Functional of V is additive homogeneous Functional of V;

    end

    theorem :: ZMATRLIN:56

    

     VS10Th1: for a be Element of INT.Ring , V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , v be Vector of V holds (( 0. INT.Ring ) * v) = ( 0. V) & (a * ( 0. V)) = ( 0. V)

    proof

      let x be Element of INT.Ring ;

      let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , v be Vector of V;

      

       A1: (v + (( 0. INT.Ring ) * v)) = ((( 1. INT.Ring ) * v) + (( 0. INT.Ring ) * v)) by VECTSP_1:def 17

      .= ((( 1. INT.Ring ) + ( 0. INT.Ring )) * v) by VECTSP_1:def 15

      .= (v + ( 0. V)) by VECTSP_1:def 17;

      hence (( 0. INT.Ring ) * v) = ( 0. V) by RLVECT_1: 8;

      

      hence (x * ( 0. V)) = ((x * ( 0. INT.Ring )) * v) by VECTSP_1:def 16

      .= ( 0. V) by A1, RLVECT_1: 8;

    end;

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster additive 0-preserving for Functional of V;

      existence

      proof

        take ( 0Functional V);

        thus thesis;

      end;

    end

    registration

      let V be right_zeroed non empty ModuleStr over INT.Ring ;

      cluster additive -> 0-preserving for Functional of V;

      coherence

      proof

        let f be Functional of V;

        assume

         A1: f is additive;

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

        .= ((f . ( 0. V)) + (f . ( 0. V))) by A1;

        hence (f . ( 0. V)) = ( 0. INT.Ring );

      end;

    end

    registration

      let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring ;

      cluster homogeneous -> 0-preserving for Functional of V;

      coherence

      proof

        let f be Functional of V;

        assume

         A1: f is homogeneous;

        

        thus (f . ( 0. V)) = (f . (( 0. INT.Ring ) * ( 0. V))) by VS10Th1

        .= (( 0. INT.Ring ) * (f . ( 0. V))) by A1

        .= ( 0. INT.Ring );

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster ( 0Functional V) -> constant;

      coherence ;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster constant for Functional of V;

      existence

      proof

        take ( 0Functional V);

        thus thesis;

      end;

    end

    definition

      let V be right_zeroed non empty ModuleStr over INT.Ring ;

      let f be 0-preserving Functional of V;

      :: original: constant

      redefine

      :: ZMATRLIN:def9

      attr f is constant means f = ( 0Functional V);

      compatibility

      proof

        

         A1: (f . ( 0. V)) = ( 0. INT.Ring ) & the carrier of V = ( dom f) by FUNCT_2:def 1, HAHNBAN1:def 9;

        hereby

          assume f is constant;

          then for v be Vector of V holds (f . v) = (( 0Functional V) . v) by A1;

          hence f = ( 0Functional V) by FUNCT_2: 63;

        end;

        assume

         A3: f = ( 0Functional V);

        now

          let x,y be object;

          assume x in ( dom f) & y in ( dom f);

          then

          reconsider v = x, w = y as Vector of V;

          

          thus (f . x) = (( 0Functional V) . v) by A3

          .= 0

          .= (( 0Functional V) . w)

          .= (f . y) by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let V be right_zeroed non empty ModuleStr over INT.Ring ;

      cluster constant additive 0-preserving for Functional of V;

      existence

      proof

        take ( 0Functional V);

        thus thesis;

      end;

    end

    

     LMPROJ1: for V be free Z_Module, A,B be Subset of V st A c= B & B is Basis of V holds ex F be linear-transformation of V, V st (for v be Vector of V holds ex vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) & (F . v) = vA) & for v,vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) holds (F . v) = vA

    proof

      let V be free Z_Module, A,B be Subset of V;

      assume A c= B & B is Basis of V;

      then

       P0: V is_the_direct_sum_of (( Lin A),( Lin (B \ A))) by ZMODUL05: 50;

      defpred P[ Element of V, object] means ex vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & $1 = (vA + vB) & $2 = vA;

      

       A1: for v be Element of V holds ex vA be Element of V st P[v, vA]

      proof

        let v be Element of V;

        consider vA,vB be Vector of V such that

         A2: vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) by P0, ZMODUL01: 133;

        take vA;

        thus thesis by A2;

      end;

      consider f be Function of V, V such that

       A9: for v be Vector of V holds P[v, (f . v)] from FUNCT_2:sch 3( A1);

      

       A10: for v,vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) holds (f . v) = vA

      proof

        let v,vA,vB be Vector of V;

        assume

         A11: vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB);

        consider vA1,vB1 be Vector of V such that

         A12: vA1 in ( Lin A) & vB1 in ( Lin (B \ A)) & v = (vA1 + vB1) & (f . v) = vA1 by A9;

        thus thesis by A11, A12, P0, ZMODUL01: 134;

      end;

      

       A13: f is additive

      proof

        let x,y be Element of V;

        consider xA,xB be Vector of V such that

         A14: xA in ( Lin A) & xB in ( Lin (B \ A)) & x = (xA + xB) & (f . x) = xA by A9;

        consider yA,yB be Vector of V such that

         A15: yA in ( Lin A) & yB in ( Lin (B \ A)) & y = (yA + yB) & (f . y) = yA by A9;

        consider xyA,xyB be Vector of V such that

         A16: xyA in ( Lin A) & xyB in ( Lin (B \ A)) & (x + y) = (xyA + xyB) & (f . (x + y)) = xyA by A9;

        

         A17: (xyA + xyB) = (((xA + xB) + yA) + yB) by A14, A15, A16, RLVECT_1:def 3

        .= ((xB + (xA + yA)) + yB) by RLVECT_1:def 3

        .= ((xA + yA) + (xB + yB)) by RLVECT_1:def 3;

        

         A18: (xA + yA) in ( Lin A) by A14, A15, ZMODUL01: 36;

        (xB + yB) in ( Lin (B \ A)) by A14, A15, ZMODUL01: 36;

        hence (f . (x + y)) = ((f . x) + (f . y)) by A14, A15, A16, A17, A18, P0, ZMODUL01: 134;

      end;

      for r be Element of INT.Ring , x be Element of V holds (f . (r * x)) = (r * (f . x))

      proof

        let r be Element of INT.Ring , x be Element of V;

        consider xA,xB be Vector of V such that

         A14: xA in ( Lin A) & xB in ( Lin (B \ A)) & x = (xA + xB) & (f . x) = xA by A9;

        consider rxA,rxB be Vector of V such that

         A15: rxA in ( Lin A) & rxB in ( Lin (B \ A)) & (r * x) = (rxA + rxB) & (f . (r * x)) = rxA by A9;

        

         A16: (rxA + rxB) = ((r * xA) + (r * xB)) by A14, A15, VECTSP_1:def 14;

        

         A18: (r * xA) in ( Lin A) by A14, ZMODUL01: 37;

        (r * xB) in ( Lin (B \ A)) by A14, ZMODUL01: 37;

        hence (f . (r * x)) = (r * (f . x)) by A14, A15, A16, A18, P0, ZMODUL01: 134;

      end;

      then f is homogeneous;

      then

      reconsider f as linear-transformation of V, V by A13;

      take f;

      thus thesis by A10, A9;

    end;

    definition

      let V be free Z_Module, A,B be Subset of V;

      assume

       AS: A c= B & B is Basis of V;

      :: ZMATRLIN:def10

      func Proj (A,B) -> linear-transformation of V, V means (for v be Vector of V holds ex vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) & (it . v) = vA) & for v,vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) holds (it . v) = vA;

      existence by LMPROJ1, AS;

      uniqueness

      proof

        let F1,F2 be linear-transformation of V, V;

        assume

         A1: (for v be Vector of V holds ex vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) & (F1 . v) = vA) & for v,vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) holds (F1 . v) = vA;

        assume

         A2: (for v be Vector of V holds ex vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) & (F2 . v) = vA) & for v,vA,vB be Vector of V st vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) holds (F2 . v) = vA;

        now

          let v be Vector of V;

          consider vA,vB be Vector of V such that

           A3: vA in ( Lin A) & vB in ( Lin (B \ A)) & v = (vA + vB) & (F1 . v) = vA by A1;

          thus (F1 . v) = (F2 . v) by A2, A3;

        end;

        hence F1 = F2 by FUNCT_2:def 7;

      end;

    end

    definition

      let V be free Z_Module, B be Basis of V, u be Vector of V;

      :: ZMATRLIN:def11

      func Coordinate (u,B) -> Function of V, INT.Ring means

      : defCoord: (for v be Vector of V holds ex Lu be Linear_Combination of B st v = ( Sum Lu) & (it . v) = (Lu . u)) & (for v be Vector of V, Lv be Linear_Combination of B st v = ( Sum Lv) holds (it . v) = (Lv . u)) & (for v1,v2 be Vector of V holds (it . (v1 + v2)) = ((it . v1) + (it . v2))) & (for v be Vector of V, r be Element of INT.Ring holds (it . (r * v)) = (r * (it . v)));

      existence

      proof

        

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

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

        

         A1: for v be Element of V holds ex r be Element of INT.Ring st P[v, r]

        proof

          let v be Element of V;

          v in ( Lin B) by X1;

          then

          consider Lv be Linear_Combination of B such that

           A4: v = ( Sum Lv) by ZMODUL02: 64;

          reconsider r = (Lv . u) as Element of INT.Ring ;

          take r;

          thus thesis by A4;

        end;

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

         A9: for v be Vector of V holds P[v, (f . v)] from FUNCT_2:sch 3( A1);

        

         A10: for v be Vector of V, Lv be Linear_Combination of B st v = ( Sum Lv) holds (f . v) = (Lv . u)

        proof

          let v be Vector of V, Lv be Linear_Combination of B;

          assume

           A11: v = ( Sum Lv);

          consider L be Linear_Combination of B such that

           A12: v = ( Sum L) & (f . v) = (L . u) by A9;

          ( Carrier L) c= B & ( Carrier Lv) c= B by VECTSP_6:def 4;

          hence (f . v) = (Lv . u) by A11, A12, Th5, VECTSP_7:def 3;

        end;

        

         A15: for v1,v2 be Vector of V holds (f . (v1 + v2)) = ((f . v1) + (f . v2))

        proof

          let v1,v2 be Vector of V;

          consider Lv1 be Linear_Combination of B such that

           P1: v1 = ( Sum Lv1) & (f . v1) = (Lv1 . u) by A9;

          consider Lv2 be Linear_Combination of B such that

           P2: v2 = ( Sum Lv2) & (f . v2) = (Lv2 . u) by A9;

          consider Lv12 be Linear_Combination of B such that

           P3: (v1 + v2) = ( Sum Lv12) & (f . (v1 + v2)) = (Lv12 . u) by A9;

          ( Carrier Lv1) c= B & ( Carrier Lv2) c= B & ( Carrier Lv12) c= B by VECTSP_6:def 4;

          then

           S: Lv12 = (Lv1 + Lv2) by P1, P2, P3, Th6, VECTSP_7:def 3;

          (f . (v1 + v2)) = (Lv12 . u) by P3

          .= ((Lv1 . u) + (Lv2 . u)) by S, VECTSP_6: 22

          .= ((f . v1) + (f . v2)) by P1, P2;

          hence (f . (v1 + v2)) = ((f . v1) + (f . v2));

        end;

        

         A15A: (f . ( 0. V)) = (f . (( 0. V) + ( 0. V)))

        .= ((f . ( 0. V)) + (f . ( 0. V))) by A15;

        

         A16: for v be Vector of V, r be Element of INT.Ring holds (f . (r * v)) = (r * (f . v))

        proof

          let v be Vector of V, r be Element of INT.Ring ;

          per cases ;

            suppose r = ( 0. INT.Ring );

            hence (f . (r * v)) = (r * (f . v)) by A15A, ZMODUL01: 1;

          end;

            suppose

             A162: r <> ( 0. INT.Ring );

            consider Lv be Linear_Combination of B such that

             P1: v = ( Sum Lv) & (f . v) = (Lv . u) by A9;

            consider rLv be Linear_Combination of B such that

             P2: (r * v) = ( Sum rLv) & (f . (r * v)) = (rLv . u) by A9;

            ( Carrier Lv) c= B & ( Carrier rLv) c= B by VECTSP_6:def 4;

            then (r * Lv) = rLv by A162, P1, P2, Th7, VECTSP_7:def 3;

            hence (f . (r * v)) = (r * (f . v)) by P1, P2, VECTSP_6:def 9;

          end;

        end;

        take f;

        thus thesis by A9, A10, A15, A16;

      end;

      uniqueness

      proof

        let f1,f2 be Function of V, INT.Ring ;

        assume

         A1: (for v be Vector of V holds ex Lu be Linear_Combination of B st v = ( Sum Lu) & (f1 . v) = (Lu . u)) & (for v be Vector of V, Lv be Linear_Combination of B st v = ( Sum Lv) holds (f1 . v) = (Lv . u)) & (for v1,v2 be Vector of V holds (f1 . (v1 + v2)) = ((f1 . v1) + (f1 . v2))) & (for v be Vector of V, r be Element of INT.Ring holds (f1 . (r * v)) = (r * (f1 . v)));

        assume

         A2: (for v be Vector of V holds ex Lu be Linear_Combination of B st v = ( Sum Lu) & (f2 . v) = (Lu . u)) & (for v be Vector of V, Lv be Linear_Combination of B st v = ( Sum Lv) holds (f2 . v) = (Lv . u)) & (for v1,v2 be Vector of V holds (f2 . (v1 + v2)) = ((f2 . v1) + (f2 . v2))) & (for v be Vector of V, r be Element of INT.Ring holds (f2 . (r * v)) = (r * (f2 . v)));

        now

          let v be Vector of V;

          consider Lu be Linear_Combination of B such that

           A3: v = ( Sum Lu) & (f1 . v) = (Lu . u) by A1;

          thus (f1 . v) = (f2 . v) by A2, A3;

        end;

        hence f1 = f2 by FUNCT_2:def 7;

      end;

    end

    theorem :: ZMATRLIN:57

    

     PROJ4: for V be free Z_Module, B be Basis of V, u be Vector of V holds (( Coordinate (u,B)) . ( 0. V)) = 0

    proof

      let V be free Z_Module, B be Basis of V, u be Vector of V;

      set f = ( Coordinate (u,B));

      (f . ( 0. V)) = (f . (( 0. V) + ( 0. V)))

      .= ((f . ( 0. V)) + (f . ( 0. V))) by defCoord;

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

    end;

    theorem :: ZMATRLIN:58

    

     PROJ5: for V be free Z_Module, X be Basis of V, v be Vector of V st v in X & v <> ( 0. V) holds (( Coordinate (v,X)) . v) = 1

    proof

      let V be free Z_Module, X be Basis of V, v be Vector of V;

      assume

       AS: v in X & v <> ( 0. V);

      set f = ( Coordinate (v,X));

      consider KL be Linear_Combination of X such that

       A1: v = ( Sum KL) & (f . v) = (KL . v) by defCoord;

      

       A3: ( Carrier KL) c= X by VECTSP_6:def 4;

      v in {v} by TARSKI:def 1;

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

      then

      consider Lb be Linear_Combination of {v} such that

       A4: v = ( Sum Lb) by ZMODUL02: 64;

      

       A7: ( Carrier Lb) c= {v} by VECTSP_6:def 4;

       {v} c= X by AS, ZFMISC_1: 31;

      then ( Carrier Lb) c= X by A7;

      then

       A9: Lb = KL by A4, A1, A3, Th5, VECTSP_7:def 3;

      ((Lb . v) * v) = v by A4, ZMODUL02: 21

      .= (( 1. INT.Ring ) * v) by VECTSP_1:def 17;

      hence (f . v) = 1 by AS, A1, A9, ZMODUL01: 11;

    end;

    registration

      let V be non trivial free Z_Module;

      cluster additive homogeneous non constant non trivial for Functional of V;

      existence

      proof

        set X = the Basis of V;

        

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

        X <> {}

        proof

          assume X = {} ;

          then X = ( {} the carrier of V);

          then

           X3: the ModuleStr of V = ( (0). V) by X1, ZMODUL02: 67;

          for x,y be object st x in the carrier of V & y in the carrier of V holds x = y

          proof

            let x,y be object;

            assume x in the carrier of V & y in the carrier of V;

            then

            reconsider x1 = x, y1 = y as Vector of V;

            x1 in ( (0). V) & y1 in ( (0). V) by X3;

            then x1 = ( 0. V) & y1 = ( 0. V) by ZMODUL02: 66;

            hence thesis;

          end;

          then V is trivial;

          hence contradiction;

        end;

        then

        consider v be object such that

         X2: v in X by XBOOLE_0:def 1;

        reconsider v as Vector of V by X2;

        

         X20: v <> ( 0. V) by X2, ZMODUL02: 57, VECTSP_7:def 3;

        reconsider f = ( Coordinate (v,X)) as Function of V, INT.Ring ;

        

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

        

         J1: (f . ( 0. V)) = 0 by PROJ4;

        

         A16: (f . v) = 1 by X2, X20, PROJ5;

        take f;

        thus thesis by A16, DM1, J1, defCoord;

      end;

    end

    theorem :: ZMATRLIN:59

    

     VS10Th28: for V be non trivial free Z_Module, f be non constant 0-preserving Functional of V holds ex v be Vector of V st v <> ( 0. V) & (f . v) <> ( 0. INT.Ring )

    proof

      let V be non trivial free Z_Module, f be non constant 0-preserving Functional of V;

      

       A1: (f . ( 0. V)) = ( 0. INT.Ring ) by HAHNBAN1:def 9;

      assume

       A2: for v be Vector of V st v <> ( 0. V) holds (f . v) = ( 0. INT.Ring );

      now

        let x,y be object;

        assume x in ( dom f) & y in ( dom f);

        then

        reconsider v = x, w = y as Vector of V;

        

        thus (f . x) = (f . v)

        .= 0 by A2, A1

        .= (f . w) by A2, A1

        .= (f . y);

      end;

      hence contradiction by FUNCT_1:def 10;

    end;

    begin

    definition

      let V,W be ModuleStr over INT.Ring ;

      :: ZMATRLIN:def12

      func NulForm (V,W) -> Form of V, W equals ( [:the carrier of V, the carrier of W:] --> ( 0. INT.Ring ));

      coherence ;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be Form of V, W;

      :: ZMATRLIN:def13

      func f + g -> Form of V, W means

      : BLDef2: for v be Vector of V, w be Vector of W holds (it . (v,w)) = ((f . (v,w)) + (g . (v,w)));

      existence

      proof

        set X = the carrier of V, Y = the carrier of W;

        deffunc F( Element of X, Element of Y) = ((f . ($1,$2)) + (g . ($1,$2)));

        consider ff be Function of [:X, Y:], INT.Ring such that

         A1: for x be Element of X holds for y be Element of Y holds (ff . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider ff as Form of V, W;

        take ff;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Form of V, W such that

         A2: for v be Vector of V, w be Vector of W holds (F . (v,w)) = ((f . (v,w)) + (g . (v,w))) and

         A3: for v be Vector of V, w be Vector of W holds (G . (v,w)) = ((f . (v,w)) + (g . (v,w)));

        now

          let v be Vector of V, w be Vector of W;

          

          thus (F . (v,w)) = ((f . (v,w)) + (g . (v,w))) by A2

          .= (G . (v,w)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Form of V, W;

      let a be Element of INT.Ring ;

      :: ZMATRLIN:def14

      func a * f -> Form of V, W means

      : BLDef3: for v be Vector of V, w be Vector of W holds (it . (v,w)) = (a * (f . (v,w)));

      existence

      proof

        reconsider aa = a as Element of INT.Ring ;

        set X = the carrier of V, Y = the carrier of W;

        deffunc F( Element of X, Element of Y) = ( In ((aa * (f . ($1,$2))),the carrier of INT.Ring ));

        consider ff be Function of [:X, Y:], INT.Ring such that

         A1: for x be Element of X holds for y be Element of Y holds (ff . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider ff as Form of V, W;

        take ff;

        let v be Vector of V, w be Vector of W;

        (ff . (v,w)) = F(v,w) by A1;

        then (ff . (v,w)) = (a * (f . (v,w)));

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Form of V, W such that

         A2: for v be Vector of V, w be Vector of W holds (F . (v,w)) = (a * (f . (v,w))) and

         A3: for v be Vector of V, w be Vector of W holds (G . (v,w)) = (a * (f . (v,w)));

        now

          let v be Vector of V, w be Vector of W;

          

          thus (F . (v,w)) = (a * (f . (v,w))) by A2

          .= (G . (v,w)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Form of V, W;

      :: ZMATRLIN:def15

      func - f -> Form of V, W means

      : BLDef4: for v be Vector of V, w be Vector of W holds (it . (v,w)) = ( - (f . (v,w)));

      existence

      proof

        set X = the carrier of V, Y = the carrier of W;

        deffunc F( Element of X, Element of Y) = ( In (( - (f . ($1,$2))),the carrier of INT.Ring ));

        consider ff be Function of [:X, Y:], INT.Ring such that

         A1: for x be Element of X holds for y be Element of Y holds (ff . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider ff as Form of V, W;

        take ff;

        let v be Vector of V, w be Vector of W;

        (ff . (v,w)) = F(v,w) by A1;

        then (ff . (v,w)) = ( - (f . (v,w)));

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Form of V, W such that

         A2: for v be Vector of V, w be Vector of W holds (F . (v,w)) = ( - (f . (v,w))) and

         A3: for v be Vector of V, w be Vector of W holds (G . (v,w)) = ( - (f . (v,w)));

        now

          let v be Vector of V, w be Vector of W;

          

          thus (F . (v,w)) = ( - (f . (v,w))) by A2

          .= (G . (v,w)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Form of V, W;

      :: original: -

      redefine

      :: ZMATRLIN:def16

      func - f equals (( - ( 1. INT.Ring )) * f);

      compatibility

      proof

        let g be Form of V, W;

        thus g = ( - f) implies g = (( - ( 1. INT.Ring )) * f)

        proof

          assume

           A1: g = ( - f);

          now

            let v be Vector of V, w be Vector of W;

            

            thus (g . (v,w)) = ( - (f . (v,w))) by A1, BLDef4

            .= (( - ( 1. INT.Ring )) * (f . (v,w)))

            .= ((( - ( 1. INT.Ring )) * f) . (v,w)) by BLDef3;

          end;

          hence thesis;

        end;

        assume

         A2: g = (( - ( 1. INT.Ring )) * f);

        now

          let v be Vector of V, w be Vector of W;

          

          thus (g . (v,w)) = (( - ( 1. INT.Ring )) * (f . (v,w))) by A2, BLDef3

          .= ( - (f . (v,w)))

          .= (( - f) . (v,w)) by BLDef4;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be Form of V, W;

      :: ZMATRLIN:def17

      func f - g -> Form of V, W equals (f + ( - g));

      correctness ;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be Form of V, W;

      :: original: -

      redefine

      :: ZMATRLIN:def18

      func f - g means

      : BLDef7: for v be Vector of V, w be Vector of W holds (it . (v,w)) = ((f . (v,w)) - (g . (v,w)));

      compatibility

      proof

        let h be Form of V, W;

        thus h = (f - g) implies for v be Vector of V, w be Vector of W holds (h . (v,w)) = ((f . (v,w)) - (g . (v,w)))

        proof

          assume

           A1: h = (f - g);

          let v be Vector of V, w be Vector of W;

          

          thus (h . (v,w)) = ((f . (v,w)) + (( - g) . (v,w))) by A1, BLDef2

          .= ((f . (v,w)) - (g . (v,w))) by BLDef4;

        end;

        assume

         A2: for v be Vector of V, w be Vector of W holds (h . (v,w)) = ((f . (v,w)) - (g . (v,w)));

        now

          let v be Vector of V, w be Vector of W;

          

          thus (h . (v,w)) = ((f . (v,w)) - (g . (v,w))) by A2

          .= ((f . (v,w)) + (( - g) . (v,w))) by BLDef4

          .= ((f - g) . (v,w)) by BLDef2;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be Form of V, W;

      :: original: +

      redefine

      func f + g;

      commutativity

      proof

        let f,g be Form of V, W;

        now

          let v be Vector of V, w be Vector of W;

          

          thus ((f + g) . (v,w)) = ((f . (v,w)) + (g . (v,w))) by BLDef2

          .= ((g + f) . (v,w)) by BLDef2;

        end;

        hence (f + g) = (g + f);

      end;

    end

    theorem :: ZMATRLIN:60

    for V,W be non empty ModuleStr over INT.Ring , f be Form of V, W holds (f + ( NulForm (V,W))) = f

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be Form of V, W;

      set g = ( NulForm (V,W));

      now

        let v be Vector of V, w be Vector of W;

        

        thus ((f + g) . (v,w)) = ((f . (v,w)) + (g . (v,w))) by BLDef2

        .= ((f . (v,w)) + 0 ) by FUNCOP_1: 70

        .= (f . (v,w));

      end;

      hence thesis;

    end;

    theorem :: ZMATRLIN:61

    for V,W be non empty ModuleStr over INT.Ring , f,g,h be Form of V, W holds ((f + g) + h) = (f + (g + h))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g,h be Form of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus (((f + g) + h) . (v,w)) = (((f + g) . (v,w)) + (h . (v,w))) by BLDef2

        .= (((f . (v,w)) + (g . (v,w))) + (h . (v,w))) by BLDef2

        .= ((f . (v,w)) + ((g . (v,w)) + (h . (v,w))))

        .= ((f . (v,w)) + ((g + h) . (v,w))) by BLDef2

        .= ((f + (g + h)) . (v,w)) by BLDef2;

      end;

      hence thesis;

    end;

    theorem :: ZMATRLIN:62

    for V,W be non empty ModuleStr over INT.Ring , f be Form of V, W holds (f - f) = ( NulForm (V,W))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be Form of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus ((f - f) . (v,w)) = ((f . (v,w)) - (f . (v,w))) by BLDef7

        .= (( NulForm (V,W)) . (v,w)) by FUNCOP_1: 70;

      end;

      hence thesis;

    end;

    theorem :: ZMATRLIN:63

    for V,W be non empty ModuleStr over INT.Ring , a be Element of INT.Ring , f,g be Form of V, W holds (a * (f + g)) = ((a * f) + (a * g))

    proof

      let V,W be non empty ModuleStr over INT.Ring , r be Element of INT.Ring , f,g be Form of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus ((r * (f + g)) . (v,w)) = (r * ((f + g) . (v,w))) by BLDef3

        .= (r * ((f . (v,w)) + (g . (v,w)))) by BLDef2

        .= ((r * (f . (v,w))) + (r * (g . (v,w))))

        .= (((r * f) . (v,w)) + (r * (g . (v,w)))) by BLDef3

        .= (((r * f) . (v,w)) + ((r * g) . (v,w))) by BLDef3

        .= (((r * f) + (r * g)) . (v,w)) by BLDef2;

      end;

      hence thesis;

    end;

    theorem :: ZMATRLIN:64

    for V,W be non empty ModuleStr over INT.Ring , a,b be Element of INT.Ring , f be Form of V, W holds ((a + b) * f) = ((a * f) + (b * f))

    proof

      let V,W be non empty ModuleStr over INT.Ring , r,s be Element of INT.Ring , f be Form of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus (((r + s) * f) . (v,w)) = ((r + s) * (f . (v,w))) by BLDef3

        .= ((r * (f . (v,w))) + (s * (f . (v,w))))

        .= (((r * f) . (v,w)) + (s * (f . (v,w)))) by BLDef3

        .= (((r * f) . (v,w)) + ((s * f) . (v,w))) by BLDef3

        .= (((r * f) + (s * f)) . (v,w)) by BLDef2;

      end;

      hence thesis;

    end;

    theorem :: ZMATRLIN:65

    for V,W be non empty ModuleStr over INT.Ring , a,b be Element of INT.Ring , f be Form of V, W holds ((a * b) * f) = (a * (b * f))

    proof

      let V,W be non empty ModuleStr over INT.Ring , r,s be Element of INT.Ring , f be Form of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus (((r * s) * f) . (v,w)) = ((r * s) * (f . (v,w))) by BLDef3

        .= (r * (s * (f . (v,w))))

        .= (r * ((s * f) . (v,w))) by BLDef3

        .= ((r * (s * f)) . (v,w)) by BLDef3;

      end;

      hence thesis;

    end;

    theorem :: ZMATRLIN:66

    for V,W be non empty ModuleStr over INT.Ring , f be Form of V, W holds (( 1. INT.Ring ) * f) = f

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be Form of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus ((( 1. INT.Ring ) * f) . (v,w)) = (( 1. INT.Ring ) * (f . (v,w))) by BLDef3

        .= (f . (v,w));

      end;

      hence thesis;

    end;

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Form of V, W, v be Vector of V;

      :: ZMATRLIN:def19

      func FunctionalFAF (f,v) -> Functional of W equals (( curry f) . v);

      correctness ;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Form of V, W, w be Vector of W;

      :: ZMATRLIN:def20

      func FunctionalSAF (f,w) -> Functional of V equals (( curry' f) . w);

      correctness ;

    end

    theorem :: ZMATRLIN:67

    

     BLTh8: for V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, v be Vector of V holds ( dom ( FunctionalFAF (f,v))) = the carrier of W & ( rng ( FunctionalFAF (f,v))) c= the carrier of INT.Ring & for w be Vector of W holds (( FunctionalFAF (f,v)) . w) = (f . (v,w))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Form of V, W, v be Vector of V;

      set F = ( FunctionalFAF (f,v));

      ( dom f) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

      then

       A1: ex g be Function st (( curry f) . v) = g & ( dom g) = the carrier of W & ( rng g) c= ( rng f) & for y be object st y in the carrier of W holds (g . y) = (f . (v,y)) by FUNCT_5: 29;

      hence ( dom F) = the carrier of W & ( rng F) c= the carrier of INT.Ring ;

      let y be Vector of W;

      thus thesis by A1;

    end;

    theorem :: ZMATRLIN:68

    

     BLTh9: for V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, w be Vector of W holds ( dom ( FunctionalSAF (f,w))) = the carrier of V & ( rng ( FunctionalSAF (f,w))) c= the carrier of INT.Ring & for v be Vector of V holds (( FunctionalSAF (f,w)) . v) = (f . (v,w))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, w be Vector of W;

      set F = ( FunctionalSAF (f,w));

      ( dom f) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

      then

       A1: ex g be Function st (( curry' f) . w) = g & ( dom g) = the carrier of V & ( rng g) c= ( rng f) & for y be object st y in the carrier of V holds (g . y) = (f . (y,w)) by FUNCT_5: 32;

      hence ( dom F) = the carrier of V & ( rng F) c= the carrier of INT.Ring ;

      let v be Vector of V;

      thus thesis by A1;

    end;

    theorem :: ZMATRLIN:69

    

     BLTh10: for V,W be non empty ModuleStr over INT.Ring , v be Vector of V holds ( FunctionalFAF (( NulForm (V,W)),v)) = ( 0Functional W)

    proof

      let V,W be non empty ModuleStr over INT.Ring , v be Vector of V;

      set N = ( NulForm (V,W));

      now

        let y be Vector of W;

        

        thus (( FunctionalFAF (N,v)) . y) = (N . (v,y)) by BLTh8

        .= ( 0. INT.Ring ) by FUNCOP_1: 70

        .= (( 0Functional W) . y);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:70

    

     BLTh11: for V,W be non empty ModuleStr over INT.Ring , w be Vector of W holds ( FunctionalSAF (( NulForm (V,W)),w)) = ( 0Functional V)

    proof

      let V,W be non empty ModuleStr over INT.Ring , y be Vector of W;

      set N = ( NulForm (V,W));

      now

        let v be Vector of V;

        

        thus (( FunctionalSAF (N,y)) . v) = (N . (v,y)) by BLTh9

        .= ( 0. INT.Ring ) by FUNCOP_1: 70

        .= (( 0Functional V) . v);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:71

    

     BLTh12: for V,W be non empty ModuleStr over INT.Ring , f,g be Form of V, W, w be Vector of W holds ( FunctionalSAF ((f + g),w)) = (( FunctionalSAF (f,w)) + ( FunctionalSAF (g,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g be Form of V, W, w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FunctionalSAF ((f + g),w)) . v) = ((f + g) . (v,w)) by BLTh9

        .= ((f . (v,w)) + (g . (v,w))) by BLDef2

        .= ((( FunctionalSAF (f,w)) . v) + (g . (v,w))) by BLTh9

        .= ((( FunctionalSAF (f,w)) . v) + (( FunctionalSAF (g,w)) . v)) by BLTh9

        .= ((( FunctionalSAF (f,w)) + ( FunctionalSAF (g,w))) . v) by HAHNBAN1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:72

    

     BLTh13: for V,W be non empty ModuleStr over INT.Ring , f,g be Form of V, W, v be Vector of V holds ( FunctionalFAF ((f + g),v)) = (( FunctionalFAF (f,v)) + ( FunctionalFAF (g,v)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g be Form of V, W, w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FunctionalFAF ((f + g),w)) . v) = ((f + g) . (w,v)) by BLTh8

        .= ((f . (w,v)) + (g . (w,v))) by BLDef2

        .= ((( FunctionalFAF (f,w)) . v) + (g . (w,v))) by BLTh8

        .= ((( FunctionalFAF (f,w)) . v) + (( FunctionalFAF (g,w)) . v)) by BLTh8

        .= ((( FunctionalFAF (f,w)) + ( FunctionalFAF (g,w))) . v) by HAHNBAN1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:73

    

     BLTh14: for V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, a be Element of INT.Ring , w be Vector of W holds ( FunctionalSAF ((a * f),w)) = (a * ( FunctionalSAF (f,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, a be Element of INT.Ring , w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FunctionalSAF ((a * f),w)) . v) = ((a * f) . (v,w)) by BLTh9

        .= (a * (f . (v,w))) by BLDef3

        .= (a * (( FunctionalSAF (f,w)) . v)) by BLTh9

        .= ((a * ( FunctionalSAF (f,w))) . v) by HAHNBAN1:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:74

    

     BLTh15: for V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, a be Element of INT.Ring , v be Vector of V holds ( FunctionalFAF ((a * f),v)) = (a * ( FunctionalFAF (f,v)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, a be Element of INT.Ring , w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FunctionalFAF ((a * f),w)) . v) = ((a * f) . (w,v)) by BLTh8

        .= (a * (f . (w,v))) by BLDef3

        .= (a * (( FunctionalFAF (f,w)) . v)) by BLTh8

        .= ((a * ( FunctionalFAF (f,w))) . v) by HAHNBAN1:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:75

    for V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, w be Vector of W holds ( FunctionalSAF (( - f),w)) = ( - ( FunctionalSAF (f,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FunctionalSAF (( - f),w)) . v) = (( - f) . (v,w)) by BLTh9

        .= ( - (f . (v,w))) by BLDef4

        .= ( - (( FunctionalSAF (f,w)) . v)) by BLTh9

        .= (( - ( FunctionalSAF (f,w))) . v) by HAHNBAN1:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:76

    for V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, v be Vector of V holds ( FunctionalFAF (( - f),v)) = ( - ( FunctionalFAF (f,v)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be Form of V, W, w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FunctionalFAF (( - f),w)) . v) = (( - f) . (w,v)) by BLTh8

        .= ( - (f . (w,v))) by BLDef4

        .= ( - (( FunctionalFAF (f,w)) . v)) by BLTh8

        .= (( - ( FunctionalFAF (f,w))) . v) by HAHNBAN1:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:77

    for V,W be non empty ModuleStr over INT.Ring , f,g be Form of V, W, w be Vector of W holds ( FunctionalSAF ((f - g),w)) = (( FunctionalSAF (f,w)) - ( FunctionalSAF (g,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g be Form of V, W, w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FunctionalSAF ((f - g),w)) . v) = ((f - g) . (v,w)) by BLTh9

        .= ((f . (v,w)) - (g . (v,w))) by BLDef7

        .= ((( FunctionalSAF (f,w)) . v) - (g . (v,w))) by BLTh9

        .= ((( FunctionalSAF (f,w)) . v) - (( FunctionalSAF (g,w)) . v)) by BLTh9

        .= ((( FunctionalSAF (f,w)) . v) + (( - ( FunctionalSAF (g,w))) . v)) by HAHNBAN1:def 4

        .= ((( FunctionalSAF (f,w)) - ( FunctionalSAF (g,w))) . v) by HAHNBAN1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:78

    for V,W be non empty ModuleStr over INT.Ring , f,g be Form of V, W, v be Vector of V holds ( FunctionalFAF ((f - g),v)) = (( FunctionalFAF (f,v)) - ( FunctionalFAF (g,v)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g be Form of V, W, w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FunctionalFAF ((f - g),w)) . v) = ((f - g) . (w,v)) by BLTh8

        .= ((f . (w,v)) - (g . (w,v))) by BLDef7

        .= ((( FunctionalFAF (f,w)) . v) - (g . (w,v))) by BLTh8

        .= ((( FunctionalFAF (f,w)) . v) - (( FunctionalFAF (g,w)) . v)) by BLTh8

        .= ((( FunctionalFAF (f,w)) . v) + (( - ( FunctionalFAF (g,w))) . v)) by HAHNBAN1:def 4

        .= ((( FunctionalFAF (f,w)) - ( FunctionalFAF (g,w))) . v) by HAHNBAN1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Functional of V;

      let g be Functional of W;

      :: ZMATRLIN:def21

      func FormFunctional (f,g) -> Form of V, W means

      : BLDef10: for v be Vector of V, w be Vector of W holds (it . (v,w)) = ((f . v) * (g . w));

      existence

      proof

        deffunc F( Vector of V, Vector of W) = ((f . $1) * (g . $2));

        set c1 = the carrier of V, c2 = the carrier of W;

        consider i be Function of [:c1, c2:], the carrier of INT.Ring such that

         A1: for x be Element of c1 holds for y be Element of c2 holds (i . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider i as Form of V, W;

        take i;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be Form of V, W such that

         A2: for v be Vector of V, y be Vector of W holds (F1 . (v,y)) = ((f . v) * (g . y)) and

         A3: for v be Vector of V, y be Vector of W holds (F2 . (v,y)) = ((f . v) * (g . y));

        now

          let v be Vector of V, y be Vector of W;

          

          thus (F1 . (v,y)) = ((f . v) * (g . y)) by A2

          .= (F2 . (v,y)) by A3;

        end;

        hence thesis;

      end;

    end

    theorem :: ZMATRLIN:79

    

     BLTh20: for V,W be non empty ModuleStr over INT.Ring , f be Functional of V, v be Vector of V, w be Vector of W holds (( FormFunctional (f,( 0Functional W))) . (v,w)) = 0

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Functional of V, v be Vector of V, y be Vector of W;

      set 0F = ( 0Functional W), F = ( FormFunctional (f,0F));

      

      thus (F . (v,y)) = ((f . v) * (0F . y)) by BLDef10

      .= ((f . v) * 0 )

      .= 0 ;

    end;

    theorem :: ZMATRLIN:80

    

     BLTh21: for V,W be non empty ModuleStr over INT.Ring , g be Functional of W, v be Vector of V, w be Vector of W holds (( FormFunctional (( 0Functional V),g)) . (v,w)) = 0

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let h be Functional of W, v be Vector of V, y be Vector of W;

      set 0F = ( 0Functional V), F = ( FormFunctional (0F,h));

      

      thus (F . (v,y)) = ((0F . v) * (h . y)) by BLDef10

      .= ( 0 * (h . y))

      .= 0 ;

    end;

    theorem :: ZMATRLIN:81

    for V,W be non empty ModuleStr over INT.Ring , f be Functional of V holds ( FormFunctional (f,( 0Functional W))) = ( NulForm (V,W))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be Functional of V;

      now

        let v be Vector of V, y be Vector of W;

        

        thus (( FormFunctional (f,( 0Functional W))) . (v,y)) = 0 by BLTh20

        .= (( NulForm (V,W)) . (v,y)) by FUNCOP_1: 70;

      end;

      hence thesis;

    end;

    theorem :: ZMATRLIN:82

    for V,W be non empty ModuleStr over INT.Ring , g be Functional of W holds ( FormFunctional (( 0Functional V),g)) = ( NulForm (V,W))

    proof

      let V,W be non empty ModuleStr over INT.Ring , h be Functional of W;

      now

        let v be Vector of V, y be Vector of W;

        

        thus (( FormFunctional (( 0Functional V),h)) . (v,y)) = 0 by BLTh21

        .= (( NulForm (V,W)) . (v,y)) by FUNCOP_1: 70;

      end;

      hence thesis;

    end;

    theorem :: ZMATRLIN:83

    

     BLTh24: for V,W be non empty ModuleStr over INT.Ring , f be Functional of V, g be Functional of W, v be Vector of V holds ( FunctionalFAF (( FormFunctional (f,g)),v)) = ((f . v) * g)

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Functional of V, h be Functional of W, v be Vector of V;

      set F = ( FormFunctional (f,h)), FF = ( FunctionalFAF (F,v));

      now

        let y be Vector of W;

        

        thus (FF . y) = (F . (v,y)) by BLTh8

        .= ((f . v) * (h . y)) by BLDef10

        .= (((f . v) * h) . y) by HAHNBAN1:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMATRLIN:84

    

     BLTh25: for V,W be non empty ModuleStr over INT.Ring , f be Functional of V, g be Functional of W, w be Vector of W holds ( FunctionalSAF (( FormFunctional (f,g)),w)) = ((g . w) * f)

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Functional of V, h be Functional of W, y be Vector of W;

      set F = ( FormFunctional (f,h)), FF = ( FunctionalSAF (F,y));

      now

        let v be Vector of V;

        

        thus (FF . v) = (F . (v,y)) by BLTh9

        .= ((f . v) * (h . y)) by BLDef10

        .= (((h . y) * f) . v) by HAHNBAN1:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Form of V, W;

      :: ZMATRLIN:def22

      attr f is additiveFAF means

      : BLDef11: for v be Vector of V holds ( FunctionalFAF (f,v)) is additive;

      :: ZMATRLIN:def23

      attr f is additiveSAF means

      : BLDef12: for w be Vector of W holds ( FunctionalSAF (f,w)) is additive;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Form of V, W;

      :: ZMATRLIN:def24

      attr f is homogeneousFAF means

      : BLDef13: for v be Vector of V holds ( FunctionalFAF (f,v)) is homogeneous;

      :: ZMATRLIN:def25

      attr f is homogeneousSAF means

      : BLDef14: for w be Vector of W holds ( FunctionalSAF (f,w)) is homogeneous;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      cluster ( NulForm (V,W)) -> additiveFAF;

      coherence

      proof

        let v be Vector of V;

        ( FunctionalFAF (( NulForm (V,W)),v)) = ( 0Functional W) by BLTh10;

        hence thesis;

      end;

      cluster ( NulForm (V,W)) -> additiveSAF;

      coherence

      proof

        let y be Vector of W;

        ( FunctionalSAF (( NulForm (V,W)),y)) = ( 0Functional V) by BLTh11;

        hence thesis;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      cluster ( NulForm (V,W)) -> homogeneousFAF;

      coherence

      proof

        let v be Vector of V;

        ( FunctionalFAF (( NulForm (V,W)),v)) = ( 0Functional W) by BLTh10;

        hence thesis;

      end;

      cluster ( NulForm (V,W)) -> homogeneousSAF;

      coherence

      proof

        let y be Vector of W;

        ( FunctionalSAF (( NulForm (V,W)),y)) = ( 0Functional V) by BLTh11;

        hence thesis;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      cluster additiveFAF homogeneousFAF additiveSAF homogeneousSAF for Form of V, W;

      existence

      proof

        take ( NulForm (V,W));

        thus thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      mode bilinear-Form of V,W is additiveSAF homogeneousSAF additiveFAF homogeneousFAF Form of V, W;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveFAF Form of V, W, v be Vector of V;

      cluster ( FunctionalFAF (f,v)) -> additive;

      coherence by BLDef11;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveSAF Form of V, W, w be Vector of W;

      cluster ( FunctionalSAF (f,w)) -> additive;

      coherence by BLDef12;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousFAF Form of V, W, v be Vector of V;

      cluster ( FunctionalFAF (f,v)) -> homogeneous;

      coherence by BLDef13;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousSAF Form of V, W, w be Vector of W;

      cluster ( FunctionalSAF (f,w)) -> homogeneous;

      coherence by BLDef14;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Functional of V, g be additive Functional of W;

      cluster ( FormFunctional (f,g)) -> additiveFAF;

      coherence

      proof

        let v be Vector of V;

        set fg = ( FormFunctional (f,g)), F = ( FunctionalFAF (fg,v));

        let y,y9 be Vector of W;

        

         A1: F = ((f . v) * g) by BLTh24;

        

        hence (F . (y + y9)) = ((f . v) * (g . (y + y9))) by HAHNBAN1:def 6

        .= ((f . v) * ((g . y) + (g . y9))) by VECTSP_1:def 20

        .= (((f . v) * (g . y)) + ((f . v) * (g . y9)))

        .= (((f . v) * (g . y)) + (F . y9)) by A1, HAHNBAN1:def 6

        .= ((F . y) + (F . y9)) by A1, HAHNBAN1:def 6;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additive Functional of V, g be Functional of W;

      cluster ( FormFunctional (f,g)) -> additiveSAF;

      coherence

      proof

        let y be Vector of W;

        set fg = ( FormFunctional (f,g)), F = ( FunctionalSAF (fg,y));

        F = ((g . y) * f) by BLTh25;

        hence thesis;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be Functional of V, g be homogeneous Functional of W;

      cluster ( FormFunctional (f,g)) -> homogeneousFAF;

      coherence

      proof

        let v be Vector of V;

        set fg = ( FormFunctional (f,g)), F = ( FunctionalFAF (fg,v));

        let y be Vector of W, r be Element of INT.Ring ;

        

         A1: F = ((f . v) * g) by BLTh24;

        

        hence (F . (r * y)) = ((f . v) * (g . (r * y))) by HAHNBAN1:def 6

        .= ((f . v) * (r * (g . y))) by HAHNBAN1:def 8

        .= (r * ((f . v) * (g . y)))

        .= (r * (F . y)) by A1, HAHNBAN1:def 6;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneous Functional of V, g be Functional of W;

      cluster ( FormFunctional (f,g)) -> homogeneousSAF;

      coherence

      proof

        let y be Vector of W;

        set fg = ( FormFunctional (f,g));

        set F = ( FunctionalSAF (fg,y));

        let v be Vector of V, r be Element of INT.Ring ;

        

         A1: F = ((g . y) * f) by BLTh25;

        

        hence (F . (r * v)) = ((g . y) * (f . (r * v))) by HAHNBAN1:def 6

        .= ((g . y) * (r * (f . v))) by HAHNBAN1:def 8

        .= (r * ((g . y) * (f . v)))

        .= (r * (F . v)) by A1, HAHNBAN1:def 6;

      end;

    end

    registration

      let V be non trivial ModuleStr over INT.Ring , W be Z_Module;

      let f be Functional of V, g be Functional of W;

      cluster ( FormFunctional (f,g)) -> non trivial;

      coherence

      proof

        set fg = ( FormFunctional (f,g));

        set w = the Vector of W;

        consider v be Vector of V such that

         A1: v <> ( 0. V) by STRUCT_0:def 18;

        

         A2: [( 0. V), ( 0. W)] <> [v, w] by A1, XTUPLE_0: 1;

        ( dom fg) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

        then

         A3: [ [( 0. V), ( 0. W)], (fg . (( 0. V),( 0. W)))] in fg & [ [v, w], (fg . (v,w))] in fg by FUNCT_1: 1;

        assume

         A4: fg is trivial;

        per cases by A4, ZFMISC_1: 131;

          suppose fg = {} ;

          hence contradiction;

        end;

          suppose ex x be object st fg = {x};

          then

          consider x be object such that

           A5: fg = {x};

           [ [( 0. V), ( 0. W)], (fg . (( 0. V),( 0. W)))] = x & x = [ [v, w], (fg . (v,w))] by A3, A5, TARSKI:def 1;

          hence contradiction by A2, XTUPLE_0: 1;

        end;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring , W be non trivial Z_Module;

      let f be Functional of V, g be Functional of W;

      cluster ( FormFunctional (f,g)) -> non trivial;

      coherence

      proof

        set fg = ( FormFunctional (f,g));

        set v = the Vector of V;

        consider w be Vector of W such that

         A1: w <> ( 0. W) by STRUCT_0:def 18;

        

         A2: [( 0. V), ( 0. W)] <> [v, w] by A1, XTUPLE_0: 1;

        ( dom fg) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

        then

         A3: [ [( 0. V), ( 0. W)], (fg . (( 0. V),( 0. W)))] in fg & [ [v, w], (fg . (v,w))] in fg by FUNCT_1: 1;

        assume

         A4: fg is trivial;

        per cases by A4, ZFMISC_1: 131;

          suppose fg = {} ;

          hence contradiction;

        end;

          suppose ex x be object st fg = {x};

          then

          consider x be object such that

           A5: fg = {x};

           [ [( 0. V), ( 0. W)], (fg . (( 0. V),( 0. W)))] = x & x = [ [v, w], (fg . (v,w))] by A3, A5, TARSKI:def 1;

          hence contradiction by A2, XTUPLE_0: 1;

        end;

      end;

    end

    registration

      let V,W be non trivial free Z_Module;

      let f be non constant 0-preserving Functional of V, g be non constant 0-preserving Functional of W;

      cluster ( FormFunctional (f,g)) -> non constant;

      coherence

      proof

        set fg = ( FormFunctional (f,g));

        consider v be Vector of V such that v <> ( 0. V) and

         A1: (f . v) <> 0 by VS10Th28;

        consider w be Vector of W such that w <> ( 0. W) and

         A2: (g . w) <> 0 by VS10Th28;

        (fg . (v,w)) = ((f . v) * (g . w)) by BLDef10;

        then

         A3: ( dom fg) = [:the carrier of V, the carrier of W:] & (fg . (v,w)) <> 0 by A1, A2, FUNCT_2:def 1;

        (fg . (( 0. V),( 0. W))) = ((f . ( 0. V)) * (g . ( 0. W))) by BLDef10

        .= (( 0. INT.Ring ) * (g . ( 0. W))) by HAHNBAN1:def 9

        .= ( 0. INT.Ring );

        hence thesis by A3, BINOP_1: 19;

      end;

    end

    registration

      let V,W be non trivial free Z_Module;

      cluster non trivial non constant additiveFAF homogeneousFAF additiveSAF homogeneousSAF for Form of V, W;

      existence

      proof

        set f = the non constant non trivial linear-Functional of V, g = the non constant non trivial linear-Functional of W;

        take ( FormFunctional (f,g));

        thus thesis;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be additiveSAF Form of V, W;

      cluster (f + g) -> additiveSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF ((f + g),w)), Ff = ( FunctionalSAF (f,w));

        set Fg = ( FunctionalSAF (g,w));

        let v,y be Vector of V;

        

         A1: Ff is additive;

        

         A2: Fg is additive;

        

        thus (Ffg . (v + y)) = ((Ff + Fg) . (v + y)) by BLTh12

        .= ((Ff . (v + y)) + (Fg . (v + y))) by HAHNBAN1:def 3

        .= (((Ff . v) + (Ff . y)) + (Fg . (v + y))) by A1

        .= (((Ff . v) + (Ff . y)) + ((Fg . v) + (Fg . y))) by A2

        .= ((((Ff . v) + (Fg . v)) + (Ff . y)) + (Fg . y))

        .= ((((Ff + Fg) . v) + (Ff . y)) + (Fg . y)) by HAHNBAN1:def 3

        .= (((Ff + Fg) . v) + ((Ff . y) + (Fg . y)))

        .= (((Ff + Fg) . v) + ((Ff + Fg) . y)) by HAHNBAN1:def 3

        .= ((Ffg . v) + ((Ff + Fg) . y)) by BLTh12

        .= ((Ffg . v) + (Ffg . y)) by BLTh12;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be additiveFAF Form of V, W;

      cluster (f + g) -> additiveFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF ((f + g),w)), Ff = ( FunctionalFAF (f,w));

        set Fg = ( FunctionalFAF (g,w));

        let v,y be Vector of W;

        

         A1: Ff is additive;

        

         A2: Fg is additive;

        

        thus (Ffg . (v + y)) = ((Ff + Fg) . (v + y)) by BLTh13

        .= ((Ff . (v + y)) + (Fg . (v + y))) by HAHNBAN1:def 3

        .= (((Ff . v) + (Ff . y)) + (Fg . (v + y))) by A1

        .= (((Ff . v) + (Ff . y)) + ((Fg . v) + (Fg . y))) by A2

        .= ((((Ff . v) + (Fg . v)) + (Ff . y)) + (Fg . y))

        .= ((((Ff + Fg) . v) + (Ff . y)) + (Fg . y)) by HAHNBAN1:def 3

        .= (((Ff + Fg) . v) + ((Ff . y) + (Fg . y)))

        .= (((Ff + Fg) . v) + ((Ff + Fg) . y)) by HAHNBAN1:def 3

        .= ((Ffg . v) + ((Ff + Fg) . y)) by BLTh13

        .= ((Ffg . v) + (Ffg . y)) by BLTh13;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveSAF Form of V, W;

      let a be Element of INT.Ring ;

      cluster (a * f) -> additiveSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF ((a * f),w)), Ff = ( FunctionalSAF (f,w));

        let v,y be Vector of V;

        

         A1: Ff is additive;

        

        thus (Ffg . (v + y)) = ((a * Ff) . (v + y)) by BLTh14

        .= (a * (Ff . (v + y))) by HAHNBAN1:def 6

        .= (a * ((Ff . v) + (Ff . y))) by A1

        .= ((a * (Ff . v)) + (a * (Ff . y)))

        .= (((a * Ff) . v) + (a * (Ff . y))) by HAHNBAN1:def 6

        .= (((a * Ff) . v) + ((a * Ff) . y)) by HAHNBAN1:def 6

        .= ((Ffg . v) + ((a * Ff) . y)) by BLTh14

        .= ((Ffg . v) + (Ffg . y)) by BLTh14;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveFAF Form of V, W;

      let a be Element of INT.Ring ;

      cluster (a * f) -> additiveFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF ((a * f),w)), Ff = ( FunctionalFAF (f,w));

        let v,y be Vector of W;

        

         A1: Ff is additive;

        

        thus (Ffg . (v + y)) = ((a * Ff) . (v + y)) by BLTh15

        .= (a * (Ff . (v + y))) by HAHNBAN1:def 6

        .= (a * ((Ff . v) + (Ff . y))) by A1

        .= ((a * (Ff . v)) + (a * (Ff . y)))

        .= (((a * Ff) . v) + (a * (Ff . y))) by HAHNBAN1:def 6

        .= (((a * Ff) . v) + ((a * Ff) . y)) by HAHNBAN1:def 6

        .= ((Ffg . v) + ((a * Ff) . y)) by BLTh15

        .= ((Ffg . v) + (Ffg . y)) by BLTh15;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveSAF Form of V, W;

      cluster ( - f) -> additiveSAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveFAF Form of V, W;

      cluster ( - f) -> additiveFAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be additiveSAF Form of V, W;

      cluster (f - g) -> additiveSAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be additiveFAF Form of V, W;

      cluster (f - g) -> additiveFAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be homogeneousSAF Form of V, W;

      cluster (f + g) -> homogeneousSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF ((f + g),w)), Ff = ( FunctionalSAF (f,w));

        set Fg = ( FunctionalSAF (g,w));

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

        

        thus (Ffg . (a * v)) = ((Ff + Fg) . (a * v)) by BLTh12

        .= ((Ff . (a * v)) + (Fg . (a * v))) by HAHNBAN1:def 3

        .= ((a * (Ff . v)) + (Fg . (a * v))) by HAHNBAN1:def 8

        .= ((a * (Ff . v)) + (a * (Fg . v))) by HAHNBAN1:def 8

        .= (a * ((Ff . v) + (Fg . v)))

        .= (a * ((Ff + Fg) . v)) by HAHNBAN1:def 3

        .= (a * (Ffg . v)) by BLTh12;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be homogeneousFAF Form of V, W;

      cluster (f + g) -> homogeneousFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF ((f + g),w)), Ff = ( FunctionalFAF (f,w));

        set Fg = ( FunctionalFAF (g,w));

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

        

        thus (Ffg . (a * v)) = ((Ff + Fg) . (a * v)) by BLTh13

        .= ((Ff . (a * v)) + (Fg . (a * v))) by HAHNBAN1:def 3

        .= ((a * (Ff . v)) + (Fg . (a * v))) by HAHNBAN1:def 8

        .= ((a * (Ff . v)) + (a * (Fg . v))) by HAHNBAN1:def 8

        .= (a * ((Ff . v) + (Fg . v)))

        .= (a * ((Ff + Fg) . v)) by HAHNBAN1:def 3

        .= (a * (Ffg . v)) by BLTh13;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousSAF Form of V, W;

      let a be Element of INT.Ring ;

      cluster (a * f) -> homogeneousSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF ((a * f),w)), Ff = ( FunctionalSAF (f,w));

        let v be Vector of V, b be Element of INT.Ring ;

        

        thus (Ffg . (b * v)) = ((a * Ff) . (b * v)) by BLTh14

        .= (a * (Ff . (b * v))) by HAHNBAN1:def 6

        .= (a * (b * (Ff . v))) by HAHNBAN1:def 8

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

        .= (b * ((a * Ff) . v)) by HAHNBAN1:def 6

        .= (b * (Ffg . v)) by BLTh14;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousFAF Form of V, W;

      let a be Element of INT.Ring ;

      cluster (a * f) -> homogeneousFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF ((a * f),w)), Ff = ( FunctionalFAF (f,w));

        let v be Vector of W, b be Element of INT.Ring ;

        

        thus (Ffg . (b * v)) = ((a * Ff) . (b * v)) by BLTh15

        .= (a * (Ff . (b * v))) by HAHNBAN1:def 6

        .= (a * (b * (Ff . v))) by HAHNBAN1:def 8

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

        .= (b * ((a * Ff) . v)) by HAHNBAN1:def 6

        .= (b * (Ffg . v)) by BLTh15;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousSAF Form of V, W;

      cluster ( - f) -> homogeneousSAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousFAF Form of V, W;

      cluster ( - f) -> homogeneousFAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be homogeneousSAF Form of V, W;

      cluster (f - g) -> homogeneousSAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be homogeneousFAF Form of V, W;

      cluster (f - g) -> homogeneousFAF;

      correctness ;

    end

    theorem :: ZMATRLIN:85

    

     BLTh26: for V,W be non empty ModuleStr over INT.Ring , v,u be Vector of V, w be Vector of W, f be Form of V, W st f is additiveSAF holds (f . ((v + u),w)) = ((f . (v,w)) + (f . (u,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v,w be Vector of V, y be Vector of W, f be Form of V, W;

      set F = ( FunctionalSAF (f,y));

      assume f is additiveSAF;

      then

       A1: F is additive;

      

      thus (f . ((v + w),y)) = (F . (v + w)) by BLTh9

      .= ((F . v) + (F . w)) by A1

      .= ((f . (v,y)) + (F . w)) by BLTh9

      .= ((f . (v,y)) + (f . (w,y))) by BLTh9;

    end;

    theorem :: ZMATRLIN:86

    

     BLTh27: for V,W be non empty ModuleStr over INT.Ring , v be Vector of V, u,w be Vector of W, f be Form of V, W st f is additiveFAF holds (f . (v,(u + w))) = ((f . (v,u)) + (f . (v,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v be Vector of V, y,z be Vector of W, f be Form of V, W;

      set F = ( FunctionalFAF (f,v));

      assume f is additiveFAF;

      then

       A1: F is additive;

      

      thus (f . (v,(y + z))) = (F . (y + z)) by BLTh8

      .= ((F . y) + (F . z)) by A1

      .= ((f . (v,y)) + (F . z)) by BLTh8

      .= ((f . (v,y)) + (f . (v,z))) by BLTh8;

    end;

    theorem :: ZMATRLIN:87

    

     BLTh28: for V,W be non empty ModuleStr over INT.Ring , v,u be Vector of V, w,t be Vector of W, f be additiveSAF additiveFAF Form of V, W holds (f . ((v + u),(w + t))) = (((f . (v,w)) + (f . (v,t))) + ((f . (u,w)) + (f . (u,t))))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v,w be Vector of V, y,z be Vector of W, f be additiveSAF additiveFAF Form of V, W;

      set v1 = (f . (v,y)), v3 = (f . (v,z)), v4 = (f . (w,y)), v5 = (f . (w,z));

      

      thus (f . ((v + w),(y + z))) = ((f . (v,(y + z))) + (f . (w,(y + z)))) by BLTh26

      .= ((v1 + v3) + (f . (w,(y + z)))) by BLTh27

      .= ((v1 + v3) + (v4 + v5)) by BLTh27;

    end;

    theorem :: ZMATRLIN:88

    

     BLTh29: for V,W be right_zeroed non empty ModuleStr over INT.Ring , f be additiveFAF Form of V, W, v be Vector of V holds (f . (v,( 0. W))) = 0

    proof

      let V,W be right_zeroed non empty ModuleStr over INT.Ring ;

      let f be additiveFAF Form of V, W, v be Vector of V;

      (f . (v,( 0. W))) = (f . (v,(( 0. W) + ( 0. W)))) by RLVECT_1:def 4

      .= ((f . (v,( 0. W))) + (f . (v,( 0. W)))) by BLTh27;

      hence thesis;

    end;

    theorem :: ZMATRLIN:89

    

     BLTh30: for V,W be right_zeroed non empty ModuleStr over INT.Ring , f be additiveSAF Form of V, W, w be Vector of W holds (f . (( 0. V),w)) = 0

    proof

      let V,W be right_zeroed non empty ModuleStr over INT.Ring ;

      let f be additiveSAF Form of V, W, v be Vector of W;

      (f . (( 0. V),v)) = (f . ((( 0. V) + ( 0. V)),v)) by RLVECT_1:def 4

      .= ((f . (( 0. V),v)) + (f . (( 0. V),v))) by BLTh26;

      hence thesis;

    end;

    theorem :: ZMATRLIN:90

    

     BLTh31: for V,W be non empty ModuleStr over INT.Ring , v be Vector of V, w be Vector of W, a be Element of INT.Ring , f be Form of V, W st f is homogeneousSAF holds (f . ((a * v),w)) = (a * (f . (v,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v be Vector of V, y be Vector of W, r be Element of INT.Ring , f be Form of V, W;

      set F = ( FunctionalSAF (f,y));

      assume f is homogeneousSAF;

      then

       A1: F is homogeneous;

      

      thus (f . ((r * v),y)) = (F . (r * v)) by BLTh9

      .= (r * (F . v)) by A1

      .= (r * (f . (v,y))) by BLTh9;

    end;

    theorem :: ZMATRLIN:91

    

     BLTh32: for V,W be non empty ModuleStr over INT.Ring , v be Vector of V, w be Vector of W, a be Element of INT.Ring , f be Form of V, W st f is homogeneousFAF holds (f . (v,(a * w))) = (a * (f . (v,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v be Vector of V, y be Vector of W, r be Element of INT.Ring , f be Form of V, W;

      set F = ( FunctionalFAF (f,v));

      assume f is homogeneousFAF;

      then

       A1: F is homogeneous;

      

      thus (f . (v,(r * y))) = (F . (r * y)) by BLTh8

      .= (r * (F . y)) by A1

      .= (r * (f . (v,y))) by BLTh8;

    end;

    theorem :: ZMATRLIN:92

    for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , f be homogeneousSAF Form of V, W, w be Vector of W holds (f . (( 0. V),w)) = ( 0. INT.Ring )

    proof

      let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring ;

      let f be homogeneousSAF Form of V, W, v be Vector of W;

      (( 0. INT.Ring ) * ( 0. V)) = ( 0. V) by VS10Th1;

      

      hence (f . (( 0. V),v)) = (( 0. INT.Ring ) * (f . (( 0. V),v))) by BLTh31

      .= ( 0. INT.Ring );

    end;

    theorem :: ZMATRLIN:93

    for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , f be homogeneousFAF Form of V, W, v be Vector of V holds (f . (v,( 0. W))) = ( 0. INT.Ring )

    proof

      let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring ;

      let f be homogeneousFAF Form of V, W, v be Vector of V;

      (( 0. INT.Ring ) * ( 0. W)) = ( 0. W) by VS10Th1;

      

      hence (f . (v,( 0. W))) = (( 0. INT.Ring ) * (f . (v,( 0. W)))) by BLTh32

      .= ( 0. INT.Ring );

    end;

    theorem :: ZMATRLIN:94

    

     BLTh35: for V,W be Z_Module, v,u be Vector of V, w be Vector of W, f be additiveSAF homogeneousSAF Form of V, W holds (f . ((v - u),w)) = ((f . (v,w)) - (f . (u,w)))

    proof

      let V,W be Z_Module, v,w be Vector of V, y be Vector of W;

      let f be additiveSAF homogeneousSAF Form of V, W;

      

      thus (f . ((v - w),y)) = ((f . (v,y)) + (f . (( - w),y))) by BLTh26

      .= ((f . (v,y)) + (f . ((( - ( 1. INT.Ring )) * w),y))) by ZMODUL01: 2

      .= ((f . (v,y)) + (( - ( 1. INT.Ring )) * (f . (w,y)))) by BLTh31

      .= ((f . (v,y)) - (f . (w,y)));

    end;

    theorem :: ZMATRLIN:95

    

     BLTh36: for V,W be Z_Module, v be Vector of V, w,t be Vector of W, f be additiveFAF homogeneousFAF Form of V, W holds (f . (v,(w - t))) = ((f . (v,w)) - (f . (v,t)))

    proof

      let V,W be Z_Module, v be Vector of V, y,z be Vector of W, f be additiveFAF homogeneousFAF Form of V, W;

      

      thus (f . (v,(y - z))) = ((f . (v,y)) + (f . (v,( - z)))) by BLTh27

      .= ((f . (v,y)) + (f . (v,(( - ( 1. INT.Ring )) * z)))) by ZMODUL01: 2

      .= ((f . (v,y)) + (( - ( 1. INT.Ring )) * (f . (v,z)))) by BLTh32

      .= ((f . (v,y)) - (f . (v,z)));

    end;

    theorem :: ZMATRLIN:96

    

     BLTh37: for V,W be Z_Module, v,u be Vector of V, w,t be Vector of W, f be bilinear-Form of V, W holds (f . ((v - u),(w - t))) = (((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t))))

    proof

      let V,W be Z_Module;

      let v,w be Vector of V, y,z be Vector of W, f be bilinear-Form of V, W;

      set v1 = (f . (v,y)), v3 = (f . (v,z)), v4 = (f . (w,y)), v5 = (f . (w,z));

      

      thus (f . ((v - w),(y - z))) = ((f . (v,(y - z))) - (f . (w,(y - z)))) by BLTh35

      .= ((v1 - v3) - (f . (w,(y - z)))) by BLTh36

      .= ((v1 - v3) - (v4 - v5)) by BLTh36;

    end;

    theorem :: ZMATRLIN:97

    for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , v,u be Vector of V, w,t be Vector of W, a,b be Element of INT.Ring , f be bilinear-Form of V, W holds (f . ((v + (a * u)),(w + (b * t)))) = (((f . (v,w)) + (b * (f . (v,t)))) + ((a * (f . (u,w))) + (a * (b * (f . (u,t))))))

    proof

      let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , v,w be Vector of V, y,z be Vector of W, a,b be Element of INT.Ring ;

      let f be bilinear-Form of V, W;

      set v1 = (f . (v,y)), v3 = (f . (v,z)), v4 = (f . (w,y)), v5 = (f . (w,z));

      

      thus (f . ((v + (a * w)),(y + (b * z)))) = ((v1 + (f . (v,(b * z)))) + ((f . ((a * w),y)) + (f . ((a * w),(b * z))))) by BLTh28

      .= ((v1 + (b * v3)) + ((f . ((a * w),y)) + (f . ((a * w),(b * z))))) by BLTh32

      .= ((v1 + (b * v3)) + ((a * v4) + (f . ((a * w),(b * z))))) by BLTh31

      .= ((v1 + (b * v3)) + ((a * v4) + (a * (f . (w,(b * z)))))) by BLTh31

      .= ((v1 + (b * v3)) + ((a * v4) + (a * (b * v5)))) by BLTh32;

    end;

    theorem :: ZMATRLIN:98

    for V,W be Z_Module, v,u be Vector of V, w,t be Vector of W, a,b be Element of INT.Ring , f be bilinear-Form of V, W holds (f . ((v - (a * u)),(w - (b * t)))) = (((f . (v,w)) - (b * (f . (v,t)))) - ((a * (f . (u,w))) - (a * (b * (f . (u,t))))))

    proof

      let V,W be Z_Module, v,w be Vector of V, y,z be Vector of W, a,b be Element of INT.Ring , f be bilinear-Form of V, W;

      set v1 = (f . (v,y)), v3 = (f . (v,z)), v4 = (f . (w,y)), v5 = (f . (w,z));

      

      thus (f . ((v - (a * w)),(y - (b * z)))) = ((v1 - (f . (v,(b * z)))) - ((f . ((a * w),y)) - (f . ((a * w),(b * z))))) by BLTh37

      .= ((v1 - (b * v3)) - ((f . ((a * w),y)) - (f . ((a * w),(b * z))))) by BLTh32

      .= ((v1 - (b * v3)) - ((a * v4) - (f . ((a * w),(b * z))))) by BLTh31

      .= ((v1 - (b * v3)) - ((a * v4) - (a * (f . (w,(b * z)))))) by BLTh31

      .= ((v1 - (b * v3)) - ((a * v4) - (a * (b * v5)))) by BLTh32;

    end;

    theorem :: ZMATRLIN:99

    for V,W be right_zeroed non empty ModuleStr over INT.Ring , f be Form of V, W st f is additiveFAF or f is additiveSAF holds f is constant iff for v be Vector of V, w be Vector of W holds (f . (v,w)) = 0

    proof

      let V,W be right_zeroed non empty ModuleStr over INT.Ring , f be Form of V, W;

      

       A1: ( dom f) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

      assume

       A2: f is additiveFAF or f is additiveSAF;

      hereby

        assume

         A3: f is constant;

        let v be Vector of V, w be Vector of W;

        per cases by A2;

          suppose

           A4: f is additiveFAF;

          

          thus (f . (v,w)) = (f . (v,( 0. W))) by A1, A3, BINOP_1: 19

          .= 0 by A4, BLTh29;

        end;

          suppose

           A5: f is additiveSAF;

          

          thus (f . (v,w)) = (f . (( 0. V),w)) by A1, A3, BINOP_1: 19

          .= 0 by A5, BLTh30;

        end;

      end;

      hereby

        assume

         A6: for v be Vector of V, w be Vector of W holds (f . (v,w)) = 0 ;

        now

          let x,y be object such that

           A7: x in ( dom f) and

           A8: y in ( dom f);

          consider v be Vector of V, w be Vector of W such that

           A9: x = [v, w] by A7, DOMAIN_1: 1;

          consider s be Vector of V, t be Vector of W such that

           A10: y = [s, t] by A8, DOMAIN_1: 1;

          

          thus (f . x) = (f . (v,w)) by A9

          .= 0 by A6

          .= (f . (s,t)) by A6

          .= (f . y) by A10;

        end;

        hence f is constant;

      end;

    end;

    begin

    definition

      let V1,V2 be finite-rank free Z_Module;

      let b1 be OrdBasis of V1, b2 be OrdBasis of V2;

      let f be bilinear-Form of V1, V2;

      :: ZMATRLIN:def26

      func BilinearM (f,b1,b2) -> Matrix of ( len b1), ( len b2), INT.Ring means

      : defBilinearM: for i,j be Nat st i in ( dom b1) & j in ( dom b2) holds (it * (i,j)) = (f . ((b1 /. i),(b2 /. j)));

      existence

      proof

        deffunc F( Nat, Nat) = ( In ((f . ((b1 /. $1),(b2 /. $2))),the carrier of INT.Ring ));

        consider M be Matrix of ( len b1), ( len b2), INT.Ring such that

         A20: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        take M;

        thus for i,j be Nat st i in ( dom b1) & j in ( dom b2) holds (M * (i,j)) = (f . ((b1 /. i),(b2 /. j)))

        proof

          let i,j be Nat;

          assume

           A21: i in ( dom b1) & j in ( dom b2);

          ( len b1) <> 0

          proof

            assume ( len b1) = 0 ;

            then ( Seg ( len b1)) = {} ;

            hence contradiction by A21, FINSEQ_1:def 3;

          end;

          

          then ( Indices M) = [:( Seg ( len b1)), ( Seg ( len b2)):] by MATRIX_0: 23

          .= [:( dom b1), ( Seg ( len b2)):] by FINSEQ_1:def 3

          .= [:( dom b1), ( dom b2):] by FINSEQ_1:def 3;

          then [i, j] in ( Indices M) by A21, ZFMISC_1: 87;

          then (M * (i,j)) = F(i,j) by A20;

          hence (M * (i,j)) = (f . ((b1 /. i),(b2 /. j)));

        end;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of ( len b1), ( len b2), INT.Ring ;

        assume that

         A22: for i,j be Nat st i in ( dom b1) & j in ( dom b2) holds (M1 * (i,j)) = (f . ((b1 /. i),(b2 /. j))) and

         A23: for i,j be Nat st i in ( dom b1) & j in ( dom b2) holds (M2 * (i,j)) = (f . ((b1 /. i),(b2 /. j)));

        now

          let i, j;

          assume

           A25: [i, j] in ( Indices M1);

          then ( len b1) <> 0 by MATRIX_0: 22;

          

          then ( Indices M1) = [:( Seg ( len b1)), ( Seg ( len b2)):] by MATRIX_0: 23

          .= [:( dom b1), ( Seg ( len b2)):] by FINSEQ_1:def 3

          .= [:( dom b1), ( dom b2):] by FINSEQ_1:def 3;

          then

           A26: i in ( dom b1) & j in ( dom b2) by A25, ZFMISC_1: 87;

          

          thus (M1 * (i,j)) = (f . ((b1 /. i),(b2 /. j))) by A22, A26

          .= (M2 * (i,j)) by A26, A23;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    theorem :: ZMATRLIN:100

    for V be finite-rank free Z_Module, i be Nat, a1 be Element of INT.Ring , a2 be Element of V, p1 be FinSequence of INT.Ring , p2 be FinSequence of V st i in ( dom ( lmlt (p1,p2))) & a1 = (p1 . i) & a2 = (p2 . i) holds (( lmlt (p1,p2)) . i) = (a1 * a2) by FUNCOP_1: 22;

    theorem :: ZMATRLIN:101

    

     LMThMBF1X0: for V be finite-rank free Z_Module, F be linear-Functional of V, y be FinSequence of V, x be FinSequence of INT.Ring , X,Y be FinSequence of INT.Ring st X = x & ( len y) = ( len x) & ( len X) = ( len Y) & (for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . (y /. k))) holds (X "*" Y) = (F . ( Sum ( lmlt (x,y))))

    proof

      let V be finite-rank free Z_Module, F be linear-Functional of V;

      defpred P[ FinSequence of V] means for x be FinSequence of INT.Ring , X,Y be FinSequence of INT.Ring st X = x & ( len $1) = ( len x) & ( len X) = ( len Y) & (for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . ($1 /. k))) holds (X "*" Y) = (F . ( Sum ( lmlt (x,$1))));

      

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

      proof

        let y be FinSequence of V;

        let w be Element of V such that

         P1: for x be FinSequence of INT.Ring , X,Y be FinSequence of INT.Ring st X = x & ( len y) = ( len x) & ( len X) = ( len Y) & (for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . (y /. k))) holds (X "*" Y) = (F . ( Sum ( lmlt (x,y))));

        thus for x be FinSequence of INT.Ring , X,Y be FinSequence of INT.Ring st X = x & ( len (y ^ <*w*>)) = ( len x) & ( len X) = ( len Y) & (for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . ((y ^ <*w*>) /. k))) holds (X "*" Y) = (F . ( Sum ( lmlt (x,(y ^ <*w*>)))))

        proof

          let x be FinSequence of INT.Ring , X,Y be FinSequence of INT.Ring ;

          assume that

           R1: X = x and

           R2: ( len (y ^ <*w*>)) = ( len x) and

           R3: ( len X) = ( len Y) and

           R4: for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . ((y ^ <*w*>) /. k));

          

           X1: F is additive;

          

           X2: F is homogeneous;

          set n = ( len y);

          set X0 = (X | n);

          set Y0 = (Y | n);

          set x0 = (x | n);

          

           Q0: ( len (y ^ <*w*>)) = (( len y) + ( len <*w*>)) by FINSEQ_1: 22

          .= (n + 1) by FINSEQ_1: 39;

          

           LN4: ( len x0) = n by Q0, R2, FINSEQ_1: 59, NAT_1: 11;

          

           LN5: ( len X0) = n by Q0, R1, R2, FINSEQ_1: 59, NAT_1: 11;

          

           LN6: ( len Y0) = n by Q0, R1, R2, R3, FINSEQ_1: 59, NAT_1: 11;

          

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

          

           W1: X0 = (X | ( Seg n)) by FINSEQ_1:def 15;

          

           W2: Y0 = (Y | ( Seg n)) by FINSEQ_1:def 15;

          

           W3: x0 = (x | ( Seg n)) by FINSEQ_1:def 15;

          

           Q2: ( len y) = ( len x0) by Q0, R2, FINSEQ_1: 59, NAT_1: 11;

          

           Q3: ( len X0) = ( len Y0) by LN5, Q0, R1, R2, R3, FINSEQ_1: 59, NAT_1: 11;

          for k be Nat st k in ( Seg ( len x0)) holds (Y0 . k) = (F . (y /. k))

          proof

            let k be Nat;

            assume

             Q31: k in ( Seg ( len x0));

            then

             Q34: k in ( dom y) by LN4, FINSEQ_1:def 3;

            

             Q32: ( Seg ( len x0)) c= ( Seg ( len x)) by FINSEQ_3: 18, Q0, R2, LN4;

            then k in ( Seg ( len x)) by Q31;

            then

             Q33: k in ( dom (y ^ <*w*>)) by R2, FINSEQ_1:def 3;

            

             Q35: ((y ^ <*w*>) /. k) = ((y ^ <*w*>) . k) by Q33, PARTFUN1:def 6

            .= (y . k) by FINSEQ_1:def 7, Q34

            .= (y /. k) by Q34, PARTFUN1:def 6;

            

            thus (Y0 . k) = (Y . k) by W2, LN4, Q31, FUNCT_1: 49

            .= (F . (y /. k)) by R4, Q31, Q32, Q35;

          end;

          then

           Q4: (X0 "*" Y0) = (F . ( Sum ( lmlt (x0,y)))) by R1, Q2, Q3, P1;

          

           Q51: (n + 1) in ( dom X) by LN7, Q0, R1, R2, FINSEQ_1:def 3;

          

           Q61: (n + 1) in ( dom Y) by LN7, Q0, R1, R2, R3, FINSEQ_1:def 3;

          

           Q71: (n + 1) in ( dom x) by LN7, Q0, R2, FINSEQ_1:def 3;

          

           Q9: (X /. (n + 1)) = (X . (n + 1)) by Q51, PARTFUN1:def 6

          .= (x /. (n + 1)) by R1, Q71, PARTFUN1:def 6;

          

           Q103: (n + 1) in ( dom (y ^ <*w*>)) by LN7, Q0, FINSEQ_1:def 3;

          

           Q102: ((y ^ <*w*>) /. (n + 1)) = ((y ^ <*w*>) . (n + 1)) by Q103, PARTFUN1:def 6

          .= w by FINSEQ_1: 42;

          (Y /. (n + 1)) = (Y . (n + 1)) by Q61, PARTFUN1:def 6

          .= (F . w) by Q0, Q102, R2, R4, FINSEQ_1: 4;

          

          then

           Q11: ((X /. (n + 1)) * (Y /. (n + 1))) = ((x /. (n + 1)) * (F . w)) by Q9

          .= (F . ((x /. (n + 1)) * w)) by X2;

          ( len ( mlt (X,Y))) = (n + 1) by Q0, R1, R2, R3, MATRIX_3: 6;

          then

           Q85: ( dom ( mlt (X,Y))) = ( Seg (n + 1)) by FINSEQ_1:def 3;

          

           Q82: ( len ( mlt (X0,Y0))) = n by LN5, LN6, MATRIX_3: 6;

          

           Q88: ( len (( mlt (X0,Y0)) ^ <*((X /. (n + 1)) * (Y /. (n + 1)))*>)) = (( len ( mlt (X0,Y0))) + ( len <*((X /. (n + 1)) * (Y /. (n + 1)))*>)) by FINSEQ_1: 22

          .= (n + 1) by Q82, FINSEQ_1: 39;

          for k be Nat st k in ( dom ( mlt (X,Y))) holds (( mlt (X,Y)) . k) = ((( mlt (X0,Y0)) ^ <*((X /. (n + 1)) * (Y /. (n + 1)))*>) . k)

          proof

            let k be Nat;

            assume

             V1: k in ( dom ( mlt (X,Y)));

            then

             V2: 1 <= k & k <= (n + 1) by Q85, FINSEQ_1: 1;

            set f = (( mlt (X0,Y0)) ^ <*((X /. (n + 1)) * (Y /. (n + 1)))*>);

            per cases ;

              suppose k <= n;

              then

               V3: k in ( Seg n) by FINSEQ_1: 1, V2;

              then

               V4: k in ( dom ( mlt (X0,Y0))) by Q82, FINSEQ_1:def 3;

              

               V5: k in ( dom X0) by LN5, V3, FINSEQ_1:def 3;

              

               V6: k in ( dom Y0) by LN6, V3, FINSEQ_1:def 3;

              (X0 . k) in ( rng X0) by V5, FUNCT_1: 3;

              then

              reconsider X0k = (X0 . k) as Element of INT.Ring ;

              (Y0 . k) in ( rng Y0) by V6, FUNCT_1: 3;

              then

              reconsider Y0k = (Y0 . k) as Element of INT.Ring ;

              k in ( dom X) by V1, Q0, Q85, R1, R2, FINSEQ_1:def 3;

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

              then

              reconsider Xk = (X . k) as Element of INT.Ring ;

              k in ( dom Y) by V1, Q0, Q85, R1, R2, R3, FINSEQ_1:def 3;

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

              then

              reconsider Yk = (Y . k) as Element of INT.Ring ;

              (f . k) = (( mlt (X0,Y0)) . k) by V4, FINSEQ_1:def 7

              .= (X0k * Y0k) by V4, FVSUM_1: 60

              .= ((X . k) * (Y0 . k)) by W1, V5, FUNCT_1: 47

              .= (Xk * Yk) by W2, V6, FUNCT_1: 47

              .= (( mlt (X,Y)) . k) by V1, FVSUM_1: 60;

              hence thesis;

            end;

              suppose not k <= n;

              then (n + 1) <= k by NAT_1: 13;

              then

               V8: k = (n + 1) by XXREAL_0: 1, V2;

              ( Seg 1) = ( dom <*((X /. (n + 1)) * (Y /. (n + 1)))*>) by FINSEQ_1: 38;

              then

               V10: 1 in ( dom <*((X /. (n + 1)) * (Y /. (n + 1)))*>) by FINSEQ_1: 3;

              

               Q9: (X /. (n + 1)) = (X . (n + 1)) by Q51, PARTFUN1:def 6;

              then

              reconsider Xn = (X . (n + 1)) as Element of INT.Ring ;

              

               Q10: (Y /. (n + 1)) = (Y . (n + 1)) by Q61, PARTFUN1:def 6;

              then

              reconsider Yn = (Y . (n + 1)) as Element of INT.Ring ;

              (f . k) = ( <*((X /. (n + 1)) * (Y /. (n + 1)))*> . 1) by Q82, FINSEQ_1:def 7, V8, V10

              .= ((X /. (n + 1)) * (Y /. (n + 1))) by FINSEQ_1: 40

              .= (( mlt (X,Y)) . k) by Q9, Q10, V1, V8, FVSUM_1: 60;

              hence thesis;

            end;

          end;

          then

           Q8: ( mlt (X,Y)) = (( mlt (X0,Y0)) ^ <*((X /. (n + 1)) * (Y /. (n + 1)))*>) by Q85, Q88, FINSEQ_1:def 3;

          

           QX121: ( dom x) = ( Seg (n + 1)) by Q0, R2, FINSEQ_1:def 3

          .= ( dom (y ^ <*w*>)) by Q0, FINSEQ_1:def 3;

          then

           Q121: ( dom ( lmlt (x,(y ^ <*w*>)))) = ( dom x) by Th12;

          ( dom x0) = ( Seg n) by FINSEQ_1:def 3, LN4

          .= ( dom y) by FINSEQ_1:def 3;

          then ( dom ( lmlt (x0,y))) = ( dom x0) by Th12;

          then

           Q124: ( dom ( lmlt (x0,y))) = ( Seg n) by LN4, FINSEQ_1:def 3;

          then

           Q125: ( len ( lmlt (x0,y))) = n by FINSEQ_1:def 3;

          ( len (( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>)) = (( len ( lmlt (x0,y))) + ( len <*((x /. (n + 1)) * w)*>)) by FINSEQ_1: 22

          .= (n + 1) by Q125, FINSEQ_1: 39;

          then

           Q126: ( dom (( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>)) = ( Seg (n + 1)) by FINSEQ_1:def 3;

          for k be Nat st k in ( dom ( lmlt (x,(y ^ <*w*>)))) holds (( lmlt (x,(y ^ <*w*>))) . k) = ((( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>) . k)

          proof

            let k be Nat;

            assume

             V1: k in ( dom ( lmlt (x,(y ^ <*w*>))));

            then

             V0: k in ( Seg (n + 1)) by Q121, Q0, R2, FINSEQ_1:def 3;

            then

             V2: 1 <= k & k <= (n + 1) by FINSEQ_1: 1;

            set f = (( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>);

            per cases ;

              suppose

               VX3: k <= n;

              then

               V3: k in ( Seg n) by V2, FINSEQ_1: 1;

              

               V5: k in ( dom x0) by V3, LN4, FINSEQ_1:def 3;

              

               V6: k in ( dom y) by V3, FINSEQ_1:def 3;

              

               XX1: (x0 . k) in ( rng x0) by V5, FUNCT_1: 3;

              reconsider x0k = (x0 . k) as Element of INT.Ring by XX1;

              (y . k) in ( rng y) by V6, FUNCT_1: 3;

              then

              reconsider y0k = (y . k) as Element of V;

              k in ( dom x) by V1, QX121, Th12;

              then

               XX2: (x . k) in ( rng x) by FUNCT_1: 3;

              reconsider xk = (x . k) as Element of INT.Ring by XX2;

              k in ( dom (y ^ <*w*>)) by V0, Q0, FINSEQ_1:def 3;

              then ((y ^ <*w*>) . k) in ( rng (y ^ <*w*>)) by FUNCT_1: 3;

              then

              reconsider yk = ((y ^ <*w*>) . k) as Element of V;

              

               W: y0k = ((y ^ <*w*>) . k) by FINSEQ_1:def 7, V6

              .= yk;

              (f . k) = (( lmlt (x0,y)) . k) by V3, Q124, FINSEQ_1:def 7

              .= (x0k * y0k) by V2, VX3, Q124, FUNCOP_1: 22, FINSEQ_1: 1

              .= (xk * y0k) by V5, W3, FUNCT_1: 47

              .= (( lmlt (x,(y ^ <*w*>))) . k) by W, V1, FUNCOP_1: 22;

              hence thesis;

            end;

              suppose not k <= n;

              then (n + 1) <= k by NAT_1: 13;

              then

               V8: k = (n + 1) by XXREAL_0: 1, V2;

              ( Seg 1) = ( dom <*((x /. (n + 1)) * w)*>) by FINSEQ_1: 38;

              then

               V10: 1 in ( dom <*((x /. (n + 1)) * w)*>) by FINSEQ_1: 3;

              ( Seg 1) = ( dom <*w*>) by FINSEQ_1: 38;

              then

               V11: 1 in ( dom <*w*>) by FINSEQ_1: 3;

              

               Q9: (x /. (n + 1)) = (x . (n + 1)) by Q71, PARTFUN1:def 6;

              then

              reconsider xn = (x . (n + 1)) as Element of INT.Ring ;

              ((y ^ <*w*>) /. (n + 1)) = ((y ^ <*w*>) . (n + 1)) by Q103, PARTFUN1:def 6;

              then

              reconsider yn = ((y ^ <*w*>) . (n + 1)) as Element of V;

              

               Q11: ((y ^ <*w*>) . (n + 1)) = ( <*w*> . 1) by V11, FINSEQ_1:def 7

              .= w by FINSEQ_1: 40;

              (f . k) = ( <*((x /. (n + 1)) * w)*> . 1) by Q125, V8, V10, FINSEQ_1:def 7

              .= (xn * w) by Q9, FINSEQ_1: 40

              .= (( lmlt (x,(y ^ <*w*>))) . k) by Q11, V1, V8, FUNCOP_1: 22;

              hence thesis;

            end;

          end;

          then

           Q12: ( lmlt (x,(y ^ <*w*>))) = (( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>) by Q0, Q121, Q126, R2, FINSEQ_1:def 3;

          

          thus (X "*" Y) = (( Sum ( mlt (X0,Y0))) + ((X /. (n + 1)) * (Y /. (n + 1)))) by FVSUM_1: 71, Q8

          .= (F . (( Sum ( lmlt (x0,y))) + ((x /. (n + 1)) * w))) by Q4, Q11, X1

          .= (F . ( Sum ( lmlt (x,(y ^ <*w*>))))) by FVSUM_1: 71, Q12;

        end;

      end;

      

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

      proof

        let x be FinSequence of INT.Ring , X,Y be FinSequence of INT.Ring ;

        assume that

         R1: X = x and

         R2: ( len ( <*> the carrier of V)) = ( len x) and ( len X) = ( len Y) and for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . (( <*> the carrier of V) /. k));

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

        

         Q2: X = ( <*> the carrier of INT.Ring ) by R1, R2;

        

         Q4: ( mlt (X,Y)) = (the multF of INT.Ring * <:X, Y:>) by FUNCOP_1:def 3

        .= ( <*> the carrier of INT.Ring ) by Q2;

        

         Q5: ( lmlt (x,y)) = (the lmult of V * <:x, y:>) by FUNCOP_1:def 3

        .= ( <*> the carrier of V);

        reconsider I0 = 0 as Element of INT.Ring ;

        

         X1: F is additive;

        

         X2: (F . ( 0. V)) = (F . (( 0. V) + ( 0. V)))

        .= ((F . ( 0. V)) + (F . ( 0. V))) by X1;

        

        thus (X "*" Y) = ( 0. INT.Ring ) by Q4, RLVECT_1: 43

        .= (F . ( Sum ( lmlt (x,y)))) by Q5, X2, RLVECT_1: 43;

      end;

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

      hence thesis;

    end;

    theorem :: ZMATRLIN:102

    

     LMThMBF1X: for V1,V2 be finite-rank free Z_Module, b2 be OrdBasis of V2, b3 be OrdBasis of V2, f be bilinear-Form of V1, V2, v1 be Vector of V1, v2 be Vector of V2, X,Y be FinSequence of INT.Ring st ( len X) = ( len b2) & ( len Y) = ( len b2) & (for k be Nat st k in ( Seg ( len b2)) holds (Y . k) = (f . (v1,(b2 /. k)))) & X = (v2 |-- b2) holds (Y "*" X) = (f . (v1,v2))

    proof

      let V1,V2 be finite-rank free Z_Module, b2 be OrdBasis of V2, b3 be OrdBasis of V2, f be bilinear-Form of V1, V2, v1 be Vector of V1, v2 be Vector of V2, X,Y be FinSequence of INT.Ring ;

      assume that

       A1: ( len X) = ( len b2) and

       A2: ( len Y) = ( len b2) and

       A3: (for k be Nat st k in ( Seg ( len b2)) holds (Y . k) = (f . (v1,(b2 /. k)))) and

       A4: X = (v2 |-- b2);

      set x = (v2 |-- b2);

      

       P2: for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (( FunctionalFAF (f,v1)) . (b2 /. k))

      proof

        let k be Nat;

        assume k in ( Seg ( len x));

        then (Y . k) = (f . (v1,(b2 /. k))) by A1, A3, A4;

        hence (Y . k) = (( FunctionalFAF (f,v1)) . (b2 /. k)) by BLTh8;

      end;

      

      thus (Y "*" X) = (X "*" Y) by FVSUM_1: 90

      .= (( FunctionalFAF (f,v1)) . ( Sum ( lmlt ((v2 |-- b2),b2)))) by LMThMBF1X0, A1, A2, A4, P2

      .= (f . (v1,( Sum ( lmlt ((v2 |-- b2),b2))))) by BLTh8

      .= (f . (v1,v2)) by Th35;

    end;

    theorem :: ZMATRLIN:103

    

     LMThMBF1Y: for V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, f be bilinear-Form of V1, V2, v1 be Vector of V1, v2 be Vector of V2, X,Y be FinSequence of INT.Ring st ( len X) = ( len b1) & ( len Y) = ( len b1) & (for k be Nat st k in ( Seg ( len b1)) holds (Y . k) = (f . ((b1 /. k),v2))) & X = (v1 |-- b1) holds (X "*" Y) = (f . (v1,v2))

    proof

      let V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, f be bilinear-Form of V1, V2, v1 be Vector of V1, v2 be Vector of V2, X,Y be FinSequence of INT.Ring ;

      assume that

       A1: ( len X) = ( len b1) and

       A2: ( len Y) = ( len b1) and

       A3: for k be Nat st k in ( Seg ( len b1)) holds (Y . k) = (f . ((b1 /. k),v2)) and

       A4: X = (v1 |-- b1);

      set x = (v1 |-- b1);

      

       P2: for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (( FunctionalSAF (f,v2)) . (b1 /. k))

      proof

        let k be Nat;

        assume k in ( Seg ( len x));

        then (Y . k) = (f . ((b1 /. k),v2)) by A1, A3, A4;

        hence (Y . k) = (( FunctionalSAF (f,v2)) . (b1 /. k)) by BLTh9;

      end;

      

      thus (X "*" Y) = (( FunctionalSAF (f,v2)) . ( Sum ( lmlt ((v1 |-- b1),b1)))) by LMThMBF1X0, A1, A2, A4, P2

      .= (f . (( Sum ( lmlt ((v1 |-- b1),b1))),v2)) by BLTh9

      .= (f . (v1,v2)) by Th35;

    end;

    theorem :: ZMATRLIN:104

    

     ThMBF1: for V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V2, f be bilinear-Form of V1, V2 st 0 < ( rank V1) holds ( BilinearM (f,b1,b3)) = (( BilinearM (f,b1,b2)) * (( AutMt (( id V2),b3,b2)) @ ))

    proof

      let V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V2, f be bilinear-Form of V1, V2;

      assume

       AS: 0 < ( rank V1);

      set n = ( len b2);

      

       A2: ( len b2) = ( rank V2) by ThRank1;

      

       A3: ( len b3) = ( rank V2) by ThRank1;

      reconsider IM1 = ( AutMt (( id V2),b3,b2)) as Matrix of n, INT.Ring by LMThMBF3, A2;

      reconsider M1 = (IM1 @ ) as Matrix of n, INT.Ring ;

      set M2 = (( BilinearM (f,b1,b2)) * M1);

      

       B1: ( len M1) = n & ( width M1) = n & ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       F1: ( len IM1) = n & ( width IM1) = n & ( Indices IM1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       B2: 0 < ( len b1) by AS, ThRank1;

      then

       B3: ( len ( BilinearM (f,b1,b2))) = ( len b1) & ( width ( BilinearM (f,b1,b2))) = ( len b2) by MATRIX_0: 23;

      

       C1: ( width ( BilinearM (f,b1,b2))) = ( len M1) by B1, B2, MATRIX_0: 23;

      ( len M2) = ( len b1) & ( width M2) = n by B1, B3, MATRIX_3:def 4;

      then

      reconsider M2 as Matrix of ( len b1), n, INT.Ring by B2, MATRIX_0: 20;

      set FM1 = M1;

      set FBM = ( BilinearM (f,b1,b2));

      for i,j be Nat st [i, j] in ( Indices ( BilinearM (f,b1,b3))) holds (( BilinearM (f,b1,b3)) * (i,j)) = (M2 * (i,j))

      proof

        let i,j be Nat;

        assume [i, j] in ( Indices ( BilinearM (f,b1,b3)));

        then

         B6: [i, j] in [:( Seg ( len b1)), ( Seg ( len b3)):] by B2, MATRIX_0: 23;

        then

         B7: i in ( Seg ( len b1)) & j in ( Seg ( len b3)) by ZFMISC_1: 87;

        then

         B8: i in ( dom b1) & j in ( dom b3) by FINSEQ_1:def 3;

        then

         B9: (( BilinearM (f,b1,b3)) * (i,j)) = (f . ((b1 /. i),(b3 /. j))) by defBilinearM;

         [i, j] in ( Indices M2) by B2, B6, A2, A3, MATRIX_0: 23;

        then

         B11: (M2 * (i,j)) = (( Line (FBM,i)) "*" ( Col (FM1,j))) by C1, MATRIX_3:def 4;

        

         B12: ( len ( Line (FBM,i))) = ( len b2) by B3, MATRIX_0:def 7;

         B13:

        now

          let k be Nat;

          assume

           B131: k in ( Seg ( len b2));

          then

           B132: k in ( Seg ( width FBM)) by B2, MATRIX_0: 23;

          

           B81: k in ( dom b2) by FINSEQ_1:def 3, B131;

          

          thus (( Line (FBM,i)) . k) = (FBM * (i,k)) by B132, MATRIX_0:def 7

          .= (f . ((b1 /. i),(b2 /. k))) by B8, B81, defBilinearM;

        end;

        

         B14: ( len ( Col (FM1,j))) = ( len b2) by B1, MATRIX_0:def 8;

        

         B135: j in ( Seg n) by B6, A2, A3, ZFMISC_1: 87;

         B15:

        now

          let k be Nat;

          assume 1 <= k & k <= ( len ( Col (FM1,j)));

          then

           B131: k in ( Seg ( len b2)) by FINSEQ_1: 1, B14;

          then

           B132: k in ( dom FM1) by B1, FINSEQ_1:def 3;

          

           B132A: j in ( dom IM1) by B135, F1, FINSEQ_1:def 3;

          

           Y1: [j, k] in ( Indices IM1) by F1, B131, B135, ZFMISC_1: 87;

          then

          consider p be FinSequence of INT such that

           B133: p = (IM1 . j) & (IM1 * (j,k)) = (p . k) by MATRIX_0:def 5;

          

           B81A: j in ( dom b3) by B7, FINSEQ_1:def 3;

          

           X0: (( Col (FM1,j)) . k) = (FM1 * (k,j)) by B132, MATRIX_0:def 8

          .= (( AutMt (( id V2),b3,b2)) * (j,k)) by Y1, MATRIX_0:def 6;

          (IM1 . j) = (( AutMt (( id V2),b3,b2)) /. j) by B132A, PARTFUN1:def 6

          .= ((( id V2) . (b3 /. j)) |-- b2) by B81A, Def8;

          hence (( Col (FM1,j)) . k) = (((b3 /. j) |-- b2) . k) by B133, X0;

        end;

        ( len ( Col (FM1,j))) = ( len ((b3 /. j) |-- b2)) by B14, Def7;

        hence thesis by B9, B11, B12, B13, B14, B15, LMThMBF1X, FINSEQ_1:def 17;

      end;

      hence thesis by MATRIX_0: 27, A2, A3;

    end;

    theorem :: ZMATRLIN:105

    

     ThMBF2: for V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V1, f be bilinear-Form of V1, V2 st 0 < ( rank V1) holds ( BilinearM (f,b3,b2)) = (( AutMt (( id V1),b3,b1)) * ( BilinearM (f,b1,b2)))

    proof

      let V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V1, f be bilinear-Form of V1, V2;

      assume

       AS: 0 < ( rank V1);

      set n = ( len b3);

      

       A1: ( len b1) = ( rank V1) by ThRank1;

      

       A3: ( len b3) = ( rank V1) by ThRank1;

      reconsider IM1 = ( AutMt (( id V1),b3,b1)) as Matrix of n, INT.Ring by LMThMBF3, A3;

      reconsider M1 = IM1 as Matrix of n, INT.Ring ;

      set M2 = (M1 * ( BilinearM (f,b1,b2)));

      

       B1: ( len M1) = n & ( width M1) = n & ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

       0 < ( len b1) by AS, ThRank1;

      then

       B3: ( len ( BilinearM (f,b1,b2))) = ( len b1) & ( width ( BilinearM (f,b1,b2))) = ( len b2) by MATRIX_0: 23;

      then ( len M2) = n & ( width M2) = ( len b2) by A1, A3, B1, MATRIX_3:def 4;

      then

      reconsider M2 as Matrix of n, ( len b2), INT.Ring by A3, AS, MATRIX_0: 20;

      set FM1 = M1;

      set FBM = ( BilinearM (f,b1,b2));

      for i,j be Nat st [i, j] in ( Indices ( BilinearM (f,b3,b2))) holds (( BilinearM (f,b3,b2)) * (i,j)) = (M2 * (i,j))

      proof

        let i,j be Nat;

        assume [i, j] in ( Indices ( BilinearM (f,b3,b2)));

        then

         B6: [i, j] in [:( Seg ( len b3)), ( Seg ( len b2)):] by AS, A3, MATRIX_0: 23;

        then i in ( Seg ( len b3)) & j in ( Seg ( len b2)) by ZFMISC_1: 87;

        then

         B8: i in ( dom b3) & j in ( dom b2) by FINSEQ_1:def 3;

        then

         B9: (( BilinearM (f,b3,b2)) * (i,j)) = (f . ((b3 /. i),(b2 /. j))) by defBilinearM;

         [i, j] in ( Indices M2) by AS, A3, B6, MATRIX_0: 23;

        then

         B11: (M2 * (i,j)) = (( Line (FM1,i)) "*" ( Col (FBM,j))) by A1, A3, B1, B3, MATRIX_3:def 4;

        

         B12: ( len ( Line (FM1,i))) = ( len b3) by B1, MATRIX_0:def 7;

        

         B14: ( len ( Col (FBM,j))) = ( len b3) by B3, A1, A3, MATRIX_0:def 8;

         B13:

        now

          let k be Nat;

          assume

           B131: k in ( Seg ( len b1));

          then

           B132: k in ( dom FBM) by B3, FINSEQ_1:def 3;

          

           B81: k in ( dom b1) by FINSEQ_1:def 3, B131;

          

          thus (( Col (FBM,j)) . k) = (FBM * (k,j)) by B132, MATRIX_0:def 8

          .= (f . ((b1 /. k),(b2 /. j))) by B8, B81, defBilinearM;

        end;

        

         B135: i in ( Seg n) by B6, ZFMISC_1: 87;

        then

         B135A: i in ( dom M1) by B1, FINSEQ_1:def 3;

        

         B136: i in ( dom b3) by B135, FINSEQ_1:def 3;

         B15:

        now

          let k be Nat;

          assume

           BX131: 1 <= k & k <= ( len ( Line (FM1,i)));

          then

           B131: k in ( Seg ( len b1)) by FINSEQ_1: 1, B12, A1, A3;

           [i, k] in ( Indices M1) by A1, A3, B1, B131, B135, ZFMISC_1: 87;

          then

          consider p be FinSequence of INT.Ring such that

           B133: p = (M1 . i) & (M1 * (i,k)) = (p . k) by MATRIX_0:def 5;

          

           X0: (( Line (FM1,i)) . k) = (FM1 * (i,k)) by B1, B12, BX131, FINSEQ_1: 1, MATRIX_0:def 7

          .= (( AutMt (( id V1),b3,b1)) * (i,k));

          (M1 . i) = (( AutMt (( id V1),b3,b1)) /. i) by B135A, PARTFUN1:def 6

          .= ((( id V1) . (b3 /. i)) |-- b1) by B136, Def8;

          hence (( Line (FM1,i)) . k) = (((b3 /. i) |-- b1) . k) by B133, X0;

        end;

        ( len ( Line (FM1,i))) = ( len ((b3 /. i) |-- b1)) by A1, A3, B12, Def7;

        hence thesis by A1, A3, B9, B11, B12, B13, B14, B15, LMThMBF1Y, FINSEQ_1:def 17;

      end;

      hence thesis by MATRIX_0: 27;

    end;

    theorem :: ZMATRLIN:106

    

     ThMBF3: for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, f be bilinear-Form of V, V st 0 < ( rank V) holds ( BilinearM (f,b2,b2)) = ((( AutMt (( id V),b2,b1)) * ( BilinearM (f,b1,b1))) * (( AutMt (( id V),b2,b1)) @ ))

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, f be bilinear-Form of V, V;

      assume

       AS: 0 < ( rank V);

      set n = ( len b1);

      

       A1: ( len b1) = ( rank V) by ThRank1;

      reconsider IM1 = ( AutMt (( id V),b2,b1)) as Matrix of n, INT.Ring by LMThMBF3, A1;

      reconsider IM2 = ( AutMt (( id V),b2,b1)) as Matrix of n, INT.Ring by LMThMBF3, A1;

      reconsider M1 = (IM1 @ ) as Matrix of n, INT.Ring ;

      reconsider M2 = IM2 as Matrix of n, INT.Ring ;

      

       Y1: ( width IM1) = n by MATRIX_0: 24;

      

       Yb: ( width ( BilinearM (f,b1,b1))) = ( len b1) by MATRIX_0: 24;

      

       X1: ( width ( AutMt (( id V),b2,b1))) = ( len ( BilinearM (f,b1,b1))) & ( width ( BilinearM (f,b1,b1))) = ( len (( AutMt (( id V),b2,b1)) @ )) by MATRIX_0:def 2, Y1, Yb;

      

      thus ( BilinearM (f,b2,b2)) = (( AutMt (( id V),b2,b1)) * ( BilinearM (f,b1,b2))) by ThMBF2, AS

      .= (( AutMt (( id V),b2,b1)) * (( BilinearM (f,b1,b1)) * (( AutMt (( id V),b2,b1)) @ ))) by ThMBF1, AS

      .= ((( AutMt (( id V),b2,b1)) * ( BilinearM (f,b1,b1))) * (( AutMt (( id V),b2,b1)) @ )) by MATRIX_3: 33, X1;

    end;

    theorem :: ZMATRLIN:107

    for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, f be bilinear-Form of V, V holds |.( Det ( BilinearM (f,b2,b2))).| = |.( Det ( BilinearM (f,b1,b1))).|

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, f be bilinear-Form of V, V;

      set n = ( len b1);

      

       A1: ( len b1) = ( rank V) by ThRank1;

      

       A2: ( len b2) = ( rank V) by ThRank1;

      reconsider B1 = ( BilinearM (f,b1,b1)) as Matrix of n, INT.Ring ;

      reconsider B2 = ( BilinearM (f,b2,b2)) as Matrix of n, INT.Ring by A1, A2;

      per cases ;

        suppose ( rank V) = 0 ;

        hence |.( Det ( BilinearM (f,b2,b2))).| = |.( Det ( BilinearM (f,b1,b1))).| by A1, A2, MATRIX_0: 45;

      end;

        suppose

         ZZ: ( rank V) > 0 ;

        then

         B2: ( BilinearM (f,b2,b2)) = ((( AutMt (( id V),b2,b1)) * ( BilinearM (f,b1,b1))) * (( AutMt (( id V),b2,b1)) @ )) by ThMBF3;

        reconsider IM1 = ( AutMt (( id V),b2,b1)) as Matrix of n, INT.Ring by A1, LMThMBF3;

        reconsider IM2 = ( AutMt (( id V),b2,b1)) as Matrix of n, INT.Ring by A1, LMThMBF3;

        reconsider M1 = (IM1 @ ) as Matrix of n, INT.Ring ;

        reconsider M2 = IM2 as Matrix of n, INT.Ring ;

        n >= (1 + 0 ) by A1, ZZ, NAT_1: 13;

        then

         X1: ( Det IM1) = ( Det M1) by MATRIX_7: 37;

        reconsider M2B1 = (M2 * B1) as Matrix of n, INT.Ring ;

        ( Det B2) = (( Det M2B1) * ( Det M1)) by B2, MATRIX11: 62, ZZ, A1

        .= ((( Det M2) * ( Det B1)) * ( Det M1)) by ZZ, A1, MATRIX11: 62;

        

        hence |.( Det ( BilinearM (f,b2,b2))).| = ( |.(( Det M2) * ( Det B1)).| * |.( Det M1).|) by A1, A2, COMPLEX1: 65

        .= ( |.(( Det M2) * ( Det B1)).| * 1) by A1, X1, ThSign1

        .= ( |.( Det M2).| * |.( Det B1).|) by COMPLEX1: 65

        .= ( |.( Det B1).| * 1) by A1, ThSign1

        .= |.( Det ( BilinearM (f,b1,b1))).|;

      end;

    end;