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:3;
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:25;
hence contradiction by NAT_1:13; :: thesis:

end;

then len (AutMt (F,b1,b2)) = 0 by MATRIX_0:def 2;
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:29;
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 object such that
A12: x in FF by A10, CARD_1:27, 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 A13: len b1 <> 0 ;
A14: dom b1 = Seg (len b1) by FINSEQ_1:def 3;
then A15: not (len b1) + 1 in dom b1 by FINSEQ_3:8;
A16: len b1 in dom b1 by A14, A13, FINSEQ_1:3;
then F . (b1 /. (len b1)) = L * (b2 /. (len b1)) by A11, A15;
then A17: len b1 in FF by A16;

per cases ;

suppose A18: 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 :: thesis:

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

end;

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

A21: now :: thesis:

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

now :: thesis:

per cases ;

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

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

end;

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

ex z being object st FF = {z} by A10, A18, CARD_2:42;
then FF = {(len b1)} by A17, TARSKI:def 1;
then not j in FF by A27, TARSKI:def 1;
then A28: F . (b1 /. j) <> L * (b2 /. j) by A22;
((Mx2Tran (BB,b1,b2)) * b1) . y = (L * (b2 /. j)) + (b2 /. (j + 1)) by A20, A22, A23, A24, A27, Th23;
hence ((Mx2Tran (BB,b1,b2)) * b1) . y = (F9 * b1) . y by A11, A22, A25, A24, A28; :: thesis:

end;

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

end;

take JJ ; :: thesis:
A29: rng b1 c= [#] V1 by FINSEQ_1:def 4;
dom (Mx2Tran (BB,b1,b2)) = [#] V1 by FUNCT_2:def 1;
then A30: dom ((Mx2Tran (BB,b1,b2)) * b1) = dom b1 by A29, RELAT_1:27;
dom F = [#] V1 by FUNCT_2:def 1;
then dom (F9 * b1) = dom b1 by A29, RELAT_1:27;
then F = Mx2Tran (BB,b1,b2) by A13, A30, A21, FUNCT_1:2, MATRLIN:22;
hence AutMt (F,b1,b2) = block_diagonal (JJ,(0. K)) by MATRLIN2:36; :: thesis:

end;

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

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

proof

card FF <> 1 by A10, A31;
then FF <> {(len b1)} by CARD_2:42;
then consider y being object such that
A33: y in FF and
A34: y <> len b1 by A17, ZFMISC_1:35;
consider j being Element of NAT such that
A35: j = y and
A36: j in dom b1 and
F . (b1 /. j) = L * (b2 /. j) by A33;
take j ; :: thesis:
j <= len b1 by A36, FINSEQ_3:25;
hence S₂[j] by A33, A34, A35, XXREAL_0:1; :: thesis:

end;

A37: for k being Nat st S₂[k] holds
k <= len b1 ;
consider m being Nat such that
A38: S₂[m] and
A39: for k being Nat st S₂[k] holds
k <= m from NAT_1:sch 6(A37, A32);
set b1m = b1 | m;
A40: len (b1 | m) = m by A38, FINSEQ_1:59;
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;
A41: len (b1 /^ m) = (len b1) - m by A38, RFINSEQ:def 1;
set b29m = b2 /^ m;
A42: len (b2 /^ m) = (len b1) - m by A8, A38, RFINSEQ:def 1;
set b2m = b2 | m;
A43: len (b2 | m) = m by A8, A38, FINSEQ_1:59;
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;
A44: rng (F | (Lin Rb1)) = F .: the carrier of (Lin Rb1) by RELAT_1:115;
reconsider b2m = b2 | m as OrdBasis of Lin Rb2 by MATRLIN2:22;
reconsider b1m = b1 | m as OrdBasis of Lin Rb1 by MATRLIN2:22;
A45: dom b1m = dom b2m by A40, A43, FINSEQ_3:29;
reconsider b19m = b1 /^ m as OrdBasis of Lin Rb19 by MATRLIN2:23;
reconsider b29m = b2 /^ m as OrdBasis of Lin Rb29 by MATRLIN2:23;
A46: b2 = b2m ^ b29m by RFINSEQ:8;
A47: b1 = b1m ^ b19m by RFINSEQ:8;
then A48: dom b1m c= dom b1 by FINSEQ_1:26;
A49: 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 A50: i in dom b1m ; :: thesis:
A51: b1m . i = b1m /. i by A50, PARTFUN1:def 6;
set i1 = i + 1;
A52: F . (b1m /. i) = (F | (Lin Rb1)) . (b1m /. i) by FUNCT_1:49;
A53: ( b2 /. i = b2 . i & b2 . i = b2m . i ) by A9, A46, A48, A45, A50, FINSEQ_1:def 7, PARTFUN1:def 6;
A54: ( b1 /. i = b1 . i & b1 . i = b1m . i ) by A47, A48, A50, FINSEQ_1:def 7, PARTFUN1:def 6;

per cases by A11, A48, A50;

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 A45, A50, A53, A54, A51, A52, PARTFUN1:def 6, VECTSP_4:14; :: thesis:

end;

suppose A55: ( 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 2;
A56: i + 1 <= m

proof

assume i + 1 > m ; :: thesis:
then A57: i >= m by NAT_1:13;
i <= m by A40, A50, FINSEQ_3:25;
then A58: i = m by A57, XXREAL_0:1;
ex ii being Element of NAT st
( m = ii & ii in dom b1 & F . (b1 /. ii) = L * (b2 /. ii) ) by A38;
then F . (b1 /. i) = (L * (b2 /. i)) + (0. V2) by A58, RLVECT_1:def 4;
then A59: b2 /. (i + 1) = 0. V2 by A55, RLVECT_1:8;
A60: rngb2 is linearly-independent by VECTSP_7:def 3;
( b2 /. (i + 1) = b2 . (i + 1) & b2 . (i + 1) in rngb2 ) by A9, A55, FUNCT_1:def 3, PARTFUN1:def 6;
hence contradiction by A59, A60, VECTSP_7:2; :: thesis:

end;

A61: 1 <= i + 1 by NAT_1:11;
then A62: i + 1 in dom b1m by A40, A56, FINSEQ_3:25;
then A63: b2m . (i + 1) = b2m /. (i + 1) by A45, PARTFUN1:def 6;
A64: L * (b2 /. i) = L * (b2m /. i) by A45, A50, A53, PARTFUN1:def 6, VECTSP_4:14;
( b2 /. (i + 1) = b2 . (i + 1) & b2 . (i + 1) = b2m . (i + 1) ) by A9, A46, A48, A45, A62, FINSEQ_1:def 7, PARTFUN1:def 6;
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 A40, A54, A51, A52, A55, A56, A61, A63, A64, FINSEQ_3:25, VECTSP_4:13; :: thesis:

end;

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in F .: Rb1 ; :: thesis:
then consider x being object such that
x in dom F and
A65: x in Rb1 and
A66: F . x = y by FUNCT_1:def 6;
consider i being object such that
A67: i in dom b1m and
A68: b1m . i = x by A65, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A67;
b1m /. i = b1m . i by A67, PARTFUN1:def 6;
then (F | (Lin Rb1)) . (b1m /. i) = y by A66, A68, FUNCT_1:49;
then ( y = L * (b2m /. i) or y = (L * (b2m /. i)) + (b2m /. (i + 1)) ) by A49, A67;
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:16;
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 A44, Lm4, FUNCT_2:6;
A69: 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 A49;
set FF1 = { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } ;
A70: 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 object ; :: according to TARSKI:def 3 :: thesis:
assume A71: x in FF \ {(len b1)} ; :: thesis:
A72: x <> len b1 by A71, ZFMISC_1:56;
x in FF by A71;
then consider j being Element of NAT such that
A73: j = x and
A74: j in dom b1 and
A75: F . (b1 /. j) = L * (b2 /. j) ;
j <= len b1 by A74, FINSEQ_3:25;
then j < len b1 by A72, A73, XXREAL_0:1;
then A76: j <= m by A39, A71, A73;
1 <= j by A74, FINSEQ_3:25;
then A77: j in dom b1m by A40, A76, FINSEQ_3:25;
then A78: ( b1m /. j = b1m . j & b1m . j = b1 . j ) by A47, FINSEQ_1:def 7, PARTFUN1:def 6;
A79: ( FL . (b1m /. j) = F . (b1m /. j) & b1 /. j = b1 . j ) by A48, A77, FUNCT_1:49, PARTFUN1:def 6;
( b2m . j = b2 . j & b2 /. j = b2 . j ) by A9, A46, A48, A45, A77, FINSEQ_1:def 7, PARTFUN1:def 6;
then FL . (b1m /. j) = L * (b2m /. j) by A45, A75, A77, A78, A79, PARTFUN1:def 6, VECTSP_4:14;
hence x in { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } by A73, A77; :: 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 object ; :: 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
A80: x = j and
A81: j in dom b1m and
A82: FL . (b1m /. j) = L * (b2m /. j) ;
A83: ( b1m /. j = b1m . j & b1m . j = b1 . j ) by A47, A81, FINSEQ_1:def 7, PARTFUN1:def 6;
A84: ( FL . (b1m /. j) = F . (b1m /. j) & b1 /. j = b1 . j ) by A48, A81, FUNCT_1:49, PARTFUN1:def 6;
( b2m . j = b2 . j & b2 /. j = b2 . j ) by A9, A46, A48, A45, A81, FINSEQ_1:def 7, PARTFUN1:def 6;
then F . (b1 /. j) = L * (b2 /. j) by A45, A81, A82, A83, A84, PARTFUN1:def 6, VECTSP_4:14;
then A85: j in FF by A48, A81;
j <= m by A40, A81, FINSEQ_3:25;
hence x in FF \ {(len b1)} by A38, A80, A85, ZFMISC_1:56; :: thesis:

end;

then { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } = FF \ {(len b1)} by A70, 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, A17, STIRL2_1:55;
then consider J being non-empty FinSequence_of_Jordan_block of L,K such that
A86: AutMt (FL,b1m,b2m) = block_diagonal (J,(0. K)) by A7, A40, A43, A69;
set JJJ = J ^ JJ;
A87: (len b1) - m = (len b1) -' m by A38, XREAL_1:233;

A88: now :: thesis:

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

per cases by A89, FINSEQ_1:25;

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

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

end;

suppose A91: 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 A92: len (Jordan_block (L,((len b1) -' m))) <> 0 by A38, A87;
consider j being Nat such that
A93: j in dom JJ and
A94: i = (len J) + j by A91;
dom JJ = Seg 1 by FINSEQ_1:38;
then j = 1 by A93, FINSEQ_1:2, TARSKI:def 1;
then (J ^ JJ) . i = JJ . 1 by A93, A94, FINSEQ_1:def 7;
hence not (J ^ JJ) . x is empty by A92; :: thesis:

end;

len b19m = len b29m by A8, A38, A41, RFINSEQ:def 1;
then reconsider JB = Jordan_block (L,((len b1) -' m)) as Matrix of len b19m, len b29m,K by A41, A87;
A95: width JB = len b19m by A41, A42, MATRIX_0:24;
reconsider JJJ = J ^ JJ as non-empty FinSequence_of_Jordan_block of L,K by A88, FUNCT_1:def 9;
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 A86;
A96: width B = len b1m by A40, A43, MATRIX_0:24;
A97: ( Sum (Len <*B,JB*>) = (len B) + (len JB) & Sum (Width <*B,JB*>) = (width B) + (width JB) ) by MATRIXJ1:16, MATRIXJ1:20;
set BB = block_diagonal (<*B,JB*>,(0. K));
A98: len B = len b1m by A40, A43, MATRIX_0:24;
A99: Sum (Len <*B,JB*>) = len b1 by A40, A41, A42, A97, A96, A95, A98, MATRIX_0:24;
Sum (Width <*B,JB*>) = len b2 by A8, A40, A41, A97, A96, A95;
then reconsider BB = block_diagonal (<*B,JB*>,(0. K)) as Matrix of len b1, len b2,K by A99;
set T = Mx2Tran (BB,b1,b2);
A100: dom b19m = dom b29m by A41, A42, FINSEQ_3:29;

A101: now :: thesis:

let x be object ; :: 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:13;
A104: b1 . I = b1 /. I by A102, PARTFUN1:def 6;
A105: (F9 * b1) . x = F . (b1 . I) by A102, FUNCT_1:13;

now :: thesis:

per cases by A47, A102, FINSEQ_1:25;

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

then A107: ( b1m /. I = b1m . I & b1 . I = b1m . I ) by A47, FINSEQ_1:def 7, PARTFUN1:def 6;
A108: FL . (b1m /. I) = F . (b1m /. I) by FUNCT_1:49;
thus ((Mx2Tran (BB,b1,b2)) * b1) . x = (Mx2Tran (B,b1m,b2m)) . (b1m /. I) by A40, A43, A41, A42, A47, A46, A96, A95, A103, A104, A106, Th19
.= FL . (b1m /. I) by A86, MATRLIN2:34
.= (F9 * b1) . x by A102, A108, A107, FUNCT_1:13 ; :: 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 :: thesis:

per cases ;

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

A112: ( b2 . I = b29m . j & b2 /. I = b2 . I ) by A9, A40, A43, A46, A100, A102, A109, A110, FINSEQ_1:def 7, PARTFUN1:def 6;
thus (F9 * b1) . x = L * (b2 /. I) by A11, A16, A15, A40, A41, A105, A104, A110, A111
.= L * (b29m /. j) by A100, A109, A112, PARTFUN1:def 6, VECTSP_4:14
.= (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 A40, A41, A102, A110, A113, FINSEQ_3:25;
then I < len b1 by XXREAL_0:1;
then (len b1m) + j <= (len b1m) + 0 by A39, A40, A110, A115;
then j <= 0 by XREAL_1:6;
hence contradiction by A109, FINSEQ_3:25; :: thesis:

end;

j <= len b19m by A109, FINSEQ_3:25;
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:25;
then ( b29m /. (j + 1) = b29m . (j + 1) & b2 . ((len b1m) + (j + 1)) = b29m . (j + 1) ) by A40, A43, A46, A100, FINSEQ_1:def 7, PARTFUN1:def 6;
then A117: b29m /. (j + 1) = b2 /. (I + 1) by A9, A47, A110, A116, FINSEQ_1:28, PARTFUN1:def 6;
( b2 . I = b29m . j & b2 /. I = b2 . I ) by A9, A40, A43, A46, A100, A102, A109, A110, FINSEQ_1:def 7, PARTFUN1:def 6;
then L * (b29m /. j) = L * (b2 /. I) by A100, A109, PARTFUN1:def 6, VECTSP_4:14;
then (L * (b2 /. I)) + (b2 /. (I + 1)) = (L * (b29m /. j)) + (b29m /. (j + 1)) by A117, VECTSP_4:13
.= (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 A40, A43, A41, A42, A47, A46, A96, A95, 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:27;
dom F = [#] V1 by FUNCT_2:def 1;
then dom (F9 * b1) = dom b1 by A118, RELAT_1:27;
then ( block_diagonal (JJJ,(0. K)) = block_diagonal (<*B,JB*>,(0. K)) & F = Mx2Tran (BB,b1,b2) ) by A13, A119, A101, FUNCT_1:2, MATRIXJ1:35, MATRLIN:22;
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 object ; :: 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: