let K be Field; :: thesis:
defpred S₁[ Nat] means for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for L being Element of K st len b1 = len b2 holds
for F being linear-transformation of V1,V2 st $1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( for i being Nat holds
( not i in dom b1 or F . (b1 /. i) = L * (b2 /. i) or ( i + 1 in dom b1 & F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) ) ) ) holds
ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K));
A1: S₁[ 0 ]

let V1, V2 be finite-dimensional VectSp of K; :: thesis:
let b1 be OrdBasis of V1; :: thesis:
let b2 be OrdBasis of V2; :: thesis:
let L be Element of K; :: thesis:
assume len b1 = len b2 ; :: thesis:
set Lb = len b1;
reconsider J = {} as FinSequence_of_Jordan_block of L,K by Th10;
let F be linear-transformation of V1,V2; :: thesis:
assume that
A2: 0 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } and
A3: for i being Nat holds
( not i in dom b1 or F . (b1 /. i) = L * (b2 /. i) or ( i + 1 in dom b1 & F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) ) ) ; :: thesis:
reconsider J = J as non-empty FinSequence_of_Jordan_block of L,K ;
take J ; :: thesis:
len b1 = 0

assume len b1 <> 0 ; :: thesis:
then A4: len b1 in Seg (len b1) by FINSEQ_1:5;
A5: dom b1 = Seg (len b1) by FINSEQ_1:def 3;

per cases by A3, A4, A5;

suppose F . (b1 /. (len b1)) = L * (b2 /. (len b1)) ; :: thesis:

then len b1 in { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } by A4, A5;
hence contradiction by A2; :: thesis:

end;

suppose ( (len b1) + 1 in dom b1 & F . (b1 /. (len b1)) = (L * (b2 /. (len b1))) + (b2 /. ((len b1) + 1)) ) ; :: thesis:

then (len b1) + 1 <= len b1 by FINSEQ_3:27;
hence contradiction by NAT_1:13; :: thesis:

end;

then len (AutMt (F,b1,b2)) = 0 by MATRIX_1:def 3;
then AutMt (F,b1,b2) = {} ;
hence AutMt (F,b1,b2) = block_diagonal (J,(0. K)) by MATRIXJ1:22; :: thesis:

end;

A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A7: S₁[n] ; :: thesis:
set n1 = n + 1;
let V1, V2 be finite-dimensional VectSp of K; :: thesis:
let b1 be OrdBasis of V1; :: thesis:
let b2 be OrdBasis of V2; :: thesis:
let L be Element of K; :: thesis:
assume A8: len b1 = len b2 ; :: thesis:
A9: dom b1 = dom b2 by A8, FINSEQ_3:31;
set Lb = len b1;
let F be linear-transformation of V1,V2; :: thesis:
assume that
A10: n + 1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } and
A11: for i being Nat holds
( not i in dom b1 or F . (b1 /. i) = L * (b2 /. i) or ( i + 1 in dom b1 & F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) ) ) ; :: thesis:
set FF = { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } ;
reconsider FF = { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } as finite set by A10;
consider x being set such that
A12: x in FF by A10, CARD_1:47, XBOOLE_0:def 1;
ex ii being Element of NAT st
( ii = x & ii in dom b1 & F . (b1 /. ii) = L * (b2 /. ii) ) by A12;
then dom b1 <> {} ;
then Seg (len b1) <> {} by FINSEQ_1:def 3;
then A14: len b1 <> 0 ;
A15: dom b1 = Seg (len b1) by FINSEQ_1:def 3;
then A16: not (len b1) + 1 in dom b1 by FINSEQ_3:9;
A17: len b1 in dom b1 by A15, A14, FINSEQ_1:5;
then F . (b1 /. (len b1)) = L * (b2 /. (len b1)) by A11, A16;
then A18: len b1 in FF by A17;

per cases ;

suppose A19: n = 0 ; :: thesis:

set J = Jordan_block (L,(len b1));
reconsider JJ = <*(Jordan_block (L,(len b1)))*> as FinSequence_of_Jordan_block of L,K by Th11;

now

A20: dom JJ = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
let x be set ; :: thesis:
assume x in dom JJ ; :: thesis:
then ( JJ . 1 = Jordan_block (L,(len b1)) & x = 1 ) by A20, FINSEQ_1:def 8, TARSKI:def 1;
hence not JJ . x is empty by A14, Def1; :: thesis:

end;

then reconsider JJ = JJ as non-empty FinSequence_of_Jordan_block of L,K by FUNCT_1:def 15;
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);
A21: block_diagonal (JJ,(0. K)) = Jordan_block (L,(len b1)) by MATRIXJ1:34;

A22: now

let y be set ; :: thesis:
assume A23: y in dom b1 ; :: thesis:
reconsider j = y as Element of NAT by A23;
A24: ((Mx2Tran (BB,b1,b2)) * b1) . y = (Mx2Tran (BB,b1,b2)) . (b1 . y) by A23, FUNCT_1:23;
A25: b1 /. j = b1 . j by A23, PARTFUN1:def 8;
A26: (F9 * b1) . y = F . (b1 . y) by A23, FUNCT_1:23;

now

per cases ;

suppose A27: j = len b1 ; :: thesis:

hence ((Mx2Tran (BB,b1,b2)) * b1) . y = L * (b2 /. (len b1)) by A21, A23, A24, A25, Th23
.= (F9 * b1) . y by A11, A17, A16, A26, A25, A27 ;
:: thesis:

end;

suppose A28: j <> len b1 ; :: thesis:

ex z being set st FF = {z} by A10, A19, CARD_2:60;
then FF = {(len b1)} by A18, TARSKI:def 1;
then not j in FF by A28, TARSKI:def 1;
then A29: F . (b1 /. j) <> L * (b2 /. j) by A23;
((Mx2Tran (BB,b1,b2)) * b1) . y = (L * (b2 /. j)) + (b2 /. (j + 1)) by A21, A23, A24, A25, A28, Th23;
hence ((Mx2Tran (BB,b1,b2)) * b1) . y = (F9 * b1) . y by A11, A23, A26, A25, A29; :: thesis:

end;

hence (F9 * b1) . y = ((Mx2Tran (BB,b1,b2)) * b1) . y ; :: thesis:

end;

take JJ ; :: thesis:
A30: rng b1 c= [#] V1 by FINSEQ_1:def 4;
dom (Mx2Tran (BB,b1,b2)) = [#] V1 by FUNCT_2:def 1;
then A31: dom ((Mx2Tran (BB,b1,b2)) * b1) = dom b1 by A30, RELAT_1:46;
dom F = [#] V1 by FUNCT_2:def 1;
then dom (F9 * b1) = dom b1 by A30, RELAT_1:46;
then F = Mx2Tran (BB,b1,b2) by A14, A31, A22, FUNCT_1:9, MATRLIN:26;
hence AutMt (F,b1,b2) = block_diagonal (JJ,(0. K)) by MATRLIN2:36; :: thesis:

end;

suppose A32: n <> 0 ; :: thesis:

defpred S₂[ Nat] means ( $1 in FF & $1 < len b1 );
A33: ex k being Nat st S₂[k]

proof

card FF <> 1 by A10, A32;
then FF <> {(len b1)} by CARD_2:60;
then consider y being set such that
A34: y in FF and
A35: y <> len b1 by A18, ZFMISC_1:41;
consider j being Element of NAT such that
A36: j = y and
A37: j in dom b1 and
F . (b1 /. j) = L * (b2 /. j) by A34;
take j ; :: thesis:
j <= len b1 by A37, FINSEQ_3:27;
hence S₂[j] by A34, A35, A36, XXREAL_0:1; :: thesis:

end;

A38: for k being Nat st S₂[k] holds
k <= len b1 ;
consider m being Nat such that
A39: S₂[m] and
A40: for k being Nat st S₂[k] holds
k <= m from NAT_1:sch 6(A38, A33);
set b1m = b1 | m;
A41: len (b1 | m) = m by A39, FINSEQ_1:80;
set JB = Jordan_block (L,((len b1) -' m));
reconsider JJ = <*(Jordan_block (L,((len b1) -' m)))*> as FinSequence_of_Jordan_block of L,K by Th11;
set b19m = b1 /^ m;
A43: len (b1 /^ m) = (len b1) - m by A39, RFINSEQ:def 2;
set b29m = b2 /^ m;
A44: len (b2 /^ m) = (len b1) - m by A8, A39, RFINSEQ:def 2;
set b2m = b2 | m;
A45: len (b2 | m) = m by A8, A39, FINSEQ_1:80;
reconsider Rb2 = rng (b2 | m), Rb29 = rng (b2 /^ m) as linearly-independent Subset of V2 by MATRLIN2:22, MATRLIN2:23;
reconsider Rb1 = rng (b1 | m), Rb19 = rng (b1 /^ m) 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;
A46: rng (F | (Lin Rb1)) = F .: the carrier of (Lin Rb1) by RELAT_1:148;
reconsider b2m = b2 | m as OrdBasis of Lin Rb2 by MATRLIN2:22;
reconsider b1m = b1 | m as OrdBasis of Lin Rb1 by MATRLIN2:22;
A47: dom b1m = dom b2m by A41, A45, FINSEQ_3:31;
reconsider b19m = b1 /^ m as OrdBasis of Lin Rb19 by MATRLIN2:23;
reconsider b29m = b2 /^ m as OrdBasis of Lin Rb29 by MATRLIN2:23;
A48: b2 = b2m ^ b29m by RFINSEQ:21;
A49: b1 = b1m ^ b19m by RFINSEQ:21;
then A50: dom b1m c= dom b1 by FINSEQ_1:39;
A51: for i being Nat holds
( not i in dom b1m or (F | (Lin Rb1)) . (b1m /. i) = L * (b2m /. i) or ( i + 1 in dom b1m & (F | (Lin Rb1)) . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) )

proof

let i be Nat; :: thesis:
assume A52: i in dom b1m ; :: thesis:
A53: b1m . i = b1m /. i by A52, PARTFUN1:def 8;
set i1 = i + 1;
A54: F . (b1m /. i) = (F | (Lin Rb1)) . (b1m /. i) by FUNCT_1:72;
A55: ( b2 /. i = b2 . i & b2 . i = b2m . i ) by A9, A48, A50, A47, A52, FINSEQ_1:def 7, PARTFUN1:def 8;
A56: ( b1 /. i = b1 . i & b1 . i = b1m . i ) by A49, A50, A52, FINSEQ_1:def 7, PARTFUN1:def 8;

per cases by A11, A50, A52;

suppose F . (b1 /. i) = L * (b2 /. i) ; :: thesis:

hence ( (F | (Lin Rb1)) . (b1m /. i) = L * (b2m /. i) or ( i + 1 in dom b1m & (F | (Lin Rb1)) . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) ) by A47, A52, A55, A56, A53, A54, PARTFUN1:def 8, VECTSP_4:22; :: thesis:

end;

suppose A57: ( i + 1 in dom b1 & F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) ) ; :: thesis:

reconsider rngb2 = rng b2 as Basis of V2 by MATRLIN:def 4;
A58: i + 1 <= m

proof

assume i + 1 > m ; :: thesis:
then A59: i >= m by NAT_1:13;
i <= m by A41, A52, FINSEQ_3:27;
then A60: i = m by A59, XXREAL_0:1;
ex ii being Element of NAT st
( m = ii & ii in dom b1 & F . (b1 /. ii) = L * (b2 /. ii) ) by A39;
then F . (b1 /. i) = (L * (b2 /. i)) + (0. V2) by A60, RLVECT_1:def 7;
then A61: b2 /. (i + 1) = 0. V2 by A57, RLVECT_1:21;
A62: rngb2 is linearly-independent by VECTSP_7:def 3;
( b2 /. (i + 1) = b2 . (i + 1) & b2 . (i + 1) in rngb2 ) by A9, A57, FUNCT_1:def 5, PARTFUN1:def 8;
hence contradiction by A61, A62, VECTSP_7:3; :: thesis:

end;

A63: 1 <= i + 1 by NAT_1:11;
then A64: i + 1 in dom b1m by A41, A58, FINSEQ_3:27;
then A65: b2m . (i + 1) = b2m /. (i + 1) by A47, PARTFUN1:def 8;
A66: L * (b2 /. i) = L * (b2m /. i) by A47, A52, A55, PARTFUN1:def 8, VECTSP_4:22;
( b2 /. (i + 1) = b2 . (i + 1) & b2 . (i + 1) = b2m . (i + 1) ) by A9, A48, A50, A47, A64, FINSEQ_1:def 7, PARTFUN1:def 8;
hence ( (F | (Lin Rb1)) . (b1m /. i) = L * (b2m /. i) or ( i + 1 in dom b1m & (F | (Lin Rb1)) . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) ) by A41, A56, A53, A54, A57, A58, A63, A65, A66, FINSEQ_3:27, VECTSP_4:21; :: thesis:

end;

F .: Rb1 c= the carrier of (Lin Rb2)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in F .: Rb1 ; :: thesis:
then consider x being set such that
x in dom F and
A67: x in Rb1 and
A68: F . x = y by FUNCT_1:def 12;
consider i being set such that
A69: i in dom b1m and
A70: b1m . i = x by A67, FUNCT_1:def 5;
reconsider i = i as Element of NAT by A69;
b1m /. i = b1m . i by A69, PARTFUN1:def 8;
then (F | (Lin Rb1)) . (b1m /. i) = y by A68, A70, FUNCT_1:72;
then ( y = L * (b2m /. i) or y = (L * (b2m /. i)) + (b2m /. (i + 1)) ) by A51, A69;
hence y in the carrier of (Lin Rb2) ; :: thesis:

end;

then ( the carrier of (Lin (F .: Rb1)) = F .: the carrier of (Lin Rb1) & Lin (F .: Rb1) is Subspace of Lin Rb2 ) by VECTSP11:42, VECTSP_9:20;
then F .: the carrier of (Lin Rb1) c= the carrier of (Lin Rb2) by VECTSP_4:def 2;
then reconsider FL = F | (Lin Rb1) as linear-transformation of (Lin Rb1),(Lin Rb2) by A46, Lm4, FUNCT_2:8;
A71: for i being Nat holds
( not i in dom b1m or FL . (b1m /. i) = L * (b2m /. i) or ( i + 1 in dom b1m & FL . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) ) by A51;
set FF1 = { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } ;
A72: FF \ {(len b1)} c= { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A73: x in FF \ {(len b1)} ; :: thesis:
A74: x <> len b1 by A73, ZFMISC_1:64;
x in FF by A73;
then consider j being Element of NAT such that
A75: j = x and
A76: j in dom b1 and
A77: F . (b1 /. j) = L * (b2 /. j) ;
j <= len b1 by A76, FINSEQ_3:27;
then j < len b1 by A74, A75, XXREAL_0:1;
then A78: j <= m by A40, A73, A75;
1 <= j by A76, FINSEQ_3:27;
then A79: j in dom b1m by A41, A78, FINSEQ_3:27;
then A80: ( b1m /. j = b1m . j & b1m . j = b1 . j ) by A49, FINSEQ_1:def 7, PARTFUN1:def 8;
A81: ( FL . (b1m /. j) = F . (b1m /. j) & b1 /. j = b1 . j ) by A50, A79, FUNCT_1:72, PARTFUN1:def 8;
( b2m . j = b2 . j & b2 /. j = b2 . j ) by A9, A48, A50, A47, A79, FINSEQ_1:def 7, PARTFUN1:def 8;
then FL . (b1m /. j) = L * (b2m /. j) by A47, A77, A79, A80, A81, PARTFUN1:def 8, VECTSP_4:22;
hence x in { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } by A75, A79; :: thesis:

end;

{ i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } c= FF \ {(len b1)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } ; :: thesis:
then consider j being Element of NAT such that
A82: x = j and
A83: j in dom b1m and
A84: FL . (b1m /. j) = L * (b2m /. j) ;
A85: ( b1m /. j = b1m . j & b1m . j = b1 . j ) by A49, A83, FINSEQ_1:def 7, PARTFUN1:def 8;
A86: ( FL . (b1m /. j) = F . (b1m /. j) & b1 /. j = b1 . j ) by A50, A83, FUNCT_1:72, PARTFUN1:def 8;
( b2m . j = b2 . j & b2 /. j = b2 . j ) by A9, A48, A50, A47, A83, FINSEQ_1:def 7, PARTFUN1:def 8;
then F . (b1 /. j) = L * (b2 /. j) by A47, A83, A84, A85, A86, PARTFUN1:def 8, VECTSP_4:22;
then A87: j in FF by A50, A83;
j <= m by A41, A83, FINSEQ_3:27;
hence x in FF \ {(len b1)} by A39, A82, A87, ZFMISC_1:64; :: thesis:

end;

then { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } = FF \ {(len b1)} by A72, XBOOLE_0:def 10;
then card { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } = n by A10, A18, STIRL2_1:65;
then consider J being non-empty FinSequence_of_Jordan_block of L,K such that
A88: AutMt (FL,b1m,b2m) = block_diagonal (J,(0. K)) by A7, A41, A45, A71;
set JJJ = J ^ JJ;
A89: (len b1) - m = (len b1) -' m by A39, XREAL_1:235;

A90: now

let x be set ; :: thesis:
assume A91: x in dom (J ^ JJ) ; :: thesis:
reconsider i = x as Nat by A91;

per cases by A91, FINSEQ_1:38;

suppose A92: i in dom J ; :: thesis:

then not J . i is empty by FUNCT_1:def 15;
hence not (J ^ JJ) . x is empty by A92, FINSEQ_1:def 7; :: thesis:

end;

suppose A93: ex j being Nat st
( j in dom JJ & i = (len J) + j ) ; :: thesis:

len (Jordan_block (L,((len b1) -' m))) = (len b1) -' m by Def1;
then A94: len (Jordan_block (L,((len b1) -' m))) <> 0 by A39, A89;
consider j being Nat such that
A95: j in dom JJ and
A96: i = (len J) + j by A93;
dom JJ = Seg 1 by FINSEQ_1:55;
then j = 1 by A95, FINSEQ_1:4, TARSKI:def 1;
then (J ^ JJ) . i = JJ . 1 by A95, A96, FINSEQ_1:def 7;
hence not (J ^ JJ) . x is empty by A94, FINSEQ_1:57; :: thesis:

end;

reconsider JB = Jordan_block (L,((len b1) -' m)) as Matrix of len b19m, len b29m,K by A8, A39, A43, A89, RFINSEQ:def 2;
A97: width JB = len b19m by A43, A44, MATRIX_1:25;
reconsider JJJ = J ^ JJ as non-empty FinSequence_of_Jordan_block of L,K by A90, FUNCT_1:def 15;
take JJJ ; :: thesis:
reconsider F9 = F as Function of V1,V2 ;
reconsider B = block_diagonal (J,(0. K)) as Matrix of len b1m, len b2m,K by A88;
A98: width B = len b1m by A41, A45, MATRIX_1:25;
A99: ( Sum (Len <*B,JB*>) = (len B) + (len JB) & Sum (Width <*B,JB*>) = (width B) + (width JB) ) by MATRIXJ1:16, MATRIXJ1:20;
len B = len b1m by A41, A45, MATRIX_1:25;
then reconsider BB = block_diagonal (<*B,JB*>,(0. K)) as Matrix of len b1, len b2,K by A8, A41, A43, A44, A99, A98, A97, MATRIX_1:25;
set T = Mx2Tran (BB,b1,b2);
A100: dom b19m = dom b29m by A43, A44, FINSEQ_3:31;

A101: now

let x be set ; :: thesis:
assume A102: x in dom b1 ; :: thesis:
reconsider I = x as Element of NAT by A102;
A103: ((Mx2Tran (BB,b1,b2)) * b1) . x = (Mx2Tran (BB,b1,b2)) . (b1 . I) by A102, FUNCT_1:23;
A104: b1 . I = b1 /. I by A102, PARTFUN1:def 8;
A105: (F9 * b1) . x = F . (b1 . I) by A102, FUNCT_1:23;

now

per cases by A49, A102, FINSEQ_1:38;

suppose A106: I in dom b1m ; :: thesis:

then A107: ( b1m /. I = b1m . I & b1 . I = b1m . I ) by A49, FINSEQ_1:def 7, PARTFUN1:def 8;
A108: FL . (b1m /. I) = F . (b1m /. I) by FUNCT_1:72;
thus ((Mx2Tran (BB,b1,b2)) * b1) . x = (Mx2Tran (B,b1m,b2m)) . (b1m /. I) by A41, A45, A43, A44, A49, A48, A98, A97, A103, A104, A106, Th19
.= FL . (b1m /. I) by A88, MATRLIN2:34
.= (F9 * b1) . x by A102, A108, A107, FUNCT_1:23 ; :: thesis:

end;

suppose ex j being Nat st
( j in dom b19m & I = (len b1m) + j ) ; :: thesis:

then consider j being Nat such that
A109: j in dom b19m and
A110: I = (len b1m) + j ;

now

per cases ;

suppose A111: j = len b19m ; :: thesis:

A112: ( b2 . I = b29m . j & b2 /. I = b2 . I ) by A9, A41, A45, A48, A100, A102, A109, A110, FINSEQ_1:def 7, PARTFUN1:def 8;
thus (F9 * b1) . x = L * (b2 /. I) by A11, A17, A16, A41, A43, A105, A104, A110, A111
.= L * (b29m /. j) by A100, A109, A112, PARTFUN1:def 8, VECTSP_4:22
.= (Mx2Tran (JB,b19m,b29m)) . (b19m /. j) by A109, A111, Th23 ; :: thesis:

end;

suppose A113: j <> len b19m ; :: thesis:

A114: (F9 * b1) . x = (L * (b2 /. I)) + (b2 /. (I + 1))

proof

assume (F9 * b1) . x <> (L * (b2 /. I)) + (b2 /. (I + 1)) ; :: thesis:
then F . (b1 /. I) = L * (b2 /. I) by A11, A102, A105, A104;
then A115: I in FF by A102;
( I <> len b1 & I <= len b1 ) by A41, A43, A102, A110, A113, FINSEQ_3:27;
then I < len b1 by XXREAL_0:1;
then (len b1m) + j <= (len b1m) + 0 by A40, A41, A110, A115;
then j <= 0 by XREAL_1:8;
hence contradiction by A109, FINSEQ_3:27; :: thesis:

end;

j <= len b19m by A109, FINSEQ_3:27;
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:27;
then ( b29m /. (j + 1) = b29m . (j + 1) & b2 . ((len b1m) + (j + 1)) = b29m . (j + 1) ) by A41, A45, A48, A100, FINSEQ_1:def 7, PARTFUN1:def 8;
then A117: b29m /. (j + 1) = b2 /. (I + 1) by A9, A49, A110, A116, FINSEQ_1:41, PARTFUN1:def 8;
( b2 . I = b29m . j & b2 /. I = b2 . I ) by A9, A41, A45, A48, A100, A102, A109, A110, FINSEQ_1:def 7, PARTFUN1:def 8;
then L * (b29m /. j) = L * (b2 /. I) by A100, A109, PARTFUN1:def 8, VECTSP_4:22;
then (L * (b2 /. I)) + (b2 /. (I + 1)) = (L * (b29m /. j)) + (b29m /. (j + 1)) by A117, VECTSP_4:21
.= (Mx2Tran (JB,b19m,b29m)) . (b19m /. j) by A109, A113, Th23 ;
hence (F9 * b1) . x = (Mx2Tran (JB,b19m,b29m)) . (b19m /. j) by A114; :: thesis:

end;

hence (F9 * b1) . x = ((Mx2Tran (BB,b1,b2)) * b1) . x by A41, A45, A43, A44, A49, A48, A98, A97, A103, A104, A109, A110, Th19; :: thesis:

end;

hence (F9 * b1) . x = ((Mx2Tran (BB,b1,b2)) * b1) . x ; :: thesis:

end;

A118: rng b1 c= [#] V1 by FINSEQ_1:def 4;
dom (Mx2Tran (BB,b1,b2)) = [#] V1 by FUNCT_2:def 1;
then A119: dom ((Mx2Tran (BB,b1,b2)) * b1) = dom b1 by A118, RELAT_1:46;
dom F = [#] V1 by FUNCT_2:def 1;
then dom (F9 * b1) = dom b1 by A118, RELAT_1:46;
then ( block_diagonal (JJJ,(0. K)) = block_diagonal (<*B,JB*>,(0. K)) & F = Mx2Tran (BB,b1,b2) ) by A14, A119, A101, FUNCT_1:9, MATRIXJ1:35, MATRLIN:26;
hence AutMt (F,b1,b2) = block_diagonal (JJJ,(0. K)) by MATRLIN2:36; :: thesis:

end;

let V1, V2 be finite-dimensional VectSp of K; :: thesis:
let b1 be OrdBasis of V1; :: thesis:
let b2 be OrdBasis of V2; :: thesis:
let L be Element of K; :: thesis:
assume A120: len b1 = len b2 ; :: thesis:
let F be linear-transformation of V1,V2; :: thesis:
assume A121: for i being Nat holds
( not i in dom b1 or F . (b1 /. i) = L * (b2 /. i) or ( i + 1 in dom b1 & F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) ) ) ; :: thesis:
set FF = { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } ;
{ i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } c= dom b1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } ; :: thesis:
then ex i being Element of NAT st
( x = i & i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) ;
hence x in dom b1 ; :: thesis:

end;

then reconsider FF = { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } as finite set ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A6);
then S₁[ card FF] ;
hence ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K)) by A120, A121; :: thesis: