let n be Nat; :: thesis: for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being 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 )
let K be Field; :: thesis: for L being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being 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 )
let L be Element of K; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being 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 )
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being 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 )
let b1 be OrdBasis of V1; :: thesis: for J being FinSequence_of_Jordan_block of L,K
for M being 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 )
let J be FinSequence_of_Jordan_block of L,K; :: thesis: for M being 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 )
set B = len b1;
set m = min (Len J),(len b1);
set S = Sum (Len (J | (min (Len J),(len b1))));
A1: Seg (len b1) = dom b1 by FINSEQ_1:def 3;
let M be Matrix of len b1, len b1,K; :: thesis: ( M = block_diagonal J,(0. K) & len b1 <> 0 implies ( ((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 ) )
assume A2: M = block_diagonal J,(0. K) ; :: thesis: ( not len b1 <> 0 or ( ((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 ) )
A3: ( len b1 = len M & len M = Sum (Len J) ) by A2, MATRIX_1:25;
set MT = Mx2Tran M,b1,b1;
defpred S₁[ Nat] means ((Mx2Tran M,b1,b1) |^ $1) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,$1) * (b1 /. (Sum (Len (J | (min (Len J),(len b1))))));
((Mx2Tran M,b1,b1) |^ 0 ) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = (id V1) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by VECTSP11:18
.= b1 /. (Sum (Len (J | (min (Len J),(len b1))))) by FUNCT_1:35
.= (1_ K) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by VECTSP_1:def 29
.= ((power K) . L,0 ) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by GROUP_1:def 8 ;
then A4: S₁[ 0 ] ;
A5: ( Sum ((Len J) | (min (Len J),(len b1))) = Sum (Len (J | (min (Len J),(len b1)))) & (Len J) | (len (Len J)) = Len J ) by FINSEQ_1:79, MATRIXJ1:17;
assume len b1 <> 0 ; :: thesis: ( ((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 )
then A6: len b1 in Seg (len b1) by FINSEQ_1:5;
then min (Len J),(len b1) in dom (Len J) by A3, MATRIXJ1:def 1;
then min (Len J),(len b1) <= len (Len J) by FINSEQ_3:27;
then A7: Sum ((Len J) | (min (Len J),(len b1))) <= Sum ((Len J) | (len (Len J))) by POLYNOM3:18;
A8: len b1 <= Sum ((Len J) | (min (Len J),(len b1))) by A3, A6, MATRIXJ1:def 1;
then len b1 = Sum (Len (J | (min (Len J),(len b1)))) by A3, A7, A5, XXREAL_0:1;
then A9: (Mx2Tran M,b1,b1) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = L * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by A2, A6, A1, Th24;
A10: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A11: S₁[n] ; :: thesis: S₁[n + 1]
A12: dom ((Mx2Tran M,b1,b1) |^ n) = the carrier of V1 by FUNCT_2:def 1;
A13: n in NAT by ORDINAL1:def 13;
thus ((Mx2Tran M,b1,b1) |^ (n + 1)) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = (((Mx2Tran M,b1,b1) |^ 1) * ((Mx2Tran M,b1,b1) |^ n)) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by VECTSP11:20
.= ((Mx2Tran M,b1,b1) * ((Mx2Tran M,b1,b1) |^ n)) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by VECTSP11:19
.= (Mx2Tran M,b1,b1) . (((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1))))))) by A11, A12, FUNCT_1:23
.= ((power K) . L,n) * (L * (b1 /. (Sum (Len (J | (min (Len J),(len b1))))))) by A9, MOD_2:def 3
.= (((power K) . L,n) * L) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by VECTSP_1:def 28
.= ((power K) . L,(n + 1)) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) by A13, GROUP_1:def 8 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A10);
hence ( ((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 ) by A3, A6, A1, A8, A7, A5, XXREAL_0:1; :: thesis: verum