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 J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal J,(0. K) holds
for i, m being Nat 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)) ) )
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 J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal J,(0. K) holds
for i, m being Nat 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)) ) )
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal J,(0. K) holds
for i, m being Nat 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)) ) )
let b1 be OrdBasis of V1; :: thesis: for B2 being FinSequence of V2
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal J,(0. K) holds
for i, m being Nat 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)) ) )
let B2 be FinSequence of V2; :: thesis: for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal J,(0. K) holds
for i, m being Nat 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)) ) )
let J be FinSequence_of_Jordan_block of L,K; :: thesis: for M being Matrix of len b1, len B2,K st M = block_diagonal J,(0. K) holds
for i, m being Nat 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)) ) )
let M be Matrix of len b1, len B2,K; :: thesis: ( M = block_diagonal J,(0. K) implies for i, m being Nat 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)) ) ) )
assume A1: M = block_diagonal J,(0. K) ; :: thesis: for i, m being Nat 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)) ) )
let i, m be Nat; :: thesis: ( i in dom b1 & m = min (Len J),i implies ( ( 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)) ) ) )
assume A2: ( i in dom b1 & m = min (Len J),i ) ; :: thesis: ( ( 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)) ) )
A3: ( 1 <= i & i <= len b1 ) by A2, FINSEQ_3:27;
set B = block_diagonal J,(0. K);
set BBB = (B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))));
set S = Sum (Len (J | (m -' 1)));
set Sm = Sum (Len (J | m));
set iS = i -' (Sum (Len (J | (m -' 1))));
A4: (Len J) | (m -' 1) = Len (J | (m -' 1)) by MATRIXJ1:17;
A5: (Len J) | m = Len (J | m) by MATRIXJ1:17;
A6: ( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (J . m),(i -' (Sum (Len (J | (m -' 1)))))),((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1)))))) & len ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) = width (J . m) ) by Th20, A1, A2;
A7: ( len M = len b1 & Width J = Len J & dom b1 = Seg (len b1) & len M = Sum (Len J) & width M = Sum (Width J) & width M = len B2 ) by A3, A1, FINSEQ_1:def 3, MATRIXJ1:46, MATRIXJ1:def 5, MATRIX_1:24;
then A8: ( m -' 1 = m - 1 & Sum (Len (J | (m -' 1))) < i & m in dom (Len J) & i <= Sum (Len (J | m)) & dom (Len J) = dom J ) by A2, A4, A5, MATRIXJ1:7, MATRIXJ1:def 1, MATRIXJ1:def 3;
then A9: ( (Len J) | ((m -' 1) + 1) = (Len (J | (m -' 1))) ^ <*((Len J) . m)*> & (Len J) . m = len (J . m) & m = (m -' 1) + 1 & i -' (Sum (Len (J | (m -' 1)))) = i - (Sum (Len (J | (m -' 1)))) & (Len J) . m = width (J . m) ) by A7, A4, FINSEQ_5:11, MATRIXJ1:def 3, MATRIXJ1:def 4, XREAL_1:235;
then A10: Sum (Len (J | m)) = (Sum (Len (J | (m -' 1)))) + (len (J . m)) by A5, RVSUM_1:104;
then (Sum (Len (J | (m -' 1)))) + (i -' (Sum (Len (J | (m -' 1))))) <= (Sum (Len (J | (m -' 1)))) + (len (J . m)) by A7, A9, A2, A5, MATRIXJ1:def 1;
then A11: i -' (Sum (Len (J | (m -' 1)))) <= len (J . m) by XREAL_1:8;
i -' (Sum (Len (J | (m -' 1)))) <> 0 by A7, A9, A2, A4, MATRIXJ1:7;
then 1 <= i -' (Sum (Len (J | (m -' 1)))) by NAT_1:14;
then A12: i -' (Sum (Len (J | (m -' 1)))) in dom ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) by A11, A6, A9, FINSEQ_3:27;
A13: m in NAT by ORDINAL1:def 13;
m <= len (Len J) by A8, FINSEQ_3:27;
then Sum (Len (J | m)) <= Sum ((Len J) | (len (Len J))) by A5, A13, POLYNOM3:18;
then Sum (Len (J | m)) <= Sum (Len J) by FINSEQ_1:79;
then A14: len (B2 | (Sum (Len (J | m)))) = Sum (Len (J | m)) by A7, FINSEQ_1:80;
then A15: i in dom (B2 | (Sum (Len (J | m)))) by A3, A8, FINSEQ_3:27;
consider n being Nat such that
A16: J . m = Jordan_block L,n by A8, Def3;
A17: len (J . m) = n by A16, MATRIX_1:25;
A18: ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) /. (i -' (Sum (Len (J | (m -' 1))))) = (B2 | (Sum (Width (J | m)))) /. ((Sum (Width (J | (m -' 1)))) + (i -' (Sum (Len (J | (m -' 1)))))) by A12, FINSEQ_5:30
.= (B2 | (Sum (Width (J | m)))) /. ((Sum (Len (J | (m -' 1)))) + (i -' (Sum (Len (J | (m -' 1)))))) by MATRIXJ1:46
.= (B2 | (Sum ((Len J) | m))) /. i by A7, A9, MATRIXJ1:21
.= B2 /. i by A5, A15, FINSEQ_4:85 ;
hence ( i = Sum (Len (J | m)) implies (Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) by A6, A9, A10, A12, Th21, A16, A17; :: thesis: ( i <> Sum (Len (J | m)) implies (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) )
assume A19: i <> Sum (Len (J | m)) ; :: thesis: (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1))
then i < Sum (Len (J | m)) by A8, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= Sum (Len (J | m)) ) by NAT_1:11, NAT_1:13;
then A20: i + 1 in dom (B2 | (Sum (Len (J | m)))) by A14, FINSEQ_3:27;
A21: i -' (Sum (Len (J | (m -' 1)))) <> len (J . m) by A9, A10, A19;
then i -' (Sum (Len (J | (m -' 1)))) < len (J . m) by A11, XXREAL_0:1;
then ( 1 <= (i -' (Sum (Len (J | (m -' 1))))) + 1 & (i -' (Sum (Len (J | (m -' 1))))) + 1 <= len (J . m) ) by NAT_1:11, NAT_1:13;
then (i -' (Sum (Len (J | (m -' 1))))) + 1 in dom ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) by A6, A9, FINSEQ_3:27;
then ((B2 | (Sum (Width (J | m)))) /^ (Sum (Width (J | (m -' 1))))) /. ((i -' (Sum (Len (J | (m -' 1))))) + 1) = (B2 | (Sum (Width (J | m)))) /. ((Sum (Width (J | (m -' 1)))) + ((i -' (Sum (Len (J | (m -' 1))))) + 1)) by FINSEQ_5:30
.= (B2 | (Sum (Width (J | m)))) /. ((Sum ((Len J) | (m -' 1))) + ((i -' (Sum (Len (J | (m -' 1))))) + 1)) by A7, MATRIXJ1:21
.= (B2 | (Sum ((Len J) | m))) /. (i + 1) by A4, A7, A9, MATRIXJ1:21
.= B2 /. (i + 1) by A5, A20, FINSEQ_4:85 ;
hence (Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) by A6, A9, A21, A12, Th22, A16, A17, A18; :: thesis: verum