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 ]

proof

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:
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:
set Lb = len b1;
A4: len b1 = 0

proof

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

per cases by A3, 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 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;

reconsider J = {} as FinSequence_of_Jordan_block of L,K by Th10;
for x being set st x in dom J holds
not J . x is empty ;
then reconsider J = J as non-empty FinSequence_of_Jordan_block of L,K by FUNCT_1:def 15;
take J ; :: thesis:
len (AutMt F,b1,b2) = 0 by A4, MATRIX_1:def 3;
then ( AutMt F,b1,b2 = {} & block_diagonal J,(0. K) = {} ) by MATRIXJ1:22;
hence AutMt F,b1,b2 = block_diagonal J,(0. K) ; :: 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:
set Lb = len b1;
let F be linear-transformation of V1,V2; :: thesis:
assume that
A9: n + 1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } and
A10: 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 A9;
consider x being set such that
A11: x in FF by A9, CARD_1:47, XBOOLE_0:def 1;
consider ii being Element of NAT such that
A12: ( ii = x & ii in dom b1 & F . (b1 /. ii) = L * (b2 /. ii) ) by A11;
A13: ( dom b1 = Seg (len b1) & dom b1 = dom b2 & len b1 <> 0 ) by A8, A12, FINSEQ_1:4, FINSEQ_1:def 3, FINSEQ_3:31;
then A14: ( len b1 in dom b1 & not (len b1) + 1 in dom b1 & len b1 > 0 ) by FINSEQ_1:5, FINSEQ_3:9;
then F . (b1 /. (len b1)) = L * (b2 /. (len b1)) by A10;
then A15: len b1 in FF by A14;

per cases ;

suppose A16: 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

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

end;

then reconsider JJ = JJ as non-empty FinSequence_of_Jordan_block of L,K by FUNCT_1:def 15;
take JJ ; :: thesis:
A18: block_diagonal JJ,(0. K) = Jordan_block L,(len b1) by MATRIXJ1:34;
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;
reconsider F' = F as Function of V1,V2 ;
( rng b1 c= [#] V1 & dom F = [#] V1 & dom (Mx2Tran BB,b1,b2) = [#] V1 ) by FINSEQ_1:def 4, FUNCT_2:def 1;
then A19: ( dom (F' * b1) = dom b1 & dom ((Mx2Tran BB,b1,b2) * b1) = dom b1 ) by RELAT_1:46;

now

let y be set ; :: thesis:
assume A20: y in dom b1 ; :: thesis:
reconsider j = y as Element of NAT by A20;
A21: ( (F' * b1) . y = F . (b1 . y) & ((Mx2Tran BB,b1,b2) * b1) . y = (Mx2Tran BB,b1,b2) . (b1 . y) & b1 /. j = b1 . j ) by A20, FUNCT_1:23, PARTFUN1:def 8;

now

per cases ;

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

hence ((Mx2Tran BB,b1,b2) * b1) . y = L * (b2 /. (len b1)) by A18, A20, A21, Th23
.= (F' * b1) . y by A14, A10, A21, A22 ;
:: thesis:

end;

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

then A24: ((Mx2Tran BB,b1,b2) * b1) . y = (L * (b2 /. j)) + (b2 /. (j + 1)) by A18, A20, A21, Th23;
ex z being set st FF = {z} by A9, A16, CARD_2:60;
then FF = {(len b1)} by A15, TARSKI:def 1;
then not j in FF by A23, TARSKI:def 1;
then F . (b1 /. j) <> L * (b2 /. j) by A20;
hence ((Mx2Tran BB,b1,b2) * b1) . y = (F' * b1) . y by A20, A21, A24, A10; :: thesis:

end;

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

end;

then F = Mx2Tran BB,b1,b2 by A14, A19, FUNCT_1:9, MATRLIN:26;
hence AutMt F,b1,b2 = block_diagonal JJ,(0. K) by MATRLIN2:36; :: thesis:

end;

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

defpred S₂[ Nat] means ( $1 in FF & $1 < len b1 );
A26: for k being Nat st S₂[k] holds
k <= len b1 ;
A27: ex k being Nat st S₂[k]

proof

card FF <> 1 by A9, A25;
then FF <> {(len b1)} by CARD_2:60;
then consider y being set such that
A28: ( y in FF & y <> len b1 ) by A15, ZFMISC_1:41;
consider j being Element of NAT such that
A29: ( j = y & j in dom b1 & F . (b1 /. j) = L * (b2 /. j) ) by A28;
take j ; :: thesis:
j <= len b1 by A29, FINSEQ_3:27;
hence S₂[j] by A28, A29, XXREAL_0:1; :: thesis:

end;

consider m being Nat such that
A30: S₂[m] and
A31: for k being Nat st S₂[k] holds
k <= m from NAT_1:sch 6(A26, A27);
set b1m = b1 | m;
set b2m = b2 | m;
set b1'm = b1 /^ m;
set b2'm = b2 /^ m;
A32: ( len (b1 | m) = m & len (b2 | m) = m & len (b1 /^ m) = (len b1) - m & len (b2 /^ m) = (len b1) - m & (len b1) - m = (len b1) -' m ) by A8, A30, FINSEQ_1:80, RFINSEQ:def 2, XREAL_1:235;
reconsider Rb1 = rng (b1 | m), Rb1' = rng (b1 /^ m) as linearly-independent Subset of V1 by MATRLIN2:22, MATRLIN2:23;
reconsider Rb2 = rng (b2 | m), Rb2' = rng (b2 /^ m) as linearly-independent Subset of V2 by MATRLIN2:22, MATRLIN2:23;
set Lb1 = Lin Rb1;
set Lb2 = Lin Rb2;
set Lb1' = Lin Rb1';
set Lb2' = Lin Rb2';
reconsider b1m = b1 | m as OrdBasis of Lin Rb1 by MATRLIN2:22;
reconsider b1'm = b1 /^ m as OrdBasis of Lin Rb1' by MATRLIN2:23;
reconsider b2m = b2 | m as OrdBasis of Lin Rb2 by MATRLIN2:22;
reconsider b2'm = b2 /^ m as OrdBasis of Lin Rb2' by MATRLIN2:23;
A33: ( b1 = b1m ^ b1'm & b2 = b2m ^ b2'm ) by RFINSEQ:21;
then A34: ( dom b1m c= dom b1 & dom b1'm = dom b2'm & dom b1m = dom b2m ) by A32, FINSEQ_1:39, FINSEQ_3:31;
set FRb1 = F .: Rb1;
A35: the carrier of (Lin (F .: Rb1)) = F .: the carrier of (Lin Rb1) by VECTSP11:42;
A36: 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 A37: i in dom b1m ; :: thesis:
A38: ( b1 /. i = b1 . i & b2 /. i = b2 . i & b2 . i = b2m . i & b1 . i = b1m . i & b1m . i = b1m /. i & b2m . i = b2m /. i & F . (b1m /. i) = (F | (Lin Rb1)) . (b1m /. i) ) by A13, A37, A33, A34, FINSEQ_1:def 7, FUNCT_1:72, PARTFUN1:def 8;
set i1 = i + 1;

per cases by A37, A10, A34;

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 A38, VECTSP_4:22; :: thesis:

end;

suppose A39: ( 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;
A40: i + 1 <= m

proof

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

end;

A41: 1 <= i + 1 by NAT_1:11;
then i + 1 in dom b1m by A40, A32, FINSEQ_3:27;
then ( b2 /. (i + 1) = b2 . (i + 1) & b2 . (i + 1) = b2m . (i + 1) & b2m . (i + 1) = b2m /. (i + 1) & L * (b2 /. i) = L * (b2m /. i) ) by A38, A13, A33, A34, FINSEQ_1:def 7, PARTFUN1:def 8, VECTSP_4:22;
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 A38, A39, A41, A40, A32, 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 A42: y in F .: Rb1 ; :: thesis:
consider x being set such that
A43: ( x in dom F & x in Rb1 & F . x = y ) by A42, FUNCT_1:def 12;
consider i being set such that
A44: ( i in dom b1m & b1m . i = x ) by A43, FUNCT_1:def 5;
reconsider i = i as Element of NAT by A44;
b1m /. i = b1m . i by A44, PARTFUN1:def 8;
then (F | (Lin Rb1)) . (b1m /. i) = y by A43, A44, FUNCT_1:72;
then ( y = L * (b2m /. i) or y = (L * (b2m /. i)) + (b2m /. (i + 1)) ) by A44, A36;
hence y in the carrier of (Lin Rb2) ; :: thesis:

end;

then Lin (F .: Rb1) is Subspace of Lin Rb2 by VECTSP_9:20;
then ( F .: the carrier of (Lin Rb1) c= the carrier of (Lin Rb2) & rng (F | (Lin Rb1)) = F .: the carrier of (Lin Rb1) ) by A35, RELAT_1:148, VECTSP_4:def 2;
then reconsider FL = F | (Lin Rb1) as linear-transformation of (Lin Rb1),(Lin Rb2) by Lm4, FUNCT_2:8;
A45: 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 A36;
set FF1 = { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } ;
A46: { 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
A47: ( x = j & j in dom b1m & FL . (b1m /. j) = L * (b2m /. j) ) ;
( b1m /. j = b1m . j & b2m /. j = b2m . j & b1m . j = b1 . j & b2m . j = b2 . j & FL . (b1m /. j) = F . (b1m /. j) & b2 /. j = b2 . j & b1 /. j = b1 . j ) by A13, A33, A34, A47, FINSEQ_1:def 7, FUNCT_1:72, PARTFUN1:def 8;
then F . (b1 /. j) = L * (b2 /. j) by A47, VECTSP_4:22;
then A48: j in FF by A47, A34;
j <= m by A47, A32, FINSEQ_3:27;
hence x in FF \ {(len b1)} by A47, A48, A30, ZFMISC_1:64; :: thesis:

end;

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 A49: x in FF \ {(len b1)} ; :: thesis:
A50: ( x in FF & x <> len b1 ) by A49, ZFMISC_1:64;
then consider j being Element of NAT such that
A51: ( j = x & j in dom b1 & F . (b1 /. j) = L * (b2 /. j) ) ;
j <= len b1 by A51, FINSEQ_3:27;
then j < len b1 by A50, A51, XXREAL_0:1;
then ( 1 <= j & j <= m ) by A31, A49, A51, FINSEQ_3:27;
then A52: j in dom b1m by A32, FINSEQ_3:27;
then ( b1m /. j = b1m . j & b2m /. j = b2m . j & b1m . j = b1 . j & b2m . j = b2 . j & FL . (b1m /. j) = F . (b1m /. j) & b2 /. j = b2 . j & b1 /. j = b1 . j ) by A13, A33, A34, FINSEQ_1:def 7, FUNCT_1:72, PARTFUN1:def 8;
then FL . (b1m /. j) = L * (b2m /. j) by A51, VECTSP_4:22;
hence x in { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } by A51, A52; :: thesis:

end;

then ( { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } = FF \ {(len b1)} & n in NAT ) by A46, ORDINAL1:def 13, 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 A9, A15, STIRL2_1:65;
then consider J being non-empty FinSequence_of_Jordan_block of L,K such that
A53: AutMt FL,b1m,b2m = block_diagonal J,(0. K) by A7, A32, A45;
reconsider B = block_diagonal J,(0. K) as Matrix of len b1m, len b2m,K by A53;
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 JJJ = J ^ JJ;

now

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

per cases by A54, FINSEQ_1:38;

suppose i in dom J ; :: thesis:

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

end;

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

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

end;

then reconsider JJJ = J ^ JJ as non-empty FinSequence_of_Jordan_block of L,K by FUNCT_1:def 15;
take JJJ ; :: thesis:
reconsider JB = Jordan_block L,((len b1) -' m) as Matrix of len b1'm, len b2'm,K by A32;
A56: ( block_diagonal JJJ,(0. K) = block_diagonal <*B,JB*>,(0. K) & Sum (Len <*B,JB*>) = (len B) + (len JB) & Sum (Width <*B,JB*>) = (width B) + (width JB) & len B = len b1m & len JB = len b1'm & width B = len b1m & width JB = len b1'm ) by A32, MATRIXJ1:16, MATRIXJ1:20, MATRIXJ1:35, MATRIX_1:25;
then reconsider BB = block_diagonal <*B,JB*>,(0. K) as Matrix of len b1, len b2,K by A8, A32;
set T = Mx2Tran BB,b1,b2;
reconsider F' = F as Function of V1,V2 ;
( rng b1 c= [#] V1 & dom F = [#] V1 & dom (Mx2Tran BB,b1,b2) = [#] V1 ) by FINSEQ_1:def 4, FUNCT_2:def 1;
then A57: ( dom (F' * b1) = dom b1 & dom ((Mx2Tran BB,b1,b2) * b1) = dom b1 ) by RELAT_1:46;

now

let x be set ; :: thesis:
assume A58: x in dom b1 ; :: thesis:
reconsider I = x as Element of NAT by A58;
A59: ( (F' * b1) . x = F . (b1 . I) & ((Mx2Tran BB,b1,b2) * b1) . x = (Mx2Tran BB,b1,b2) . (b1 . I) & b1 . I = b1 /. I ) by A58, FUNCT_1:23, PARTFUN1:def 8;

now

per cases by A58, A33, FINSEQ_1:38;

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

then A61: ( b1m /. I = b1m . I & FL . (b1m /. I) = F . (b1m /. I) & b1 . I = b1m . I ) by A33, FINSEQ_1:def 7, FUNCT_1:72, PARTFUN1:def 8;
thus ((Mx2Tran BB,b1,b2) * b1) . x = (Mx2Tran B,b1m,b2m) . (b1m /. I) by A56, A33, Th19, A32, A59, A60
.= FL . (b1m /. I) by A53, MATRLIN2:34
.= (F' * b1) . x by A61, A58, FUNCT_1:23 ; :: thesis:

end;

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

then consider j being Nat such that
A62: ( j in dom b1'm & I = (len b1m) + j ) ;

now

per cases ;

suppose A63: j = len b1'm ; :: thesis:

A64: ( b2'm /. j = b2'm . j & b2 . I = b2'm . j & b2 /. I = b2 . I ) by A13, A33, A58, A62, A34, A32, FINSEQ_1:def 7, PARTFUN1:def 8;
thus (F' * b1) . x = L * (b2 /. I) by A59, A63, A14, A10, A62, A32
.= L * (b2'm /. j) by A64, VECTSP_4:22
.= (Mx2Tran JB,b1'm,b2'm) . (b1'm /. j) by A63, A62, Th23 ; :: thesis:

end;

suppose A65: j <> len b1'm ; :: thesis:

j <= len b1'm by A62, FINSEQ_3:27;
then j < len b1'm by A65, XXREAL_0:1;
then ( 1 <= j + 1 & j + 1 <= len b1'm ) by NAT_1:11, NAT_1:13;
then j + 1 in dom b1'm by FINSEQ_3:27;
then ( b2'm /. j = b2'm . j & b2 . I = b2'm . j & b2 /. I = b2 . I & b2'm /. (j + 1) = b2'm . (j + 1) & b2 . ((len b1m) + (j + 1)) = b2'm . (j + 1) & (len b1m) + (j + 1) in dom b2 ) by A13, A33, A58, A62, A34, A32, FINSEQ_1:41, FINSEQ_1:def 7, PARTFUN1:def 8;
then ( L * (b2'm /. j) = L * (b2 /. I) & b2'm /. (j + 1) = b2 /. (I + 1) ) by A62, PARTFUN1:def 8, VECTSP_4:22;
then A66: (L * (b2 /. I)) + (b2 /. (I + 1)) = (L * (b2'm /. j)) + (b2'm /. (j + 1)) by VECTSP_4:21
.= (Mx2Tran JB,b1'm,b2'm) . (b1'm /. j) by A62, A65, Th23 ;
(F' * b1) . x = (L * (b2 /. I)) + (b2 /. (I + 1))

proof

assume (F' * b1) . x <> (L * (b2 /. I)) + (b2 /. (I + 1)) ; :: thesis:
then ( F . (b1 /. I) = L * (b2 /. I) & I <> len b1 & I <= len b1 ) by A10, A58, A59, A62, A65, A32, FINSEQ_3:27;
then ( I in FF & I < len b1 ) by A58, XXREAL_0:1;
then (len b1m) + j <= (len b1m) + 0 by A62, A31, A32;
then j <= 0 by XREAL_1:8;
hence contradiction by A62, FINSEQ_3:27; :: thesis:

end;

hence (F' * b1) . x = (Mx2Tran JB,b1'm,b2'm) . (b1'm /. j) by A66; :: thesis:

end;

hence (F' * b1) . x = ((Mx2Tran BB,b1,b2) * b1) . x by A56, A33, Th19, A32, A59, A62; :: thesis:

end;

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

end;

then F = Mx2Tran BB,b1,b2 by A14, A57, FUNCT_1:9, MATRLIN:26;
hence AutMt F,b1,b2 = block_diagonal JJJ,(0. K) by A56, MATRLIN2:36; :: thesis:

end;

A67: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A6);
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 A68: len b1 = len b2 ; :: thesis:
let F be linear-transformation of V1,V2; :: thesis:
assume A69: 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 ;
S₁[ card FF] by A67;
hence ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt F,b1,b2 = block_diagonal J,(0. K) by A68, A69; :: thesis: