let n be Nat; :: thesis: for K being Field
for L being Element of K
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds
for i being Nat 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)) ) )
let K be Field; :: thesis: for L being Element of K
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds
for i being Nat 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)) ) )
let L be Element of K; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds
for i being Nat 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)) ) )
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds
for i being Nat 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)) ) )
let b1 be OrdBasis of V1; :: thesis: for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds
for i being Nat 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)) ) )
let B2 be FinSequence of V2; :: thesis: for M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds
for i being Nat 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)) ) )
set ONE = 1. (K,(len b1));
set J = Jordan_block (L,n);
let M be Matrix of len b1, len B2,K; :: thesis: ( M = Jordan_block (L,n) implies for i being Nat 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)) ) ) )
assume A1: M = Jordan_block (L,n) ; :: thesis: for i being Nat 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)) ) )
A2: len M = n by A1, MATRIX_0:24;
len (1. (K,(len b1))) = len b1 by MATRIX_0:def 2;
then A3: dom (1. (K,(len b1))) = dom b1 by FINSEQ_3:29;
let i be Nat; :: thesis: ( i in dom b1 implies ( ( 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)) ) ) )
assume A4: i in dom b1 ; :: thesis: ( ( 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)) ) )
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 ((1. (K,(len b1))),i))) * M),1)),B2)) by A4, MATRLIN2:19
.= Sum (lmlt ((Line ((LineVec2Mx (Line (((1. (K,(len b1))) * 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 (Jordan_block (L,n)) = n & width (Jordan_block (L,n)) = len B2 ) by A1, A5, A2, MATRIX_0:20;
then dom B2 = dom b1 by A5, A2, FINSEQ_3:29;
hence ( ( 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)) ) ) by A1, A4, A5, A2, A7, A6, Th21, Th22; :: thesis: verum