matrixj2.miz



    begin

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

x,y for set,

K for Field,

a,L for Element of K;

    

     Lm1: for f be Function st f is one-to-one & x in ( dom f) holds ( rng (f +* (x,y))) = ((( rng f) \ {(f . x)}) \/ {y})

    proof

      let f be Function such that

       A1: f is one-to-one and

       A2: x in ( dom f);

      set xy = (x .--> y);

      ( dom xy) = {x} & ( rng xy) = {y} by FUNCOP_1: 8;

      

      then ( rng (f +* xy)) = ((f .: (( dom f) \ {x})) \/ {y}) by FRECHET: 12

      .= (((f .: ( dom f)) \ (f .: {x})) \/ {y}) by A1, FUNCT_1: 64

      .= ((( rng f) \ ( Im (f,x))) \/ {y}) by RELAT_1: 113

      .= ((( rng f) \ {(f . x)}) \/ {y}) by A2, FUNCT_1: 59;

      hence thesis by A2, FUNCT_7:def 3;

    end;

    definition

      let K, L, n;

      :: MATRIXJ2:def1

      func Jordan_block (L,n) -> Matrix of K means

      : Def1: ( len it ) = n & ( width it ) = n & for i, j st [i, j] in ( Indices it ) holds (i = j implies (it * (i,j)) = L) & ((i + 1) = j implies (it * (i,j)) = ( 1_ K)) & (i <> j & (i + 1) <> j implies (it * (i,j)) = ( 0. K));

      existence

      proof

        defpred P[ Nat, Nat, set] means ($1 = $2 implies $3 = L) & (($1 + 1) = $2 implies $3 = ( 1_ K)) & ($1 <> $2 & ($1 + 1) <> $2 implies $3 = ( 0. K));

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

        

         A1: for i, j st [i, j] in [:( Seg N), ( Seg N):] holds ex x be Element of K st P[i, j, x]

        proof

          let i, j such that [i, j] in [:( Seg N), ( Seg N):];

          per cases ;

            suppose

             A2: i = j;

            take L;

            thus thesis by A2;

          end;

            suppose

             A3: (i + 1) = j;

            take ( 1_ K);

            thus thesis by A3;

          end;

            suppose

             A4: i <> j & (i + 1) <> j;

            take ( 0. K);

            thus thesis by A4;

          end;

        end;

        consider M be Matrix of N, K such that

         A5: for i, j st [i, j] in ( Indices M) holds P[i, j, (M * (i,j))] from MATRIX_0:sch 2( A1);

        take M;

        thus thesis by A5, MATRIX_0: 24;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of K such that

         A6: ( len M1) = n & ( width M1) = n and

         A7: for i, j st [i, j] in ( Indices M1) holds (i = j implies (M1 * (i,j)) = L) & ((i + 1) = j implies (M1 * (i,j)) = ( 1_ K)) & (i <> j & (i + 1) <> j implies (M1 * (i,j)) = ( 0. K)) and

         A8: ( len M2) = n & ( width M2) = n and

         A9: for i, j st [i, j] in ( Indices M2) holds (i = j implies (M2 * (i,j)) = L) & ((i + 1) = j implies (M2 * (i,j)) = ( 1_ K)) & (i <> j & (i + 1) <> j implies (M2 * (i,j)) = ( 0. K));

        now

          let i, j such that

           A10: [i, j] in ( Indices M1);

          

           A11: ( Indices M1) = [:( Seg n), ( Seg n):] by A6, FINSEQ_1:def 3

          .= ( Indices M2) by A8, FINSEQ_1:def 3;

          i = j or (i + 1) = j or i <> j & (i + 1) <> j;

          then (M1 * (i,j)) = L & (M2 * (i,j)) = L or (M1 * (i,j)) = ( 1_ K) & (M2 * (i,j)) = ( 1_ K) or (M1 * (i,j)) = ( 0. K) & (M2 * (i,j)) = ( 0. K) by A7, A9, A10, A11;

          hence (M1 * (i,j)) = (M2 * (i,j));

        end;

        hence thesis by A6, A8, MATRIX_0: 21;

      end;

    end

    definition

      let K, L, n;

      :: original: Jordan_block

      redefine

      func Jordan_block (L,n) -> upper_triangular Matrix of n, K ;

      coherence

      proof

        ( len ( Jordan_block (L,n))) = n & ( width ( Jordan_block (L,n))) = n by Def1;

        then

        reconsider LBn = ( Jordan_block (L,n)) as Matrix of n, K by MATRIX_0: 51;

        now

          let i, j such that

           A1: [i, j] in ( Indices LBn);

          assume

           A2: i > j;

          then (i + 1) > j by NAT_1: 13;

          hence (LBn * (i,j)) = ( 0. K) by A1, A2, Def1;

        end;

        hence thesis by MATRIX_1:def 8;

      end;

    end

    theorem :: MATRIXJ2:1

    

     Th1: ( diagonal_of_Matrix ( Jordan_block (L,n))) = (n |-> L)

    proof

      set B = ( Jordan_block (L,n));

       A1:

      now

        

         A2: [:( Seg n), ( Seg n):] = ( Indices B) by MATRIX_0: 24;

        let i;

        assume 1 <= i & i <= n;

        then

         A3: i in ( Seg n);

        then

         A4: [i, i] in [:( Seg n), ( Seg n):] by ZFMISC_1: 87;

        

        thus (( diagonal_of_Matrix B) . i) = (B * (i,i)) by A3, MATRIX_3:def 10

        .= L by A4, A2, Def1

        .= ((n |-> L) . i) by A3, FINSEQ_2: 57;

      end;

      ( len ( diagonal_of_Matrix B)) = n & ( len (n |-> L)) = n by CARD_1:def 7, MATRIX_3:def 10;

      hence thesis by A1;

    end;

    theorem :: MATRIXJ2:2

    

     Th2: ( Det ( Jordan_block (L,n))) = (( power K) . (L,n))

    proof

      

      thus ( Det ( Jordan_block (L,n))) = (the multF of K $$ ( diagonal_of_Matrix ( Jordan_block (L,n)))) by MATRIX13: 7

      .= ( Product (n |-> L)) by Th1

      .= (( power K) . (L,n)) by MATRIXJ1: 5;

    end;

    theorem :: MATRIXJ2:3

    

     Th3: ( Jordan_block (L,n)) is invertible iff n = 0 or L <> ( 0. K)

    proof

      set B = ( Jordan_block (L,n));

      

       A1: B is invertible implies L <> ( 0. K) or n = 0

      proof

        assume B is invertible;

        then

         A2: ( Det B) <> ( 0. K) by LAPLACE: 34;

        assume

         A3: L = ( 0. K);

        assume n <> 0 ;

        then

         A4: n in ( Seg n) by FINSEQ_1: 3;

        then ( dom (n |-> L)) = ( Seg n) & ((n |-> L) . n) = L by FINSEQ_2: 57, FINSEQ_2: 124;

        

        then ( 0. K) = ( Product (n |-> L)) by A3, A4, FVSUM_1: 82

        .= (( power K) . (L,n)) by MATRIXJ1: 5;

        hence thesis by A2, Th2;

      end;

      n = 0 or L <> ( 0. K) implies B is invertible

      proof

        assume

         A5: n = 0 or L <> ( 0. K);

        assume not B is invertible;

        

        then ( 0. K) = ( Det B) by LAPLACE: 34

        .= (( power K) . (L,n)) by Th2

        .= ( Product (n |-> L)) by MATRIXJ1: 5;

        then

         A6: ex k be Nat st k in ( dom (n |-> L)) & ((n |-> L) . k) = ( 0. K) by FVSUM_1: 82;

        ( dom (n |-> L)) = ( Seg n) by FINSEQ_2: 124;

        hence thesis by A5, A6, FINSEQ_2: 57;

      end;

      hence thesis by A1;

    end;

    theorem :: MATRIXJ2:4

    

     Th4: i in ( Seg n) & i <> n implies ( Line (( Jordan_block (L,n)),i)) = ((L * ( Line (( 1. (K,n)),i))) + ( Line (( 1. (K,n)),(i + 1))))

    proof

      assume that

       A1: i in ( Seg n) and

       A2: i <> n;

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

      set J = ( Jordan_block (L,n));

      set i1 = (i + 1);

      set ONE = ( 1. (K,n));

      set Li = ( Line (ONE,i));

      set Li1 = ( Line (ONE,i1));

      set LJ = ( Line (J,i));

      

       A3: ( width ONE) = n by MATRIX_0: 24;

      

       A4: ( Indices ONE) = ( Indices J) by MATRIX_0: 26;

      reconsider Li, Li1, LJ as Element of (N -tuples_on the carrier of K) by MATRIX_0: 24;

      

       A5: ( Indices ONE) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( width J) = n by MATRIX_0: 24;

      now

        let j such that

         A7: j in ( Seg n);

        (Li . j) = (ONE * (i,j)) by A3, A7, MATRIX_0:def 7;

        then

         A8: ((L * Li) . j) = (L * (ONE * (i,j))) by A7, FVSUM_1: 51;

        

         A9: [i, j] in [:( Seg n), ( Seg n):] by A1, A7, ZFMISC_1: 87;

        i <= n by A1, FINSEQ_1: 1;

        then i < n by A2, XXREAL_0: 1;

        then 1 <= i1 & i1 <= n by NAT_1: 11, NAT_1: 13;

        then i1 in ( Seg n);

        then

         A10: [i1, j] in [:( Seg n), ( Seg n):] by A7, ZFMISC_1: 87;

        (Li1 . j) = (ONE * (i1,j)) by A3, A7, MATRIX_0:def 7;

        then

         A11: (((L * Li) + Li1) . j) = ((L * (ONE * (i,j))) + (ONE * (i1,j))) by A7, A8, FVSUM_1: 18;

        

         A12: (LJ . j) = (J * (i,j)) by A6, A7, MATRIX_0:def 7;

        now

          per cases ;

            suppose

             A13: i = j;

            then

             A14: i1 > j by NAT_1: 13;

            

            thus (LJ . j) = L by A5, A4, A9, A12, A13, Def1

            .= (L + ( 0. K)) by RLVECT_1:def 4

            .= ((L * ( 1_ K)) + ( 0. K))

            .= ((L * (ONE * (i,j))) + ( 0. K)) by A5, A9, A13, MATRIX_1:def 3

            .= (((L * Li) + Li1) . j) by A5, A10, A11, A14, MATRIX_1:def 3;

          end;

            suppose

             A15: i1 = j;

            then

             A16: i < j by NAT_1: 13;

            

            thus (LJ . j) = ( 1_ K) by A5, A4, A9, A12, A15, Def1

            .= (( 0. K) + ( 1_ K)) by RLVECT_1:def 4

            .= ((L * ( 0. K)) + ( 1_ K))

            .= ((L * (ONE * (i,j))) + ( 1_ K)) by A5, A9, A16, MATRIX_1:def 3

            .= (((L * Li) + Li1) . j) by A5, A10, A11, A15, MATRIX_1:def 3;

          end;

            suppose

             A17: i <> j & i1 <> j;

            

            hence (LJ . j) = ( 0. K) by A5, A4, A9, A12, Def1

            .= (( 0. K) + ( 0. K)) by RLVECT_1:def 4

            .= ((L * ( 0. K)) + ( 0. K))

            .= ((L * (ONE * (i,j))) + ( 0. K)) by A5, A9, A17, MATRIX_1:def 3

            .= (((L * Li) + Li1) . j) by A5, A10, A11, A17, MATRIX_1:def 3;

          end;

        end;

        hence (((L * Li) + Li1) . j) = (LJ . j);

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: MATRIXJ2:5

    

     Th5: ( Line (( Jordan_block (L,n)),n)) = (L * ( Line (( 1. (K,n)),n)))

    proof

      set ONE = ( 1. (K,n));

      set Ln = ( Line (ONE,n));

      set J = ( Jordan_block (L,n));

      set LJ = ( Line (J,n));

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

      

       A1: ( width J) = n by MATRIX_0: 24;

      

       A2: ( Indices ONE) = ( Indices J) by MATRIX_0: 26;

      reconsider Ln, LJ as Element of (N -tuples_on the carrier of K) by MATRIX_0: 24;

      

       A3: ( Indices ONE) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( width ONE) = n by MATRIX_0: 24;

      now

        let j such that

         A5: j in ( Seg n);

        n <> 0 by A5;

        then n in ( Seg n) by FINSEQ_1: 3;

        then

         A6: [n, j] in [:( Seg n), ( Seg n):] by A5, ZFMISC_1: 87;

        (Ln . j) = (ONE * (n,j)) by A4, A5, MATRIX_0:def 7;

        then

         A7: ((L * Ln) . j) = (L * (ONE * (n,j))) by A5, FVSUM_1: 51;

        

         A8: (LJ . j) = (J * (n,j)) by A1, A5, MATRIX_0:def 7;

        now

          per cases ;

            suppose

             A9: n = j;

            

            hence (LJ . j) = L by A3, A2, A6, A8, Def1

            .= (L * ( 1_ K))

            .= ((L * Ln) . j) by A3, A6, A7, A9, MATRIX_1:def 3;

          end;

            suppose (n + 1) = j;

            then j > n by NAT_1: 13;

            hence ((L * Ln) . j) = (LJ . j) by A5, FINSEQ_1: 1;

          end;

            suppose

             A10: n <> j & (n + 1) <> j;

            

            hence (LJ . j) = ( 0. K) by A3, A2, A6, A8, Def1

            .= (L * ( 0. K))

            .= ((L * Ln) . j) by A3, A6, A7, A10, MATRIX_1:def 3;

          end;

        end;

        hence ((L * Ln) . j) = (LJ . j);

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: MATRIXJ2:6

    

     Th6: for F be Element of (n -tuples_on the carrier of K) st i in ( Seg n) holds (i <> n implies (( Line (( Jordan_block (L,n)),i)) "*" F) = ((L * (F /. i)) + (F /. (i + 1)))) & (i = n implies (( Line (( Jordan_block (L,n)),i)) "*" F) = (L * (F /. i)))

    proof

      let F be Element of (n -tuples_on the carrier of K) such that

       A1: i in ( Seg n);

      set J = ( Jordan_block (L,n));

      

       A2: ( width J) = n by MATRIX_0: 24;

      then

       A3: (( Line (J,i)) . i) = (J * (i,i)) by A1, MATRIX_0:def 7;

      

       A4: ( Indices J) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      then

       A5: [i, i] in ( Indices J) by A1, ZFMISC_1: 87;

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

      set Li = ( Line (J,i));

      reconsider Li, f = F as Element of (N -tuples_on the carrier of K) by MATRIX_0: 24;

      

       A6: ( dom f) = ( Seg n) by FINSEQ_2: 124;

      then

       A7: (f . i) = (f /. i) by A1, PARTFUN1:def 6;

      

       A8: ( dom ( mlt (Li,f))) = ( Seg n) by FINSEQ_2: 124;

      thus i <> n implies (( Line (J,i)) "*" F) = ((L * (F /. i)) + (F /. (i + 1)))

      proof

         A9:

        now

          let j such that

           A10: j in ( Seg n) and

           A11: j <> i & j <> (i + 1);

           [i, j] in ( Indices J) by A1, A4, A10, ZFMISC_1: 87;

          

          then

           A12: ( 0. K) = (J * (i,j)) by A11, Def1

          .= (Li . j) by A2, A10, MATRIX_0:def 7;

          (f . j) = (f /. j) by A6, A10, PARTFUN1:def 6;

          

          hence (( mlt (Li,f)) . j) = (( 0. K) * (f /. j)) by A10, A12, FVSUM_1: 61

          .= ( 0. K);

        end;

        

         A13: [i, i] in ( Indices J) by A1, A4, ZFMISC_1: 87;

        assume

         A14: i <> n;

        i <= n by A1, FINSEQ_1: 1;

        then i < n by A14, XXREAL_0: 1;

        then 1 <= (i + 1) & (i + 1) <= n by NAT_1: 11, NAT_1: 13;

        then

         A15: (i + 1) in ( Seg n);

        then

         A16: [i, (i + 1)] in ( Indices J) by A1, A4, ZFMISC_1: 87;

        

         A17: (f . i) = (f /. i) & (J * (i,i)) = (Li . i) by A1, A2, A6, MATRIX_0:def 7, PARTFUN1:def 6;

        

         A18: (( mlt (Li,f)) /. i) = (( mlt (Li,f)) . i) by A1, A8, PARTFUN1:def 6

        .= ((J * (i,i)) * (f /. i)) by A1, A17, FVSUM_1: 61

        .= (L * (f /. i)) by A13, Def1;

        

         A19: (i + 1) > i by NAT_1: 13;

        

         A20: (f . (i + 1)) = (f /. (i + 1)) & (J * (i,(i + 1))) = (Li . (i + 1)) by A2, A6, A15, MATRIX_0:def 7, PARTFUN1:def 6;

        (( mlt (Li,f)) /. (i + 1)) = (( mlt (Li,f)) . (i + 1)) by A8, A15, PARTFUN1:def 6

        .= ((J * (i,(i + 1))) * (f /. (i + 1))) by A15, A20, FVSUM_1: 61

        .= (( 1_ K) * (f /. (i + 1))) by A16, Def1

        .= (f /. (i + 1));

        hence thesis by A1, A8, A15, A19, A18, A9, MATRIX15: 7;

      end;

      assume

       A21: i = n;

      now

        let j such that

         A22: j in ( Seg n) and

         A23: j <> i;

        

         A24: (f . j) = (f /. j) by A6, A22, PARTFUN1:def 6;

        j <= n by A22, FINSEQ_1: 1;

        then

         A25: j < (i + 1) by A21, NAT_1: 13;

        

         A26: [i, j] in ( Indices J) by A1, A4, A22, ZFMISC_1: 87;

        (( Line (J,i)) . j) = (J * (i,j)) by A2, A22, MATRIX_0:def 7

        .= ( 0. K) by A23, A25, A26, Def1;

        

        hence (( mlt (( Line (J,i)),f)) . j) = (( 0. K) * (f /. j)) by A8, A22, A24, FVSUM_1: 61

        .= ( 0. K);

      end;

      

      hence (( Line (J,i)) "*" F) = (( mlt (( Line (J,i)),f)) . i) by A1, A8, MATRIX_3: 12

      .= ((J * (i,i)) * (f /. i)) by A1, A8, A3, A7, FVSUM_1: 61

      .= (L * (F /. i)) by A5, Def1;

    end;

    theorem :: MATRIXJ2:7

    

     Th7: for F be Element of (n -tuples_on the carrier of K) st i in ( Seg n) holds (i = 1 implies (( Col (( Jordan_block (L,n)),i)) "*" F) = (L * (F /. i))) & (i <> 1 implies (( Col (( Jordan_block (L,n)),i)) "*" F) = ((L * (F /. i)) + (F /. (i - 1))))

    proof

      set J = ( Jordan_block (L,n));

      set Ci = ( Col (J,i));

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

      let F be Element of (n -tuples_on the carrier of K) such that

       A1: i in ( Seg n);

      

       A2: i >= 1 by A1, FINSEQ_1: 1;

      then

      reconsider i1 = (i - 1) as Element of NAT by NAT_1: 21;

      

       A3: ( len J) = n & ( dom J) = ( Seg ( len J)) by FINSEQ_1:def 3, MATRIX_0: 24;

      then

       A4: (( Col (J,i)) . i) = (J * (i,i)) by A1, MATRIX_0:def 8;

      

       A5: (i1 + 1) >= i1 by NAT_1: 11;

      n >= i by A1, FINSEQ_1: 1;

      then

       A6: n >= i1 by A5, XXREAL_0: 2;

      

       A7: ( Indices J) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      then

       A8: [i, i] in ( Indices J) by A1, ZFMISC_1: 87;

      reconsider Ci, f = F as Element of (N -tuples_on the carrier of K) by MATRIX_0: 24;

      

       A9: ( dom f) = ( Seg n) by FINSEQ_2: 124;

      then

       A10: (f . i) = (f /. i) by A1, PARTFUN1:def 6;

      

       A11: ( dom ( mlt (Ci,f))) = ( Seg n) by FINSEQ_2: 124;

      

      then

       A12: (( mlt (Ci,f)) /. i) = (( mlt (Ci,f)) . i) by A1, PARTFUN1:def 6

      .= ((J * (i,i)) * (f /. i)) by A1, A4, A10, FVSUM_1: 61

      .= (L * (f /. i)) by A8, Def1;

      thus i = 1 implies (( Col (J,i)) "*" F) = (L * (F /. i))

      proof

        

         A13: (( Col (J,i)) . i) = (J * (i,i)) & (f . i) = (f /. i) by A1, A3, A9, MATRIX_0:def 8, PARTFUN1:def 6;

        

         A14: [i, i] in ( Indices J) by A1, A7, ZFMISC_1: 87;

        assume

         A15: i = 1;

        now

          let j such that

           A16: j in ( Seg n) and

           A17: j <> i;

          

           A18: (f . j) = (f /. j) by A9, A16, PARTFUN1:def 6;

          1 <= j by A16, FINSEQ_1: 1;

          then

           A19: i < (j + 1) by A15, NAT_1: 13;

          

           A20: [j, i] in ( Indices J) by A1, A7, A16, ZFMISC_1: 87;

          (( Col (J,i)) . j) = (J * (j,i)) by A3, A16, MATRIX_0:def 8

          .= ( 0. K) by A17, A19, A20, Def1;

          

          hence (( mlt (( Col (J,i)),f)) . j) = (( 0. K) * (f /. j)) by A11, A16, A18, FVSUM_1: 61

          .= ( 0. K);

        end;

        

        hence (( Col (J,i)) "*" F) = (( mlt (( Col (J,i)),f)) . i) by A1, A11, MATRIX_3: 12

        .= ((J * (i,i)) * (f /. i)) by A1, A11, A13, FVSUM_1: 61

        .= (L * (F /. i)) by A14, Def1;

      end;

      

       A21: i1 <> i;

      assume i <> 1;

      then (i1 + 1) > ( 0 + 1) by A2, XXREAL_0: 1;

      then i1 >= 1 by NAT_1: 14;

      then

       A22: i1 in ( Seg n) by A6;

      then

       A23: (i1 + 1) = i & [i1, i] in ( Indices J) by A1, A7, ZFMISC_1: 87;

       A24:

      now

        let j such that

         A25: j in ( Seg n) and

         A26: j <> i and

         A27: j <> i1;

         [j, i] in ( Indices J) & (j + 1) <> i by A1, A7, A25, A27, ZFMISC_1: 87;

        

        then

         A28: ( 0. K) = (J * (j,i)) by A26, Def1

        .= (Ci . j) by A3, A25, MATRIX_0:def 8;

        (f . j) = (f /. j) by A9, A25, PARTFUN1:def 6;

        

        hence (( mlt (Ci,f)) . j) = (( 0. K) * (f /. j)) by A25, A28, FVSUM_1: 61

        .= ( 0. K);

      end;

      

       A29: (f . i1) = (f /. i1) by A9, A22, PARTFUN1:def 6;

      

       A30: (( Col (J,i)) . i1) = (J * (i1,i)) by A3, A22, MATRIX_0:def 8;

      (( mlt (Ci,f)) /. i1) = (( mlt (Ci,f)) . i1) by A11, A22, PARTFUN1:def 6

      .= ((J * (i1,i)) * (f /. i1)) by A22, A30, A29, FVSUM_1: 61

      .= (( 1_ K) * (f /. i1)) by A23, Def1

      .= (f /. i1);

      hence thesis by A1, A11, A22, A21, A12, A24, MATRIX15: 7;

    end;

    theorem :: MATRIXJ2:8

    L <> ( 0. K) implies ex M be Matrix of n, K st (( Jordan_block (L,n)) ~ ) = M & for i, j st [i, j] in ( Indices M) holds (i > j implies (M * (i,j)) = ( 0. K)) & (i <= j implies (M * (i,j)) = ( - (( power K) . (( - (L " )),((j -' i) + 1)))))

    proof

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

      defpred P[ Nat, Nat, set] means ($1 > $2 implies $3 = ( 0. K)) & ($1 <= $2 implies $3 = ( - (( power K) . (( - (L " )),(($2 -' $1) + 1)))));

      

       A1: for i, j st [i, j] in [:( Seg N), ( Seg N):] holds ex x be Element of K st P[i, j, x]

      proof

        let i, j such that [i, j] in [:( Seg N), ( Seg N):];

        per cases ;

          suppose

           A2: i > j;

          take ( 0. K);

          thus thesis by A2;

        end;

          suppose

           A3: i <= j;

          take ( - (( power K) . (( - (L " )),((j -' i) + 1))));

          thus thesis by A3;

        end;

      end;

      consider M be Matrix of N, K such that

       A4: for i, j st [i, j] in ( Indices M) holds P[i, j, (M * (i,j))] from MATRIX_0:sch 2( A1);

      set ONE = ( 1. (K,n));

      set J = ( Jordan_block (L,n));

      

       A5: ( Indices ONE) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A6: L <> ( 0. K);

      then

       A7: J is invertible by Th3;

      reconsider M as Matrix of n, K;

      set MJ = (M * J);

      

       A8: ( Indices M) = ( Indices J) & ( Indices J) = ( Indices ONE) by MATRIX_0: 26;

      

       A9: ( width M) = n by MATRIX_0: 24;

      

       A10: ( Indices MJ) = ( Indices ONE) by MATRIX_0: 26;

      

       A11: ( len J) = n by MATRIX_0: 24;

      now

        let i, j such that

         A12: [i, j] in ( Indices ONE);

        

         A13: i in ( Seg n) by A5, A12, ZFMISC_1: 87;

        set LL = ( Line (M,i));

        

         A14: (MJ * (i,j)) = (LL "*" ( Col (J,j))) by A9, A10, A12, A11, MATRIX_3:def 4

        .= (( Col (J,j)) "*" LL) by FVSUM_1: 90;

        

         A15: j in ( Seg n) by A5, A12, ZFMISC_1: 87;

        then

         A16: (LL . j) = (M * (i,j)) by A9, MATRIX_0:def 7;

        

         A17: ( dom LL) = ( Seg n) by A9, FINSEQ_2: 124;

        then

         A18: (LL /. j) = (LL . j) by A15, PARTFUN1:def 6;

        now

          per cases ;

            suppose

             A19: j = 1;

            then

             A20: (MJ * (i,j)) = (L * (M * (i,j))) by A9, A15, A18, A16, A14, Th7;

            now

              per cases ;

                suppose

                 A21: i = j;

                

                hence (MJ * (i,j)) = (L * ( - (( power K) . (( - (L " )),((i -' i) + 1))))) by A4, A8, A12, A20

                .= (L * ( - (( power K) . (( - (L " )),( 0 + 1))))) by XREAL_1: 232

                .= (L * ( - ( - (L " )))) by GROUP_1: 50

                .= (L * (L " )) by RLVECT_1: 17

                .= ( 1_ K) by A6, VECTSP_1:def 10

                .= (ONE * (i,j)) by A12, A21, MATRIX_1:def 3;

              end;

                suppose

                 A22: i <> j;

                1 <= i by A13, FINSEQ_1: 1;

                then j < i by A19, A22, XXREAL_0: 1;

                

                hence (MJ * (i,j)) = (L * ( 0. K)) by A4, A8, A12, A20

                .= ( 0. K)

                .= (ONE * (i,j)) by A12, A22, MATRIX_1:def 3;

              end;

            end;

            hence (ONE * (i,j)) = (MJ * (i,j));

          end;

            suppose

             A23: j <> 1;

            

             A24: j >= 1 by A15, FINSEQ_1: 1;

            then

            reconsider j1 = (j - 1) as Element of NAT by NAT_1: 21;

            j1 <= (j1 + 1) & j <= n by A15, FINSEQ_1: 1, NAT_1: 11;

            then

             A25: n >= j1 by XXREAL_0: 2;

            (j1 + 1) > ( 0 + 1) by A23, A24, XXREAL_0: 1;

            then j1 >= 1 by NAT_1: 14;

            then

             A26: j1 in ( Seg n) by A25;

            then

             A27: [i, j1] in ( Indices ONE) by A5, A13, ZFMISC_1: 87;

            (LL /. j1) = (LL . j1) & (LL . j1) = (M * (i,j1)) by A9, A17, A26, MATRIX_0:def 7, PARTFUN1:def 6;

            then

             A28: (MJ * (i,j)) = ((L * (M * (i,j))) + (M * (i,j1))) by A9, A15, A18, A16, A14, A23, Th7;

            now

              per cases by XXREAL_0: 1;

                suppose

                 A29: i < (j1 + 1);

                set P = (( power K) . (( - (L " )),((j1 -' i) + 1)));

                

                 A30: (j -' i) = (j - i) by A29, XREAL_1: 233;

                

                 A31: i <= j1 by A29, NAT_1: 13;

                then

                 A32: (j1 -' i) = (j1 - i) by XREAL_1: 233;

                

                thus (MJ * (i,j)) = ((L * (M * (i,j))) + ( - P)) by A4, A8, A27, A28, A31

                .= ((L * ( - (( power K) . (( - (L " )),((j -' i) + 1))))) + ( - P)) by A4, A8, A12, A29

                .= ((L * ( - (( - (L " )) * P))) + ( - P)) by A32, A30, GROUP_1:def 7

                .= ((L * (( - ( - (L " ))) * P)) + ( - P)) by VECTSP_1: 9

                .= ((L * ((L " ) * P)) + ( - P)) by RLVECT_1: 17

                .= (((L * (L " )) * P) + ( - P)) by GROUP_1:def 3

                .= ((( 1_ K) * P) + ( - P)) by A6, VECTSP_1:def 10

                .= (P + ( - P))

                .= ( 0. K) by RLVECT_1:def 10

                .= (ONE * (i,j)) by A12, A29, MATRIX_1:def 3;

              end;

                suppose

                 A33: i = (j1 + 1);

                then i > j1 by NAT_1: 13;

                

                hence (MJ * (i,j)) = ((L * (M * (i,j))) + ( 0. K)) by A4, A8, A27, A28

                .= (L * (M * (i,j))) by RLVECT_1:def 4

                .= (L * ( - (( power K) . (( - (L " )),((i -' i) + 1))))) by A4, A8, A12, A33

                .= (L * ( - (( power K) . (( - (L " )),( 0 + 1))))) by XREAL_1: 232

                .= (L * ( - ( - (L " )))) by GROUP_1: 50

                .= (L * (L " )) by RLVECT_1: 17

                .= ( 1_ K) by A6, VECTSP_1:def 10

                .= (ONE * (i,j)) by A12, A33, MATRIX_1:def 3;

              end;

                suppose

                 A34: i > (j1 + 1);

                then i > j1 by NAT_1: 13;

                

                hence (MJ * (i,j)) = ((L * (M * (i,j))) + ( 0. K)) by A4, A8, A27, A28

                .= (L * (M * (i,j))) by RLVECT_1:def 4

                .= (L * ( 0. K)) by A4, A8, A12, A34

                .= ( 0. K)

                .= (ONE * (i,j)) by A12, A34, MATRIX_1:def 3;

              end;

            end;

            hence (MJ * (i,j)) = (ONE * (i,j));

          end;

        end;

        hence (ONE * (i,j)) = (MJ * (i,j));

      end;

      then

       A35: ONE = MJ by MATRIX_0: 27;

      set JM = (J * M);

      

       A36: ( len M) = n by MATRIX_0: 24;

      take M;

      

       A37: ( Indices JM) = ( Indices ONE) & ( width J) = n by MATRIX_0: 24, MATRIX_0: 26;

      now

        let i, j such that

         A38: [i, j] in ( Indices ONE);

        

         A39: i in ( Seg n) by A5, A38, ZFMISC_1: 87;

        set i1 = (i + 1);

        

         A40: j in ( Seg n) by A5, A38, ZFMISC_1: 87;

        

         A41: (JM * (i,j)) = (( Line (J,i)) "*" ( Col (M,j))) by A36, A37, A38, MATRIX_3:def 4;

        set C = ( Col (M,j));

        

         A42: ( dom M) = ( Seg n) by A36, FINSEQ_1:def 3;

        then

         A43: (C . i) = (M * (i,j)) by A39, MATRIX_0:def 8;

        

         A44: ( dom C) = ( Seg n) by A36, FINSEQ_2: 124;

        then

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

        now

          per cases ;

            suppose

             A46: i = n;

            then

             A47: (JM * (i,j)) = (L * (M * (i,j))) by A36, A39, A45, A43, A41, Th6;

            now

              per cases ;

                suppose

                 A48: i > j;

                

                hence (JM * (i,j)) = (L * ( 0. K)) by A4, A8, A38, A47

                .= ( 0. K)

                .= (ONE * (i,j)) by A38, A48, MATRIX_1:def 3;

              end;

                suppose

                 A49: i <= j;

                j <= n by A40, FINSEQ_1: 1;

                then

                 A50: j = n by A46, A49, XXREAL_0: 1;

                

                hence (JM * (i,j)) = (L * ( - (( power K) . (( - (L " )),((n -' n) + 1))))) by A4, A8, A38, A46, A47

                .= (L * ( - (( power K) . (( - (L " )),( 0 + 1))))) by XREAL_1: 232

                .= (L * ( - ( - (L " )))) by GROUP_1: 50

                .= (L * (L " )) by RLVECT_1: 17

                .= ( 1_ K) by A6, VECTSP_1:def 10

                .= (ONE * (i,j)) by A38, A46, A50, MATRIX_1:def 3;

              end;

            end;

            hence (JM * (i,j)) = (ONE * (i,j));

          end;

            suppose

             A51: i <> n;

            i <= n by A39, FINSEQ_1: 1;

            then i < n by A51, XXREAL_0: 1;

            then 1 <= i1 & i1 <= n by NAT_1: 11, NAT_1: 13;

            then

             A52: i1 in ( Seg n);

            then

             A53: [i1, j] in ( Indices M) by A8, A5, A40, ZFMISC_1: 87;

            (C /. i1) = (C . i1) & (C . i1) = (M * (i1,j)) by A42, A44, A52, MATRIX_0:def 8, PARTFUN1:def 6;

            then

             A54: (JM * (i,j)) = ((L * (M * (i,j))) + (M * (i1,j))) by A36, A39, A45, A43, A41, A51, Th6;

            now

              per cases by XXREAL_0: 1;

                suppose

                 A55: i > j;

                then i1 > j by NAT_1: 13;

                

                hence (JM * (i,j)) = ((L * (M * (i,j))) + ( 0. K)) by A4, A53, A54

                .= (L * (M * (i,j))) by RLVECT_1:def 4

                .= (L * ( 0. K)) by A4, A8, A38, A55

                .= ( 0. K)

                .= (ONE * (i,j)) by A38, A55, MATRIX_1:def 3;

              end;

                suppose

                 A56: i = j;

                then i1 > j by NAT_1: 13;

                

                hence (JM * (i,j)) = ((L * (M * (i,j))) + ( 0. K)) by A4, A53, A54

                .= (L * (M * (i,i))) by A56, RLVECT_1:def 4

                .= (L * ( - (( power K) . (( - (L " )),((i -' i) + 1))))) by A4, A8, A38, A56

                .= (L * ( - (( power K) . (( - (L " )),( 0 + 1))))) by XREAL_1: 232

                .= (L * ( - ( - (L " )))) by GROUP_1: 50

                .= (L * (L " )) by RLVECT_1: 17

                .= ( 1_ K) by A6, VECTSP_1:def 10

                .= (ONE * (i,j)) by A38, A56, MATRIX_1:def 3;

              end;

                suppose

                 A57: i < j;

                set P = (( power K) . (( - (L " )),((j -' i1) + 1)));

                

                 A58: (j -' i) = (j - i) by A57, XREAL_1: 233;

                

                 A59: i1 <= j by A57, NAT_1: 13;

                then

                 A60: (j -' i1) = (j - i1) by XREAL_1: 233;

                

                thus (JM * (i,j)) = ((L * (M * (i,j))) + ( - P)) by A4, A53, A54, A59

                .= ((L * ( - (( power K) . (( - (L " )),((j -' i) + 1))))) + ( - P)) by A4, A8, A38, A57

                .= ((L * ( - (( - (L " )) * P))) + ( - P)) by A60, A58, GROUP_1:def 7

                .= ((L * (( - ( - (L " ))) * P)) + ( - P)) by VECTSP_1: 9

                .= ((L * ((L " ) * P)) + ( - P)) by RLVECT_1: 17

                .= (((L * (L " )) * P) + ( - P)) by GROUP_1:def 3

                .= ((( 1_ K) * P) + ( - P)) by A6, VECTSP_1:def 10

                .= (P + ( - P))

                .= ( 0. K) by RLVECT_1:def 10

                .= (ONE * (i,j)) by A38, A57, MATRIX_1:def 3;

              end;

            end;

            hence (ONE * (i,j)) = (JM * (i,j));

          end;

        end;

        hence (ONE * (i,j)) = (JM * (i,j));

      end;

      then ONE = JM by MATRIX_0: 27;

      then M is_reverse_of J by A35, MATRIX_6:def 2;

      hence thesis by A4, A7, MATRIX_6:def 4;

    end;

    theorem :: MATRIXJ2:9

    

     Th9: (( Jordan_block (L,n)) + (a * ( 1. (K,n)))) = ( Jordan_block ((L + a),n))

    proof

      set J = ( Jordan_block (L,n));

      set Ja = ( Jordan_block ((L + a),n));

      set ONE = ( 1. (K,n));

      now

        

         A1: ( Indices J) = ( Indices Ja) by MATRIX_0: 26;

        let i, j such that

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

        

         A3: ( Indices J) = ( Indices ONE) by MATRIX_0: 26;

        now

          per cases ;

            suppose

             A4: i = j;

            

            hence (Ja * (i,j)) = (L + a) by A2, Def1

            .= ((J * (i,j)) + a) by A2, A1, A4, Def1

            .= ((J * (i,j)) + (a * ( 1_ K)))

            .= ((J * (i,j)) + (a * (ONE * (i,j)))) by A2, A1, A3, A4, MATRIX_1:def 3

            .= ((J * (i,j)) + ((a * ONE) * (i,j))) by A2, A1, A3, MATRIX_3:def 5

            .= ((J + (a * ONE)) * (i,j)) by A2, A1, MATRIX_3:def 3;

          end;

            suppose

             A5: (i + 1) = j;

            then

             A6: i <> j;

            

            thus (Ja * (i,j)) = ( 1_ K) by A2, A5, Def1

            .= (( 1_ K) + ( 0. K)) by RLVECT_1:def 4

            .= ((J * (i,j)) + ( 0. K)) by A2, A1, A5, Def1

            .= ((J * (i,j)) + (a * ( 0. K)))

            .= ((J * (i,j)) + (a * (ONE * (i,j)))) by A2, A1, A3, A6, MATRIX_1:def 3

            .= ((J * (i,j)) + ((a * ONE) * (i,j))) by A2, A1, A3, MATRIX_3:def 5

            .= ((J + (a * ONE)) * (i,j)) by A2, A1, MATRIX_3:def 3;

          end;

            suppose

             A7: i <> j & (i + 1) <> j;

            

            hence (Ja * (i,j)) = ( 0. K) by A2, Def1

            .= (( 0. K) + ( 0. K)) by RLVECT_1:def 4

            .= ((J * (i,j)) + ( 0. K)) by A2, A1, A7, Def1

            .= ((J * (i,j)) + (a * ( 0. K)))

            .= ((J * (i,j)) + (a * (ONE * (i,j)))) by A2, A1, A3, A7, MATRIX_1:def 3

            .= ((J * (i,j)) + ((a * ONE) * (i,j))) by A2, A1, A3, MATRIX_3:def 5

            .= ((J + (a * ONE)) * (i,j)) by A2, A1, MATRIX_3:def 3;

          end;

        end;

        hence (Ja * (i,j)) = ((J + (a * ONE)) * (i,j));

      end;

      hence thesis by MATRIX_0: 27;

    end;

    begin

    definition

      let K;

      let G be FinSequence of ((the carrier of K * ) * );

      :: MATRIXJ2:def2

      attr G is Jordan-block-yielding means

      : Def2: for i st i in ( dom G) holds ex L, n st (G . i) = ( Jordan_block (L,n));

    end

    registration

      let K;

      cluster Jordan-block-yielding for FinSequence of ((the carrier of K * ) * );

      existence

      proof

        reconsider F = ( <*> ((the carrier of K * ) * )) as FinSequence of ((the carrier of K * ) * );

        take F;

        thus thesis;

      end;

    end

    registration

      let K;

      cluster Jordan-block-yielding -> Square-Matrix-yielding for FinSequence of ((the carrier of K * ) * );

      coherence

      proof

        let F be FinSequence of ((the carrier of K * ) * ) such that

         A1: F is Jordan-block-yielding;

        let i;

        assume i in ( dom F);

        then ex L, n st (F . i) = ( Jordan_block (L,n)) by A1;

        hence thesis;

      end;

    end

    definition

      let K;

      mode FinSequence_of_Jordan_block of K is Jordan-block-yielding FinSequence of ((the carrier of K * ) * );

    end

    

     Lm2: {} is FinSequence_of_Jordan_block of K

    proof

      reconsider F = ( <*> ((the carrier of K * ) * )) as FinSequence of ((the carrier of K * ) * );

      for i st i in ( dom F) holds ex L, n st (F . i) = ( Jordan_block (L,n));

      hence thesis by Def2;

    end;

    definition

      let K, L;

      :: MATRIXJ2:def3

      mode FinSequence_of_Jordan_block of L,K -> FinSequence_of_Jordan_block of K means

      : Def3: for i st i in ( dom it ) holds ex n st (it . i) = ( Jordan_block (L,n));

      existence

      proof

        reconsider F = ( <*> {} ) as FinSequence_of_Jordan_block of K by Lm2;

        take F;

        thus thesis;

      end;

    end

    theorem :: MATRIXJ2:10

    

     Th10: {} is FinSequence_of_Jordan_block of L, K

    proof

      reconsider F = ( <*> {} ) as FinSequence_of_Jordan_block of K by Lm2;

      for i st i in ( dom F) holds ex n st (F . i) = ( Jordan_block (L,n));

      hence thesis by Def3;

    end;

    theorem :: MATRIXJ2:11

    

     Th11: <*( Jordan_block (L,n))*> is FinSequence_of_Jordan_block of L, K

    proof

      now

        

         A1: ( dom <*( Jordan_block (L,n))*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

        let i;

        assume i in ( dom <*( Jordan_block (L,n))*>);

        then ( <*( Jordan_block (L,n))*> . 1) = ( Jordan_block (L,n)) & i = 1 by A1, FINSEQ_1:def 8, TARSKI:def 1;

        hence ex a, k st ( <*( Jordan_block (L,n))*> . i) = ( Jordan_block (a,k));

      end;

      then

      reconsider JJ = <*( Jordan_block (L,n))*> as FinSequence_of_Jordan_block of K by Def2;

      now

        

         A2: ( dom JJ) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

        let i;

        assume i in ( dom JJ);

        then (JJ . 1) = ( Jordan_block (L,n)) & i = 1 by A2, FINSEQ_1:def 8, TARSKI:def 1;

        hence ex n st (JJ . i) = ( Jordan_block (L,n));

      end;

      hence thesis by Def3;

    end;

    registration

      let K, L;

      cluster non-empty for FinSequence_of_Jordan_block of L, K;

      existence

      proof

        reconsider JJ = <*( Jordan_block (L,1))*> as FinSequence_of_Jordan_block of L, K by Th11;

        take JJ;

        now

          

           A1: ( dom JJ) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

          let x be object;

          assume x in ( dom JJ);

          then (JJ . 1) = ( Jordan_block (L,1)) & x = 1 by A1, FINSEQ_1:def 8, TARSKI:def 1;

          hence (JJ . x) is non empty by Def1;

        end;

        hence thesis;

      end;

    end

    registration

      let K;

      cluster non-empty for FinSequence_of_Jordan_block of K;

      existence

      proof

        set F = the non-empty FinSequence_of_Jordan_block of ( 1_ K), K;

        take F;

        thus thesis;

      end;

    end

    theorem :: MATRIXJ2:12

    

     Th12: for J be FinSequence_of_Jordan_block of L, K holds (J (+) ( mlt ((( len J) |-> a),( 1. (K,( Len J)))))) is FinSequence_of_Jordan_block of (L + a), K

    proof

      let J be FinSequence_of_Jordan_block of L, K;

      set M = ( mlt ((( len J) |-> a),( 1. (K,( Len J)))));

      

       A1: for i st i in ( dom (J (+) M)) holds ex n st ((J (+) M) . i) = ( Jordan_block ((L + a),n))

      proof

        

         A2: ( dom M) = ( dom ( 1. (K,( Len J)))) by MATRIXJ1:def 9;

        

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

        

         A4: ( dom ( 1. (K,( Len J)))) = ( dom ( Len J)) by MATRIXJ1:def 8;

        let i such that

         A5: i in ( dom (J (+) M));

        

         A6: i in ( dom J) by A5, MATRIXJ1:def 10;

        then

        consider n such that

         A7: (J . i) = ( Jordan_block (L,n)) by Def3;

        take n;

        

         A8: ( len (J . i)) = n by A7, MATRIX_0: 24;

        

         A9: ( dom ( Len J)) = ( dom J) by MATRIXJ1:def 3;

        then

         A10: (( Len J) . i) = ( len (J . i)) by A6, MATRIXJ1:def 3;

        ( len (( len J) |-> a)) = ( len J) by CARD_1:def 7;

        then ( dom (( len J) |-> a)) = ( dom J) by FINSEQ_3: 29;

        

        then ((( len J) |-> a) /. i) = ((( len J) |-> a) . i) by A6, PARTFUN1:def 6

        .= a by A6, A3, FINSEQ_2: 57;

        

        then (M . i) = (a * (( 1. (K,( Len J))) . i)) by A6, A2, A4, A9, MATRIXJ1:def 9

        .= (a * ( 1. (K,n))) by A6, A4, A9, A10, A8, MATRIXJ1:def 8;

        

        hence ((J (+) M) . i) = (( Jordan_block (L,n)) + (a * ( 1. (K,n)))) by A5, A7, MATRIXJ1:def 10

        .= ( Jordan_block ((L + a),n)) by Th9;

      end;

      (J (+) M) is Jordan-block-yielding

      proof

        let i;

        assume i in ( dom (J (+) M));

        then ex n st ((J (+) M) . i) = ( Jordan_block ((L + a),n)) by A1;

        hence thesis;

      end;

      then

      reconsider JM = (J (+) M) as FinSequence_of_Jordan_block of K;

      JM is FinSequence_of_Jordan_block of (L + a), K

      proof

        let i;

        assume i in ( dom JM);

        hence thesis by A1;

      end;

      hence thesis;

    end;

    definition

      let K;

      let J1,J2 be FinSequence_of_Jordan_block of K;

      :: original: ^

      redefine

      func J1 ^ J2 -> FinSequence_of_Jordan_block of K ;

      coherence

      proof

        (J1 ^ J2) is Jordan-block-yielding

        proof

          let i such that

           A1: i in ( dom (J1 ^ J2));

          per cases by A1, FINSEQ_1: 25;

            suppose

             A2: i in ( dom J1);

            then ((J1 ^ J2) . i) = (J1 . i) by FINSEQ_1:def 7;

            hence thesis by A2, Def2;

          end;

            suppose ex n st n in ( dom J2) & i = (( len J1) + n);

            then

            consider k such that

             A3: k in ( dom J2) and

             A4: i = (( len J1) + k);

            ((J1 ^ J2) . i) = (J2 . k) by A3, A4, FINSEQ_1:def 7;

            hence thesis by A3, Def2;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let K;

      let n;

      let J be FinSequence_of_Jordan_block of K;

      :: original: |

      redefine

      func J | n -> FinSequence_of_Jordan_block of K ;

      coherence

      proof

        now

          let i;

          assume i in ( dom (J | n));

          then i in ( dom J) & ((J | n) . i) = (J . i) by FUNCT_1: 47, RELAT_1: 57;

          hence ex L, k st ((J | n) . i) = ( Jordan_block (L,k)) by Def2;

        end;

        hence thesis by Def2;

      end;

      :: original: /^

      redefine

      func J /^ n -> FinSequence_of_Jordan_block of K ;

      coherence

      proof

        now

          let i such that

           A1: i in ( dom (J /^ n));

          (i + n) in ( dom J) by A1, FINSEQ_5: 26;

          then (J . (n + i)) = (J /. (n + i)) & ex L, k st (J . (n + i)) = ( Jordan_block (L,k)) by Def2, PARTFUN1:def 6;

          hence ex L, k st ((J /^ n) . i) = ( Jordan_block (L,k)) by A1, FINSEQ_5: 27;

        end;

        hence thesis by Def2;

      end;

    end

    definition

      let K, L;

      let J1,J2 be FinSequence_of_Jordan_block of L, K;

      :: original: ^

      redefine

      func J1 ^ J2 -> FinSequence_of_Jordan_block of L, K ;

      coherence

      proof

        (J1 ^ J2) is FinSequence_of_Jordan_block of L, K

        proof

          let i such that

           A1: i in ( dom (J1 ^ J2));

          per cases by A1, FINSEQ_1: 25;

            suppose

             A2: i in ( dom J1);

            then ((J1 ^ J2) . i) = (J1 . i) by FINSEQ_1:def 7;

            hence thesis by A2, Def3;

          end;

            suppose ex n st n in ( dom J2) & i = (( len J1) + n);

            then

            consider k such that

             A3: k in ( dom J2) and

             A4: i = (( len J1) + k);

            ((J1 ^ J2) . i) = (J2 . k) by A3, A4, FINSEQ_1:def 7;

            hence thesis by A3, Def3;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let K, L;

      let n;

      let J be FinSequence_of_Jordan_block of L, K;

      :: original: |

      redefine

      func J | n -> FinSequence_of_Jordan_block of L, K ;

      coherence

      proof

        now

          let i;

          assume i in ( dom (J | n));

          then i in ( dom J) & ((J | n) . i) = (J . i) by FUNCT_1: 47, RELAT_1: 57;

          hence ex k st ((J | n) . i) = ( Jordan_block (L,k)) by Def3;

        end;

        hence thesis by Def3;

      end;

      :: original: /^

      redefine

      func J /^ n -> FinSequence_of_Jordan_block of L, K ;

      coherence

      proof

        now

          let i such that

           A1: i in ( dom (J /^ n));

          (i + n) in ( dom J) by A1, FINSEQ_5: 26;

          then (J . (n + i)) = (J /. (n + i)) & ex k st (J . (n + i)) = ( Jordan_block (L,k)) by Def3, PARTFUN1:def 6;

          hence ex k st ((J /^ n) . i) = ( Jordan_block (L,k)) by A1, FINSEQ_5: 27;

        end;

        hence thesis by Def3;

      end;

    end

    begin

    definition

      let K be doubleLoopStr;

      let V be non empty ModuleStr over K;

      let f be Function of V, V;

      :: MATRIXJ2:def4

      attr f is nilpotent means

      : Def4: ex n st for v be Vector of V holds ((f |^ n) . v) = ( 0. V);

    end

    theorem :: MATRIXJ2:13

    

     Th13: for K be doubleLoopStr holds for V be non empty ModuleStr over K holds for f be Function of V, V holds f is nilpotent iff ex n st (f |^ n) = ( ZeroMap (V,V))

    proof

      let K be doubleLoopStr;

      let V be non empty ModuleStr over K;

      let f be Function of V, V;

      hereby

        assume f is nilpotent;

        then

        consider n such that

         A1: for v be Vector of V holds ((f |^ n) . v) = ( 0. V);

        now

          let x be object;

          assume x in ( dom (f |^ n));

          then

          reconsider v = x as Vector of V by FUNCT_2:def 1;

          

          thus ((f |^ n) . x) = ((f |^ n) . v)

          .= ( 0. V) by A1;

        end;

        

        then (f |^ n) = (( dom (f |^ n)) --> ( 0. V)) by FUNCOP_1: 11

        .= (the carrier of V --> ( 0. V)) by FUNCT_2:def 1

        .= ( ZeroMap (V,V)) by GRCAT_1:def 7;

        hence ex n st (f |^ n) = ( ZeroMap (V,V));

      end;

      given n such that

       A2: (f |^ n) = ( ZeroMap (V,V));

      take n;

      let v be Vector of V;

      

      thus ((f |^ n) . v) = ((the carrier of V --> ( 0. V)) . v) by A2, GRCAT_1:def 7

      .= ( 0. V);

    end;

    registration

      let K be doubleLoopStr;

      let V be non empty ModuleStr over K;

      cluster nilpotent for Function of V, V;

      existence

      proof

        take F = ( ZeroMap (V,V));

        (F |^ 1) = F by VECTSP11: 19;

        hence thesis by Th13;

      end;

    end

    registration

      let R be Ring;

      let V be LeftMod of R;

      cluster nilpotent additive homogeneous for Function of V, V;

      existence

      proof

        take F = ( ZeroMap (V,V));

        (F |^ 1) = F by VECTSP11: 19;

        hence thesis by Th13;

      end;

    end

    theorem :: MATRIXJ2:14

    

     Th14: for V be VectSp of K, f be linear-transformation of V, V holds (f | ( ker (f |^ n))) is nilpotent linear-transformation of ( ker (f |^ n)), ( ker (f |^ n))

    proof

      let V be VectSp of K, f be linear-transformation of V, V;

      set KER = ( ker (f |^ n));

      reconsider fK = (f | KER) as linear-transformation of KER, KER by VECTSP11: 28;

      now

        let v be Vector of KER;

        reconsider v1 = v as Vector of V by VECTSP_4: 10;

        

         A1: v1 in KER;

        

        thus ((fK |^ n) . v) = (((f |^ n) | KER) . v) by VECTSP11: 22

        .= ((f |^ n) . v1) by FUNCT_1: 49

        .= ( 0. V) by A1, RANKNULL: 10

        .= ( 0. KER) by VECTSP_4: 11;

      end;

      hence thesis by Def4;

    end;

    definition

      let K be doubleLoopStr;

      let V be non empty ModuleStr over K;

      let f be nilpotent Function of V, V;

      :: MATRIXJ2:def5

      func degree_of_nilpotent f -> Nat means

      : Def5: (f |^ it ) = ( ZeroMap (V,V)) & for k st (f |^ k) = ( ZeroMap (V,V)) holds it <= k;

      existence

      proof

        defpred P[ Nat] means (f |^ $1) = ( ZeroMap (V,V));

        

         A1: ex n st P[n] by Th13;

        consider n such that

         A2: P[n] & for k st P[k] holds n <= k from NAT_1:sch 5( A1);

        take n;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let i, j;

        assume (f |^ i) = ( ZeroMap (V,V)) & (for k st (f |^ k) = ( ZeroMap (V,V)) holds i <= k) & (f |^ j) = ( ZeroMap (V,V)) & for k st (f |^ k) = ( ZeroMap (V,V)) holds j <= k;

        then i <= j & j <= i;

        hence thesis by XXREAL_0: 1;

      end;

    end

    notation

      let K be doubleLoopStr;

      let V be non empty ModuleStr over K;

      let f be nilpotent Function of V, V;

      synonym deg f for degree_of_nilpotent f;

    end

    theorem :: MATRIXJ2:15

    

     Th15: for K be doubleLoopStr holds for V be non empty ModuleStr over K holds for f be nilpotent Function of V, V holds ( deg f) = 0 iff ( [#] V) = {( 0. V)}

    proof

      let K be doubleLoopStr;

      let V be non empty ModuleStr over K;

      let f be nilpotent Function of V, V;

      hereby

        assume

         A1: ( deg f) = 0 ;

        ( [#] V) c= {( 0. V)}

        proof

          let x be object such that

           A2: x in ( [#] V);

          ( id V) = (f |^ 0 ) by VECTSP11: 18

          .= ( ZeroMap (V,V)) by A1, Def5

          .= (the carrier of V --> ( 0. V)) by GRCAT_1:def 7;

          

          then x = ((the carrier of V --> ( 0. V)) . x) by A2, FUNCT_1: 18

          .= ( 0. V) by A2, FUNCOP_1: 7;

          hence thesis by TARSKI:def 1;

        end;

        hence ( [#] V) = {( 0. V)} by ZFMISC_1: 33;

      end;

      assume

       A3: ( [#] V) = {( 0. V)};

      now

        let x be object;

        assume x in ( dom (f |^ 0 ));

        then

        reconsider v = x as Vector of V by FUNCT_2:def 1;

        

        thus ((f |^ 0 ) . x) = (( id V) . v) by VECTSP11: 18

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

      end;

      

      then (f |^ 0 ) = (( dom (f |^ 0 )) --> ( 0. V)) by FUNCOP_1: 11

      .= (the carrier of V --> ( 0. V)) by FUNCT_2:def 1

      .= ( ZeroMap (V,V)) by GRCAT_1:def 7;

      hence thesis by Def5;

    end;

    theorem :: MATRIXJ2:16

    

     Th16: for K be doubleLoopStr holds for V be non empty ModuleStr over K holds for f be nilpotent Function of V, V holds ex v be Vector of V st for i st i < ( deg f) holds ((f |^ i) . v) <> ( 0. V)

    proof

      let K be doubleLoopStr;

      let V be non empty ModuleStr over K;

      let f be nilpotent Function of V, V;

      set D = ( deg f);

      defpred P[ Nat] means 0 < $1 & $1 < D & ((f |^ $1) . ( 0. V)) = ( 0. V);

      assume

       A1: for v be Vector of V holds ex i st i < D & ((f |^ i) . v) = ( 0. V);

      then ex i st i < D & ((f |^ i) . ( 0. V)) = ( 0. V);

      then ( [#] V) <> {( 0. V)} by Th15;

      then

      consider v be object such that

       A2: v in ( [#] V) and

       A3: v <> ( 0. V) by ZFMISC_1: 35;

      reconsider v as Vector of V by A2;

      consider j such that

       A4: j < D and

       A5: ((f |^ j) . v) = ( 0. V) by A1;

      

       A6: (j - j) < (D - j) by A4, XREAL_1: 9;

      j > 0

      proof

        assume j <= 0 ;

        then j = 0 ;

        

        then ( 0. V) = (( id V) . v) by A5, VECTSP11: 18

        .= v by FUNCT_1: 18;

        hence thesis by A3;

      end;

      then

       A7: (D - j) < (D - 0 ) by XREAL_1: 10;

      

       A8: ( dom (f |^ j)) = ( [#] V) by FUNCT_2:def 1;

      

       A9: (D - j) = (D -' j) by A4, XREAL_1: 233;

      then

       A10: D = ((D -' j) + j);

      

       A11: (f |^ D) = ( ZeroMap (V,V)) by Def5

      .= (the carrier of V --> ( 0. V)) by GRCAT_1:def 7;

      

      then ( 0. V) = ((f |^ D) . v)

      .= (((f |^ (D -' j)) * (f |^ j)) . v) by A10, VECTSP11: 20

      .= ((f |^ (D -' j)) . ( 0. V)) by A5, A8, FUNCT_1: 13;

      then

       A12: ex j st P[j] by A9, A6, A7;

      consider m such that

       A13: P[m] & for n be Nat st P[n] holds m <= n from NAT_1:sch 5( A12);

      

       A14: (D -' m) = (D - m) by A13, XREAL_1: 233;

       A15:

      now

        let x be object;

        assume x in ( dom (f |^ (D -' m)));

        then

        reconsider X = x as Vector of V by FUNCT_2:def 1;

        consider k such that

         A16: k < D and

         A17: ((f |^ k) . X) = ( 0. V) by A1;

        defpred F[ Nat] means $1 <= D & ex i st $1 = (k + (i * m));

        k = (k + ( 0 * m));

        then

         A18: ex k st F[k] by A16;

        

         A19: for i be Nat st F[i] holds i <= D;

        consider MAX be Nat such that

         A20: F[MAX] and

         A21: for k be Nat st F[k] holds k <= MAX from NAT_1:sch 6( A19, A18);

        consider I be Nat such that

         A22: MAX = (k + (I * m)) by A20;

        now

          per cases by A20, XXREAL_0: 1;

            suppose

             A23: MAX = D;

            then I <> 0 by A16, A22;

            then

            reconsider I1 = (I - 1) as Nat by NAT_1: 20;

            (D -' m) = (k + (I1 * m)) by A14, A22, A23;

            hence ((f |^ (D -' m)) . X) = ( 0. V) by A13, A17, VECTSP11: 21;

          end;

            suppose

             A24: MAX < D;

            MAX <> 0

            proof

              assume

               A25: MAX = 0 ;

              then k = 0 by A22;

              then (k + (1 * m)) < D by A13;

              hence thesis by A13, A21, A25;

            end;

            then

             A26: (D - MAX) < (D - 0 ) by XREAL_1: 10;

            

             A27: ((f |^ MAX) . X) = ( 0. V) & ( dom (f |^ MAX)) = the carrier of V by A13, A17, A22, FUNCT_2:def 1, VECTSP11: 21;

            

             A28: (MAX - MAX) < (D - MAX) by A24, XREAL_1: 9;

            

             A29: (D - MAX) = (D -' MAX) by A24, XREAL_1: 233;

            then

             A30: D = ((D -' MAX) + MAX);

            ( 0. V) = ((f |^ D) . X) by A11

            .= (((f |^ (D -' MAX)) * (f |^ MAX)) . X) by A30, VECTSP11: 20

            .= ((f |^ (D -' MAX)) . ( 0. V)) by A27, FUNCT_1: 13;

            then m <= (D -' MAX) by A13, A29, A28, A26;

            then

             A31: (MAX + m) <= (MAX + (D - MAX)) by A29, XREAL_1: 6;

            (MAX + m) = (k + ((I + 1) * m)) by A22;

            then (MAX + m) <= (MAX + 0 ) by A21, A31;

            hence ((f |^ (D -' m)) . X) = ( 0. V) by A13, XREAL_1: 6;

          end;

        end;

        hence ((f |^ (D -' m)) . x) = ( 0. V);

      end;

      

       A32: (D - m) < (D - 0 ) by A13, XREAL_1: 10;

      ( dom (f |^ (D -' m))) = ( [#] V) by FUNCT_2:def 1;

      

      then (f |^ (D -' m)) = (the carrier of V --> ( 0. V)) by A15, FUNCOP_1: 11

      .= ( ZeroMap (V,V)) by GRCAT_1:def 7;

      hence contradiction by A14, A32, Def5;

    end;

    theorem :: MATRIXJ2:17

    

     Th17: for K be Field, V be VectSp of K, W be Subspace of V holds for f be nilpotent Function of V, V st (f | W) is Function of W, W holds (f | W) is nilpotent Function of W, W

    proof

      let K be Field, V be VectSp of K, W be Subspace of V;

      let f be nilpotent Function of V, V;

      assume (f | W) is Function of W, W;

      then

      reconsider fW = (f | W) as Function of W, W;

      consider n such that

       A1: (f |^ n) = ( ZeroMap (V,V)) by Th13;

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

      then

       A2: ( [#] W) = (( [#] V) /\ ( [#] W)) by XBOOLE_1: 28;

      (fW |^ n) = (( ZeroMap (V,V)) | W) by A1, VECTSP11: 22

      .= ((the carrier of V --> ( 0. V)) | ( [#] W)) by GRCAT_1:def 7

      .= ((the carrier of V /\ ( [#] W)) --> ( 0. V)) by FUNCOP_1: 12

      .= (the carrier of W --> ( 0. W)) by A2, VECTSP_4: 11

      .= ( ZeroMap (W,W)) by GRCAT_1:def 7;

      hence thesis by Th13;

    end;

    theorem :: MATRIXJ2:18

    

     Th18: for K be Field, V be VectSp of K, W be Subspace of V holds for f be nilpotent linear-transformation of V, V, fI be nilpotent Function of ( im (f |^ n)), ( im (f |^ n)) st fI = (f | ( im (f |^ n))) & n <= ( deg f) holds (( deg fI) + n) = ( deg f)

    proof

      let K be Field, V be VectSp of K, W be Subspace of V;

      let f be nilpotent linear-transformation of V, V;

      set IM = ( im (f |^ n));

      let fI be nilpotent Function of IM, IM;

      assume

       A1: fI = (f | IM);

      set D = ( deg f);

      assume n <= D;

      then

      reconsider Dn = (D - n) as Element of NAT by NAT_1: 21;

       A2:

      now

        let x be object;

        assume x in ( dom (fI |^ Dn));

        then

        reconsider X = x as Vector of IM by FUNCT_2:def 1;

        reconsider v = X as Vector of V by VECTSP_4: 10;

        

         A3: ( dom (f |^ n)) = the carrier of V by FUNCT_2:def 1;

        X in IM;

        then

        consider w be Element of V such that

         A4: v = ((f |^ n) . w) by RANKNULL: 13;

        ((f |^ D) . w) = (( ZeroMap (V,V)) . w) by Def5

        .= ((the carrier of V --> ( 0. V)) . w) by GRCAT_1:def 7

        .= ( 0. V);

        

        hence ( 0. IM) = ((f |^ (Dn + n)) . w) by VECTSP_4: 11

        .= (((f |^ Dn) * (f |^ n)) . w) by VECTSP11: 20

        .= ((f |^ Dn) . v) by A4, A3, FUNCT_1: 13

        .= (((f |^ Dn) | IM) . X) by FUNCT_1: 49

        .= ((fI |^ Dn) . x) by A1, VECTSP11: 22;

      end;

      ( dom (fI |^ Dn)) = ( [#] IM) by FUNCT_2:def 1;

      

      then (fI |^ Dn) = (the carrier of IM --> ( 0. IM)) by A2, FUNCOP_1: 11

      .= ( ZeroMap (IM,IM)) by GRCAT_1:def 7;

      then

       A5: ( deg fI) <= Dn by Def5;

      ( deg fI) = Dn

      proof

        set DI = ( deg fI);

        

         A6: ( dom (f |^ n)) = the carrier of V by FUNCT_2:def 1;

        assume DI <> Dn;

        then DI < Dn by A5, XXREAL_0: 1;

        then

         A7: (DI + n) < (Dn + n) by XREAL_1: 6;

        consider v be Vector of V such that

         A8: for i st i < D holds ((f |^ i) . v) <> ( 0. V) by Th16;

        ((f |^ n) . v) in IM by RANKNULL: 13;

        then

         A9: ((f |^ n) . v) in the carrier of IM;

        (fI |^ DI) = ( ZeroMap (IM,IM)) by Def5

        .= (the carrier of IM --> ( 0. IM)) by GRCAT_1:def 7;

        

        then ( 0. IM) = ((fI |^ DI) . ((f |^ n) . v)) by A9, FUNCOP_1: 7

        .= (((f |^ DI) | IM) . ((f |^ n) . v)) by A1, VECTSP11: 22

        .= ((f |^ DI) . ((f |^ n) . v)) by A9, FUNCT_1: 49

        .= (((f |^ DI) * (f |^ n)) . v) by A6, FUNCT_1: 13

        .= ((f |^ (DI + n)) . v) by VECTSP11: 20;

        hence thesis by A7, A8, VECTSP_4: 11;

      end;

      hence thesis;

    end;

    reserve V1,V2 for finite-dimensional VectSp of K,

W1,W2 for Subspace of V1,

U1,U2 for Subspace of V2,

b1 for OrdBasis of V1,

B1 for FinSequence of V1,

b2 for OrdBasis of V2,

B2 for FinSequence of V2,

bw1 for OrdBasis of W1,

bw2 for OrdBasis of W2,

Bu1 for FinSequence of U1,

Bu2 for FinSequence of U2;

    theorem :: MATRIXJ2:19

    

     Th19: for M be Matrix of ( len b1), ( len B2), K, M1 be Matrix of ( len bw1), ( len Bu1), K, M2 be Matrix of ( len bw2), ( len Bu2), K st b1 = (bw1 ^ bw2) & B2 = (Bu1 ^ Bu2) & M = ( block_diagonal ( <*M1, M2*>,( 0. K))) & ( width M1) = ( len Bu1) & ( width M2) = ( len Bu2) holds (i in ( dom bw1) implies (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = (( Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i))) & (i in ( dom bw2) implies (( Mx2Tran (M,b1,B2)) . (b1 /. (i + ( len bw1)))) = (( Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i)))

    proof

      let M be Matrix of ( len b1), ( len B2), K, M1 be Matrix of ( len bw1), ( len Bu1), K, M2 be Matrix of ( len bw2), ( len Bu2), K such that

       A1: b1 = (bw1 ^ bw2) and

       A2: B2 = (Bu1 ^ Bu2) and

       A3: M = ( block_diagonal ( <*M1, M2*>,( 0. K))) and

       A4: ( width M1) = ( len Bu1) and

       A5: ( width M2) = ( len Bu2);

      

       A6: ( dom bw1) c= ( dom b1) by A1, FINSEQ_1: 26;

      ( rng Bu2) c= the carrier of U2 & the carrier of U2 c= the carrier of V2 by FINSEQ_1:def 4, VECTSP_4:def 2;

      then

       A7: ( rng Bu2) c= the carrier of V2;

      ( rng Bu1) c= the carrier of U1 & the carrier of U1 c= the carrier of V2 by FINSEQ_1:def 4, VECTSP_4:def 2;

      then ( rng Bu1) c= the carrier of V2;

      then

      reconsider bu1 = Bu1, bu2 = Bu2 as FinSequence of V2 by A7, FINSEQ_1:def 4;

      set F1 = ( Mx2Tran (M1,bw1,Bu1));

      set F = ( Mx2Tran (M,b1,B2));

      

       A8: ( dom b1) = ( Seg ( len b1)) & ( len ( 1. (K,( len b1)))) = ( len b1) by FINSEQ_1:def 3, MATRIX_0: 24;

      

       A9: ( dom ( 1. (K,( len bw1)))) = ( Seg ( len ( 1. (K,( len bw1))))) by FINSEQ_1:def 3;

      

       A10: ( dom ( 1. (K,( len b1)))) = ( Seg ( len ( 1. (K,( len b1))))) by FINSEQ_1:def 3;

      set BI = (( len bw1) + i);

      

       A11: ( dom bw2) = ( Seg ( len bw2)) & ( len ( 1. (K,( len bw2)))) = ( len bw2) by FINSEQ_1:def 3, MATRIX_0: 24;

      set F2 = ( Mx2Tran (M2,bw2,Bu2));

      

       A12: ( width ( 1. (K,( len b1)))) = ( len b1) by MATRIX_0: 24;

      

       A13: ( len ( Line (M2,i))) = ( width M2) & ( len (( width M1) |-> ( 0. K))) = ( width M1) by CARD_1:def 7;

      

       A14: ( dom bw1) = ( Seg ( len bw1)) & ( len ( 1. (K,( len bw1)))) = ( len bw1) by FINSEQ_1:def 3, MATRIX_0: 24;

      

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

      

       A16: ( len M1) = ( len bw1) by MATRIX_0:def 2;

      then

       A17: ( dom M1) = ( dom bw1) by FINSEQ_3: 29;

      thus i in ( dom bw1) implies (F . (b1 /. i)) = (F1 . (bw1 /. i))

      proof

        

         A18: ( len ( Line (M1,i))) = ( width M1) & ( len (( width M2) |-> ( 0. K))) = ( width M2) by CARD_1:def 7;

        assume

         A19: i in ( dom bw1);

        then

         A20: ( Line (M,i)) = (( Line (M1,i)) ^ (( width M2) |-> ( 0. K))) by A3, A17, MATRIXJ1: 23;

        

        thus (F . (b1 /. i)) = ( Sum ( lmlt (( Line ((( LineVec2Mx ((b1 /. i) |-- b1)) * M),1)),B2))) by MATRLIN2:def 3

        .= ( Sum ( lmlt (( Line ((( LineVec2Mx ( Line (( 1. (K,( len b1))),i))) * M),1)),B2))) by A6, A19, MATRLIN2: 19

        .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line ((( 1. (K,( len b1))) * M),i))),1)),B2))) by A6, A8, A15, A10, A19, MATRIX_0: 24, MATRLIN2: 35

        .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line (M,i))),1)),B2))) by A15, MATRIXR2: 68

        .= ( Sum ( lmlt (( Line (M,i)),B2))) by MATRIX15: 25

        .= ( Sum (( lmlt (( Line (M1,i)),bu1)) ^ ( lmlt ((( width M2) |-> ( 0. K)),bu2)))) by A2, A4, A5, A20, A18, MATRLIN2: 9

        .= (( Sum ( lmlt (( Line (M1,i)),bu1))) + ( Sum ( lmlt ((( width M2) |-> ( 0. K)),bu2)))) by RLVECT_1: 41

        .= (( Sum ( lmlt (( Line (M1,i)),bu1))) + (( 0. K) * ( Sum bu2))) by A5, MATRLIN2: 11

        .= (( Sum ( lmlt (( Line (M1,i)),bu1))) + ( 0. V2)) by VECTSP_1: 14

        .= ( Sum ( lmlt (( Line (M1,i)),bu1))) by RLVECT_1:def 4

        .= ( Sum ( lmlt (( Line (M1,i)),Bu1))) by MATRLIN2: 14, MATRLIN2: 15

        .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line (M1,i))),1)),Bu1))) by MATRIX15: 25

        .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line ((( 1. (K,( len bw1))) * M1),i))),1)),Bu1))) by A16, MATRIXR2: 68

        .= ( Sum ( lmlt (( Line ((( LineVec2Mx ( Line (( 1. (K,( len bw1))),i))) * M1),1)),Bu1))) by A14, A9, A16, A19, MATRIX_0: 24, MATRLIN2: 35

        .= ( Sum ( lmlt (( Line ((( LineVec2Mx ((bw1 /. i) |-- bw1)) * M1),1)),Bu1))) by A19, MATRLIN2: 19

        .= (F1 . (bw1 /. i)) by MATRLIN2:def 3;

      end;

      

       A21: ( dom ( 1. (K,( len bw2)))) = ( Seg ( len ( 1. (K,( len bw2))))) by FINSEQ_1:def 3;

      assume

       A22: i in ( dom bw2);

      then

       A23: BI in ( dom b1) by A1, FINSEQ_1: 28;

      

       A24: ( len M2) = ( len bw2) by MATRIX_0:def 2;

      then ( dom M2) = ( dom bw2) by FINSEQ_3: 29;

      then

       A25: ( Line (M,BI)) = ((( width M1) |-> ( 0. K)) ^ ( Line (M2,i))) by A3, A16, A22, MATRIXJ1: 23;

      

      thus (F . (b1 /. (i + ( len bw1)))) = ( Sum ( lmlt (( Line ((( LineVec2Mx ((b1 /. BI) |-- b1)) * M),1)),B2))) by MATRLIN2:def 3

      .= ( Sum ( lmlt (( Line ((( LineVec2Mx ( Line (( 1. (K,( len b1))),BI))) * M),1)),B2))) by A23, MATRLIN2: 19

      .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line ((( 1. (K,( len b1))) * M),BI))),1)),B2))) by A1, A12, A8, A15, A10, A22, FINSEQ_1: 28, MATRLIN2: 35

      .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line (M,BI))),1)),B2))) by A15, MATRIXR2: 68

      .= ( Sum ( lmlt (( Line (M,BI)),B2))) by MATRIX15: 25

      .= ( Sum (( lmlt ((( width M1) |-> ( 0. K)),bu1)) ^ ( lmlt (( Line (M2,i)),bu2)))) by A2, A4, A5, A25, A13, MATRLIN2: 9

      .= (( Sum ( lmlt ((( width M1) |-> ( 0. K)),bu1))) + ( Sum ( lmlt (( Line (M2,i)),bu2)))) by RLVECT_1: 41

      .= ((( 0. K) * ( Sum bu1)) + ( Sum ( lmlt (( Line (M2,i)),bu2)))) by A4, MATRLIN2: 11

      .= (( 0. V2) + ( Sum ( lmlt (( Line (M2,i)),bu2)))) by VECTSP_1: 14

      .= ( Sum ( lmlt (( Line (M2,i)),bu2))) by RLVECT_1:def 4

      .= ( Sum ( lmlt (( Line (M2,i)),Bu2))) by MATRLIN2: 14, MATRLIN2: 15

      .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line (M2,i))),1)),Bu2))) by MATRIX15: 25

      .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line ((( 1. (K,( len bw2))) * M2),i))),1)),Bu2))) by A24, MATRIXR2: 68

      .= ( Sum ( lmlt (( Line ((( LineVec2Mx ( Line (( 1. (K,( len bw2))),i))) * M2),1)),Bu2))) by A11, A21, A24, A22, MATRIX_0: 24, MATRLIN2: 35

      .= ( Sum ( lmlt (( Line ((( LineVec2Mx ((bw2 /. i) |-- bw2)) * M2),1)),Bu2))) by A22, MATRLIN2: 19

      .= (F2 . (bw2 /. i)) by MATRLIN2:def 3;

    end;

    theorem :: MATRIXJ2:20

    

     Th20: for M be Matrix of ( len b1), ( len B2), K, F be FinSequence_of_Matrix of K st M = ( block_diagonal (F,( 0. K))) holds for i, m st i in ( dom b1) & m = ( min (( Len F),i)) holds (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = ( Sum ( lmlt (( Line ((F . m),(i -' ( Sum ( Len (F | (m -' 1))))))),((B2 | ( Sum ( Width (F | m)))) /^ ( Sum ( Width (F | (m -' 1)))))))) & ( len ((B2 | ( Sum ( Width (F | m)))) /^ ( Sum ( Width (F | (m -' 1)))))) = ( width (F . m))

    proof

      set ONE = ( 1. (K,( len b1)));

      let M be Matrix of ( len b1), ( len B2), K, F be FinSequence_of_Matrix of K such that

       A1: M = ( block_diagonal (F,( 0. K)));

      

       A2: ( width M) = ( Sum ( Width F)) by A1, MATRIXJ1:def 5;

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

      then

       A3: ( dom ONE) = ( dom b1) by FINSEQ_3: 29;

      set L = ( Len F);

      set W = ( Width F);

      let i, m such that

       A4: i in ( dom b1) and

       A5: m = ( min (( Len F),i));

      

       A6: 1 <= i & i <= ( len b1) by A4, FINSEQ_3: 25;

      then

       A7: ( len M) = ( len b1) by MATRIX_0: 23;

      set Fm = (F . m);

      set Wm1 = ( Sum (W | (m -' 1)));

      

       A8: ( len (( Sum (W | (m -' 1))) |-> ( 0. K))) = ( Sum (W | (m -' 1))) & ( len ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1)))))))) = ( width Fm) by CARD_1:def 7;

      set Wm = ( Sum (W | m));

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

      then

       A9: ( Sum W) = (Wm + ( Sum (W /^ m))) by RVSUM_1: 75;

      

      then

       A10: (( Sum W) -' Wm) = (( Sum W) - Wm) by NAT_1: 11, XREAL_1: 233

      .= ( Sum (W /^ m)) by A9;

      then

       A11: ( len ((( Sum W) -' ( Sum (W | m))) |-> ( 0. K))) = ( Sum (W /^ m)) by CARD_1:def 7;

      

       A12: ( dom b1) = ( Seg ( len b1)) & ( len M) = ( Sum ( Len F)) by A1, FINSEQ_1:def 3, MATRIXJ1:def 5;

      then

       A13: m in ( dom ( Len F)) by A4, A5, A7, MATRIXJ1:def 1;

      then

       A14: 1 <= m by FINSEQ_3: 25;

      reconsider wF = ( width Fm) as Element of NAT by ORDINAL1:def 12;

      ( dom L) = ( dom F) & ( dom W) = ( dom F) by MATRIXJ1:def 3, MATRIXJ1:def 4;

      then m <= ( len W) & (W . m) = ( width Fm) by A13, FINSEQ_3: 25, MATRIXJ1:def 4;

      then W = (((W | (m -' 1)) ^ <*( width Fm)*>) ^ (W /^ m)) by A5, A14, POLYNOM4: 1;

      

      then

       A15: ( Sum W) = (( Sum ((W | (m -' 1)) ^ <*wF*>)) + ( Sum (W /^ m))) by RVSUM_1: 75

      .= ((Wm1 + ( width Fm)) + ( Sum (W /^ m))) by RVSUM_1: 74;

      then

       A16: ( len ((( Sum (W | (m -' 1))) |-> ( 0. K)) ^ ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1))))))))) = Wm by A9, CARD_1:def 7;

      set B2W = (B2 | Wm);

      

       A17: (B2W /^ Wm1) = ((B2 | ( Sum ( Width (F | m)))) /^ Wm1) by MATRIXJ1: 21

      .= ((B2 | ( Sum ( Width (F | m)))) /^ ( Sum ( Width (F | (m -' 1))))) by MATRIXJ1: 21;

      

       A18: ( width M) = ( len B2) by A6, MATRIX_0: 23;

      then

       A19: ( len B2W) = Wm by A2, A9, FINSEQ_1: 59, NAT_1: 11;

      ( Sum W) = (Wm1 + (( width Fm) + ( Sum (W /^ m)))) by A15;

      then

       A20: ( len (B2 | Wm1)) = Wm1 by A2, A18, FINSEQ_1: 59, NAT_1: 11;

      Wm >= Wm1 by A9, A15, NAT_1: 11;

      then ( Seg Wm1) c= ( Seg Wm) by FINSEQ_1: 5;

      then (B2W | Wm1) = (B2 | Wm1) by RELAT_1: 74;

      then

       A21: B2W = ((B2 | Wm1) ^ (B2W /^ Wm1)) by RFINSEQ: 8;

      then

       A22: ( len B2W) = (( len (B2 | Wm1)) + ( len (B2W /^ Wm1))) by FINSEQ_1: 22;

      

       A23: B2 = (B2W ^ (B2 /^ Wm)) by RFINSEQ: 8;

      then

       A24: ( len B2) = (( len B2W) + ( len (B2 /^ Wm))) by FINSEQ_1: 22;

      (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = ( Sum ( lmlt (( Line ((( LineVec2Mx ((b1 /. i) |-- b1)) * M),1)),B2))) by MATRLIN2:def 3

      .= ( Sum ( lmlt (( Line ((( LineVec2Mx ( Line (ONE,i))) * M),1)),B2))) by A4, MATRLIN2: 19

      .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line ((ONE * M),i))),1)),B2))) by A4, A6, A3, A7, MATRIX_0: 23, MATRLIN2: 35

      .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line (M,i))),1)),B2))) by A7, MATRIXR2: 68

      .= ( Sum ( lmlt (( Line (M,i)),B2))) by MATRIX15: 25

      .= ( Sum ( lmlt ((((( Sum ( Width (F | (m -' 1)))) |-> ( 0. K)) ^ ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1)))))))) ^ ((( Sum W) -' ( Sum ( Width (F | m)))) |-> ( 0. K))),B2))) by A1, A4, A5, A7, A12, MATRIXJ1: 37

      .= ( Sum ( lmlt ((((( Sum (W | (m -' 1))) |-> ( 0. K)) ^ ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1)))))))) ^ ((( Sum W) -' ( Sum ( Width (F | m)))) |-> ( 0. K))),B2))) by MATRIXJ1: 21

      .= ( Sum ( lmlt ((((( Sum (W | (m -' 1))) |-> ( 0. K)) ^ ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1)))))))) ^ ((( Sum W) -' ( Sum (W | m))) |-> ( 0. K))),B2))) by MATRIXJ1: 21

      .= ( Sum (( lmlt (((( Sum (W | (m -' 1))) |-> ( 0. K)) ^ ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1)))))))),B2W)) ^ ( lmlt (((( Sum W) -' ( Sum (W | m))) |-> ( 0. K)),(B2 /^ Wm))))) by A2, A18, A9, A23, A24, A19, A11, A16, MATRLIN2: 9

      .= (( Sum ( lmlt (((( Sum (W | (m -' 1))) |-> ( 0. K)) ^ ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1)))))))),B2W))) + ( Sum ( lmlt (((( Sum W) -' ( Sum (W | m))) |-> ( 0. K)),(B2 /^ Wm))))) by RLVECT_1: 41

      .= (( Sum ( lmlt (((( Sum (W | (m -' 1))) |-> ( 0. K)) ^ ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1)))))))),B2W))) + (( 0. K) * ( Sum (B2 /^ Wm)))) by A2, A18, A9, A10, A24, A19, MATRLIN2: 11

      .= (( Sum ( lmlt (((( Sum (W | (m -' 1))) |-> ( 0. K)) ^ ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1)))))))),B2W))) + ( 0. V2)) by VECTSP_1: 14

      .= ( Sum ( lmlt (((( Sum (W | (m -' 1))) |-> ( 0. K)) ^ ( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1)))))))),B2W))) by RLVECT_1:def 4

      .= ( Sum (( lmlt ((( Sum (W | (m -' 1))) |-> ( 0. K)),(B2 | Wm1))) ^ ( lmlt (( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1))))))),(B2W /^ Wm1))))) by A9, A15, A19, A21, A22, A20, A8, MATRLIN2: 9

      .= (( Sum ( lmlt ((( Sum (W | (m -' 1))) |-> ( 0. K)),(B2 | Wm1)))) + ( Sum ( lmlt (( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1))))))),(B2W /^ Wm1))))) by RLVECT_1: 41

      .= ((( 0. K) * ( Sum (B2 | Wm1))) + ( Sum ( lmlt (( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1))))))),(B2W /^ Wm1))))) by A20, MATRLIN2: 11

      .= (( 0. V2) + ( Sum ( lmlt (( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1))))))),(B2W /^ Wm1))))) by VECTSP_1: 14

      .= ( Sum ( lmlt (( Line (Fm,(i -' ( Sum ( Len (F | (m -' 1))))))),(B2W /^ Wm1)))) by RLVECT_1:def 4;

      hence thesis by A9, A15, A19, A22, A20, A17;

    end;

    theorem :: MATRIXJ2:21

    

     Th21: ( len B1) in ( dom B1) implies ( Sum ( lmlt (( Line (( Jordan_block (L,( len B1))),( len B1))),B1))) = (L * (B1 /. ( len B1)))

    proof

      set N = ( len B1);

      assume

       A1: N in ( dom B1);

      set J = ( Jordan_block (L,N));

      set ONE = ( 1. (K,N));

      

      thus ( Sum ( lmlt (( Line (J,N)),B1))) = ( Sum ( lmlt ((L * ( Line (ONE,N))),B1))) by Th5

      .= (L * ( Sum ( lmlt (( Line (ONE,N)),B1)))) by MATRLIN2: 13

      .= (L * (B1 /. N)) by A1, MATRLIN2: 16;

    end;

    theorem :: MATRIXJ2:22

    

     Th22: i in ( dom B1) & i <> ( len B1) implies ( Sum ( lmlt (( Line (( Jordan_block (L,( len B1))),i)),B1))) = ((L * (B1 /. i)) + (B1 /. (i + 1)))

    proof

      assume that

       A1: i in ( dom B1) and

       A2: i <> ( len B1);

      set N = ( len B1);

      

       A3: ( dom B1) = ( Seg N) by FINSEQ_1:def 3;

      i <= N by A1, FINSEQ_3: 25;

      then i < N by A2, XXREAL_0: 1;

      then 1 <= (i + 1) & (i + 1) <= N by NAT_1: 11, NAT_1: 13;

      then

       A4: (i + 1) in ( dom B1) by A3;

      set ONE = ( 1. (K,N));

      

       A5: ( len ( Line (ONE,(i + 1)))) = ( width ONE) by CARD_1:def 7;

      ( width ONE) = N by MATRIX_0: 24;

      then

       A6: ( dom ( Line (ONE,(i + 1)))) = ( dom B1) by A5, FINSEQ_3: 29;

      ( len (L * ( Line (ONE,i)))) = ( len ( Line (ONE,i))) & ( len ( Line (ONE,i))) = ( width ONE) by CARD_1:def 7, MATRIXR1: 16;

      then ( dom (L * ( Line (ONE,i)))) = ( dom ( Line (ONE,(i + 1)))) by A5, FINSEQ_3: 29;

      then

       A7: ( dom ( lmlt ((L * ( Line (ONE,i))),B1))) = ( dom B1) by A6, MATRLIN: 12;

      ( dom ( lmlt (( Line (ONE,(i + 1))),B1))) = ( dom B1) by A6, MATRLIN: 12;

      then

       A8: ( len ( lmlt ((L * ( Line (ONE,i))),B1))) = ( len ( lmlt (( Line (ONE,(i + 1))),B1))) by A7, FINSEQ_3: 29;

      

      thus ( Sum ( lmlt (( Line (( Jordan_block (L,( len B1))),i)),B1))) = ( Sum ( lmlt (((L * ( Line (ONE,i))) + ( Line (ONE,(i + 1)))),B1))) by A1, A2, A3, Th4

      .= ( Sum (( lmlt ((L * ( Line (ONE,i))),B1)) + ( lmlt (( Line (ONE,(i + 1))),B1)))) by MATRLIN2: 7

      .= (( Sum ( lmlt ((L * ( Line (ONE,i))),B1))) + ( Sum ( lmlt (( Line (ONE,(i + 1))),B1)))) by A8, MATRLIN2: 10

      .= ((L * ( Sum ( lmlt (( Line (ONE,i)),B1)))) + ( Sum ( lmlt (( Line (ONE,(i + 1))),B1)))) by MATRLIN2: 13

      .= ((L * (B1 /. i)) + ( Sum ( lmlt (( Line (ONE,(i + 1))),B1)))) by A1, MATRLIN2: 16

      .= ((L * (B1 /. i)) + (B1 /. (i + 1))) by A4, MATRLIN2: 16;

    end;

    theorem :: MATRIXJ2:23

    

     Th23: for M be Matrix of ( len b1), ( len B2), K st M = ( Jordan_block (L,n)) holds for i st i in ( dom b1) holds (i = ( len b1) implies (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = (L * (B2 /. i))) & (i <> ( len b1) implies (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = ((L * (B2 /. i)) + (B2 /. (i + 1))))

    proof

      set ONE = ( 1. (K,( len b1)));

      set J = ( Jordan_block (L,n));

      let M be Matrix of ( len b1), ( len B2), K such that

       A1: M = ( Jordan_block (L,n));

      

       A2: ( len M) = n by A1, MATRIX_0: 24;

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

      then

       A3: ( dom ONE) = ( dom b1) by FINSEQ_3: 29;

      let i such that

       A4: i in ( dom b1);

      

       A5: ( len M) = ( len b1) by MATRIX_0: 25;

      

       A6: (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = ( Sum ( lmlt (( Line ((( LineVec2Mx ((b1 /. i) |-- b1)) * M),1)),B2))) by MATRLIN2:def 3

      .= ( Sum ( lmlt (( Line ((( LineVec2Mx ( Line (ONE,i))) * M),1)),B2))) by A4, MATRLIN2: 19

      .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line ((ONE * M),i))),1)),B2))) by A4, A3, A5, MATRIX_0: 24, MATRLIN2: 35

      .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line (M,i))),1)),B2))) by A5, MATRIXR2: 68

      .= ( Sum ( lmlt (( Line (M,i)),B2))) by MATRIX15: 25;

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

      then n <> 0 by A4, A5, A2;

      then

       A7: ( width J) = n & ( width J) = ( len B2) by A1, A5, A2, MATRIX_0: 20;

      then ( dom B2) = ( dom b1) by A5, A2, FINSEQ_3: 29;

      hence thesis by A1, A4, A5, A2, A7, A6, Th21, Th22;

    end;

    theorem :: MATRIXJ2:24

    

     Th24: for J be FinSequence_of_Jordan_block of L, K holds for M be Matrix of ( len b1), ( len B2), K st M = ( block_diagonal (J,( 0. K))) holds for i, m st i in ( dom b1) & m = ( min (( Len J),i)) holds (i = ( Sum ( Len (J | m))) implies (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = (L * (B2 /. i))) & (i <> ( Sum ( Len (J | m))) implies (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = ((L * (B2 /. i)) + (B2 /. (i + 1))))

    proof

      let J be FinSequence_of_Jordan_block of L, K;

      let M be Matrix of ( len b1), ( len B2), K such that

       A1: M = ( block_diagonal (J,( 0. K)));

      

       A2: ( dom b1) = ( Seg ( len b1)) & ( len M) = ( Sum ( Len J)) by A1, FINSEQ_1:def 3, MATRIXJ1:def 5;

      let i, m such that

       A3: i in ( dom b1) and

       A4: m = ( min (( Len J),i));

      set Sm = ( Sum ( Len (J | m)));

      

       A5: 1 <= i by A3, FINSEQ_3: 25;

      

       A6: i <= ( len b1) by A3, FINSEQ_3: 25;

      then

       A7: ( len M) = ( len b1) by A5, MATRIX_0: 23;

      then

       A8: m in ( dom ( Len J)) by A3, A4, A2, MATRIXJ1:def 1;

      then

       A9: (( Len J) . m) = ( len (J . m)) by MATRIXJ1:def 3;

      set S = ( Sum ( Len (J | (m -' 1))));

      set iS = (i -' S);

      set BBB = ((B2 | ( Sum ( Width (J | m)))) /^ ( Sum ( Width (J | (m -' 1)))));

      

       A10: (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = ( Sum ( lmlt (( Line ((J . m),iS)),BBB))) by A1, A3, A4, Th20;

      

       A11: ( width M) = ( Sum ( Width J)) by A1, MATRIXJ1:def 5;

      

       A12: ( len BBB) = ( width (J . m)) by A1, A3, A4, Th20;

      

       A13: (( Len J) | m) = ( Len (J | m)) by MATRIXJ1: 17;

      then

       A14: i <= Sm by A3, A4, A7, A2, MATRIXJ1:def 1;

      

       A15: (( Len J) | (m -' 1)) = ( Len (J | (m -' 1))) by MATRIXJ1: 17;

      then S < i by A3, A4, A7, A2, MATRIXJ1: 7;

      then

       A16: iS = (i - S) by XREAL_1: 233;

      

       A17: (m -' 1) = (m - 1) by A3, A4, A7, A2, MATRIXJ1: 7;

      then (( Len J) | ((m -' 1) + 1)) = (( Len (J | (m -' 1))) ^ <*(( Len J) . m)*>) by A15, A8, FINSEQ_5: 10;

      then

       A18: Sm = (S + ( len (J . m))) by A13, A17, A9, RVSUM_1: 74;

      then (S + iS) <= (S + ( len (J . m))) by A3, A4, A13, A7, A2, A16, MATRIXJ1:def 1;

      then

       A19: iS <= ( len (J . m)) by XREAL_1: 6;

      ( dom ( Len J)) = ( dom J) by MATRIXJ1:def 3;

      then

      consider n such that

       A20: (J . m) = ( Jordan_block (L,n)) by A8, Def3;

      m in NAT & m <= ( len ( Len J)) by A8, FINSEQ_3: 25;

      then Sm <= ( Sum (( Len J) | ( len ( Len J)))) by A13, POLYNOM3: 18;

      then

       A21: Sm <= ( Sum ( Len J)) by FINSEQ_1: 58;

      

       A22: ( Width J) = ( Len J) by MATRIXJ1: 46;

      then

       A23: (( Len J) . m) = ( width (J . m)) by A8, MATRIXJ1:def 4;

      ( width M) = ( len B2) by A5, A6, MATRIX_0: 23;

      then

       A24: ( len (B2 | Sm)) = Sm by A22, A11, A21, FINSEQ_1: 59;

      then

       A25: i in ( dom (B2 | Sm)) by A5, A14, FINSEQ_3: 25;

      

       A26: ( len (J . m)) = n by A20, MATRIX_0: 24;

      iS <> 0 by A3, A4, A15, A7, A2, A16, MATRIXJ1: 7;

      then 1 <= iS by NAT_1: 14;

      then

       A27: iS in ( dom BBB) by A12, A9, A23, A19, FINSEQ_3: 25;

      

      then

       A28: (BBB /. iS) = ((B2 | ( Sum ( Width (J | m)))) /. (( Sum ( Width (J | (m -' 1)))) + iS)) by FINSEQ_5: 27

      .= ((B2 | ( Sum ( Width (J | m)))) /. (S + iS)) by MATRIXJ1: 46

      .= ((B2 | ( Sum (( Len J) | m))) /. i) by A22, A16, MATRIXJ1: 21

      .= (B2 /. i) by A13, A25, FINSEQ_4: 70;

      hence i = Sm implies (( Mx2Tran (M,b1,B2)) . (b1 /. i)) = (L * (B2 /. i)) by A10, A12, A9, A16, A23, A18, A27, A20, A26, Th21;

      assume

       A29: i <> Sm;

      then i < Sm by A14, XXREAL_0: 1;

      then 1 <= (i + 1) & (i + 1) <= Sm by NAT_1: 11, NAT_1: 13;

      then

       A30: (i + 1) in ( dom (B2 | Sm)) by A24, FINSEQ_3: 25;

      

       A31: iS <> ( len (J . m)) by A16, A18, A29;

      then iS < ( len (J . m)) by A19, XXREAL_0: 1;

      then 1 <= (iS + 1) & (iS + 1) <= ( len (J . m)) by NAT_1: 11, NAT_1: 13;

      then (iS + 1) in ( dom BBB) by A12, A9, A23, FINSEQ_3: 25;

      

      then (BBB /. (iS + 1)) = ((B2 | ( Sum ( Width (J | m)))) /. (( Sum ( Width (J | (m -' 1)))) + (iS + 1))) by FINSEQ_5: 27

      .= ((B2 | ( Sum ( Width (J | m)))) /. (( Sum (( Len J) | (m -' 1))) + (iS + 1))) by A22, MATRIXJ1: 21

      .= ((B2 | ( Sum (( Len J) | m))) /. (i + 1)) by A15, A22, A16, MATRIXJ1: 21

      .= (B2 /. (i + 1)) by A13, A30, FINSEQ_4: 70;

      hence thesis by A10, A12, A9, A23, A27, A20, A26, A28, A31, Th22;

    end;

    theorem :: MATRIXJ2:25

    

     Th25: for J be FinSequence_of_Jordan_block of ( 0. K), K holds for M be Matrix of ( len b1), ( len b1), K st M = ( block_diagonal (J,( 0. K))) holds for m st for i st i in ( dom J) holds ( len (J . i)) <= m holds (( Mx2Tran (M,b1,b1)) |^ m) = ( ZeroMap (V1,V1))

    proof

      let J be FinSequence_of_Jordan_block of ( 0. K), K;

      let M be Matrix of ( len b1), ( len b1), K such that

       A1: M = ( block_diagonal (J,( 0. K)));

      reconsider Z = ( ZeroMap (V1,V1)) as linear-transformation of V1, V1;

      set MT = ( Mx2Tran (M,b1,b1));

      let m such that

       A2: for i st i in ( dom J) holds ( len (J . i)) <= m;

      

       A3: ( dom Z) = the carrier of V1 & ( rng b1) c= the carrier of V1 by FUNCT_2:def 1, RELAT_1:def 19;

      set MTm = (MT |^ m);

      

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

      per cases ;

        suppose ( len b1) = 0 ;

        then ( dim V1) = 0 by MATRLIN2: 21;

        then ( (Omega). V1) = ( (0). V1) by VECTSP_9: 29;

        then

         A5: the carrier of V1 = {( 0. V1)} by VECTSP_4:def 3;

        ( rng MTm) c= the carrier of V1 by RELAT_1:def 19;

        then ( rng MTm) = {( 0. V1)} by A5, ZFMISC_1: 33;

        

        then MTm = (the carrier of V1 --> ( 0. V1)) by A4, FUNCOP_1: 9

        .= Z by GRCAT_1:def 7;

        hence thesis;

      end;

        suppose

         A6: ( len b1) > 0 ;

        

         A7: ( dom J) = ( dom ( Len J)) by MATRIXJ1:def 3;

        

         A8: ( len M) = ( len b1) & ( len M) = ( Sum ( Len J)) by A1, MATRIX_0: 24;

         A9:

        now

          let x be object such that

           A10: x in ( dom b1);

          reconsider n = x as Element of NAT by A10;

          set mm = ( min (( Len J),n));

          

           A11: n in ( Seg ( Sum ( Len J))) by A8, A10, FINSEQ_1:def 3;

          then

           A12: mm in ( dom ( Len J)) by MATRIXJ1:def 1;

          then

           A13: (( Len J) . mm) = ( len (J . mm)) by MATRIXJ1:def 3;

          

           A14: (( Len J) | mm) = ( Len (J | mm)) by MATRIXJ1: 17;

           A15:

          now

            mm <= ( len ( Len J)) by A12, FINSEQ_3: 25;

            then ( Sum ( Len (J | mm))) <= ( Sum (( Len J) | ( len ( Len J)))) by A14, POLYNOM3: 18;

            then

             A16: ( Sum ( Len (J | mm))) <= ( len b1) by A8, FINSEQ_1: 58;

            let k;

            assume (n + k) <= ( Sum ( Len (J | mm)));

            then

             A17: (n + k) <= ( len b1) by A16, XXREAL_0: 2;

            1 <= n & n <= (n + k) by A11, FINSEQ_1: 1, NAT_1: 11;

            then 1 <= (n + k) by XXREAL_0: 2;

            hence (n + k) in ( dom b1) by A17, FINSEQ_3: 25;

          end;

          defpred Q[ Nat] means ((MT |^ ($1 + 1)) . (b1 /. n)) = ( 0. V1);

          defpred P[ Nat] means (n + $1) < ( Sum ( Len (J | mm))) implies ((MT |^ ($1 + 1)) . (b1 /. n)) = (b1 /. ((n + $1) + 1));

          set Sm = ( Sum (( Len J) | (mm -' 1)));

          

           A18: (( Len J) . mm) = (( Len J) /. mm) by A12, PARTFUN1:def 6;

          (mm -' 1) = (mm - 1) by A11, MATRIXJ1: 7;

          then ((mm -' 1) + 1) = mm;

          then (( Len J) | mm) = ((( Len J) | (mm -' 1)) ^ <*(( Len J) . mm)*>) by A12, FINSEQ_5: 10;

          then

           A19: ( Sum ( Len (J | mm))) = (Sm + ( len (J . mm))) by A14, A13, RVSUM_1: 74;

          

           A20: Sm < n by A11, MATRIXJ1: 7;

          then

           A21: (n -' Sm) = (n - Sm) by XREAL_1: 233;

          then

           A22: (n -' Sm) <> 0 by A11, MATRIXJ1: 7;

           A23:

          now

            let k;

            assume (n + k) <= ( Sum ( Len (J | mm)));

            then

             A24: ((n + k) - Sm) <= ((Sm + ( len (J . mm))) - Sm) by A19, XREAL_1: 9;

            1 <= ((n -' Sm) + k) by A22, NAT_1: 14;

            then ((n -' Sm) + k) in ( Seg (( Len J) /. mm)) by A18, A21, A13, A24;

            then ( min (( Len J),(((n -' Sm) + k) + ( Sum (( Len J) | (mm -' 1)))))) = mm by A12, MATRIXJ1: 10;

            hence ( min (( Len J),(n + k))) = mm by A21;

          end;

          

           A25: for k st P[k] holds P[(k + 1)]

          proof

            let k such that

             A26: P[k];

            set k1 = (k + 1);

            

             A27: the carrier of V1 = ( dom (MT |^ k1)) & (n + k1) = ((n + k) + 1) by FUNCT_2:def 1;

            assume

             A28: (n + k1) < ( Sum ( Len (J | mm)));

            then (n + k1) < ( Sum ( Len (J | ( min (( Len J),(n + k1)))))) & (n + k1) in ( dom b1) by A15, A23;

            

            then

             A29: (MT . (b1 /. (n + k1))) = ((( 0. K) * (b1 /. (n + k1))) + (b1 /. ((n + k1) + 1))) by A1, Th24

            .= (( 0. V1) + (b1 /. ((n + k1) + 1))) by VECTSP_1: 14

            .= (b1 /. ((n + k1) + 1)) by RLVECT_1:def 4;

            

            thus ((MT |^ (k1 + 1)) . (b1 /. n)) = (((MT |^ 1) * (MT |^ k1)) . (b1 /. n)) by VECTSP11: 20

            .= ((MT |^ 1) . (b1 /. (n + k1))) by A26, A28, A27, FUNCT_1: 13, NAT_1: 13

            .= (b1 /. ((n + k1) + 1)) by A29, VECTSP11: 19;

          end;

          n <= ( Sum (( Len J) | mm)) by A11, MATRIXJ1:def 1;

          then

           A30: (( Sum ( Len (J | mm))) -' n) = (( Sum ( Len (J | mm))) - n) by A14, XREAL_1: 233;

          

           A31: P[ 0 ]

          proof

            assume (n + 0 ) < ( Sum ( Len (J | mm)));

            

            then (MT . (b1 /. n)) = ((( 0. K) * (b1 /. n)) + (b1 /. (n + 1))) by A1, A10, Th24

            .= (( 0. V1) + (b1 /. (n + 1))) by VECTSP_1: 14

            .= (b1 /. (n + 1)) by RLVECT_1:def 4;

            hence thesis by VECTSP11: 19;

          end;

          

           A32: for k holds P[k] from NAT_1:sch 2( A31, A25);

          

           A33: Q[(( Sum ( Len (J | mm))) -' n)]

          proof

            per cases ;

              suppose

               A34: (( Sum ( Len (J | mm))) -' n) = 0 ;

              

              then (MT . (b1 /. n)) = (( 0. K) * (b1 /. n)) by A1, A10, A30, Th24

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

              hence thesis by A34, VECTSP11: 19;

            end;

              suppose (( Sum ( Len (J | mm))) -' n) > 0 ;

              then

              reconsider S1 = ((( Sum ( Len (J | mm))) -' n) - 1) as Element of NAT by NAT_1: 20;

              

               A35: the carrier of V1 = ( dom (MT |^ (( Sum ( Len (J | mm))) -' n))) by FUNCT_2:def 1;

              (( Sum ( Len (J | mm))) - 1) < (( Sum ( Len (J | mm))) - 0 ) by XREAL_1: 10;

              

              then

               A36: ((MT |^ (S1 + 1)) . (b1 /. n)) = (b1 /. ((n + S1) + 1)) by A30, A32

              .= (b1 /. ( Sum ( Len (J | mm)))) by A30;

              ((( Sum ( Len (J | mm))) -' n) + n) = ( Sum ( Len (J | mm))) by A30;

              then ( Sum ( Len (J | mm))) in ( dom b1) & ( min (( Len J),( Sum ( Len (J | mm))))) = mm by A15, A23;

              

              then

               A37: (MT . (b1 /. ( Sum ( Len (J | mm))))) = (( 0. K) * (b1 /. ( Sum ( Len (J | mm))))) by A1, Th24

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

              

              thus ((MT |^ ((( Sum ( Len (J | mm))) -' n) + 1)) . (b1 /. n)) = (((MT |^ 1) * (MT |^ (( Sum ( Len (J | mm))) -' n))) . (b1 /. n)) by VECTSP11: 20

              .= ((MT |^ 1) . ((MT |^ (( Sum ( Len (J | mm))) -' n)) . (b1 /. n))) by A35, FUNCT_1: 13

              .= ( 0. V1) by A36, A37, VECTSP11: 19;

            end;

          end;

          (Sm - n) < (n - n) by A20, XREAL_1: 9;

          then

           A38: (( len (J . mm)) + (Sm - n)) < (( len (J . mm)) + 0 ) by XREAL_1: 6;

          then 0 < m by A2, A7, A12, A30, A19;

          then

          reconsider m1 = (m - 1) as Element of NAT by NAT_1: 20;

          ( len (J . mm)) <= m by A2, A7, A12;

          then (( Sum ( Len (J | mm))) -' n) < (m1 + 1) by A30, A19, A38, XXREAL_0: 2;

          then

           A39: (( Sum ( Len (J | mm))) -' n) <= m1 by NAT_1: 13;

          

           A40: for k st (( Sum ( Len (J | mm))) -' n) <= k holds Q[k] implies Q[(k + 1)]

          proof

            let k such that (( Sum ( Len (J | mm))) -' n) <= k;

            set k1 = (k + 1);

            assume

             A41: Q[k];

            

             A42: ( dom (MT |^ k1)) = the carrier of V1 by FUNCT_2:def 1;

            

            thus ((MT |^ (k1 + 1)) . (b1 /. n)) = (((MT |^ 1) * (MT |^ k1)) . (b1 /. n)) by VECTSP11: 20

            .= ((MT |^ 1) . ((MT |^ k1) . (b1 /. n))) by A42, FUNCT_1: 13

            .= (MT . ( 0. V1)) by A41, VECTSP11: 19

            .= (MT . (( 0. K) * ( 0. V1))) by VECTSP_1: 14

            .= (( 0. K) * (MT . ( 0. V1))) by MOD_2:def 2

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

          end;

          for k st (( Sum ( Len (J | mm))) -' n) <= k holds Q[k] from NAT_1:sch 8( A33, A40);

          then

           A43: ((MT |^ (m1 + 1)) . (b1 /. n)) = ( 0. V1) by A39;

          

          thus ((Z * b1) . x) = (Z . (b1 . x)) by A10, FUNCT_1: 13

          .= (Z . (b1 /. x)) by A10, PARTFUN1:def 6

          .= ((the carrier of V1 --> ( 0. V1)) . (b1 /. x)) by GRCAT_1:def 7

          .= ( 0. V1)

          .= (MTm . (b1 . n)) by A10, A43, PARTFUN1:def 6

          .= ((MTm * b1) . x) by A10, FUNCT_1: 13;

        end;

        ( dom (Z * b1)) = ( dom b1) & ( dom (MTm * b1)) = ( dom b1) by A4, A3, RELAT_1: 27;

        hence thesis by A6, A9, FUNCT_1: 2, MATRLIN: 22;

      end;

    end;

    

     Lm3: for J be FinSequence_of_Jordan_block of L, K holds for M be Matrix of ( len b1), ( len b1), K st M = ( block_diagonal (J,( 0. K))) & ( len b1) <> 0 holds ((( Mx2Tran (M,b1,b1)) |^ n) . (b1 /. ( Sum ( Len (J | ( min (( Len J),( len b1)))))))) = ((( power K) . (L,n)) * (b1 /. ( Sum ( Len (J | ( min (( Len J),( len b1)))))))) & ( Sum ( Len (J | ( min (( Len J),( len b1)))))) in ( dom b1)

    proof

      let J be FinSequence_of_Jordan_block of L, K;

      set B = ( len b1);

      set m = ( min (( Len J),B));

      set S = ( Sum ( Len (J | m)));

      

       A1: ( Seg B) = ( dom b1) by FINSEQ_1:def 3;

      let M be Matrix of ( len b1), ( len b1), K such that

       A2: M = ( block_diagonal (J,( 0. K)));

      

       A3: ( len b1) = ( len M) & ( len M) = ( Sum ( Len J)) by A2, MATRIX_0: 24;

      set MT = ( Mx2Tran (M,b1,b1));

      defpred P[ Nat] means ((MT |^ $1) . (b1 /. S)) = ((( power K) . (L,$1)) * (b1 /. S));

      ((MT |^ 0 ) . (b1 /. S)) = (( id V1) . (b1 /. S)) by VECTSP11: 18

      .= (b1 /. S) by FUNCT_1: 18

      .= (( 1_ K) * (b1 /. S)) by VECTSP_1:def 17

      .= ((( power K) . (L, 0 )) * (b1 /. S)) by GROUP_1:def 7;

      then

       A4: P[ 0 ];

      

       A5: ( Sum (( Len J) | m)) = S & (( Len J) | ( len ( Len J))) = ( Len J) by FINSEQ_1: 58, MATRIXJ1: 17;

      assume B <> 0 ;

      then

       A6: B in ( Seg B) by FINSEQ_1: 3;

      then m in ( dom ( Len J)) by A3, MATRIXJ1:def 1;

      then m <= ( len ( Len J)) by FINSEQ_3: 25;

      then

       A7: ( Sum (( Len J) | m)) <= ( Sum (( Len J) | ( len ( Len J)))) by POLYNOM3: 18;

      

       A8: B <= ( Sum (( Len J) | m)) by A3, A6, MATRIXJ1:def 1;

      then B = S by A3, A7, A5, XXREAL_0: 1;

      then

       A9: (MT . (b1 /. S)) = (L * (b1 /. S)) by A2, A6, A1, Th24;

      

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

      proof

        let n such that

         A11: P[n];

        

         A12: ( dom (MT |^ n)) = the carrier of V1 by FUNCT_2:def 1;

        

        thus ((MT |^ (n + 1)) . (b1 /. S)) = (((MT |^ 1) * (MT |^ n)) . (b1 /. S)) by VECTSP11: 20

        .= ((MT * (MT |^ n)) . (b1 /. S)) by VECTSP11: 19

        .= (MT . ((( power K) . (L,n)) * (b1 /. S))) by A11, A12, FUNCT_1: 13

        .= ((( power K) . (L,n)) * (L * (b1 /. S))) by A9, MOD_2:def 2

        .= (((( power K) . (L,n)) * L) * (b1 /. S)) by VECTSP_1:def 16

        .= ((( power K) . (L,(n + 1))) * (b1 /. S)) by GROUP_1:def 7;

      end;

      for n holds P[n] from NAT_1:sch 2( A4, A10);

      hence thesis by A3, A6, A1, A8, A7, A5, XXREAL_0: 1;

    end;

    theorem :: MATRIXJ2:26

    for J be FinSequence_of_Jordan_block of L, K holds for M be Matrix of ( len b1), ( len b1), K st M = ( block_diagonal (J,( 0. K))) holds ( Mx2Tran (M,b1,b1)) is nilpotent iff ( len b1) = 0 or L = ( 0. K)

    proof

      let J be FinSequence_of_Jordan_block of L, K;

      let M be Matrix of ( len b1), ( len b1), K such that

       A1: M = ( block_diagonal (J,( 0. K)));

      set MT = ( Mx2Tran (M,b1,b1));

      thus MT is nilpotent implies ( len b1) = 0 or L = ( 0. K)

      proof

        set B = ( len b1);

        set m = ( min (( Len J),B));

        set S = ( Sum ( Len (J | m)));

        assume MT is nilpotent;

        then

        reconsider MT as nilpotent linear-transformation of V1, V1;

        ( rng b1) is Basis of V1 by MATRLIN:def 2;

        then

         A2: ( rng b1) is linearly-independent Subset of V1 by VECTSP_7:def 3;

        assume

         A3: B <> 0 ;

        then S in ( dom b1) by A1, Lm3;

        then (b1 . S) in ( rng b1) & (b1 /. S) = (b1 . S) by FUNCT_1:def 3, PARTFUN1:def 6;

        then

         A4: (b1 /. S) <> ( 0. V1) by A2, VECTSP_7: 2;

        ((( power K) . (L,( deg MT))) * (b1 /. S)) = ((MT |^ ( deg MT)) . (b1 /. S)) by A1, A3, Lm3

        .= (( ZeroMap (V1,V1)) . (b1 /. S)) by Def5

        .= ((the carrier of V1 --> ( 0. V1)) . (b1 /. S)) by GRCAT_1:def 7

        .= ( 0. V1)

        .= (( 0. K) * (b1 /. S)) by VECTSP_1: 14;

        

        then ( 0. K) = (( power K) . (L,( deg MT))) by A4, VECTSP10: 4

        .= ( Product (( deg MT) |-> L)) by MATRIXJ1: 5;

        then

         A5: ex k be Nat st k in ( dom (( deg MT) |-> L)) & ((( deg MT) |-> L) . k) = ( 0. K) by FVSUM_1: 82;

        ( dom (( deg MT) |-> L)) = ( Seg ( deg MT)) by FINSEQ_2: 124;

        hence thesis by A5, FINSEQ_2: 57;

      end;

      assume

       A6: ( len b1) = 0 or L = ( 0. K);

      per cases by A6;

        suppose ( len b1) = 0 ;

        then ( dim V1) = 0 by MATRLIN2: 21;

        then ( (Omega). V1) = ( (0). V1) by VECTSP_9: 29;

        then

         A7: the carrier of V1 = {( 0. V1)} by VECTSP_4:def 3;

        ( rng (MT |^ 1)) c= the carrier of V1 by RELAT_1:def 19;

        then ( rng (MT |^ 1)) = {( 0. V1)} by A7, ZFMISC_1: 33;

        

        then (MT |^ 1) = (( dom (MT |^ 1)) --> ( 0. V1)) by FUNCOP_1: 9

        .= (the carrier of V1 --> ( 0. V1)) by FUNCT_2:def 1

        .= ( ZeroMap (V1,V1)) by GRCAT_1:def 7;

        hence thesis by Th13;

      end;

        suppose

         A8: L = ( 0. K);

        now

          

           A9: ( dom J) = ( dom ( Len J)) by MATRIXJ1:def 3;

          let i such that

           A10: i in ( dom J);

          ( len (J . i)) = (( Len J) . i) by A10, A9, MATRIXJ1:def 3;

          hence ( len (J . i)) <= ( Sum ( Len J)) by A10, A9, POLYNOM3: 4;

        end;

        then (MT |^ ( Sum ( Len J))) = ( ZeroMap (V1,V1)) by A1, A8, Th25;

        hence thesis by Th13;

      end;

    end;

    theorem :: MATRIXJ2:27

    for J be FinSequence_of_Jordan_block of ( 0. K), K holds for M be Matrix of ( len b1), ( len b1), K st M = ( block_diagonal (J,( 0. K))) & ( len b1) > 0 holds for F be nilpotent Function of V1, V1 st F = ( Mx2Tran (M,b1,b1)) holds (ex i st i in ( dom J) & ( len (J . i)) = ( deg F)) & for i st i in ( dom J) holds ( len (J . i)) <= ( deg F)

    proof

      let J be FinSequence_of_Jordan_block of ( 0. K), K;

      let M be Matrix of ( len b1), ( len b1), K such that

       A1: M = ( block_diagonal (J,( 0. K))) and

       A2: ( len b1) > 0 ;

      

       A3: ( len M) = ( len b1) & ( len M) = ( Sum ( Len J)) by A1, MATRIX_0:def 2;

      defpred P[ Nat] means for i st i in ( dom J) holds ( len (J . i)) <= $1;

      set mm = ( min (( Len J),( len b1)));

      

       A4: ( dom J) = ( dom ( Len J)) by MATRIXJ1:def 3;

      now

        let i such that

         A5: i in ( dom J);

        ( len (J . i)) = (( Len J) . i) by A4, A5, MATRIXJ1:def 3;

        hence ( len (J . i)) <= ( Sum ( Len J)) by A4, A5, POLYNOM3: 4;

      end;

      then

       A6: ex k st P[k];

      consider MIN be Nat such that

       A7: P[MIN] and

       A8: for m st P[m] holds MIN <= m from NAT_1:sch 5( A6);

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

      then

       A9: ( min (( Len J),( len b1))) in ( dom ( Len J)) by A3, MATRIXJ1:def 1;

      

       A10: ex i st i in ( dom J) & ( len (J . i)) = MIN

      proof

        assume

         A11: for i st i in ( dom J) holds ( len (J . i)) <> MIN;

        ( len (J . mm)) <= MIN by A9, A4, A7;

        then ( len (J . mm)) < MIN by A9, A4, A11, XXREAL_0: 1;

        then

        reconsider M1 = (MIN - 1) as Element of NAT by NAT_1: 20;

        now

          let i such that

           A12: i in ( dom J);

          ( len (J . i)) <= MIN by A7, A12;

          then ( len (J . i)) < (M1 + 1) by A11, A12, XXREAL_0: 1;

          hence ( len (J . i)) <= M1 by NAT_1: 13;

        end;

        then (M1 + 1) <= M1 by A8;

        hence thesis by NAT_1: 13;

      end;

      

       A13: (( Len J) | ( len ( Len J))) = ( Len J) by FINSEQ_1: 58;

      let F be nilpotent Function of V1, V1 such that

       A14: F = ( Mx2Tran (M,b1,b1));

      consider i such that

       A15: i in ( dom J) and

       A16: ( len (J . i)) = MIN by A10;

      

       A17: (( Len J) . i) = (( Len J) /. i) by A4, A15, PARTFUN1:def 6;

      set S = ( Sum (( Len J) | (i -' 1)));

      defpred P[ Nat] means $1 in ( Seg MIN) & $1 <> MIN implies ((F |^ $1) . (b1 /. (S + 1))) = (b1 /. ((S + $1) + 1));

      

       A18: ( len (J . i)) = (( Len J) . i) by A4, A15, MATRIXJ1:def 3;

      i <= ( len ( Len J)) by A4, A15, FINSEQ_3: 25;

      then ( Sum (( Len J) | i)) <= ( Sum (( Len J) | ( len ( Len J)))) by POLYNOM3: 18;

      then

       A19: ( dom b1) = ( Seg ( len b1)) & ( Seg ( Sum (( Len J) | i))) c= ( Seg ( Sum ( Len J))) by A13, FINSEQ_1: 5, FINSEQ_1:def 3;

      1 <= i by A15, FINSEQ_3: 25;

      then (i -' 1) = (i - 1) by XREAL_1: 233;

      then

       A20: i = ((i -' 1) + 1);

      

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

      proof

        (( Len J) | i) = ((( Len J) | (i -' 1)) ^ <*MIN*>) by A4, A15, A16, A18, A20, FINSEQ_5: 10;

        then

         A22: ( Sum (( Len J) | i)) = (S + MIN) by RVSUM_1: 74;

        let n such that

         A23: P[n];

        

         A24: (( Len J) | i) = ( Len (J | i)) by MATRIXJ1: 17;

        set n1 = (n + 1);

        assume that

         A25: n1 in ( Seg MIN) and

         A26: n1 <> MIN;

        

         A27: n1 <= MIN by A25, FINSEQ_1: 1;

        then n1 < MIN by A26, XXREAL_0: 1;

        then

         A28: (S + n1) < ( Sum (( Len J) | i)) by A22, XREAL_1: 6;

        (S + n1) in ( Seg ( Sum (( Len J) | i))) & ( min (( Len J),(S + n1))) = i by A4, A15, A16, A18, A17, A25, MATRIXJ1: 10;

        

        then

         A29: (F . (b1 /. (S + n1))) = ((( 0. K) * (b1 /. (S + n1))) + (b1 /. ((S + n1) + 1))) by A1, A3, A14, A19, A28, A24, Th24

        .= (( 0. V1) + (b1 /. ((S + n1) + 1))) by VECTSP_1: 14

        .= (b1 /. ((S + n1) + 1)) by RLVECT_1:def 4;

        

         A30: n < MIN by A27, NAT_1: 13;

        now

          per cases by NAT_1: 14;

            suppose n = 0 ;

            hence thesis by A29, VECTSP11: 19;

          end;

            suppose

             A31: n >= 1;

            

             A32: ( dom (F |^ n)) = the carrier of V1 by FUNCT_2:def 1;

            

            thus ((F |^ n1) . (b1 /. (S + 1))) = (((F |^ 1) * (F |^ n)) . (b1 /. (S + 1))) by VECTSP11: 20

            .= ((F |^ 1) . ((F |^ n) . (b1 /. (S + 1)))) by A32, FUNCT_1: 13

            .= (b1 /. ((S + n1) + 1)) by A23, A30, A29, A31, VECTSP11: 19;

          end;

        end;

        hence thesis;

      end;

      

       A33: P[ 0 ];

      

       A34: for n holds P[n] from NAT_1:sch 2( A33, A21);

      

       A35: ( deg F) >= MIN

      proof

        set D = ( deg F);

        ( rng b1) is Basis of V1 by MATRLIN:def 2;

        then

         A36: ( rng b1) is linearly-independent Subset of V1 by VECTSP_7:def 3;

        assume

         A37: D < MIN;

        then 1 <= (1 + D) & (D + 1) <= MIN by NAT_1: 11, NAT_1: 13;

        then (D + 1) in ( Seg MIN);

        then (S + (D + 1)) in ( Seg ( Sum (( Len J) | i))) by A4, A15, A16, A18, A17, MATRIXJ1: 10;

        then

         A38: (b1 /. ((S + D) + 1)) = (b1 . ((S + D) + 1)) & (b1 . ((S + D) + 1)) in ( rng b1) by A3, A19, FUNCT_1:def 3, PARTFUN1:def 6;

        D <> 0

        proof

          assume D = 0 ;

          then ( [#] V1) = {( 0. V1)} by Th15;

          then ( (Omega). V1) = ( (0). V1) by VECTSP_4:def 3;

          then ( dim V1) = 0 by VECTSP_9: 29;

          hence thesis by A2, MATRLIN2: 21;

        end;

        then D >= 1 by NAT_1: 14;

        then D in ( Seg MIN) by A37;

        

        then (b1 /. ((S + D) + 1)) = ((F |^ D) . (b1 /. (S + 1))) by A34, A37

        .= (( ZeroMap (V1,V1)) . (b1 /. (S + 1))) by Def5

        .= ((the carrier of V1 --> ( 0. V1)) . (b1 /. (S + 1))) by GRCAT_1:def 7

        .= ( 0. V1);

        hence thesis by A38, A36, VECTSP_7: 2;

      end;

      (F |^ MIN) = ( ZeroMap (V1,V1)) by A1, A14, A7, Th25;

      then ( deg F) <= MIN by Def5;

      then ( deg F) = MIN by A35, XXREAL_0: 1;

      hence thesis by A7, A10;

    end;

    

     Lm4: for V1,V2 be VectSp of K, f be linear-transformation of V1, V2 holds for W1 be Subspace of V1, W2 be Subspace of V2 holds for F be Function of W1, W2 st F = (f | W1) holds F is linear-transformation of W1, W2

    proof

      let V1,V2 be VectSp of K, f be linear-transformation of V1, V2;

      let W1 be Subspace of V1;

      let W2 be Subspace of V2;

      let F be Function of W1, W2 such that

       A1: F = (f | W1);

       A2:

      now

        let a be Scalar of K, w be Vector of W1;

        

        thus (F . (a * w)) = (a * ((f | W1) . w)) by A1, MOD_2:def 2

        .= (a * (F . w)) by A1, VECTSP_4: 14;

      end;

      now

        let w1,w2 be Vector of W1;

        

        thus (F . (w1 + w2)) = (((f | W1) . w1) + ((f | W1) . w2)) by A1, VECTSP_1:def 20

        .= ((F . w1) + (F . w2)) by A1, VECTSP_4: 13;

      end;

      then F is additive homogeneous by A2, MOD_2:def 2, VECTSP_1:def 20;

      hence thesis;

    end;

    theorem :: MATRIXJ2:28

    

     Th28: for V1, V2, b1, b2, L st ( len b1) = ( len b2) holds for F be linear-transformation of V1, V2 st for i st i in ( dom b1) holds (F . (b1 /. i)) = (L * (b2 /. i)) or (i + 1) in ( dom b1) & (F . (b1 /. i)) = ((L * (b2 /. i)) + (b2 /. (i + 1))) holds ex J be non-empty FinSequence_of_Jordan_block of L, K st ( AutMt (F,b1,b2)) = ( block_diagonal (J,( 0. K)))

    proof

      defpred P[ Nat] means for V1, V2, b1, b2, L st ( len b1) = ( len b2) holds for F be linear-transformation of V1, V2 st $1 = ( card { i where i be Element of NAT : i in ( dom b1) & (F . (b1 /. i)) = (L * (b2 /. i)) }) & for i st i in ( dom b1) holds (F . (b1 /. i)) = (L * (b2 /. i)) or ((i + 1) in ( dom b1) & (F . (b1 /. i)) = ((L * (b2 /. i)) + (b2 /. (i + 1)))) holds ex J be non-empty FinSequence_of_Jordan_block of L, K st ( AutMt (F,b1,b2)) = ( block_diagonal (J,( 0. K)));

      

       A1: P[ 0 ]

      proof

        let V1, V2, b1, b2, L such that ( len b1) = ( len b2);

        set Lb = ( len b1);

        reconsider J = {} as FinSequence_of_Jordan_block of L, K by Th10;

        let F be linear-transformation of V1, V2 such that

         A2: 0 = ( card { i where i be Element of NAT : i in ( dom b1) & (F . (b1 /. i)) = (L * (b2 /. i)) }) and

         A3: for i st i in ( dom b1) holds (F . (b1 /. i)) = (L * (b2 /. i)) or (i + 1) in ( dom b1) & (F . (b1 /. i)) = ((L * (b2 /. i)) + (b2 /. (i + 1)));

        reconsider J as non-empty FinSequence_of_Jordan_block of L, K;

        take J;

        Lb = 0

        proof

          assume Lb <> 0 ;

          then

           A4: Lb in ( Seg Lb) by FINSEQ_1: 3;

          

           A5: ( dom b1) = ( Seg Lb) by FINSEQ_1:def 3;

          per cases by A3, A4, A5;

            suppose (F . (b1 /. Lb)) = (L * (b2 /. Lb));

            then Lb in { i where i be Element of NAT : i in ( dom b1) & (F . (b1 /. i)) = (L * (b2 /. i)) } by A4, A5;

            hence thesis by A2;

          end;

            suppose (Lb + 1) in ( dom b1) & (F . (b1 /. Lb)) = ((L * (b2 /. Lb)) + (b2 /. (Lb + 1)));

            then (Lb + 1) <= Lb by FINSEQ_3: 25;

            hence thesis by NAT_1: 13;

          end;

        end;

        then ( len ( AutMt (F,b1,b2))) = 0 by MATRIX_0:def 2;

        then ( AutMt (F,b1,b2)) = {} ;

        hence thesis by MATRIXJ1: 22;

      end;

      

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

      proof

        let n such that

         A7: P[n];

        set n1 = (n + 1);

        let V1, V2, b1, b2, L such that

         A8: ( len b1) = ( len b2);

        

         A9: ( dom b1) = ( dom b2) by A8, FINSEQ_3: 29;

        set Lb = ( len b1);

        let F be linear-transformation of V1, V2 such that

         A10: n1 = ( card { i where i be Element of NAT : i in ( dom b1) & (F . (b1 /. i)) = (L * (b2 /. i)) }) and

         A11: for i st i in ( dom b1) holds (F . (b1 /. i)) = (L * (b2 /. i)) or (i + 1) in ( dom b1) & (F . (b1 /. i)) = ((L * (b2 /. i)) + (b2 /. (i + 1)));

        set FF = { i where i be Element of NAT : i in ( dom b1) & (F . (b1 /. i)) = (L * (b2 /. i)) };

        reconsider FF as finite set by A10;

        consider x be object such that

         A12: x in FF by A10, CARD_1: 27, XBOOLE_0:def 1;

        ex ii be Element of NAT st ii = x & ii in ( dom b1) & (F . (b1 /. ii)) = (L * (b2 /. ii)) by A12;

        then ( dom b1) <> {} ;

        then ( Seg Lb) <> {} by FINSEQ_1:def 3;

        then

         A13: Lb <> 0 ;

        

         A14: ( dom b1) = ( Seg Lb) by FINSEQ_1:def 3;

        then

         A15: not (Lb + 1) in ( dom b1) by FINSEQ_3: 8;

        

         A16: Lb in ( dom b1) by A14, A13, FINSEQ_1: 3;

        then (F . (b1 /. Lb)) = (L * (b2 /. Lb)) by A11, A15;

        then

         A17: Lb in FF by A16;

        per cases ;

          suppose

           A18: n = 0 ;

          set J = ( Jordan_block (L,Lb));

          reconsider JJ = <*J*> as FinSequence_of_Jordan_block of L, K by Th11;

          now

            

             A19: ( dom JJ) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

            let x be object;

            assume x in ( dom JJ);

            then (JJ . 1) = J & x = 1 by A19, FINSEQ_1:def 8, TARSKI:def 1;

            hence (JJ . x) is non empty by A13, Def1;

          end;

          then

          reconsider JJ as non-empty FinSequence_of_Jordan_block of L, K by FUNCT_1:def 9;

          reconsider F9 = F as Function of V1, V2;

          reconsider BB = ( block_diagonal (JJ,( 0. K))) as Matrix of ( len b1), ( len b2), K by A8, MATRIXJ1: 34;

          set T = ( Mx2Tran (BB,b1,b2));

          

           A20: ( block_diagonal (JJ,( 0. K))) = J by MATRIXJ1: 34;

           A21:

          now

            let y be object such that

             A22: y in ( dom b1);

            reconsider j = y as Element of NAT by A22;

            

             A23: ((T * b1) . y) = (T . (b1 . y)) by A22, FUNCT_1: 13;

            

             A24: (b1 /. j) = (b1 . j) by A22, PARTFUN1:def 6;

            

             A25: ((F9 * b1) . y) = (F . (b1 . y)) by A22, FUNCT_1: 13;

            now

              per cases ;

                suppose

                 A26: j = Lb;

                

                hence ((T * b1) . y) = (L * (b2 /. Lb)) by A20, A22, A23, A24, Th23

                .= ((F9 * b1) . y) by A11, A16, A15, A25, A24, A26;

              end;

                suppose

                 A27: j <> Lb;

                ex z be object st FF = {z} by A10, A18, CARD_2: 42;

                then FF = {Lb} by A17, TARSKI:def 1;

                then not j in FF by A27, TARSKI:def 1;

                then

                 A28: (F . (b1 /. j)) <> (L * (b2 /. j)) by A22;

                ((T * b1) . y) = ((L * (b2 /. j)) + (b2 /. (j + 1))) by A20, A22, A23, A24, A27, Th23;

                hence ((T * b1) . y) = ((F9 * b1) . y) by A11, A22, A25, A24, A28;

              end;

            end;

            hence ((F9 * b1) . y) = ((T * b1) . y);

          end;

          take JJ;

          

           A29: ( rng b1) c= ( [#] V1) by FINSEQ_1:def 4;

          ( dom T) = ( [#] V1) by FUNCT_2:def 1;

          then

           A30: ( dom (T * b1)) = ( dom b1) by A29, RELAT_1: 27;

          ( dom F) = ( [#] V1) by FUNCT_2:def 1;

          then ( dom (F9 * b1)) = ( dom b1) by A29, RELAT_1: 27;

          then F = T by A13, A30, A21, FUNCT_1: 2, MATRLIN: 22;

          hence thesis by MATRLIN2: 36;

        end;

          suppose

           A31: n <> 0 ;

          defpred Q[ Nat] means $1 in FF & $1 < Lb;

          

           A32: ex k st Q[k]

          proof

            ( card FF) <> 1 by A10, A31;

            then FF <> {Lb} by CARD_2: 42;

            then

            consider y be object such that

             A33: y in FF and

             A34: y <> Lb by A17, ZFMISC_1: 35;

            consider j be Element of NAT such that

             A35: j = y and

             A36: j in ( dom b1) and (F . (b1 /. j)) = (L * (b2 /. j)) by A33;

            take j;

            j <= Lb by A36, FINSEQ_3: 25;

            hence thesis by A33, A34, A35, XXREAL_0: 1;

          end;

          

           A37: for k st Q[k] holds k <= Lb;

          consider m such that

           A38: Q[m] and

           A39: for k st Q[k] holds k <= m from NAT_1:sch 6( A37, A32);

          set b1m = (b1 | m);

          

           A40: ( len b1m) = m by A38, FINSEQ_1: 59;

          set JB = ( Jordan_block (L,(Lb -' m)));

          reconsider JJ = <*JB*> as FinSequence_of_Jordan_block of L, K by Th11;

          set b19m = (b1 /^ m);

          

           A41: ( len b19m) = (Lb - m) by A38, RFINSEQ:def 1;

          set b29m = (b2 /^ m);

          

           A42: ( len b29m) = (Lb - m) by A8, A38, RFINSEQ:def 1;

          set b2m = (b2 | m);

          

           A43: ( len b2m) = m by A8, A38, FINSEQ_1: 59;

          reconsider Rb2 = ( rng b2m), Rb29 = ( rng b29m) as linearly-independent Subset of V2 by MATRLIN2: 22, MATRLIN2: 23;

          reconsider Rb1 = ( rng b1m), Rb19 = ( rng b19m) as linearly-independent Subset of V1 by MATRLIN2: 22, MATRLIN2: 23;

          set Lb1 = ( Lin Rb1);

          set Lb2 = ( Lin Rb2);

          set Lb19 = ( Lin Rb19);

          set Lb29 = ( Lin Rb29);

          set FRb1 = (F .: Rb1);

          

           A44: ( rng (F | Lb1)) = (F .: the carrier of Lb1) by RELAT_1: 115;

          reconsider b2m as OrdBasis of Lb2 by MATRLIN2: 22;

          reconsider b1m as OrdBasis of Lb1 by MATRLIN2: 22;

          

           A45: ( dom b1m) = ( dom b2m) by A40, A43, FINSEQ_3: 29;

          reconsider b19m as OrdBasis of Lb19 by MATRLIN2: 23;

          reconsider b29m as OrdBasis of Lb29 by MATRLIN2: 23;

          

           A46: b2 = (b2m ^ b29m) by RFINSEQ: 8;

          

           A47: b1 = (b1m ^ b19m) by RFINSEQ: 8;

          then

           A48: ( dom b1m) c= ( dom b1) by FINSEQ_1: 26;

          

           A49: for i st i in ( dom b1m) holds ((F | Lb1) . (b1m /. i)) = (L * (b2m /. i)) or (i + 1) in ( dom b1m) & ((F | Lb1) . (b1m /. i)) = ((L * (b2m /. i)) + (b2m /. (i + 1)))

          proof

            let i such that

             A50: i in ( dom b1m);

            

             A51: (b1m . i) = (b1m /. i) by A50, PARTFUN1:def 6;

            set i1 = (i + 1);

            

             A52: (F . (b1m /. i)) = ((F | Lb1) . (b1m /. i)) by FUNCT_1: 49;

            

             A53: (b2 /. i) = (b2 . i) & (b2 . i) = (b2m . i) by A9, A46, A48, A45, A50, FINSEQ_1:def 7, PARTFUN1:def 6;

            

             A54: (b1 /. i) = (b1 . i) & (b1 . i) = (b1m . i) by A47, A48, A50, FINSEQ_1:def 7, PARTFUN1:def 6;

            per cases by A11, A48, A50;

              suppose (F . (b1 /. i)) = (L * (b2 /. i));

              hence thesis by A45, A50, A53, A54, A51, A52, PARTFUN1:def 6, VECTSP_4: 14;

            end;

              suppose

               A55: i1 in ( dom b1) & (F . (b1 /. i)) = ((L * (b2 /. i)) + (b2 /. i1));

              reconsider rngb2 = ( rng b2) as Basis of V2 by MATRLIN:def 2;

              

               A56: i1 <= m

              proof

                assume i1 > m;

                then

                 A57: i >= m by NAT_1: 13;

                i <= m by A40, A50, FINSEQ_3: 25;

                then

                 A58: i = m by A57, XXREAL_0: 1;

                ex ii be Element of NAT st m = ii & ii in ( dom b1) & (F . (b1 /. ii)) = (L * (b2 /. ii)) by A38;

                then (F . (b1 /. i)) = ((L * (b2 /. i)) + ( 0. V2)) by A58, RLVECT_1:def 4;

                then

                 A59: (b2 /. i1) = ( 0. V2) by A55, RLVECT_1: 8;

                

                 A60: rngb2 is linearly-independent by VECTSP_7:def 3;

                (b2 /. i1) = (b2 . i1) & (b2 . i1) in rngb2 by A9, A55, FUNCT_1:def 3, PARTFUN1:def 6;

                hence thesis by A59, A60, VECTSP_7: 2;

              end;

              

               A61: 1 <= i1 by NAT_1: 11;

              then

               A62: i1 in ( dom b1m) by A40, A56, FINSEQ_3: 25;

              then

               A63: (b2m . i1) = (b2m /. i1) by A45, PARTFUN1:def 6;

              

               A64: (L * (b2 /. i)) = (L * (b2m /. i)) by A45, A50, A53, PARTFUN1:def 6, VECTSP_4: 14;

              (b2 /. i1) = (b2 . i1) & (b2 . i1) = (b2m . i1) by A9, A46, A48, A45, A62, FINSEQ_1:def 7, PARTFUN1:def 6;

              hence thesis by A40, A54, A51, A52, A55, A56, A61, A63, A64, FINSEQ_3: 25, VECTSP_4: 13;

            end;

          end;

          FRb1 c= the carrier of Lb2

          proof

            let y be object;

            assume y in FRb1;

            then

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

             A65: x in Rb1 and

             A66: (F . x) = y by FUNCT_1:def 6;

            consider i be object such that

             A67: i in ( dom b1m) and

             A68: (b1m . i) = x by A65, FUNCT_1:def 3;

            reconsider i as Element of NAT by A67;

            (b1m /. i) = (b1m . i) by A67, PARTFUN1:def 6;

            then ((F | Lb1) . (b1m /. i)) = y by A66, A68, FUNCT_1: 49;

            then y = (L * (b2m /. i)) or y = ((L * (b2m /. i)) + (b2m /. (i + 1))) by A49, A67;

            hence thesis;

          end;

          then the carrier of ( Lin FRb1) = (F .: the carrier of Lb1) & ( Lin FRb1) is Subspace of Lb2 by VECTSP11: 42, VECTSP_9: 16;

          then (F .: the carrier of Lb1) c= the carrier of Lb2 by VECTSP_4:def 2;

          then

          reconsider FL = (F | Lb1) as linear-transformation of Lb1, Lb2 by A44, Lm4, FUNCT_2: 6;

          

           A69: for i st i in ( dom b1m) holds (FL . (b1m /. i)) = (L * (b2m /. i)) or (i + 1) in ( dom b1m) & (FL . (b1m /. i)) = ((L * (b2m /. i)) + (b2m /. (i + 1))) by A49;

          set FF1 = { i where i be Element of NAT : i in ( dom b1m) & (FL . (b1m /. i)) = (L * (b2m /. i)) };

          

           A70: (FF \ {Lb}) c= FF1

          proof

            let x be object such that

             A71: x in (FF \ {Lb});

            

             A72: x <> Lb by A71, ZFMISC_1: 56;

            x in FF by A71;

            then

            consider j be Element of NAT such that

             A73: j = x and

             A74: j in ( dom b1) and

             A75: (F . (b1 /. j)) = (L * (b2 /. j));

            j <= Lb by A74, FINSEQ_3: 25;

            then j < Lb by A72, A73, XXREAL_0: 1;

            then

             A76: j <= m by A39, A71, A73;

            1 <= j by A74, FINSEQ_3: 25;

            then

             A77: j in ( dom b1m) by A40, A76, FINSEQ_3: 25;

            then

             A78: (b1m /. j) = (b1m . j) & (b1m . j) = (b1 . j) by A47, FINSEQ_1:def 7, PARTFUN1:def 6;

            

             A79: (FL . (b1m /. j)) = (F . (b1m /. j)) & (b1 /. j) = (b1 . j) by A48, A77, FUNCT_1: 49, PARTFUN1:def 6;

            (b2m . j) = (b2 . j) & (b2 /. j) = (b2 . j) by A9, A46, A48, A45, A77, FINSEQ_1:def 7, PARTFUN1:def 6;

            then (FL . (b1m /. j)) = (L * (b2m /. j)) by A45, A75, A77, A78, A79, PARTFUN1:def 6, VECTSP_4: 14;

            hence thesis by A73, A77;

          end;

          FF1 c= (FF \ {Lb})

          proof

            let x be object;

            assume x in FF1;

            then

            consider j be Element of NAT such that

             A80: x = j and

             A81: j in ( dom b1m) and

             A82: (FL . (b1m /. j)) = (L * (b2m /. j));

            

             A83: (b1m /. j) = (b1m . j) & (b1m . j) = (b1 . j) by A47, A81, FINSEQ_1:def 7, PARTFUN1:def 6;

            

             A84: (FL . (b1m /. j)) = (F . (b1m /. j)) & (b1 /. j) = (b1 . j) by A48, A81, FUNCT_1: 49, PARTFUN1:def 6;

            (b2m . j) = (b2 . j) & (b2 /. j) = (b2 . j) by A9, A46, A48, A45, A81, FINSEQ_1:def 7, PARTFUN1:def 6;

            then (F . (b1 /. j)) = (L * (b2 /. j)) by A45, A81, A82, A83, A84, PARTFUN1:def 6, VECTSP_4: 14;

            then

             A85: j in FF by A48, A81;

            j <= m by A40, A81, FINSEQ_3: 25;

            hence thesis by A38, A80, A85, ZFMISC_1: 56;

          end;

          then FF1 = (FF \ {Lb}) by A70, XBOOLE_0:def 10;

          then ( card FF1) = n by A10, A17, STIRL2_1: 55;

          then

          consider J be non-empty FinSequence_of_Jordan_block of L, K such that

           A86: ( AutMt (FL,b1m,b2m)) = ( block_diagonal (J,( 0. K))) by A7, A40, A43, A69;

          set JJJ = (J ^ JJ);

          

           A87: (Lb - m) = (Lb -' m) by A38, XREAL_1: 233;

           A88:

          now

            let x be object such that

             A89: x in ( dom JJJ);

            reconsider i = x as Nat by A89;

            per cases by A89, FINSEQ_1: 25;

              suppose

               A90: i in ( dom J);

              then (J . i) is non empty by FUNCT_1:def 9;

              hence (JJJ . x) is non empty by A90, FINSEQ_1:def 7;

            end;

              suppose

               A91: ex j st j in ( dom JJ) & i = (( len J) + j);

              ( len JB) = (Lb -' m) by Def1;

              then

               A92: ( len JB) <> 0 by A38, A87;

              consider j such that

               A93: j in ( dom JJ) and

               A94: i = (( len J) + j) by A91;

              ( dom JJ) = ( Seg 1) by FINSEQ_1: 38;

              then j = 1 by A93, FINSEQ_1: 2, TARSKI:def 1;

              then (JJJ . i) = (JJ . 1) by A93, A94, FINSEQ_1:def 7;

              hence (JJJ . x) is non empty by A92, FINSEQ_1: 40;

            end;

          end;

          ( len b19m) = ( len b29m) by A8, A38, A41, RFINSEQ:def 1;

          then

          reconsider JB as Matrix of ( len b19m), ( len b29m), K by A41, A87;

          

           A95: ( width JB) = ( len b19m) by A41, A42, MATRIX_0: 24;

          reconsider JJJ as non-empty FinSequence_of_Jordan_block of L, K by A88, FUNCT_1:def 9;

          take JJJ;

          reconsider F9 = F as Function of V1, V2;

          reconsider B = ( block_diagonal (J,( 0. K))) as Matrix of ( len b1m), ( len b2m), K by A86;

          

           A96: ( width B) = ( len b1m) by A40, A43, MATRIX_0: 24;

          

           A97: ( Sum ( Len <*B, JB*>)) = (( len B) + ( len JB)) & ( Sum ( Width <*B, JB*>)) = (( width B) + ( width JB)) by MATRIXJ1: 16, MATRIXJ1: 20;

          set BB = ( block_diagonal ( <*B, JB*>,( 0. K)));

          

           A98: ( len B) = ( len b1m) by A40, A43, MATRIX_0: 24;

          

           A99: ( Sum ( Len <*B, JB*>)) = ( len b1) by A40, A41, A42, A97, A96, A95, A98, MATRIX_0: 24;

          ( Sum ( Width <*B, JB*>)) = ( len b2) by A8, A40, A41, A97, A96, A95;

          then

          reconsider BB as Matrix of ( len b1), ( len b2), K by A99;

          set T = ( Mx2Tran (BB,b1,b2));

          

           A100: ( dom b19m) = ( dom b29m) by A41, A42, FINSEQ_3: 29;

           A101:

          now

            let x be object such that

             A102: x in ( dom b1);

            reconsider I = x as Element of NAT by A102;

            

             A103: ((T * b1) . x) = (T . (b1 . I)) by A102, FUNCT_1: 13;

            

             A104: (b1 . I) = (b1 /. I) by A102, PARTFUN1:def 6;

            

             A105: ((F9 * b1) . x) = (F . (b1 . I)) by A102, FUNCT_1: 13;

            now

              per cases by A47, A102, FINSEQ_1: 25;

                suppose

                 A106: I in ( dom b1m);

                then

                 A107: (b1m /. I) = (b1m . I) & (b1 . I) = (b1m . I) by A47, FINSEQ_1:def 7, PARTFUN1:def 6;

                

                 A108: (FL . (b1m /. I)) = (F . (b1m /. I)) by FUNCT_1: 49;

                

                thus ((T * b1) . x) = (( Mx2Tran (B,b1m,b2m)) . (b1m /. I)) by A40, A43, A41, A42, A47, A46, A96, A95, A103, A104, A106, Th19

                .= (FL . (b1m /. I)) by A86, MATRLIN2: 34

                .= ((F9 * b1) . x) by A102, A108, A107, FUNCT_1: 13;

              end;

                suppose ex j st j in ( dom b19m) & I = (( len b1m) + j);

                then

                consider j such that

                 A109: j in ( dom b19m) and

                 A110: I = (( len b1m) + j);

                now

                  per cases ;

                    suppose

                     A111: j = ( len b19m);

                    

                     A112: (b2 . I) = (b29m . j) & (b2 /. I) = (b2 . I) by A9, A40, A43, A46, A100, A102, A109, A110, FINSEQ_1:def 7, PARTFUN1:def 6;

                    

                    thus ((F9 * b1) . x) = (L * (b2 /. I)) by A11, A16, A15, A40, A41, A105, A104, A110, A111

                    .= (L * (b29m /. j)) by A100, A109, A112, PARTFUN1:def 6, VECTSP_4: 14

                    .= (( Mx2Tran (JB,b19m,b29m)) . (b19m /. j)) by A109, A111, Th23;

                  end;

                    suppose

                     A113: j <> ( len b19m);

                    

                     A114: ((F9 * b1) . x) = ((L * (b2 /. I)) + (b2 /. (I + 1)))

                    proof

                      assume ((F9 * b1) . x) <> ((L * (b2 /. I)) + (b2 /. (I + 1)));

                      then (F . (b1 /. I)) = (L * (b2 /. I)) by A11, A102, A105, A104;

                      then

                       A115: I in FF by A102;

                      I <> Lb & I <= Lb by A40, A41, A102, A110, A113, FINSEQ_3: 25;

                      then I < Lb by XXREAL_0: 1;

                      then (( len b1m) + j) <= (( len b1m) + 0 ) by A39, A40, A110, A115;

                      then j <= 0 by XREAL_1: 6;

                      hence thesis by A109, FINSEQ_3: 25;

                    end;

                    j <= ( len b19m) by A109, FINSEQ_3: 25;

                    then j < ( len b19m) by A113, XXREAL_0: 1;

                    then 1 <= (j + 1) & (j + 1) <= ( len b19m) by NAT_1: 11, NAT_1: 13;

                    then

                     A116: (j + 1) in ( dom b19m) by FINSEQ_3: 25;

                    then (b29m /. (j + 1)) = (b29m . (j + 1)) & (b2 . (( len b1m) + (j + 1))) = (b29m . (j + 1)) by A40, A43, A46, A100, FINSEQ_1:def 7, PARTFUN1:def 6;

                    then

                     A117: (b29m /. (j + 1)) = (b2 /. (I + 1)) by A9, A47, A110, A116, FINSEQ_1: 28, PARTFUN1:def 6;

                    (b2 . I) = (b29m . j) & (b2 /. I) = (b2 . I) by A9, A40, A43, A46, A100, A102, A109, A110, FINSEQ_1:def 7, PARTFUN1:def 6;

                    then (L * (b29m /. j)) = (L * (b2 /. I)) by A100, A109, PARTFUN1:def 6, VECTSP_4: 14;

                    

                    then ((L * (b2 /. I)) + (b2 /. (I + 1))) = ((L * (b29m /. j)) + (b29m /. (j + 1))) by A117, VECTSP_4: 13

                    .= (( Mx2Tran (JB,b19m,b29m)) . (b19m /. j)) by A109, A113, Th23;

                    hence ((F9 * b1) . x) = (( Mx2Tran (JB,b19m,b29m)) . (b19m /. j)) by A114;

                  end;

                end;

                hence ((F9 * b1) . x) = ((T * b1) . x) by A40, A43, A41, A42, A47, A46, A96, A95, A103, A104, A109, A110, Th19;

              end;

            end;

            hence ((F9 * b1) . x) = ((T * b1) . x);

          end;

          

           A118: ( rng b1) c= ( [#] V1) by FINSEQ_1:def 4;

          ( dom T) = ( [#] V1) by FUNCT_2:def 1;

          then

           A119: ( dom (T * b1)) = ( dom b1) by A118, RELAT_1: 27;

          ( dom F) = ( [#] V1) by FUNCT_2:def 1;

          then ( dom (F9 * b1)) = ( dom b1) by A118, RELAT_1: 27;

          then ( block_diagonal (JJJ,( 0. K))) = ( block_diagonal ( <*B, JB*>,( 0. K))) & F = T by A13, A119, A101, FUNCT_1: 2, MATRIXJ1: 35, MATRLIN: 22;

          hence thesis by MATRLIN2: 36;

        end;

      end;

      let V1, V2, b1, b2, L such that

       A120: ( len b1) = ( len b2);

      let F be linear-transformation of V1, V2 such that

       A121: for i st i in ( dom b1) holds (F . (b1 /. i)) = (L * (b2 /. i)) or (i + 1) in ( dom b1) & (F . (b1 /. i)) = ((L * (b2 /. i)) + (b2 /. (i + 1)));

      set FF = { i where i be Element of NAT : i in ( dom b1) & (F . (b1 /. i)) = (L * (b2 /. i)) };

      FF c= ( dom b1)

      proof

        let x be object;

        assume x in FF;

        then ex i be Element of NAT st x = i & i in ( dom b1) & (F . (b1 /. i)) = (L * (b2 /. i));

        hence thesis;

      end;

      then

      reconsider FF as finite set;

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

      then P[( card FF)];

      hence thesis by A120, A121;

    end;

    theorem :: MATRIXJ2:29

    

     Th29: for V1 be finite-dimensional VectSp of K holds for F be nilpotent linear-transformation of V1, V1 holds ex J be non-empty FinSequence_of_Jordan_block of ( 0. K), K, b1 be OrdBasis of V1 st ( AutMt (F,b1,b1)) = ( block_diagonal (J,( 0. K)))

    proof

      defpred P[ Nat] means for V1 be finite-dimensional VectSp of K holds for F be nilpotent linear-transformation of V1, V1 st ( deg F) = $1 holds ex J be FinSequence_of_Jordan_block of ( 0. K), K, b1 be OrdBasis of V1 st ( AutMt (F,b1,b1)) = ( block_diagonal (J,( 0. K))) & for i st i in ( dom J) holds (( Len J) . i) <> 0 ;

      let V1 be finite-dimensional VectSp of K;

      let F be nilpotent linear-transformation of V1, V1;

      

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

      proof

        let n such that

         A2: P[n];

        let V1 be finite-dimensional VectSp of K;

        set n1 = (n + 1);

        let F be nilpotent linear-transformation of V1, V1 such that

         A3: ( deg F) = n1;

        set BAS = the Basis of V1;

        

         A4: BAS is linearly-independent by VECTSP_7:def 3;

        

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

        set IM = ( im (F |^ 1));

        reconsider FI = (F | IM) as linear-transformation of IM, IM by VECTSP11: 32;

        reconsider FI as nilpotent linear-transformation of IM, IM by Th17;

        (( deg FI) + 1) = n1 by A3, Th18, NAT_1: 11;

        then

        consider J be FinSequence_of_Jordan_block of ( 0. K), K, b1 be OrdBasis of IM such that

         A6: ( AutMt (FI,b1,b1)) = ( block_diagonal (J,( 0. K))) and

         A7: for i st i in ( dom J) holds (( Len J) . i) <> 0 by A2;

        

         A8: ( len b1) = ( len ( AutMt (FI,b1,b1))) by MATRIX_0:def 2

        .= ( Sum ( Len J)) by A6, MATRIXJ1:def 5;

        then

         A9: ( dom b1) = ( Seg ( Sum ( Len J))) by FINSEQ_1:def 3;

        set L = ( len J);

        set LJ = ( Len J);

        set S = ( Sum LJ);

        defpred Q[ Nat, Nat] means $2 in ( dom LJ) & $2 <= $1 & ( Sum (LJ | ($2 -' 1))) <= ($1 -' $2);

        defpred R[ object, object] means for i, k st i = $1 & k = $2 holds Q[i, k] & (i -' k) <= ( Sum (LJ | k)) & for n st Q[i, n] holds n <= k;

        

         A10: for x be object st x in ( Seg (S + L)) holds ex y be object st y in NAT & R[x, y]

        proof

          let x be object such that

           A11: x in ( Seg (S + L));

          reconsider i = x as Nat by A11;

          L <> 0

          proof

            assume

             A12: L = 0 ;

            then LJ = ( <*> NAT );

            hence thesis by A11, A12, RVSUM_1: 72;

          end;

          then

           A13: 1 <= L by NAT_1: 14;

          (1 -' 1) = 0 by XREAL_1: 232;

          then

           A14: ( Sum (LJ | (1 -' 1))) = 0 by RVSUM_1: 72;

          defpred q[ Nat] means $1 in ( dom LJ) & $1 <= i & ( Sum (LJ | ($1 -' 1))) <= (i -' $1);

          

           A15: for k st q[k] holds k <= L

          proof

            let k;

            assume q[k];

            then k <= ( len LJ) by FINSEQ_3: 25;

            hence thesis by CARD_1:def 7;

          end;

          ( len LJ) = L by CARD_1:def 7;

          then

           A16: 0 <= (i -' 1) & 1 in ( dom LJ) by A13, FINSEQ_3: 25;

          1 <= i by A11, FINSEQ_1: 1;

          then

           A17: ex k st q[k] by A14, A16;

          consider k such that

           A18: q[k] and

           A19: for n st q[n] holds n <= k from NAT_1:sch 6( A15, A17);

          

           A20: (i -' k) <= ( Sum (LJ | k))

          proof

            assume

             A21: (i -' k) > ( Sum (LJ | k));

            then (i -' k) >= (( Sum (LJ | k)) + 1) by NAT_1: 13;

            then

             A22: ((i -' k) - 1) >= ((( Sum (LJ | k)) + 1) - 1) by XREAL_1: 9;

            

             A23: (i -' k) = (i - k) by A18, XREAL_1: 233;

            

             A24: (k + 1) <= ( len LJ)

            proof

              assume (k + 1) > ( len LJ);

              then

               A25: k >= ( len LJ) by NAT_1: 13;

              then (i - k) > S by A21, A23, FINSEQ_1: 58;

              then

               A26: ((i - k) + k) > (S + k) by XREAL_1: 6;

              ( len LJ) = L by CARD_1:def 7;

              then (S + k) >= (S + L) by A25, XREAL_1: 6;

              then i > (S + L) by A26, XXREAL_0: 2;

              hence thesis by A11, FINSEQ_1: 1;

            end;

            1 <= (k + 1) by NAT_1: 14;

            then

             A27: (k + 1) in ( dom LJ) by A24, FINSEQ_3: 25;

            (i -' k) >= 1 by A21, NAT_1: 14;

            then

             A28: ((i - k) + k) >= (1 + k) by A23, XREAL_1: 6;

            then (i -' (k + 1)) = (i - (k + 1)) by XREAL_1: 233;

            then ( Sum (LJ | ((k + 1) -' 1))) <= (i -' (k + 1)) by A22, A23, NAT_D: 34;

            then (k + 1) <= k by A19, A28, A27;

            hence thesis by NAT_1: 13;

          end;

          take k;

          thus k in NAT by ORDINAL1:def 12;

          let i9,k9 be Nat;

          assume i9 = x & k9 = k;

          hence thesis by A18, A19, A20;

        end;

        consider r be Function of ( Seg (S + L)), NAT such that

         A29: for x be object st x in ( Seg (S + L)) holds R[x, (r . x)] from FUNCT_2:sch 1( A10);

        defpred P[ object, object] means for i, k st i = $1 & k = (r . i) holds ((i -' k) = ( Sum (LJ | (k -' 1))) implies ((F . $2) = (b1 . ((i -' k) + 1)) & ((i -' k) + 1) in ( dom b1))) & ((i -' k) <> ( Sum (LJ | (k -' 1))) implies ($2 = (b1 . (i -' k)) & (i -' k) in ( dom b1) & ( min (LJ,(i -' k))) = k & (((i -' k) < ( Sum (LJ | k)) implies (F . $2) = (b1 . ((i -' k) + 1)) & ((i -' k) + 1) in ( dom b1)) & ((i -' k) = ( Sum (LJ | k)) implies (F . $2) = ( 0. V1)))));

        

         A30: ( dom r) = ( Seg (S + L)) by FUNCT_2:def 1;

        

         A31: FI = ( Mx2Tran (( AutMt (FI,b1,b1)),b1,b1)) by MATRLIN2: 34;

        

         A32: for x be object st x in ( Seg (S + L)) holds ex y be object st y in the carrier of V1 & P[x, y]

        proof

          let x be object such that

           A33: x in ( Seg (S + L));

          reconsider i = x as Nat by A33;

          (r . i) = (r /. i) by A30, A33, PARTFUN1:def 6;

          then

          reconsider k = (r . i) as Element of NAT ;

          

           A34: (i -' k) <= ( Sum (LJ | k)) by A29, A33;

          

           A35: Q[i, k] by A29, A33;

          then

           A36: (LJ . k) = ( len (J . k)) by MATRIXJ1:def 3;

          k <= ( len LJ) by A35, FINSEQ_3: 25;

          then

           A37: ( Sum (LJ | k)) <= ( Sum (LJ | ( len LJ))) by POLYNOM3: 18;

          1 <= k by A35, FINSEQ_3: 25;

          then

           A38: (k -' 1) = (k - 1) by XREAL_1: 233;

          then k = ((k -' 1) + 1);

          then (LJ | k) = ((LJ | (k -' 1)) ^ <*(LJ . k)*>) by A35, FINSEQ_5: 10;

          then

           A39: ( dom LJ) = ( dom J) & ( Sum (LJ | k)) = (( Sum (LJ | (k -' 1))) + ( len (J . k))) by A36, MATRIXJ1:def 3, RVSUM_1: 74;

          

           A40: (LJ | ( len LJ)) = LJ by FINSEQ_1: 58;

          per cases ;

            suppose

             A41: (i -' k) = ( Sum (LJ | (k -' 1)));

            (b1 /. ((i -' k) + 1)) in IM & (b1 /. ((i -' k) + 1)) is Element of V1 by VECTSP_4: 10;

            then

            consider y be Element of V1 such that

             A42: ((F |^ 1) . y) = (b1 /. ((i -' k) + 1)) by RANKNULL: 13;

            take y;

            thus y in the carrier of V1;

            (i -' k) <> ( Sum (LJ | k)) by A7, A35, A36, A39, A41;

            then (i -' k) < ( Sum (LJ | k)) by A34, XXREAL_0: 1;

            then ((i -' k) + 1) <= ( Sum (LJ | k)) by NAT_1: 13;

            then

             A43: 1 <= ((i -' k) + 1) & ((i -' k) + 1) <= S by A37, A40, NAT_1: 11, XXREAL_0: 2;

            then ((i -' k) + 1) in ( dom b1) by A9;

            then (b1 /. ((i -' k) + 1)) = (b1 . ((i -' k) + 1)) by PARTFUN1:def 6;

            hence thesis by A9, A41, A43, A42, VECTSP11: 19;

          end;

            suppose

             A44: (i -' k) <> ( Sum (LJ | (k -' 1)));

            take y = (b1 /. (i -' k));

            y in IM;

            then y in V1 by VECTSP_4: 9;

            hence y in the carrier of V1;

            (i -' k) > ( Sum (LJ | (k -' 1))) by A35, A44, XXREAL_0: 1;

            then

             A45: 1 <= (i -' k) by NAT_1: 14;

            (i -' k) <= S by A34, A37, A40, XXREAL_0: 2;

            then

             A46: (i -' k) in ( dom b1) by A9, A45;

            (i -' k) <= ( Sum (LJ | k)) by A29, A33;

            then

             A47: ( min (LJ,(i -' k))) <= k by A9, A46, MATRIXJ1:def 1;

            

             A48: ( min (LJ,(i -' k))) = k

            proof

              assume ( min (LJ,(i -' k))) <> k;

              then ( min (LJ,(i -' k))) < ((k -' 1) + 1) by A38, A47, XXREAL_0: 1;

              then ( min (LJ,(i -' k))) <= (k -' 1) by NAT_1: 13;

              then

               A49: ( Sum (LJ | ( min (LJ,(i -' k))))) <= ( Sum (LJ | (k -' 1))) by POLYNOM3: 18;

              (i -' k) <= ( Sum (LJ | ( min (LJ,(i -' k))))) by A9, A46, MATRIXJ1:def 1;

              then (i -' k) <= ( Sum (LJ | (k -' 1))) by A49, XXREAL_0: 2;

              hence thesis by A35, A44, XXREAL_0: 1;

            end;

            

             A50: ( Len (J | k)) = (LJ | k) by MATRIXJ1: 17;

             A51:

            now

              assume

               A52: (i -' k) = ( Sum (LJ | k));

              (F . (b1 /. (i -' k))) = (FI . (b1 /. (i -' k))) by FUNCT_1: 49

              .= (( 0. K) * (b1 /. (i -' k))) by A6, A31, A46, A48, A50, A52, Th24

              .= ( 0. IM) by VECTSP_1: 14

              .= ( 0. V1) by VECTSP_4: 11;

              hence (F . y) = ( 0. V1);

            end;

             A53:

            now

              assume

               A54: (i -' k) < ( Sum (LJ | k));

              then ((i -' k) + 1) <= ( Sum (LJ | k)) by NAT_1: 13;

              then

               A55: 1 <= ((i -' k) + 1) & ((i -' k) + 1) <= S by A37, A40, NAT_1: 11, XXREAL_0: 2;

              then

               A56: ((i -' k) + 1) in ( dom b1) by A9;

              (F . (b1 /. (i -' k))) = (FI . (b1 /. (i -' k))) by FUNCT_1: 49

              .= ((( 0. K) * (b1 /. (i -' k))) + (b1 /. ((i -' k) + 1))) by A6, A31, A46, A48, A50, A54, Th24

              .= (( 0. IM) + (b1 /. ((i -' k) + 1))) by VECTSP_1: 14

              .= (b1 /. ((i -' k) + 1)) by RLVECT_1:def 4

              .= (b1 . ((i -' k) + 1)) by A56, PARTFUN1:def 6;

              hence (F . y) = (b1 . ((i -' k) + 1)) & ((i -' k) + 1) in ( dom b1) by A9, A55;

            end;

            let i9,k9 be Nat;

            assume x = i9 & k9 = (r . i9);

            hence thesis by A44, A46, A48, A53, A51, PARTFUN1:def 6;

          end;

        end;

        consider B be Function of ( Seg (S + L)), the carrier of V1 such that

         A57: for x be object st x in ( Seg (S + L)) holds P[x, (B . x)] from FUNCT_2:sch 1( A32);

        

         A58: ( rng B) c= the carrier of V1 by RELAT_1:def 19;

        

         A59: ( dom B) = ( Seg (S + L)) by FUNCT_2:def 1;

        then

        reconsider B as FinSequence by FINSEQ_1:def 2;

        reconsider B as FinSequence of V1 by A58, FINSEQ_1:def 4;

        reconsider RNG = ( rng B) as Subset of V1 by FINSEQ_1:def 4;

        now

          ( rng b1) is Basis of IM by MATRLIN:def 2;

          then ( rng b1) is linearly-independent Subset of IM by VECTSP_7:def 3;

          then

          reconsider rngb1 = ( rng b1) as linearly-independent Subset of V1 by VECTSP_9: 11;

          set RB = { v1 where v1 be Vector of V1 : ex i, k st i in ( Seg (L + S)) & k = (r . i) & v1 = (B . i) & (i -' k) <> ( Sum (LJ | (k -' 1))) & (i -' k) = ( Sum (LJ | k)) };

          set RA = { v1 where v1 be Vector of V1 : ex i, k st i in ( Seg (L + S)) & k = (r . i) & v1 = (B . i) & (i -' k) < ( Sum (LJ | k)) };

          

           A60: RA c= the carrier of V1

          proof

            let x be object;

            assume x in RA;

            then ex v1 be Vector of V1 st x = v1 & ex i, k st i in ( Seg (L + S)) & k = (r . i) & v1 = (B . i) & (i -' k) < ( Sum (LJ | k));

            hence thesis;

          end;

          RB c= the carrier of V1

          proof

            let x be object;

            assume x in RB;

            then ex v1 be Vector of V1 st x = v1 & ex i, k st i in ( Seg (L + S)) & k = (r . i) & v1 = (B . i) & (i -' k) <> ( Sum (LJ | (k -' 1))) & (i -' k) = ( Sum (LJ | k));

            hence thesis;

          end;

          then

          reconsider RA, RB as Subset of V1 by A60;

          let l be Linear_Combination of RNG such that

           A61: ( Sum l) = ( 0. V1);

          

           A62: (F | RA) is one-to-one

          proof

            let x1,x2 be object such that

             A63: x1 in ( dom (F | RA)) and

             A64: x2 in ( dom (F | RA)) and

             A65: ((F | RA) . x1) = ((F | RA) . x2);

            

             A66: ((F | RA) . x1) = (F . x1) & ((F | RA) . x2) = (F . x2) by A63, A64, FUNCT_1: 47;

            

             A67: ( dom (F | RA)) = (( dom F) /\ RA) by RELAT_1: 61;

            then x1 in RA by A63, XBOOLE_0:def 4;

            then

            consider v1 be Vector of V1 such that

             A68: x1 = v1 and

             A69: ex i1,k1 be Nat st i1 in ( Seg (L + S)) & k1 = (r . i1) & v1 = (B . i1) & (i1 -' k1) < ( Sum (LJ | k1));

            consider i1,k1 be Nat such that

             A70: i1 in ( Seg (L + S)) & k1 = (r . i1) and

             A71: v1 = (B . i1) and

             A72: (i1 -' k1) < ( Sum (LJ | k1)) by A69;

            k1 <= i1 by A29, A70;

            then

             A73: (i1 -' k1) = (i1 - k1) by XREAL_1: 233;

            

             A74: k1 in ( dom LJ) by A29, A70;

            then 1 <= k1 by FINSEQ_3: 25;

            then

             A75: (k1 -' 1) = (k1 - 1) by XREAL_1: 233;

            then ((k1 -' 1) + 1) <= ( len LJ) by A74, FINSEQ_3: 25;

            then

             A76: (k1 -' 1) <= ( len LJ) by NAT_1: 13;

            

             A77: b1 is one-to-one by MATRLIN:def 2;

            

             A78: ( dom LJ) = ( dom J) by MATRIXJ1:def 3;

            then

             A79: (k1 -' 1) in ( dom LJ) implies (LJ . (k1 -' 1)) <> 0 by A7;

            x2 in RA by A64, A67, XBOOLE_0:def 4;

            then

            consider v2 be Vector of V1 such that

             A80: x2 = v2 and

             A81: ex i2,k2 be Nat st i2 in ( Seg (L + S)) & k2 = (r . i2) & v2 = (B . i2) & (i2 -' k2) < ( Sum (LJ | k2));

            consider i2,k2 be Nat such that

             A82: i2 in ( Seg (L + S)) & k2 = (r . i2) and

             A83: v2 = (B . i2) and

             A84: (i2 -' k2) < ( Sum (LJ | k2)) by A81;

            

             A85: k2 <= i2 by A29, A82;

            then

             A86: (i2 -' k2) = (i2 - k2) by XREAL_1: 233;

            

             A87: k2 in ( dom LJ) by A29, A82;

            then 1 <= k2 by FINSEQ_3: 25;

            then

             A88: (k2 -' 1) = (k2 - 1) by XREAL_1: 233;

            then ((k2 -' 1) + 1) <= ( len LJ) by A87, FINSEQ_3: 25;

            then

             A89: (k2 -' 1) <= ( len LJ) by NAT_1: 13;

            

             A90: (k2 -' 1) in ( dom LJ) implies (LJ . (k2 -' 1)) <> 0 by A7, A78;

            per cases ;

              suppose

               A91: (i1 -' k1) = ( Sum (LJ | (k1 -' 1))) & (i2 -' k2) = ( Sum (LJ | (k2 -' 1)));

              then

               A92: (F . v2) = (b1 . ((i2 -' k2) + 1)) & ((i2 -' k2) + 1) in ( dom b1) by A57, A82, A83;

              (F . v1) = (b1 . ((i1 -' k1) + 1)) & ((i1 -' k1) + 1) in ( dom b1) by A57, A70, A71, A91;

              then ((i1 -' k1) + 1) = ((i2 -' k2) + 1) by A65, A66, A68, A80, A77, A92;

              then (k1 -' 1) = (k2 -' 1) by A76, A89, A79, A90, A91, MATRIXJ1: 11;

              then (i1 - k1) = (i2 - k1) by A85, A73, A75, A88, A91, XREAL_1: 233;

              hence thesis by A68, A71, A80, A83;

            end;

              suppose

               A93: (i1 -' k1) = ( Sum (LJ | (k1 -' 1))) & (i2 -' k2) <> ( Sum (LJ | (k2 -' 1)));

              then

               A94: ( min (LJ,(i2 -' k2))) = k2 by A57, A82;

              

               A95: (F . v1) = (b1 . ((i1 -' k1) + 1)) & ((i1 -' k1) + 1) in ( dom b1) by A57, A70, A71, A93;

              (F . v2) = (b1 . ((i2 -' k2) + 1)) & ((i2 -' k2) + 1) in ( dom b1) by A57, A82, A83, A84, A93;

              then

               A96: ((i1 -' k1) + 1) = ((i2 -' k2) + 1) by A65, A66, A68, A80, A77, A95;

              (k1 -' 1) <> 0

              proof

                assume (k1 -' 1) = 0 ;

                then (LJ | (k1 -' 1)) = ( <*> REAL );

                hence thesis by A29, A82, A93, A96, RVSUM_1: 72;

              end;

              then (k1 -' 1) >= 1 by NAT_1: 14;

              then

               A97: (k1 -' 1) in ( dom LJ) by A76, FINSEQ_3: 25;

              then (LJ . (k1 -' 1)) <> 0 by A7, A78;

              hence thesis by A84, A93, A94, A96, A97, MATRIXJ1: 6;

            end;

              suppose

               A98: (i1 -' k1) <> ( Sum (LJ | (k1 -' 1))) & (i2 -' k2) = ( Sum (LJ | (k2 -' 1)));

              then

               A99: ( min (LJ,(i1 -' k1))) = k1 by A57, A70;

              

               A100: (F . v2) = (b1 . ((i2 -' k2) + 1)) & ((i2 -' k2) + 1) in ( dom b1) by A57, A82, A83, A98;

              (F . v1) = (b1 . ((i1 -' k1) + 1)) & ((i1 -' k1) + 1) in ( dom b1) by A57, A70, A71, A72, A98;

              then

               A101: ((i1 -' k1) + 1) = ((i2 -' k2) + 1) by A65, A66, A68, A80, A77, A100;

              (k2 -' 1) <> 0

              proof

                assume (k2 -' 1) = 0 ;

                then (i1 -' k1) = 0 by A98, A101, RVSUM_1: 72;

                hence thesis by A29, A70, A98;

              end;

              then (k2 -' 1) >= 1 by NAT_1: 14;

              then

               A102: (k2 -' 1) in ( dom LJ) by A89, FINSEQ_3: 25;

              then (LJ . (k2 -' 1)) <> 0 by A7, A78;

              hence thesis by A72, A98, A99, A101, A102, MATRIXJ1: 6;

            end;

              suppose

               A103: (i1 -' k1) <> ( Sum (LJ | (k1 -' 1))) & (i2 -' k2) <> ( Sum (LJ | (k2 -' 1)));

              then

               A104: ( min (LJ,(i2 -' k2))) = k2 by A57, A82;

              

               A105: (F . v2) = (b1 . ((i2 -' k2) + 1)) & ((i2 -' k2) + 1) in ( dom b1) by A57, A82, A83, A84, A103;

              (F . v1) = (b1 . ((i1 -' k1) + 1)) & ((i1 -' k1) + 1) in ( dom b1) by A57, A70, A71, A72, A103;

              then ((i1 -' k1) + 1) = ((i2 -' k2) + 1) by A65, A66, A68, A80, A77, A105;

              then (i1 - k1) = (i2 - k1) by A57, A70, A73, A86, A103, A104;

              hence thesis by A68, A71, A80, A83;

            end;

          end;

          

           A106: RB c= rngb1

          proof

            let x be object;

            assume x in RB;

            then

            consider v1 be Vector of V1 such that

             A107: x = v1 and

             A108: ex i, k st i in ( Seg (L + S)) & k = (r . i) & v1 = (B . i) & (i -' k) <> ( Sum (LJ | (k -' 1))) & (i -' k) = ( Sum (LJ | k));

            consider i, k such that

             A109: i in ( Seg (L + S)) & k = (r . i) & v1 = (B . i) & (i -' k) <> ( Sum (LJ | (k -' 1))) and (i -' k) = ( Sum (LJ | k)) by A108;

            v1 = (b1 . (i -' k)) & (i -' k) in ( dom b1) by A57, A109;

            hence thesis by A107, FUNCT_1:def 3;

          end;

          

           A110: ( Carrier l) c= (RB \/ RA)

          proof

            let x be object such that

             A111: x in ( Carrier l);

            reconsider v1 = x as Vector of V1 by A111;

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

            then

            consider i be object such that

             A112: i in ( dom B) and

             A113: (B . i) = v1 by A111, FUNCT_1:def 3;

            reconsider i as Nat by A112;

            (r . i) = (r /. i) by A30, A59, A112, PARTFUN1:def 6;

            then

            reconsider k = (r . i) as Element of NAT ;

            

             A114: (i -' k) <= ( Sum (LJ | k)) by A29, A59, A112;

            per cases by A114, XXREAL_0: 1;

              suppose

               A115: (i -' k) = ( Sum (LJ | k));

              

               A116: Q[i, k] by A29, A59, A112;

              then 1 <= k by FINSEQ_3: 25;

              then (k -' 1) = (k - 1) by XREAL_1: 233;

              then ((k -' 1) + 1) = k;

              then (LJ | k) = ((LJ | (k -' 1)) ^ <*(LJ . k)*>) by A116, FINSEQ_5: 10;

              then ( dom LJ) = ( dom J) & (i -' k) = (( Sum (LJ | (k -' 1))) + (LJ . k)) by A115, MATRIXJ1:def 3, RVSUM_1: 74;

              then (i -' k) <> ( Sum (LJ | (k -' 1))) by A7, A116;

              then v1 in RB or v1 in RA by A59, A112, A113, A115;

              hence thesis by XBOOLE_0:def 3;

            end;

              suppose (i -' k) < ( Sum (LJ | k));

              then v1 in RB or v1 in RA by A59, A112, A113;

              hence thesis by XBOOLE_0:def 3;

            end;

          end;

          (F .: RA) c= rngb1

          proof

            let y be object;

            assume y in (F .: RA);

            then

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

             A117: x in RA and

             A118: y = (F . x) by FUNCT_1:def 6;

            consider v1 be Vector of V1 such that

             A119: x = v1 and

             A120: ex i, k st i in ( Seg (L + S)) & k = (r . i) & v1 = (B . i) & (i -' k) < ( Sum (LJ | k)) by A117;

            consider i, k such that

             A121: i in ( Seg (L + S)) & k = (r . i) & v1 = (B . i) & (i -' k) < ( Sum (LJ | k)) by A120;

            (i -' k) <> ( Sum (LJ | (k -' 1))) or (i -' k) = ( Sum (LJ | (k -' 1)));

            then (F . v1) = (b1 . ((i -' k) + 1)) & ((i -' k) + 1) in ( dom b1) by A57, A121;

            hence thesis by A118, A119, FUNCT_1:def 3;

          end;

          then

           A122: (F .: RA) is linearly-independent Subset of V1 by VECTSP_7: 1;

          (F .: RB) c= {( 0. V1)}

          proof

            let y be object;

            assume y in (F .: RB);

            then

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

             A123: x in RB and

             A124: y = (F . x) by FUNCT_1:def 6;

            consider v1 be Vector of V1 such that

             A125: x = v1 and

             A126: ex i, k st i in ( Seg (L + S)) & k = (r . i) & v1 = (B . i) & (i -' k) <> ( Sum (LJ | (k -' 1))) & (i -' k) = ( Sum (LJ | k)) by A123;

            (F . v1) = ( 0. V1) by A57, A126;

            hence thesis by A124, A125, TARSKI:def 1;

          end;

          then ( Carrier l) c= RB by A61, A110, A62, A122, VECTSP11: 44;

          then ( Carrier l) c= rngb1 by A106;

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

          hence ( Carrier l) = {} by A61, VECTSP_7:def 1;

        end;

        then

         A127: RNG is linearly-independent Subset of V1 by VECTSP_7:def 1;

        reconsider BAS, RNG as finite Subset of V1 by A4, VECTSP_9: 21;

        consider C be finite Subset of V1 such that C c= BAS and

         A128: ( card C) = (( card BAS) - ( card RNG)) and

         A129: the ModuleStr of V1 = ( Lin (RNG \/ C)) by A127, A5, VECTSP_9: 19;

        

         A130: ( (Omega). ( Lin BAS)) = ( (Omega). V1) by VECTSP_7:def 3;

        then

         A131: ( dim V1) = ( dim ( Lin BAS)) by VECTSP_9: 28;

        defpred W[ Nat] means $1 <= ( card C) implies ex f be FinSequence of V1 st f is one-to-one & ( len f) = ( card C) & RNG misses ( rng f) & (RNG \/ ( rng f)) is Basis of V1 & for i st i in ( dom f) & i <= $1 holds (F . (f . i)) = ( 0. V1);

        

         A132: for n st W[n] holds W[(n + 1)]

        proof

          let n such that

           A133: W[n];

          set n1 = (n + 1);

          assume

           A134: n1 <= ( card C);

          then

          consider f be FinSequence of V1 such that

           A135: f is one-to-one and

           A136: ( len f) = ( card C) and

           A137: RNG misses ( rng f) and

           A138: (RNG \/ ( rng f)) is Basis of V1 and

           A139: for i st i in ( dom f) & i <= n holds (F . (f . i)) = ( 0. V1) by A133, NAT_1: 13;

          per cases ;

            suppose (F . (f . n1)) = ( 0. V1);

            then for i st i in ( dom f) & i <= n1 holds (F . (f . i)) = ( 0. V1) by A139, NAT_1: 8;

            hence thesis by A135, A136, A137, A138;

          end;

            suppose

             A140: (F . (f . n1)) <> ( 0. V1);

            reconsider Rf = (RNG \/ ( rng f)) as finite Subset of V1 by A138;

            reconsider rngB1 = ( rng b1) as Basis of IM by MATRLIN:def 2;

            set fn = (f /. n1);

            1 <= n1 by NAT_1: 14;

            then

             A141: n1 in ( dom f) by A134, A136, FINSEQ_3: 25;

            then

             A142: (f /. n1) = (f . n1) by PARTFUN1:def 6;

            

             A143: ( rng b1) c= (F .: RNG)

            proof

              

               A144: ( dom F) = ( [#] V1) by FUNCT_2:def 1;

              let y be object;

              assume y in ( rng b1);

              then

              consider x be object such that

               A145: x in ( dom b1) and

               A146: (b1 . x) = y by FUNCT_1:def 3;

              reconsider x as Element of NAT by A145;

              

               A147: ( len LJ) = L & x <= S by A8, A145, CARD_1:def 7, FINSEQ_3: 25;

              set m = ( min (LJ,x));

              

               A148: x <= ( Sum (LJ | m)) by A9, A145, MATRIXJ1:def 1;

              

               A149: m in ( dom LJ) by A9, A145, MATRIXJ1:def 1;

              then m <= ( len LJ) by FINSEQ_3: 25;

              then (m + x) <= (L + S) by A147, XREAL_1: 7;

              then

               A150: ((m + x) - 1) <= ((L + S) - 1) by XREAL_1: 9;

              set x1 = (x -' 1);

              

               A151: 1 <= x by A145, FINSEQ_3: 25;

              then

               A152: x1 = (x - 1) by XREAL_1: 233;

              1 <= m by A149, FINSEQ_3: 25;

              then (1 + 1) <= (m + x) by A151, XREAL_1: 7;

              then

               A153: (2 - 1) <= ((m + x) - 1) by XREAL_1: 9;

              set mx = (m + x1);

              

               A154: (mx -' m) = (mx - m) by NAT_1: 11, XREAL_1: 233;

              ((L + S) - 1) <= ((L + S) - 0 ) by XREAL_1: 10;

              then mx <= (L + S) by A152, A150, XXREAL_0: 2;

              then

               A155: mx in ( Seg (S + L)) by A152, A153;

              then (r . mx) = (r /. mx) by A30, PARTFUN1:def 6;

              then

              reconsider k = (r . mx) as Element of NAT ;

              

               A156: (B . mx) in RNG by A59, A155, FUNCT_1:def 3;

              

               A157: ( Sum (LJ | (m -' 1))) < (x1 + 1) by A9, A145, A152, MATRIXJ1: 7;

              then m <= mx & ( Sum (LJ | (m -' 1))) <= (mx -' m) by A154, NAT_1: 11, NAT_1: 13;

              then

               A158: m <= k by A29, A149, A155;

              

               A159: m = k

              proof

                assume m <> k;

                then

                 A160: m < k by A158, XXREAL_0: 1;

                then

                reconsider k1 = (k - 1) as Element of NAT by NAT_1: 20;

                

                 A161: k = (k1 + 1);

                then m <= k1 by A160, NAT_1: 13;

                then

                 A162: ( Sum (LJ | m)) <= ( Sum (LJ | k1)) by POLYNOM3: 18;

                

                 A163: (mx -' k) <= (mx -' m) by A158, NAT_D: 41;

                (k -' 1) = k1 by A161, NAT_D: 34;

                then ( Sum (LJ | k1)) <= (mx -' k) by A29, A155;

                then ( Sum (LJ | m)) <= (mx -' k) by A162, XXREAL_0: 2;

                then ( Sum (LJ | m)) <= x1 by A154, A163, XXREAL_0: 2;

                hence thesis by A152, A157, A148, NAT_1: 13;

              end;

              

               A164: (mx -' m) = ( Sum (LJ | (m -' 1))) or (mx -' m) <> ( Sum (LJ | (m -' 1)));

              (mx -' m) < ( Sum (LJ | m)) by A152, A154, A157, A148, NAT_1: 13;

              then (F . (B . mx)) = (b1 . ((mx -' m) + 1)) by A57, A155, A159, A164;

              hence thesis by A146, A152, A154, A156, A144, FUNCT_1:def 6;

            end;

            (F . (f /. n1)) in ( im F) & (F |^ 1) = F by RANKNULL: 13, VECTSP11: 19;

            then (F . (f /. n1)) in ( Lin rngB1) by VECTSP_7:def 3;

            then

            consider L be Linear_Combination of rngB1 such that

             A165: (F . (f /. n1)) = ( Sum L) by VECTSP_7: 7;

            consider K be Linear_Combination of V1 such that

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

             A167: ( Sum L) = ( Sum K) by VECTSP_9: 8;

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

            then

            consider M be Linear_Combination of RNG such that

             A168: (F . ( Sum M)) = ( Sum K) by A143, A166, VECTSP11: 41, XBOOLE_1: 1;

            

             A169: (f . n1) in ( rng f) by A141, FUNCT_1:def 3;

            then

             A170: fn in Rf by A142, XBOOLE_0:def 3;

            

             A171: not fn in RNG by A137, A142, A169, XBOOLE_0: 3;

             not fn in RNG by A137, A142, A169, XBOOLE_0: 3;

            then

             A172: RNG c= (Rf \ {fn}) by XBOOLE_1: 7, ZFMISC_1: 34;

            ( Carrier M) c= RNG & ( Carrier M) = ( Carrier ( - M)) by VECTSP_6: 38, VECTSP_6:def 4;

            then ( Carrier ( - M)) c= (Rf \ {fn}) by A172;

            then

            reconsider M9 = ( - M) as Linear_Combination of (Rf \ {fn}) by VECTSP_6:def 4;

            set fnM = (fn + ( Sum M9));

            

             A173: fnM <> fn

            proof

              assume fnM = fn;

              

              then ( 0. V1) = (fnM - fn) by VECTSP_1: 16

              .= (( Sum M9) + (fn - fn)) by RLVECT_1:def 3

              .= (( Sum M9) + ( 0. V1)) by RLVECT_1:def 10

              .= ( Sum M9) by RLVECT_1:def 4

              .= ( - ( Sum M)) by VECTSP_6: 46;

              then ( 0. V1) = ( Sum M) by VECTSP_1: 28;

              hence thesis by A140, A142, A165, A167, A168, RANKNULL: 9;

            end;

            take ff = (f +* (n1,fnM));

            set fnS = (n1 .--> fnM);

            

             A174: Rf is linearly-independent by A138, VECTSP_7:def 3;

            

             A175: not fnM in (Rf \ {fn})

            proof

              ( card Rf) <> 0 by A169;

              then

              reconsider c1 = (( card Rf) - 1) as Element of NAT by NAT_1: 20;

              assume fnM in (Rf \ {fn});

              then

               A176: ((Rf \ {fn}) \/ {fnM}) = (Rf \ {fn}) by ZFMISC_1: 40;

              (c1 + 1) = ( card Rf);

              then

               A177: ( card (Rf \ {fn})) = c1 by A170, STIRL2_1: 55;

              ( card ((Rf \ {fn}) \/ {fnM})) = (c1 + 1) by A174, A170, VECTSP11: 40;

              hence thesis by A177, A176;

            end;

             not fnM in ( rng f)

            proof

              assume fnM in ( rng f);

              then fnM in Rf by XBOOLE_0:def 3;

              hence thesis by A175, A173, ZFMISC_1: 56;

            end;

            then

             A178: ( rng f) misses {fnM} by ZFMISC_1: 50;

            ( rng fnS) = {fnM} by FUNCOP_1: 8;

            then (f +* fnS) is one-to-one by A135, A178, FUNCT_4: 92;

            hence ff is one-to-one by A141, FUNCT_7:def 3;

            

             A179: ( dom ff) = ( dom f) by FUNCT_7: 30;

            hence ( len ff) = ( card C) by A136, FINSEQ_3: 29;

            

             A180: ( rng ff) = ((( rng f) \ {fn}) \/ {fnM}) by A135, A141, A142, Lm1;

            thus RNG misses ( rng ff)

            proof

              assume RNG meets ( rng ff);

              then

              consider x be object such that

               A181: x in RNG and

               A182: x in ( rng ff) by XBOOLE_0: 3;

               not x in (( rng f) \ {fn}) by A137, A181, XBOOLE_0: 3;

              then x in {fnM} by A180, A182, XBOOLE_0:def 3;

              then

               A183: x = fnM by TARSKI:def 1;

               not fnM in Rf by A175, A173, ZFMISC_1: 56;

              hence thesis by A181, A183, XBOOLE_0:def 3;

            end;

            

             A184: ((Rf \ {fn}) \/ {fnM}) = (((RNG \ {fn}) \/ (( rng f) \ {fn})) \/ {fnM}) by XBOOLE_1: 42

            .= ((RNG \/ (( rng f) \ {fn})) \/ {fnM}) by A171, ZFMISC_1: 57

            .= (RNG \/ ( rng ff)) by A180, XBOOLE_1: 4;

            then

            reconsider Rff = (RNG \/ ( rng ff)) as finite Subset of V1;

            ( dim V1) = ( card Rf) by A138, VECTSP_9:def 1

            .= ( card (RNG \/ ( rng ff))) by A174, A170, A184, VECTSP11: 40;

            then ( dim ( Lin Rff)) = ( dim V1) by A174, A170, A184, VECTSP11: 40, VECTSP_9: 26;

            then

             A185: ( (Omega). V1) = ( (Omega). ( Lin Rff)) by VECTSP_9: 28;

            ((Rf \ {fn}) \/ {fnM}) is linearly-independent by A174, A170, VECTSP11: 40;

            hence (RNG \/ ( rng ff)) is Basis of V1 by A184, A185, VECTSP_7:def 3;

            let i such that

             A186: i in ( dom ff) and

             A187: i <= n1;

            per cases by A187, XXREAL_0: 1;

              suppose i < n1;

              then (ff . i) = (f . i) & i <= n by FUNCT_7: 32, NAT_1: 13;

              hence thesis by A139, A179, A186;

            end;

              suppose i = n1;

              then (ff . i) = fnM by A179, A186, FUNCT_7: 31;

              

              hence (F . (ff . i)) = (F . (fn - ( Sum M))) by VECTSP_6: 46

              .= ((F . fn) - (F . ( Sum M))) by RANKNULL: 8

              .= ( 0. V1) by A165, A167, A168, RLVECT_1:def 10;

            end;

          end;

        end;

        

         A188: ( card (RNG \/ C)) = ((( card RNG) + ( card C)) - ( card (RNG /\ C))) by CARD_2: 45

        .= (( card BAS) - ( card (RNG /\ C))) by A128;

        then (( card (RNG \/ C)) + ( card (RNG /\ C))) = ( card BAS);

        then

         A189: ( card (RNG \/ C)) <= ( card BAS) by NAT_1: 11;

        

         A190: ( dim ( Lin BAS)) = ( card BAS) by A4, VECTSP_9: 26;

        then

         A191: ( card (RNG \/ C)) >= ( card BAS) by A130, A129, MATRLIN2: 6;

        then

         A192: ( card (RNG \/ C)) = ( card BAS) by A189, XXREAL_0: 1;

        ( dim V1) = ( dim ( Lin (RNG \/ C))) by A130, A129, VECTSP_9: 28;

        then

         A193: (RNG \/ C) is linearly-independent by A131, A190, A191, A189, MATRLIN2: 5, XXREAL_0: 1;

        

         A194: W[ 0 ]

        proof

          assume 0 <= ( card C);

          ( card C) = ( card ( Seg ( card C))) by FINSEQ_1: 57;

          then (( Seg ( card C)),C) are_equipotent by CARD_1: 5;

          then

          consider f be Function such that

           A195: f is one-to-one and

           A196: ( dom f) = ( Seg ( card C)) and

           A197: ( rng f) = C by WELLORD2:def 4;

          reconsider f as FinSequence by A196, FINSEQ_1:def 2;

          reconsider f as FinSequence of V1 by A197, FINSEQ_1:def 4;

          take f;

          thus f is one-to-one & ( len f) = ( card C) by A195, A196, FINSEQ_1:def 3;

          (RNG /\ C) = {} by A188, A192;

          hence RNG misses ( rng f) & (RNG \/ ( rng f)) is Basis of V1 by A129, A193, A197, VECTSP_7:def 3, XBOOLE_0:def 7;

          let i;

          assume i in ( dom f) & i <= 0 ;

          hence thesis by FINSEQ_3: 25;

        end;

        for n holds W[n] from NAT_1:sch 2( A194, A132);

        then

        consider f be FinSequence of V1 such that

         A198: f is one-to-one and

         A199: ( len f) = ( card C) and

         A200: RNG misses ( rng f) and

         A201: (RNG \/ ( rng f)) is Basis of V1 and

         A202: for i st i in ( dom f) & i <= ( card C) holds (F . (f . i)) = ( 0. V1);

        

         A203: ( rng (B ^ f)) = (( rng B) \/ ( rng f)) by FINSEQ_1: 31;

        now

          let x1,x2 be object such that

           A204: x1 in ( dom B) and

           A205: x2 in ( dom B) and

           A206: (B . x1) = (B . x2);

          reconsider i1 = x1, i2 = x2 as Nat by A204, A205;

          (r /. i1) = (r . i1) & (r /. i2) = (r . i2) by A30, A59, A204, A205, PARTFUN1:def 6;

          then

          reconsider k1 = (r . i1), k2 = (r . i2) as Element of NAT ;

          

           A207: (i1 -' k1) = ( Sum (LJ | (k1 -' 1))) implies (F . (B . x1)) = (b1 . ((i1 -' k1) + 1)) & ((i1 -' k1) + 1) in ( dom b1) by A57, A59, A204;

          

           A208: Q[i1, k1] by A29, A59, A204;

          then

           A209: (i1 -' k1) = (i1 - k1) by XREAL_1: 233;

          

           A210: Q[i2, k2] by A29, A59, A205;

          then

           A211: (i2 -' k2) = (i2 - k2) by XREAL_1: 233;

          

           A212: (k2 -' 1) <= k2 by NAT_D: 35;

          

           A213: (i1 -' k1) <> ( Sum (LJ | (k1 -' 1))) implies (B . x1) = (b1 . (i1 -' k1)) & (i1 -' k1) in ( dom b1) & ( min (LJ,(i1 -' k1))) = k1 & ((i1 -' k1) < ( Sum (LJ | k1)) implies (F . (B . x1)) = (b1 . ((i1 -' k1) + 1)) & ((i1 -' k1) + 1) in ( dom b1)) & ((i1 -' k1) = ( Sum (LJ | k1)) implies (F . (B . x1)) = ( 0. V1)) by A57, A59, A204;

          k2 <= ( len LJ) by A210, FINSEQ_3: 25;

          then

           A214: (k2 -' 1) <= ( len LJ) by A212, XXREAL_0: 2;

          1 <= k1 by A208, FINSEQ_3: 25;

          then

           A215: (k1 -' 1) = (k1 - 1) by XREAL_1: 233;

          

           A216: (i2 -' k2) <> ( Sum (LJ | (k2 -' 1))) implies (B . x2) = (b1 . (i2 -' k2)) & (i2 -' k2) in ( dom b1) & ( min (LJ,(i2 -' k2))) = k2 & ((i2 -' k2) < ( Sum (LJ | k2)) implies (F . (B . x2)) = (b1 . ((i2 -' k2) + 1)) & ((i2 -' k2) + 1) in ( dom b1)) & ((i2 -' k2) = ( Sum (LJ | k2)) implies (F . (B . x2)) = ( 0. V1)) by A57, A59, A205;

          1 <= k2 by A210, FINSEQ_3: 25;

          then

           A217: (k2 -' 1) = (k2 - 1) by XREAL_1: 233;

          

           A218: (i2 -' k2) = ( Sum (LJ | (k2 -' 1))) implies (F . (B . x2)) = (b1 . ((i2 -' k2) + 1)) & ((i2 -' k2) + 1) in ( dom b1) by A57, A59, A205;

          

           A219: (k1 -' 1) <= k1 by NAT_D: 35;

          k1 <= ( len LJ) by A208, FINSEQ_3: 25;

          then

           A220: (k1 -' 1) <= ( len LJ) by A219, XXREAL_0: 2;

          

           A221: ( dom LJ) = ( dom J) by MATRIXJ1:def 3;

          ( rng b1) is Basis of IM by MATRLIN:def 2;

          then

           A222: ( rng b1) is linearly-independent Subset of IM by VECTSP_7:def 3;

          

           A223: b1 is one-to-one by MATRLIN:def 2;

          

           A224: (i1 -' k1) <= ( Sum (LJ | k1)) & (i2 -' k2) <= ( Sum (LJ | k2)) by A29, A59, A204, A205;

          now

            per cases by A224, XXREAL_0: 1;

              suppose

               A225: (i1 -' k1) = ( Sum (LJ | (k1 -' 1))) & (i2 -' k2) = ( Sum (LJ | (k2 -' 1)));

              then

               A226: (F . (B . x2)) = (b1 . ((i2 -' k2) + 1)) & ((i2 -' k2) + 1) in ( dom b1) by A57, A59, A205;

              (F . (B . x1)) = (b1 . ((i1 -' k1) + 1)) & ((i1 -' k1) + 1) in ( dom b1) by A57, A59, A204, A225;

              then

               A227: ((i1 -' k1) + 1) = ((i2 -' k2) + 1) by A206, A223, A226;

              

               A228: (k2 -' 1) in ( dom LJ) implies (LJ . (k2 -' 1)) <> 0 by A7, A221;

              (k1 -' 1) in ( dom LJ) implies (LJ . (k1 -' 1)) <> 0 by A7, A221;

              then (k1 -' 1) = (k2 -' 1) by A220, A214, A225, A227, A228, MATRIXJ1: 11;

              hence i1 = i2 by A215, A217, A209, A211, A227;

            end;

              suppose

               A229: (i1 -' k1) = ( Sum (LJ | (k1 -' 1))) & (i2 -' k2) <> ( Sum (LJ | (k2 -' 1))) & (i2 -' k2) < ( Sum (LJ | k2));

              then

               A230: ( min (LJ,(i2 -' k2))) = k2 by A57, A59, A205;

              

               A231: (F . (B . x2)) = (b1 . ((i2 -' k2) + 1)) & ((i2 -' k2) + 1) in ( dom b1) by A57, A59, A205, A229;

              (F . (B . x1)) = (b1 . ((i1 -' k1) + 1)) & ((i1 -' k1) + 1) in ( dom b1) by A57, A59, A204, A229;

              then

               A232: ((i1 -' k1) + 1) = ((i2 -' k2) + 1) by A206, A223, A231;

              (k1 -' 1) <> 0

              proof

                assume (k1 -' 1) = 0 ;

                then (LJ | (k1 -' 1)) = ( <*> REAL );

                hence thesis by A29, A59, A205, A229, A232, RVSUM_1: 72;

              end;

              then (k1 -' 1) >= 1 by NAT_1: 14;

              then

               A233: (k1 -' 1) in ( dom LJ) by A220, FINSEQ_3: 25;

              then (LJ . (k1 -' 1)) <> 0 by A7, A221;

              hence i1 = i2 by A229, A230, A232, A233, MATRIXJ1: 6;

            end;

              suppose (i1 -' k1) = ( Sum (LJ | (k1 -' 1))) & (i2 -' k2) <> ( Sum (LJ | (k2 -' 1))) & (i2 -' k2) = ( Sum (LJ | k2));

              then (b1 . ((i1 -' k1) + 1)) = ( 0. IM) & (b1 . ((i1 -' k1) + 1)) in ( rng b1) by A206, A207, A216, FUNCT_1:def 3, VECTSP_4: 11;

              hence i1 = i2 by A222, VECTSP_7: 2;

            end;

              suppose

               A234: (i2 -' k2) = ( Sum (LJ | (k2 -' 1))) & (i1 -' k1) <> ( Sum (LJ | (k1 -' 1))) & (i1 -' k1) < ( Sum (LJ | k1));

              then

               A235: ( min (LJ,(i1 -' k1))) = k1 by A57, A59, A204;

              

               A236: (F . (B . x1)) = (b1 . ((i1 -' k1) + 1)) & ((i1 -' k1) + 1) in ( dom b1) by A57, A59, A204, A234;

              (F . (B . x2)) = (b1 . ((i2 -' k2) + 1)) & ((i2 -' k2) + 1) in ( dom b1) by A57, A59, A205, A234;

              then

               A237: ((i2 -' k2) + 1) = ((i1 -' k1) + 1) by A206, A223, A236;

              (k2 -' 1) <> 0

              proof

                assume (k2 -' 1) = 0 ;

                then (i1 -' k1) = 0 by A234, A237, RVSUM_1: 72;

                hence thesis by A29, A59, A204, A234;

              end;

              then (k2 -' 1) >= 1 by NAT_1: 14;

              then

               A238: (k2 -' 1) in ( dom LJ) by A214, FINSEQ_3: 25;

              then (LJ . (k2 -' 1)) <> 0 by A7, A221;

              hence i1 = i2 by A234, A235, A237, A238, MATRIXJ1: 6;

            end;

              suppose (i2 -' k2) = ( Sum (LJ | (k2 -' 1))) & (i1 -' k1) <> ( Sum (LJ | (k1 -' 1))) & (i1 -' k1) = ( Sum (LJ | k1));

              then (b1 . ((i2 -' k2) + 1)) = ( 0. IM) & (b1 . ((i2 -' k2) + 1)) in ( rng b1) by A206, A213, A218, FUNCT_1:def 3, VECTSP_4: 11;

              hence i1 = i2 by A222, VECTSP_7: 2;

            end;

              suppose

               A239: (i1 -' k1) <> ( Sum (LJ | (k1 -' 1))) & (i2 -' k2) <> ( Sum (LJ | (k2 -' 1)));

              then (i2 -' k2) = (i1 -' k1) by A206, A213, A216, A223;

              then (i2 - k1) = (i1 - k1) by A57, A59, A205, A213, A209, A211, A239;

              hence i1 = i2;

            end;

          end;

          hence x1 = x2;

        end;

        then B is one-to-one;

        then (B ^ f) is one-to-one by A198, A200, FINSEQ_3: 91;

        then

        reconsider Bf = (B ^ f) as OrdBasis of V1 by A201, A203, MATRLIN:def 2;

        for i st i in ( dom Bf) holds (F . (Bf /. i)) = (( 0. K) * (Bf /. i)) or (i + 1) in ( dom Bf) & (F . (Bf /. i)) = ((( 0. K) * (Bf /. i)) + (Bf /. (i + 1)))

        proof

          let i such that

           A240: i in ( dom Bf);

          

           A241: (Bf /. i) = (Bf . i) by A240, PARTFUN1:def 6;

          per cases by A240, FINSEQ_1: 25;

            suppose

             A242: i in ( dom B);

            then (r /. i) = (r . i) by A30, A59, PARTFUN1:def 6;

            then

            reconsider k = (r . i) as Element of NAT ;

            

             A243: (i -' k) <= ( Sum (LJ | k)) by A29, A59, A242;

            

             A244: Q[i, k] by A29, A59, A242;

            then 1 <= k by FINSEQ_3: 25;

            then (k -' 1) = (k - 1) by XREAL_1: 233;

            then ((k -' 1) + 1) = k;

            then (LJ | k) = ((LJ | (k -' 1)) ^ <*(LJ . k)*>) by A244, FINSEQ_5: 10;

            then

             A245: ( dom LJ) = ( dom J) & ( Sum (LJ | k)) = (( Sum (LJ | (k -' 1))) + (LJ . k)) by MATRIXJ1:def 3, RVSUM_1: 74;

            per cases by A243, XXREAL_0: 1;

              suppose

               A246: (i -' k) = ( Sum (LJ | k));

              then

               A247: (i -' k) <> ( Sum (LJ | (k -' 1))) by A7, A244, A245;

              (F . (Bf /. i)) = (F . (B . i)) by A241, A242, FINSEQ_1:def 7

              .= ( 0. V1) by A57, A59, A242, A246, A247

              .= (( 0. K) * (Bf /. i)) by VECTSP_1: 14;

              hence thesis;

            end;

              suppose

               A248: (i -' k) < ( Sum (LJ | k));

              

               A249: (i -' k) = ( Sum (LJ | (k -' 1))) or (i -' k) <> ( Sum (LJ | (k -' 1)));

              then

               A250: (F . (B . i)) = (b1 . ((i -' k) + 1)) by A57, A59, A242, A248;

              ( dom J) = ( dom LJ) by MATRIXJ1:def 3;

              then

               A251: k <= L by A244, FINSEQ_3: 25;

              

               A252: ((i -' k) + 1) <= ( Sum (LJ | k)) by A248, NAT_1: 13;

              

               A253: (i -' k) = (i - k) by A244, XREAL_1: 233;

              

               A254: ((i -' k) + 1) in ( dom b1) by A57, A59, A242, A248, A249;

              then

               A255: 1 <= ((i -' k) + 1) by FINSEQ_3: 25;

              then

               A256: (1 + 0 ) <= (((i - k) + 1) + k) by A253, XREAL_1: 7;

              ((i -' k) + 1) <= S by A8, A254, FINSEQ_3: 25;

              then (((i - k) + 1) + k) <= (S + L) by A251, A253, XREAL_1: 7;

              then

               A257: (i + 1) in ( Seg (S + L)) by A256;

              then (r /. (i + 1)) = (r . (i + 1)) by A30, PARTFUN1:def 6;

              then

              reconsider k1 = (r . (i + 1)) as Element of NAT ;

              set i1 = (i + 1);

              

               A258: ( dom B) c= ( dom Bf) by FINSEQ_1: 26;

              (1 + k) <= (((i - k) + 1) + k) by A255, A253, XREAL_1: 7;

              then

               A259: k <= (i + 1) by NAT_1: 13;

              then

               A260: (i1 -' k) = (i1 - k) by XREAL_1: 233;

              ( Sum (LJ | (k -' 1))) <= ((i -' k) + 1) by A244, NAT_1: 12;

              then

               A261: k <= k1 by A29, A244, A253, A257, A259, A260;

              

               A262: Q[i1, k1] by A29, A257;

              

               A263: k = k1

              proof

                assume

                 A264: k <> k1;

                then

                 A265: k < k1 by A261, XXREAL_0: 1;

                then

                reconsider K1 = (k1 - 1) as Element of NAT by NAT_1: 20;

                

                 A266: (i1 -' k1) <= (i1 -' k) by A261, NAT_D: 41;

                (i1 - k1) = (i1 -' k1) by A262, XREAL_1: 233;

                then (i1 -' k1) <> (i1 -' k) by A260, A264;

                then

                 A267: (i1 -' k1) < (i1 -' k) by A266, XXREAL_0: 1;

                

                 A268: k1 = (K1 + 1);

                then k <= K1 by A265, NAT_1: 13;

                then

                 A269: ( Sum (LJ | k)) <= ( Sum (LJ | K1)) by POLYNOM3: 18;

                (k1 -' 1) = K1 by A268, NAT_D: 34;

                then ( Sum (LJ | K1)) <= (i1 -' k1) by A29, A257;

                then ( Sum (LJ | k)) <= (i1 -' k1) by A269, XXREAL_0: 2;

                hence thesis by A252, A253, A260, A267, XXREAL_0: 2;

              end;

              ( Sum (LJ | (k -' 1))) < ((i -' k) + 1) by A244, NAT_1: 13;

              then (B . i1) = (b1 . ((i -' k) + 1)) by A57, A253, A257, A260, A263;

              then (Bf . i1) = (b1 . ((i -' k) + 1)) by A59, A257, FINSEQ_1:def 7;

              then (Bf /. i1) = (b1 . ((i -' k) + 1)) by A59, A257, A258, PARTFUN1:def 6;

              

              then (F . (Bf /. i)) = (Bf /. i1) by A241, A242, A250, FINSEQ_1:def 7

              .= (( 0. V1) + (Bf /. i1)) by RLVECT_1:def 4

              .= ((( 0. K) * (Bf /. i)) + (Bf /. i1)) by VECTSP_1: 14;

              hence thesis by A59, A257, A258;

            end;

          end;

            suppose ex j st j in ( dom f) & i = (( len B) + j);

            then

            consider j such that

             A270: j in ( dom f) and

             A271: i = (( len B) + j);

            

             A272: j <= ( len f) by A270, FINSEQ_3: 25;

            (F . (Bf /. i)) = (F . (f . j)) by A241, A270, A271, FINSEQ_1:def 7

            .= ( 0. V1) by A199, A202, A270, A272

            .= (( 0. K) * (Bf /. i)) by VECTSP_1: 14;

            hence thesis;

          end;

        end;

        then

        consider J be non-empty FinSequence_of_Jordan_block of ( 0. K), K such that

         A273: ( AutMt (F,Bf,Bf)) = ( block_diagonal (J,( 0. K))) by Th28;

        now

          

           A274: ( dom ( Len J)) = ( dom J) by MATRIXJ1:def 3;

          let i such that

           A275: i in ( dom J);

          (J . i) <> {} by A275, FUNCT_1:def 9;

          hence (( Len J) . i) <> 0 by A275, A274, MATRIXJ1:def 3;

        end;

        hence thesis by A273;

      end;

      

       A276: P[ 0 ]

      proof

        reconsider J = {} as FinSequence_of_Jordan_block of ( 0. K), K by Th10;

        let V1 be finite-dimensional VectSp of K;

        set b1 = the OrdBasis of V1;

        let F be nilpotent linear-transformation of V1, V1;

        assume ( deg F) = 0 ;

        

        then ( [#] V1) = {( 0. V1)} by Th15

        .= the carrier of ( (0). V1) by VECTSP_4:def 3;

        then ( (0). V1) = ( (Omega). V1) by VECTSP_4: 29;

        

        then

         A277: 0 = ( dim V1) by VECTSP_9: 29

        .= ( len b1) by MATRLIN2: 21

        .= ( len ( AutMt (F,b1,b1))) by MATRIX_0:def 2;

        take J, b1;

        

        thus ( AutMt (F,b1,b1)) = {} by A277

        .= ( block_diagonal (J,( 0. K))) by MATRIXJ1: 22;

        thus thesis;

      end;

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

      then P[( deg F)];

      then

      consider J be FinSequence_of_Jordan_block of ( 0. K), K, b1 be OrdBasis of V1 such that

       A278: ( AutMt (F,b1,b1)) = ( block_diagonal (J,( 0. K))) and

       A279: for i st i in ( dom J) holds (( Len J) . i) <> 0 ;

      now

        let x be object such that

         A280: x in ( dom J);

        reconsider i = x as Element of NAT by A280;

        ( dom J) = ( dom ( Len J)) & (( Len J) . i) <> 0 by A279, A280, MATRIXJ1:def 3;

        then (J . i) is non empty by A280, MATRIXJ1:def 3;

        hence (J . x) is non empty;

      end;

      then J is non-empty;

      hence thesis by A278;

    end;

    theorem :: MATRIXJ2:30

    

     Th30: for V be VectSp of K holds for F be linear-transformation of V, V, V1 be finite-dimensional Subspace of V, F1 be linear-transformation of V1, V1 st V1 = ( ker ((F + (( - L) * ( id V))) |^ n)) & (F | V1) = F1 holds ex J be non-empty FinSequence_of_Jordan_block of L, K, b1 be OrdBasis of V1 st ( AutMt (F1,b1,b1)) = ( block_diagonal (J,( 0. K)))

    proof

      let V be VectSp of K;

      let F be linear-transformation of V, V;

      let V1 be finite-dimensional Subspace of V;

      let F1 be linear-transformation of V1, V1 such that

       A1: V1 = ( ker ((F + (( - L) * ( id V))) |^ n)) and

       A2: (F | V1) = F1;

      set FL = (F + (( - L) * ( id V)));

      reconsider FLV = (FL | V1) as nilpotent linear-transformation of V1, V1 by A1, Th14;

       A3:

      now

        let x be object;

        assume x in ( dom FLV);

        then

        reconsider v1 = x as Vector of V1 by FUNCT_2:def 1;

        reconsider v = v1 as Vector of V by VECTSP_4: 10;

        (( id V) . v) = v by FUNCT_1: 18;

        then

         A4: (( - L) * (( id V) . v)) = (( - L) * (( id V1) . v1)) by FUNCT_1: 18, VECTSP_4: 14;

        

         A5: (F . v1) = (F1 . v1) by A2, FUNCT_1: 49;

        

        thus (FLV . x) = ((F + (( - L) * ( id V))) . v) by FUNCT_1: 49

        .= ((F . v) + ((( - L) * ( id V)) . v)) by MATRLIN:def 3

        .= ((F . v) + (( - L) * (( id V) . v))) by MATRLIN:def 4

        .= ((F1 . v1) + (( - L) * (( id V1) . v1))) by A4, A5, VECTSP_4: 13

        .= ((F1 . v1) + ((( - L) * ( id V1)) . v1)) by MATRLIN:def 4

        .= ((F1 + (( - L) * ( id V1))) . x) by MATRLIN:def 3;

      end;

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

      .= ( dom (F1 + (( - L) * ( id V1)))) by FUNCT_2:def 1;

      then

       A6: FLV = (F1 + (( - L) * ( id V1))) by A3;

      consider J be non-empty FinSequence_of_Jordan_block of ( 0. K), K, b1 be OrdBasis of V1 such that

       A7: ( AutMt (FLV,b1,b1)) = ( block_diagonal (J,( 0. K))) by Th29;

      (L + ( 0. K)) = L by RLVECT_1:def 4;

      then

      reconsider JM = (J (+) ( mlt ((( len J) |-> L),( 1. (K,( Len J)))))) as FinSequence_of_Jordan_block of L, K by Th12;

      now

        let x be object such that

         A8: x in ( dom JM);

        reconsider i = x as Nat by A8;

        

         A9: (JM . i) = ((J . i) + (( mlt ((( len J) |-> L),( 1. (K,( Len J))))) . i)) by A8, MATRIXJ1:def 10;

        ( dom JM) = ( dom J) by MATRIXJ1:def 10;

        then (J . i) <> {} by A8, FUNCT_1:def 9;

        hence (JM . x) is non empty by A9, MATRIX_3:def 3;

      end;

      then

      reconsider JM as non-empty FinSequence_of_Jordan_block of L, K by FUNCT_1:def 9;

      take JM, b1;

      set Aid = ( AutMt (( id V1),b1,b1));

      set AF1 = ( AutMt (F1,b1,b1));

       A10:

      now

        

         A11: ( Indices Aid) = ( Indices AF1) by MATRIX_0: 26;

        let i, j such that

         A12: [i, j] in ( Indices AF1);

        ( Indices (AF1 + (( - L) * Aid))) = ( Indices AF1) by MATRIX_0: 26;

        

        hence (((AF1 + (( - L) * Aid)) + (L * Aid)) * (i,j)) = (((AF1 + (( - L) * Aid)) * (i,j)) + ((L * Aid) * (i,j))) by A12, MATRIX_3:def 3

        .= (((AF1 * (i,j)) + ((( - L) * Aid) * (i,j))) + ((L * Aid) * (i,j))) by A12, MATRIX_3:def 3

        .= ((AF1 * (i,j)) + (((( - L) * Aid) * (i,j)) + ((L * Aid) * (i,j)))) by RLVECT_1:def 3

        .= ((AF1 * (i,j)) + ((( - L) * (Aid * (i,j))) + ((L * Aid) * (i,j)))) by A12, A11, MATRIX_3:def 5

        .= ((AF1 * (i,j)) + ((( - L) * (Aid * (i,j))) + (L * (Aid * (i,j))))) by A12, A11, MATRIX_3:def 5

        .= ((AF1 * (i,j)) + ((( - L) + L) * (Aid * (i,j)))) by VECTSP_1:def 3

        .= ((AF1 * (i,j)) + (( 0. K) * (Aid * (i,j)))) by VECTSP_1: 16

        .= ((AF1 * (i,j)) + ( 0. K))

        .= (AF1 * (i,j)) by RLVECT_1:def 4;

      end;

      

       A13: ( Len ( mlt ((( len J) |-> L),( 1. (K,( Len J)))))) = ( Len ( 1. (K,( Len J)))) by MATRIXJ1: 62

      .= ( Len J) by MATRIXJ1: 56;

      ( dom ( Len J)) = ( dom ( 1. (K,( Len J)))) by MATRIXJ1:def 8;

      

      then

       A14: ( len ( 1. (K,( Len J)))) = ( len ( Len J)) by FINSEQ_3: 29

      .= ( len J) by CARD_1:def 7;

      

       A15: ( Sum ( Len J)) = ( len ( AutMt (FLV,b1,b1))) by A7, MATRIXJ1:def 5

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

      

       A16: ( Width ( mlt ((( len J) |-> L),( 1. (K,( Len J)))))) = ( Width ( 1. (K,( Len J)))) by MATRIXJ1: 62

      .= ( Len J) by MATRIXJ1: 56

      .= ( Width J) by MATRIXJ1: 46;

      ( Mx2Tran (( AutMt ((( - L) * ( id V1)),b1,b1)),b1,b1)) = (( - L) * ( id V1)) by MATRLIN2: 34

      .= (( - L) * ( Mx2Tran (Aid,b1,b1))) by MATRLIN2: 34

      .= ( Mx2Tran ((( - L) * Aid),b1,b1)) by MATRLIN2: 38;

      then ( AutMt ((( - L) * ( id V1)),b1,b1)) = (( - L) * Aid) by MATRLIN2: 39;

      

      then (( AutMt (FLV,b1,b1)) + (L * Aid)) = ((AF1 + (( - L) * Aid)) + (L * Aid)) by A6, MATRLIN: 42

      .= AF1 by A10, MATRIX_0: 27;

      

      hence AF1 = (( block_diagonal (J,( 0. K))) + (L * ( 1. (K,( Sum ( Len J)))))) by A7, A15, MATRLIN2: 28

      .= (( block_diagonal (J,( 0. K))) + (L * ( block_diagonal (( 1. (K,( Len J))),( 0. K))))) by MATRIXJ1: 61

      .= (( block_diagonal (J,( 0. K))) + ( block_diagonal (( mlt ((( len J) |-> L),( 1. (K,( Len J))))),(L * ( 0. K))))) by A14, MATRIXJ1: 65

      .= (( block_diagonal (J,( 0. K))) + ( block_diagonal (( mlt ((( len J) |-> L),( 1. (K,( Len J))))),( 0. K))))

      .= ( block_diagonal (JM,(( 0. K) + ( 0. K)))) by A13, A16, MATRIXJ1: 72

      .= ( block_diagonal (JM,( 0. K))) by RLVECT_1:def 4;

    end;

    begin

    theorem :: MATRIXJ2:31

    

     Th31: for K be algebraic-closed Field holds for V be non trivial finite-dimensional VectSp of K, F be linear-transformation of V, V holds ex J be non-empty FinSequence_of_Jordan_block of K, b1 be OrdBasis of V st ( AutMt (F,b1,b1)) = ( block_diagonal (J,( 0. K))) & for L be Scalar of K holds L is eigenvalue of F iff ex i st i in ( dom J) & (J . i) = ( Jordan_block (L,( len (J . i))))

    proof

      let K be algebraic-closed Field;

      defpred P[ Nat] means for V be non trivial finite-dimensional VectSp of K st ( dim V) <= $1 holds for F be linear-transformation of V, V holds ex J be non-empty FinSequence_of_Jordan_block of K, b1 be OrdBasis of V st ( AutMt (F,b1,b1)) = ( block_diagonal (J,( 0. K))) & for L be Scalar of K holds L is eigenvalue of F iff ex i st i in ( dom J) & (J . i) = ( Jordan_block (L,( len (J . i))));

      let V be non trivial finite-dimensional VectSp of K, F be linear-transformation of V, V;

      

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

      proof

        let n such that

         A2: P[n];

        set n1 = (n + 1);

        let V be non trivial finite-dimensional VectSp of K such that

         A3: ( dim V) <= n1;

        per cases by A3, NAT_1: 8;

          suppose ( dim V) <= n;

          hence thesis by A2;

        end;

          suppose

           A4: ( dim V) = n1;

          let F be linear-transformation of V, V;

          

           A5: F is with_eigenvalues by VECTSP11: 16;

          then

          consider v be Vector of V, L be Scalar of K such that

           A6: v <> ( 0. V) & (F . v) = (L * v) by VECTSP11:def 1;

          set FL = (F + (( - L) * ( id V)));

          L is eigenvalue of F by A5, A6, VECTSP11:def 2;

          then ( ker FL) is non trivial by A5, VECTSP11: 14;

          then

           A7: ( dim ( ker FL)) <> 0 by MATRLIN2: 42;

          consider m such that

           A8: ( UnionKers FL) = ( ker (FL |^ m)) by VECTSP11: 27;

          set IM = ( im (FL |^ m));

          set KER = ( ker (FL |^ m));

          

           A9: ( dim V) = (( dim KER) + ( dim IM)) by A8, VECTSP11: 35, VECTSP_9: 34;

          

           A10: IM is Linear_Compl of KER by A8, VECTSP11: 35, VECTSP_5: 37;

          reconsider FK = (F | KER) as linear-transformation of KER, KER by VECTSP11: 29;

          consider Jk be non-empty FinSequence_of_Jordan_block of L, K, Bker be OrdBasis of KER such that

           A11: ( AutMt (FK,Bker,Bker)) = ( block_diagonal (Jk,( 0. K))) by Th30;

          (FL |^ 1) = FL by VECTSP11: 19;

          then

           A12: ( ker FL) is Subspace of KER by A8, VECTSP11: 25;

          

           A13: ( len Jk) <> 0

          proof

            assume ( len Jk) = 0 ;

            

            then ( Len Jk) = ( <*> NAT )

            .= ( <*> REAL );

            

            then 0 = ( len ( block_diagonal (Jk,( 0. K)))) by MATRIXJ1:def 5, RVSUM_1: 72

            .= ( len Bker) by A11, MATRIX_0:def 2

            .= ( dim KER) by MATRLIN2: 21;

            hence thesis by A12, A7, VECTSP_9: 25;

          end;

          reconsider FI = (F | IM) as linear-transformation of IM, IM by VECTSP11: 33;

          

           A14: (KER /\ IM) = ( (0). V) by A8, VECTSP11: 34;

          

           A15: V is_the_direct_sum_of (KER,IM) by A8, VECTSP11: 35;

          then

           A16: (KER + IM) = ( (Omega). V) by VECTSP_5:def 4;

          per cases ;

            suppose

             A17: IM is trivial;

            set Bim = the OrdBasis of IM;

             0 = ( dim IM) by A17, MATRLIN2: 42

            .= ( len Bim) by MATRLIN2: 21

            .= ( len ( AutMt (FI,Bim,Bim))) by MATRIX_0:def 2;

            then

             A18: ( AutMt (FI,Bim,Bim)) = {} ;

            (Bker ^ Bim) is OrdBasis of (KER + IM) by A14, MATRLIN2: 26;

            then

            reconsider BB = (Bker ^ Bim) as OrdBasis of V by A16, MATRLIN2: 4;

            take Jk, BB;

            

             A19: ( dim IM) = 0 implies ( dim IM) = 0 ;

            ( dim KER) = 0 implies ( dim KER) = 0 ;

            

            hence ( AutMt (F,BB,BB)) = ( block_diagonal ( <*( AutMt (FK,Bker,Bker)), ( AutMt (FI,Bim,Bim))*>,( 0. K))) by A15, A19, MATRLIN2: 27

            .= ( block_diagonal ( <*( AutMt (FK,Bker,Bker))*>,( 0. K))) by A18, MATRIXJ1: 40

            .= ( block_diagonal (Jk,( 0. K))) by A11, MATRIXJ1: 34;

            let L1 be Scalar of K;

            thus L1 is eigenvalue of F implies ex i st i in ( dom Jk) & (Jk . i) = ( Jordan_block (L1,( len (Jk . i))))

            proof

              assume

               A20: L1 is eigenvalue of F;

              

               A21: L1 = L

              proof

                assume L <> L1;

                then FI is with_eigenvalues & L1 is eigenvalue of FI by A5, A8, A10, A20, VECTSP11: 39;

                then ex v1 be Vector of IM st v1 <> ( 0. IM) & (FI . v1) = (L1 * v1) by VECTSP11:def 2;

                hence thesis by A17;

              end;

              take i = ( len Jk);

              i in ( Seg ( len Jk)) by A13, FINSEQ_1: 3;

              hence i in ( dom Jk) by FINSEQ_1:def 3;

              then ex k st (Jk . i) = ( Jordan_block (L,k)) by Def3;

              hence thesis by A21, Def1;

            end;

            given i such that

             A22: i in ( dom Jk) and

             A23: (Jk . i) = ( Jordan_block (L1,( len (Jk . i))));

            (Jk . i) <> {} by A22, FUNCT_1:def 9;

            then ( len (Jk . i)) in ( Seg ( len (Jk . i))) by FINSEQ_1: 3;

            then [( len (Jk . i)), ( len (Jk . i))] in [:( Seg ( len (Jk . i))), ( Seg ( len (Jk . i))):] by ZFMISC_1: 87;

            then

             A24: [( len (Jk . i)), ( len (Jk . i))] in ( Indices (Jk . i)) by MATRIX_0: 24;

            ex k st (Jk . i) = ( Jordan_block (L,k)) by A22, Def3;

            

            then L = ((Jk . i) * (( len (Jk . i)),( len (Jk . i)))) by A24, Def1

            .= L1 by A23, A24, Def1;

            hence thesis by A5, A6, VECTSP11:def 2;

          end;

            suppose

             A25: IM is non trivial;

            n1 <> ( dim IM) & ( dim IM) <= n1 by A4, A12, A7, A9, VECTSP_9: 25;

            then ( dim IM) < n1 by XXREAL_0: 1;

            then ( dim IM) <= n by NAT_1: 13;

            then

            consider Ji be non-empty FinSequence_of_Jordan_block of K, Bim be OrdBasis of IM such that

             A26: ( AutMt (FI,Bim,Bim)) = ( block_diagonal (Ji,( 0. K))) and

             A27: for L be Scalar of K holds L is eigenvalue of FI iff ex i st i in ( dom Ji) & (Ji . i) = ( Jordan_block (L,( len (Ji . i)))) by A2, A25;

            (Bker ^ Bim) is OrdBasis of (KER + IM) by A14, MATRLIN2: 26;

            then

            reconsider BB = (Bker ^ Bim) as OrdBasis of V by A16, MATRLIN2: 4;

            set JJ = (Jk ^ Ji);

             A28:

            now

              let x be object such that

               A29: x in ( dom JJ);

              reconsider i = x as Nat by A29;

              now

                per cases by A29, FINSEQ_1: 25;

                  suppose

                   A30: i in ( dom Jk);

                  then (JJ . i) = (Jk . i) by FINSEQ_1:def 7;

                  hence (JJ . i) is non empty by A30, FUNCT_1:def 9;

                end;

                  suppose ex j st j in ( dom Ji) & i = (( len Jk) + j);

                  then

                  consider j such that

                   A31: j in ( dom Ji) and

                   A32: i = (( len Jk) + j);

                  (JJ . i) = (Ji . j) by A31, A32, FINSEQ_1:def 7;

                  hence (JJ . i) is non empty by A31, FUNCT_1:def 9;

                end;

              end;

              hence (JJ . x) is non empty;

            end;

            

             A33: FI is with_eigenvalues by A25, VECTSP11: 16;

            

             A34: ( dim IM) = 0 implies ( dim IM) = 0 ;

            reconsider JJ as non-empty FinSequence_of_Jordan_block of K by A28, FUNCT_1:def 9;

            take JJ, BB;

            ( dim KER) = 0 implies ( dim KER) = 0 ;

            

            hence ( AutMt (F,BB,BB)) = ( block_diagonal ( <*( block_diagonal (Jk,( 0. K))), ( block_diagonal (Ji,( 0. K)))*>,( 0. K))) by A11, A15, A26, A34, MATRLIN2: 27

            .= ( block_diagonal (( <*( block_diagonal (Jk,( 0. K)))*> ^ Ji),( 0. K))) by MATRIXJ1: 36

            .= ( block_diagonal (JJ,( 0. K))) by MATRIXJ1: 35;

            let L1 be Scalar of K;

            thus L1 is eigenvalue of F implies ex i st i in ( dom JJ) & (JJ . i) = ( Jordan_block (L1,( len (JJ . i))))

            proof

              assume

               A35: L1 is eigenvalue of F;

              per cases ;

                suppose

                 A36: L = L1;

                take i = ( len Jk);

                

                 A37: ( dom Jk) c= ( dom JJ) by FINSEQ_1: 26;

                i in ( Seg ( len Jk)) by A13, FINSEQ_1: 3;

                then

                 A38: i in ( dom Jk) by FINSEQ_1:def 3;

                then (ex k st (Jk . i) = ( Jordan_block (L,k))) & (JJ . i) = (Jk . i) by Def3, FINSEQ_1:def 7;

                hence thesis by A36, A38, A37, Def1;

              end;

                suppose L <> L1;

                then L1 is eigenvalue of FI by A5, A8, A10, A35, VECTSP11: 39;

                then

                consider i such that

                 A39: i in ( dom Ji) and

                 A40: (Ji . i) = ( Jordan_block (L1,( len (Ji . i)))) by A27;

                take ii = (( len Jk) + i);

                (JJ . ii) = (Ji . i) by A39, FINSEQ_1:def 7;

                hence thesis by A39, A40, FINSEQ_1: 28;

              end;

            end;

            given i such that

             A41: i in ( dom JJ) and

             A42: (JJ . i) = ( Jordan_block (L1,( len (JJ . i))));

            per cases by A41, FINSEQ_1: 25;

              suppose

               A43: i in ( dom Jk);

              then (Jk . i) <> {} by FUNCT_1:def 9;

              then ( len (Jk . i)) in ( Seg ( len (Jk . i))) by FINSEQ_1: 3;

              then [( len (Jk . i)), ( len (Jk . i))] in [:( Seg ( len (Jk . i))), ( Seg ( len (Jk . i))):] by ZFMISC_1: 87;

              then

               A44: [( len (Jk . i)), ( len (Jk . i))] in ( Indices (Jk . i)) by MATRIX_0: 24;

              

               A45: (JJ . i) = (Jk . i) by A43, FINSEQ_1:def 7;

              ex k st (Jk . i) = ( Jordan_block (L,k)) by A43, Def3;

              

              then L = ((Jk . i) * (( len (Jk . i)),( len (Jk . i)))) by A44, Def1

              .= L1 by A42, A45, A44, Def1;

              hence thesis by A5, A6, VECTSP11:def 2;

            end;

              suppose ex j st j in ( dom Ji) & i = (( len Jk) + j);

              then

              consider j such that

               A46: j in ( dom Ji) and

               A47: i = (( len Jk) + j);

              (JJ . i) = (Ji . j) by A46, A47, FINSEQ_1:def 7;

              then L1 is eigenvalue of FI by A27, A42, A46;

              then

              consider w be Vector of IM such that

               A48: w <> ( 0. IM) and

               A49: (FI . w) = (L1 * w) by A33, VECTSP11:def 2;

              

               A50: ( 0. IM) = ( 0. V) by VECTSP_4: 11;

              reconsider W = w as Vector of V by VECTSP_4: 10;

              (L1 * W) = (FI . w) by A49, VECTSP_4: 14

              .= (F . W) by FUNCT_1: 49;

              hence thesis by A5, A48, A50, VECTSP11:def 2;

            end;

          end;

        end;

      end;

      

       A51: P[ 0 ]

      proof

        let V be non trivial finite-dimensional VectSp of K;

        assume ( dim V) <= 0 ;

        then ( dim V) = 0 ;

        hence thesis by MATRLIN2: 42;

      end;

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

      then P[( dim V)];

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: MATRIXJ2:32

    for K be algebraic-closed Field, M be Matrix of n, K holds ex J be non-empty FinSequence_of_Jordan_block of K, P be Matrix of n, K st ( Sum ( Len J)) = n & P is invertible & M = ((P * ( block_diagonal (J,( 0. K)))) * (P ~ ))

    proof

      let K be algebraic-closed Field, M be Matrix of n, K;

      per cases ;

        suppose

         A1: n = 0 ;

        then

        reconsider P = {} as Matrix of n, K by MATRIX_0: 13;

        reconsider J = {} as FinSequence_of_Jordan_block of K by Lm2;

        reconsider J as non-empty FinSequence_of_Jordan_block of K;

        take J, P;

        

         A2: ( Len J) = ( <*> NAT )

        .= ( <*> REAL );

        thus ( Sum ( Len J)) = n by A1, RVSUM_1: 72;

        

         A3: ( 1_ K) <> ( 0. K);

        ( Det P) = ( 1_ K) by A1, MATRIXR2: 41;

        hence P is invertible by A3, LAPLACE: 34;

        reconsider B = ( block_diagonal (J,( 0. K))) as Matrix of n, K by A1, A2, RVSUM_1: 72;

        M = ((P * B) * (P ~ )) by A1, MATRIX_0: 45;

        hence thesis;

      end;

        suppose

         A4: n > 0 ;

        set V = (n -VectSp_over K);

        set B = the OrdBasis of V;

        

         A5: ( len B) = ( dim V) by MATRLIN2: 21

        .= n by MATRIX13: 112;

        then

        reconsider M9 = M as Matrix of ( len B), K;

        set T = ( Mx2Tran (M9,B,B));

        ( dim V) = n by MATRIX13: 112;

        then V is non trivial by A4, MATRLIN2: 42;

        then

        consider J be non-empty FinSequence_of_Jordan_block of K, b1 be OrdBasis of V such that

         A6: ( AutMt (T,b1,b1)) = ( block_diagonal (J,( 0. K))) and for L be Scalar of K holds L is eigenvalue of T iff ex i st i in ( dom J) & (J . i) = ( Jordan_block (L,( len (J . i)))) by Th31;

        

         A7: ( dom T) = ( [#] V) by FUNCT_2:def 1;

        reconsider P = ( AutEqMt (( id V),B,b1)) as Matrix of n, K by A5;

        take J, P;

        

         A8: ( width P) = n & ( len (P ~ )) = n by A4, MATRIX_0: 23;

        

         A9: ( rng T) c= ( [#] V) by RELAT_1:def 19;

        

         A10: ( len b1) = ( dim V) by MATRLIN2: 21

        .= n by MATRIX13: 112;

        then

         A11: ( len ( AutMt (T,b1,b1))) = n & ( width ( AutMt (T,b1,b1))) = n by A4, MATRIX_0: 23;

        

        thus ( Sum ( Len J)) = ( len ( AutMt (T,b1,b1))) by A6, MATRIXJ1:def 5

        .= n by A10, MATRIX_0:def 2;

        thus P is invertible by A5, MATRLIN2: 29;

        

        thus M = ( AutMt (T,B,B)) by MATRLIN2: 36

        .= ( AutMt ((T * ( id V)),B,B)) by A7, RELAT_1: 52

        .= (( AutMt (( id V),B,b1)) * ( AutMt (T,b1,B))) by A4, A5, A10, MATRLIN: 41

        .= (P * ( AutMt (T,b1,B))) by A5, A10, MATRLIN2:def 2

        .= (P * ( AutMt ((( id V) * T),b1,B))) by A9, RELAT_1: 53

        .= (P * (( AutMt (T,b1,b1)) * ( AutMt (( id V),b1,B)))) by A4, A10, MATRLIN: 41

        .= (P * (( AutMt (T,b1,b1)) * ( AutEqMt (( id V),b1,B)))) by A5, A10, MATRLIN2:def 2

        .= (P * (( AutMt (T,b1,b1)) * (P ~ ))) by A5, MATRLIN2: 29

        .= ((P * ( block_diagonal (J,( 0. K)))) * (P ~ )) by A6, A8, A11, MATRIX_3: 33;

      end;

    end;