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_0:24;
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:18
.= (1_ K) * (b1 /. (Sum (Len (J | (min ((Len J),(len b1)))))))
.= ((power K) . (L,0)) * (b1 /. (Sum (Len (J | (min ((Len J),(len b1))))))) by GROUP_1:def 7 ;
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:58, 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:3;
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:25;
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;
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:13
.= ((power K) . (L,n)) * (L * (b1 /. (Sum (Len (J | (min ((Len J),(len b1)))))))) by A9, MOD_2:def 2
.= (((power K) . (L,n)) * L) * (b1 /. (Sum (Len (J | (min ((Len J),(len b1))))))) by VECTSP_1:def 16
.= ((power K) . (L,(n + 1))) * (b1 /. (Sum (Len (J | (min ((Len J),(len b1))))))) by GROUP_1:def 7 ; :: 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