let K be Field; :: thesis:
defpred S₁[ Nat] means for V1 being finite-dimensional VectSp of K
for F being nilpotent linear-transformation of V1,V1 st deg F = $1 holds
ex J being FinSequence_of_Jordan_block of 0. K,K ex b1 being OrdBasis of V1 st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for i being Nat st i in dom J holds
(Len J) . i <> 0 ) );
let V1 be finite-dimensional VectSp of K; :: thesis:
let F be nilpotent linear-transformation of V1,V1; :: thesis:
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
let V1 be finite-dimensional VectSp of K; :: thesis:
set n1 = n + 1;
let F be nilpotent linear-transformation of V1,V1; :: thesis:
assume A3: deg F = n + 1 ; :: thesis:
set BAS = the Basis of V1;
A4: the Basis of V1 is linearly-independent by VECTSP_7:def 3;
A5: Lin the Basis of V1 = ModuleStr(# the carrier of V1, the addF of V1, the ZeroF of V1, the lmult of V1 #) by VECTSP_7:def 3;
set IM = im (F |^ 1);
reconsider FI = F | (im (F |^ 1)) as linear-transformation of (im (F |^ 1)),(im (F |^ 1)) by VECTSP11:32;
reconsider FI = FI as nilpotent linear-transformation of (im (F |^ 1)),(im (F |^ 1)) by Th17;
(deg FI) + 1 = n + 1 by A3, Th18, NAT_1:11;
then consider J being FinSequence_of_Jordan_block of 0. K,K, b1 being OrdBasis of im (F |^ 1) such that
A6: AutMt (FI,b1,b1) = block_diagonal (J,(0. K)) and
A7: for i being Nat st i in dom J holds
(Len J) . i <> 0 by A2;
A8: len b1 = len (AutMt (FI,b1,b1)) by MATRIX_0:def 2
.= Sum (Len J) by A6, MATRIXJ1:def 5 ;
then A9: dom b1 = Seg (Sum (Len J)) by FINSEQ_1:def 3;
set L = len J;
set LJ = Len J;
set S = Sum (Len J);
defpred S₂[ Nat, Nat] means ( $2 in dom (Len J) & $2 <= $1 & Sum ((Len J) | ($2 -' 1)) <= $1 -' $2 );
defpred S₃[ object , object ] means for i, k being Nat st i = $1 & k = $2 holds
( S₂[i,k] & i -' k <= Sum ((Len J) | k) & ( for n being Nat st S₂[i,n] holds
n <= k ) );
A10: for x being object st x in Seg ((Sum (Len J)) + (len J)) holds
ex y being object st
( y in NAT & S₃[x,y] )

let x be object ; :: thesis:
assume A11: x in Seg ((Sum (Len J)) + (len J)) ; :: thesis:
reconsider i = x as Nat by A11;
len J <> 0

proof

assume A12: len J = 0 ; :: thesis:
then Len J = <*> NAT ;
hence contradiction by A11, A12, RVSUM_1:72; :: thesis:

end;

then A13: 1 <= len J by NAT_1:14;
1 -' 1 = 0 by XREAL_1:232;
then A14: Sum ((Len J) | (1 -' 1)) = 0 by RVSUM_1:72;
defpred S₄[ Nat] means ( $1 in dom (Len J) & $1 <= i & Sum ((Len J) | ($1 -' 1)) <= i -' $1 );
A15: for k being Nat st S₄[k] holds
k <= len J

proof

let k be Nat; :: thesis:
assume S₄[k] ; :: thesis:
then k <= len (Len J) by FINSEQ_3:25;
hence k <= len J by CARD_1:def 7; :: thesis:

end;

len (Len J) = len J by CARD_1:def 7;
then A16: ( 0 <= i -' 1 & 1 in dom (Len J) ) by A13, FINSEQ_3:25;
1 <= i by A11, FINSEQ_1:1;
then A17: ex k being Nat st S₄[k] by A14, A16;
consider k being Nat such that
A18: S₄[k] and
A19: for n being Nat st S₄[n] holds
n <= k from NAT_1:sch 6(A15, A17);
A20: i -' k <= Sum ((Len J) | k)

proof

assume A21: i -' k > Sum ((Len J) | k) ; :: thesis:
then i -' k >= (Sum ((Len J) | k)) + 1 by NAT_1:13;
then A22: (i -' k) - 1 >= ((Sum ((Len J) | k)) + 1) - 1 by XREAL_1:9;
A23: i -' k = i - k by A18, XREAL_1:233;
A24: k + 1 <= len (Len J)

proof

assume k + 1 > len (Len J) ; :: thesis:
then A25: k >= len (Len J) by NAT_1:13;
then i - k > Sum (Len J) by A21, A23, FINSEQ_1:58;
then A26: (i - k) + k > (Sum (Len J)) + k by XREAL_1:6;
len (Len J) = len J by CARD_1:def 7;
then (Sum (Len J)) + k >= (Sum (Len J)) + (len J) by A25, XREAL_1:6;
then i > (Sum (Len J)) + (len J) by A26, XXREAL_0:2;
hence contradiction by A11, FINSEQ_1:1; :: thesis:

end;

1 <= k + 1 by NAT_1:14;
then A27: k + 1 in dom (Len J) by A24, FINSEQ_3:25;
i -' k >= 1 by A21, NAT_1:14;
then A28: (i - k) + k >= 1 + k by A23, XREAL_1:6;
then i -' (k + 1) = i - (k + 1) by XREAL_1:233;
then Sum ((Len J) | ((k + 1) -' 1)) <= i -' (k + 1) by A22, A23, NAT_D:34;
then k + 1 <= k by A19, A28, A27;
hence contradiction by NAT_1:13; :: thesis:

end;

take k ; :: thesis:
thus k in NAT by ORDINAL1:def 12; :: thesis:
let i9, k9 be Nat; :: thesis:
assume ( i9 = x & k9 = k ) ; :: thesis:
hence ( S₂[i9,k9] & i9 -' k9 <= Sum ((Len J) | k9) & ( for n being Nat st S₂[i9,n] holds
n <= k9 ) ) by A18, A19, A20; :: thesis:

end;

consider r being Function of (Seg ((Sum (Len J)) + (len J))),NAT such that
A29: for x being object st x in Seg ((Sum (Len J)) + (len J)) holds
S₃[x,r . x] from FUNCT_2:sch 1(A10);
defpred S₄[ object , object ] means for i, k being Nat st i = $1 & k = r . i holds
( ( i -' k = Sum ((Len J) | (k -' 1)) implies ( F . $2 = b1 . ((i -' k) + 1) & (i -' k) + 1 in dom b1 ) ) & ( i -' k <> Sum ((Len J) | (k -' 1)) implies ( $2 = b1 . (i -' k) & i -' k in dom b1 & min ((Len J),(i -' k)) = k & ( i -' k < Sum ((Len J) | k) implies ( F . $2 = b1 . ((i -' k) + 1) & (i -' k) + 1 in dom b1 ) ) & ( i -' k = Sum ((Len J) | k) implies F . $2 = 0. V1 ) ) ) );
A30: dom r = Seg ((Sum (Len J)) + (len J)) by FUNCT_2:def 1;
A31: FI = Mx2Tran ((AutMt (FI,b1,b1)),b1,b1) by MATRLIN2:34;
A32: for x being object st x in Seg ((Sum (Len J)) + (len J)) holds
ex y being object st
( y in the carrier of V1 & S₄[x,y] )

proof

let x be object ; :: thesis:
assume A33: x in Seg ((Sum (Len J)) + (len J)) ; :: thesis:
reconsider i = x as Nat by A33;
r . i = r /. i by A30, A33, PARTFUN1:def 6;
then reconsider k = r . i as Element of NAT ;
A34: i -' k <= Sum ((Len J) | k) by A29, A33;
A35: S₂[i,k] by A29, A33;
then A36: (Len J) . k = len (J . k) by MATRIXJ1:def 3;
k <= len (Len J) by A35, FINSEQ_3:25;
then A37: Sum ((Len J) | k) <= Sum ((Len J) | (len (Len J))) by POLYNOM3:18;
1 <= k by A35, FINSEQ_3:25;
then A38: k -' 1 = k - 1 by XREAL_1:233;
then k = (k -' 1) + 1 ;
then (Len J) | k = ((Len J) | (k -' 1)) ^ <*((Len J) . k)*> by A35, FINSEQ_5:10;
then A39: ( dom (Len J) = dom J & Sum ((Len J) | k) = (Sum ((Len J) | (k -' 1))) + (len (J . k)) ) by A36, MATRIXJ1:def 3, RVSUM_1:74;
A40: (Len J) | (len (Len J)) = Len J by FINSEQ_1:58;

per cases ;

suppose A41: i -' k = Sum ((Len J) | (k -' 1)) ; :: thesis:

( b1 /. ((i -' k) + 1) in im (F |^ 1) & b1 /. ((i -' k) + 1) is Element of V1 ) by VECTSP_4:10;
then consider y being Element of V1 such that
A42: (F |^ 1) . y = b1 /. ((i -' k) + 1) by RANKNULL:13;
take y ; :: thesis:
thus y in the carrier of V1 ; :: thesis:
i -' k <> Sum ((Len J) | k) by A7, A35, A36, A39, A41;
then i -' k < Sum ((Len J) | k) by A34, XXREAL_0:1;
then (i -' k) + 1 <= Sum ((Len J) | k) by NAT_1:13;
then A43: ( 1 <= (i -' k) + 1 & (i -' k) + 1 <= Sum (Len J) ) by A37, A40, NAT_1:11, XXREAL_0:2;
then (i -' k) + 1 in dom b1 by A9;
then b1 /. ((i -' k) + 1) = b1 . ((i -' k) + 1) by PARTFUN1:def 6;
hence S₄[x,y] by A9, A41, A43, A42, VECTSP11:19; :: thesis:

end;

suppose A44: i -' k <> Sum ((Len J) | (k -' 1)) ; :: thesis:

take y = b1 /. (i -' k); :: thesis:
y in im (F |^ 1) ;
then y in V1 by VECTSP_4:9;
hence y in the carrier of V1 ; :: thesis:
i -' k > Sum ((Len J) | (k -' 1)) by A35, A44, XXREAL_0:1;
then A45: 1 <= i -' k by NAT_1:14;
i -' k <= Sum (Len J) by A34, A37, A40, XXREAL_0:2;
then A46: i -' k in dom b1 by A9, A45;
i -' k <= Sum ((Len J) | k) by A29, A33;
then A47: min ((Len J),(i -' k)) <= k by A9, A46, MATRIXJ1:def 1;
A48: min ((Len J),(i -' k)) = k

proof

assume min ((Len J),(i -' k)) <> k ; :: thesis:
then min ((Len J),(i -' k)) < (k -' 1) + 1 by A38, A47, XXREAL_0:1;
then min ((Len J),(i -' k)) <= k -' 1 by NAT_1:13;
then A49: Sum ((Len J) | (min ((Len J),(i -' k)))) <= Sum ((Len J) | (k -' 1)) by POLYNOM3:18;
i -' k <= Sum ((Len J) | (min ((Len J),(i -' k)))) by A9, A46, MATRIXJ1:def 1;
then i -' k <= Sum ((Len J) | (k -' 1)) by A49, XXREAL_0:2;
hence contradiction by A35, A44, XXREAL_0:1; :: thesis:

end;

A50: Len (J | k) = (Len J) | k by MATRIXJ1:17;

A51: now :: thesis:

assume A52: i -' k = Sum ((Len J) | k) ; :: thesis:
F . (b1 /. (i -' k)) = FI . (b1 /. (i -' k)) by FUNCT_1:49
.= (0. K) * (b1 /. (i -' k)) by A6, A31, A46, A48, A50, A52, Th24
.= 0. (im (F |^ 1)) by VECTSP_1:14
.= 0. V1 by VECTSP_4:11 ;
hence F . y = 0. V1 ; :: thesis:

end;

A53: now :: thesis:

assume A54: i -' k < Sum ((Len J) | k) ; :: thesis:
then (i -' k) + 1 <= Sum ((Len J) | k) by NAT_1:13;
then A55: ( 1 <= (i -' k) + 1 & (i -' k) + 1 <= Sum (Len J) ) by A37, A40, NAT_1:11, XXREAL_0:2;
then A56: (i -' k) + 1 in dom b1 by A9;
F . (b1 /. (i -' k)) = FI . (b1 /. (i -' k)) by FUNCT_1:49
.= ((0. K) * (b1 /. (i -' k))) + (b1 /. ((i -' k) + 1)) by A6, A31, A46, A48, A50, A54, Th24
.= (0. (im (F |^ 1))) + (b1 /. ((i -' k) + 1)) by VECTSP_1:14
.= b1 /. ((i -' k) + 1) by RLVECT_1:def 4
.= b1 . ((i -' k) + 1) by A56, PARTFUN1:def 6 ;
hence ( F . y = b1 . ((i -' k) + 1) & (i -' k) + 1 in dom b1 ) by A9, A55; :: thesis:

end;

let i9, k9 be Nat; :: thesis:
assume ( x = i9 & k9 = r . i9 ) ; :: thesis:
hence ( ( i9 -' k9 = Sum ((Len J) | (k9 -' 1)) implies ( F . y = b1 . ((i9 -' k9) + 1) & (i9 -' k9) + 1 in dom b1 ) ) & ( i9 -' k9 <> Sum ((Len J) | (k9 -' 1)) implies ( y = b1 . (i9 -' k9) & i9 -' k9 in dom b1 & min ((Len J),(i9 -' k9)) = k9 & ( i9 -' k9 < Sum ((Len J) | k9) implies ( F . y = b1 . ((i9 -' k9) + 1) & (i9 -' k9) + 1 in dom b1 ) ) & ( i9 -' k9 = Sum ((Len J) | k9) implies F . y = 0. V1 ) ) ) ) by A44, A46, A48, A53, A51, PARTFUN1:def 6; :: thesis:

end;

consider B being Function of (Seg ((Sum (Len J)) + (len J))), the carrier of V1 such that
A57: for x being object st x in Seg ((Sum (Len J)) + (len J)) holds
S₄[x,B . x] from FUNCT_2:sch 1(A32);
A58: rng B c= the carrier of V1 by RELAT_1:def 19;
A59: dom B = Seg ((Sum (Len J)) + (len J)) by FUNCT_2:def 1;
then reconsider B = B as FinSequence by FINSEQ_1:def 2;
reconsider B = B as FinSequence of V1 by A58, FINSEQ_1:def 4;
reconsider RNG = rng B as Subset of V1 by FINSEQ_1:def 4;

now :: thesis:

rng b1 is Basis of (im (F |^ 1)) by MATRLIN:def 2;
then rng b1 is linearly-independent Subset of (im (F |^ 1)) by VECTSP_7:def 3;
then reconsider rngb1 = rng b1 as linearly-independent Subset of V1 by VECTSP_9:11;
set RB = { v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) } ;
set RA = { v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) } ;
A60: { v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) } c= the carrier of V1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) } ; :: thesis:
then ex v1 being Vector of V1 st
( x = v1 & ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) ) ;
hence x in the carrier of V1 ; :: thesis:

end;

{ v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) } c= the carrier of V1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) } ; :: thesis:
then ex v1 being Vector of V1 st
( x = v1 & ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) ) ;
hence x in the carrier of V1 ; :: thesis:

end;

then reconsider RA = { v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) } , RB = { v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) } as Subset of V1 by A60;
let l be Linear_Combination of RNG; :: thesis:
assume A61: Sum l = 0. V1 ; :: thesis:
A62: F | RA is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A63: x1 in dom (F | RA) and
A64: x2 in dom (F | RA) and
A65: (F | RA) . x1 = (F | RA) . x2 ; :: thesis:
A66: ( (F | RA) . x1 = F . x1 & (F | RA) . x2 = F . x2 ) by A63, A64, FUNCT_1:47;
A67: dom (F | RA) = (dom F) /\ RA by RELAT_1:61;
then x1 in RA by A63, XBOOLE_0:def 4;
then consider v1 being Vector of V1 such that
A68: x1 = v1 and
A69: ex i1, k1 being Nat st
( i1 in Seg ((len J) + (Sum (Len J))) & k1 = r . i1 & v1 = B . i1 & i1 -' k1 < Sum ((Len J) | k1) ) ;
consider i1, k1 being Nat such that
A70: ( i1 in Seg ((len J) + (Sum (Len J))) & k1 = r . i1 ) and
A71: v1 = B . i1 and
A72: i1 -' k1 < Sum ((Len J) | k1) by A69;
k1 <= i1 by A29, A70;
then A73: i1 -' k1 = i1 - k1 by XREAL_1:233;
A74: k1 in dom (Len J) by A29, A70;
then 1 <= k1 by FINSEQ_3:25;
then A75: k1 -' 1 = k1 - 1 by XREAL_1:233;
then (k1 -' 1) + 1 <= len (Len J) by A74, FINSEQ_3:25;
then A76: k1 -' 1 <= len (Len J) by NAT_1:13;
A77: b1 is one-to-one by MATRLIN:def 2;
A78: dom (Len J) = dom J by MATRIXJ1:def 3;
then A79: ( k1 -' 1 in dom (Len J) implies (Len J) . (k1 -' 1) <> 0 ) by A7;
x2 in RA by A64, A67, XBOOLE_0:def 4;
then consider v2 being Vector of V1 such that
A80: x2 = v2 and
A81: ex i2, k2 being Nat st
( i2 in Seg ((len J) + (Sum (Len J))) & k2 = r . i2 & v2 = B . i2 & i2 -' k2 < Sum ((Len J) | k2) ) ;
consider i2, k2 being Nat such that
A82: ( i2 in Seg ((len J) + (Sum (Len J))) & k2 = r . i2 ) and
A83: v2 = B . i2 and
A84: i2 -' k2 < Sum ((Len J) | k2) by A81;
A85: k2 <= i2 by A29, A82;
then A86: i2 -' k2 = i2 - k2 by XREAL_1:233;
A87: k2 in dom (Len J) by A29, A82;
then 1 <= k2 by FINSEQ_3:25;
then A88: k2 -' 1 = k2 - 1 by XREAL_1:233;
then (k2 -' 1) + 1 <= len (Len J) by A87, FINSEQ_3:25;
then A89: k2 -' 1 <= len (Len J) by NAT_1:13;
A90: ( k2 -' 1 in dom (Len J) implies (Len J) . (k2 -' 1) <> 0 ) by A7, A78;

per cases ;

suppose A91: ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 = Sum ((Len J) | (k2 -' 1)) ) ; :: thesis:

then A92: ( F . v2 = b1 . ((i2 -' k2) + 1) & (i2 -' k2) + 1 in dom b1 ) by A57, A82, A83;
( F . v1 = b1 . ((i1 -' k1) + 1) & (i1 -' k1) + 1 in dom b1 ) by A57, A70, A71, A91;
then (i1 -' k1) + 1 = (i2 -' k2) + 1 by A65, A66, A68, A80, A77, A92;
then k1 -' 1 = k2 -' 1 by A76, A89, A79, A90, A91, MATRIXJ1:11;
then i1 - k1 = i2 - k1 by A85, A73, A75, A88, A91, XREAL_1:233;
hence x1 = x2 by A68, A71, A80, A83; :: thesis:

end;

suppose A93: ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) ) ; :: thesis:

then A94: min ((Len J),(i2 -' k2)) = k2 by A57, A82;
A95: ( F . v1 = b1 . ((i1 -' k1) + 1) & (i1 -' k1) + 1 in dom b1 ) by A57, A70, A71, A93;
( F . v2 = b1 . ((i2 -' k2) + 1) & (i2 -' k2) + 1 in dom b1 ) by A57, A82, A83, A84, A93;
then A96: (i1 -' k1) + 1 = (i2 -' k2) + 1 by A65, A66, A68, A80, A77, A95;
k1 -' 1 <> 0

proof

assume k1 -' 1 = 0 ; :: thesis:
then (Len J) | (k1 -' 1) = <*> REAL ;
hence contradiction by A29, A82, A93, A96, RVSUM_1:72; :: thesis:

end;

then k1 -' 1 >= 1 by NAT_1:14;
then A97: k1 -' 1 in dom (Len J) by A76, FINSEQ_3:25;
then (Len J) . (k1 -' 1) <> 0 by A7, A78;
hence x1 = x2 by A84, A93, A94, A96, A97, MATRIXJ1:6; :: thesis:

end;

suppose A98: ( i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i2 -' k2 = Sum ((Len J) | (k2 -' 1)) ) ; :: thesis:

then A99: min ((Len J),(i1 -' k1)) = k1 by A57, A70;
A100: ( F . v2 = b1 . ((i2 -' k2) + 1) & (i2 -' k2) + 1 in dom b1 ) by A57, A82, A83, A98;
( F . v1 = b1 . ((i1 -' k1) + 1) & (i1 -' k1) + 1 in dom b1 ) by A57, A70, A71, A72, A98;
then A101: (i1 -' k1) + 1 = (i2 -' k2) + 1 by A65, A66, A68, A80, A77, A100;
k2 -' 1 <> 0

proof

assume k2 -' 1 = 0 ; :: thesis:
then i1 -' k1 = 0 by A98, A101, RVSUM_1:72;
hence contradiction by A29, A70, A98; :: thesis:

end;

then k2 -' 1 >= 1 by NAT_1:14;
then A102: k2 -' 1 in dom (Len J) by A89, FINSEQ_3:25;
then (Len J) . (k2 -' 1) <> 0 by A7, A78;
hence x1 = x2 by A72, A98, A99, A101, A102, MATRIXJ1:6; :: thesis:

end;

suppose A103: ( i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) ) ; :: thesis:

then A104: min ((Len J),(i2 -' k2)) = k2 by A57, A82;
A105: ( F . v2 = b1 . ((i2 -' k2) + 1) & (i2 -' k2) + 1 in dom b1 ) by A57, A82, A83, A84, A103;
( F . v1 = b1 . ((i1 -' k1) + 1) & (i1 -' k1) + 1 in dom b1 ) by A57, A70, A71, A72, A103;
then (i1 -' k1) + 1 = (i2 -' k2) + 1 by A65, A66, A68, A80, A77, A105;
then i1 - k1 = i2 - k1 by A57, A70, A73, A86, A103, A104;
hence x1 = x2 by A68, A71, A80, A83; :: thesis:

end;

A106: RB c= rngb1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in RB ; :: thesis:
then consider v1 being Vector of V1 such that
A107: x = v1 and
A108: ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) ;
consider i, k being Nat such that
A109: ( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) ) and
i -' k = Sum ((Len J) | k) by A108;
( v1 = b1 . (i -' k) & i -' k in dom b1 ) by A57, A109;
hence x in rngb1 by A107, FUNCT_1:def 3; :: thesis:

end;

A110: Carrier l c= RB \/ RA

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A111: x in Carrier l ; :: thesis:
reconsider v1 = x as Vector of V1 by A111;
Carrier l c= RNG by VECTSP_6:def 4;
then consider i being object such that
A112: i in dom B and
A113: B . i = v1 by A111, FUNCT_1:def 3;
reconsider i = i as Nat by A112;
r . i = r /. i by A30, A59, A112, PARTFUN1:def 6;
then reconsider k = r . i as Element of NAT ;
A114: i -' k <= Sum ((Len J) | k) by A29, A59, A112;

per cases by A114, XXREAL_0:1;

suppose A115: i -' k = Sum ((Len J) | k) ; :: thesis:

A116: S₂[i,k] by A29, A59, A112;
then 1 <= k by FINSEQ_3:25;
then k -' 1 = k - 1 by XREAL_1:233;
then (k -' 1) + 1 = k ;
then (Len J) | k = ((Len J) | (k -' 1)) ^ <*((Len J) . k)*> by A116, FINSEQ_5:10;
then ( dom (Len J) = dom J & i -' k = (Sum ((Len J) | (k -' 1))) + ((Len J) . k) ) by A115, MATRIXJ1:def 3, RVSUM_1:74;
then i -' k <> Sum ((Len J) | (k -' 1)) by A7, A116;
then ( v1 in RB or v1 in RA ) by A59, A112, A113, A115;
hence x in RB \/ RA by XBOOLE_0:def 3; :: thesis:

end;

suppose i -' k < Sum ((Len J) | k) ; :: thesis:

then ( v1 in RB or v1 in RA ) by A59, A112, A113;
hence x in RB \/ RA by XBOOLE_0:def 3; :: thesis:

end;

F .: RA c= rngb1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in F .: RA ; :: thesis:
then consider x being object such that
x in dom F and
A117: x in RA and
A118: y = F . x by FUNCT_1:def 6;
consider v1 being Vector of V1 such that
A119: x = v1 and
A120: ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) by A117;
consider i, k being Nat such that
A121: ( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) by A120;
( i -' k <> Sum ((Len J) | (k -' 1)) or i -' k = Sum ((Len J) | (k -' 1)) ) ;
then ( F . v1 = b1 . ((i -' k) + 1) & (i -' k) + 1 in dom b1 ) by A57, A121;
hence y in rngb1 by A118, A119, FUNCT_1:def 3; :: thesis:

end;

then A122: F .: RA is linearly-independent Subset of V1 by VECTSP_7:1;
F .: RB c= {(0. V1)}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in F .: RB ; :: thesis:
then consider x being object such that
x in dom F and
A123: x in RB and
A124: y = F . x by FUNCT_1:def 6;
consider v1 being Vector of V1 such that
A125: x = v1 and
A126: ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) by A123;
F . v1 = 0. V1 by A57, A126;
hence y in {(0. V1)} by A124, A125, TARSKI:def 1; :: thesis:

end;

then Carrier l c= RB by A61, A110, A62, A122, VECTSP11:44;
then Carrier l c= rngb1 by A106;
then l is Linear_Combination of rngb1 by VECTSP_6:def 4;
hence Carrier l = {} by A61, VECTSP_7:def 1; :: thesis:

end;

then A127: RNG is linearly-independent Subset of V1 by VECTSP_7:def 1;
reconsider BAS = the Basis of V1, RNG = RNG as finite Subset of V1 ;
consider C being finite Subset of V1 such that
C c= BAS and
A128: card C = (card BAS) - (card RNG) and
A129: ModuleStr(# the carrier of V1, the addF of V1, the ZeroF of V1, the lmult of V1 #) = Lin (RNG \/ C) by A127, A5, VECTSP_9:19;
A130: (Omega). (Lin BAS) = (Omega). V1 by VECTSP_7:def 3;
then A131: dim V1 = dim (Lin BAS) by VECTSP_9:28;
defpred S₅[ Nat] means ( $1 <= card C implies ex f being FinSequence of V1 st
( f is one-to-one & len f = card C & RNG misses rng f & RNG \/ (rng f) is Basis of V1 & ( for i being Nat st i in dom f & i <= $1 holds
F . (f . i) = 0. V1 ) ) );
A132: for n being Nat st S₅[n] holds
S₅[n + 1]

proof

let n be Nat; :: thesis:
assume A133: S₅[n] ; :: thesis:
set n1 = n + 1;
assume A134: n + 1 <= card C ; :: thesis:
then consider f being FinSequence of V1 such that
A135: f is one-to-one and
A136: len f = card C and
A137: RNG misses rng f and
A138: RNG \/ (rng f) is Basis of V1 and
A139: for i being Nat st i in dom f & i <= n holds
F . (f . i) = 0. V1 by A133, NAT_1:13;

per cases ;

suppose F . (f . (n + 1)) = 0. V1 ; :: thesis:

then for i being Nat st i in dom f & i <= n + 1 holds
F . (f . i) = 0. V1 by A139, NAT_1:8;
hence ex f being FinSequence of V1 st
( f is one-to-one & len f = card C & RNG misses rng f & RNG \/ (rng f) is Basis of V1 & ( for i being Nat st i in dom f & i <= n + 1 holds
F . (f . i) = 0. V1 ) ) by A135, A136, A137, A138; :: thesis:

end;

suppose A140: F . (f . (n + 1)) <> 0. V1 ; :: thesis:

reconsider Rf = RNG \/ (rng f) as finite Subset of V1 by A138;
reconsider rngB1 = rng b1 as Basis of (im (F |^ 1)) by MATRLIN:def 2;
set fn = f /. (n + 1);
1 <= n + 1 by NAT_1:14;
then A141: n + 1 in dom f by A134, A136, FINSEQ_3:25;
then A142: f /. (n + 1) = f . (n + 1) by PARTFUN1:def 6;
A143: rng b1 c= F .: RNG

proof

A144: dom F = [#] V1 by FUNCT_2:def 1;
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng b1 ; :: thesis:
then consider x being object such that
A145: x in dom b1 and
A146: b1 . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A145;
A147: ( len (Len J) = len J & x <= Sum (Len J) ) by A8, A145, CARD_1:def 7, FINSEQ_3:25;
set m = min ((Len J),x);
A148: x <= Sum ((Len J) | (min ((Len J),x))) by A9, A145, MATRIXJ1:def 1;
A149: min ((Len J),x) in dom (Len J) by A9, A145, MATRIXJ1:def 1;
then min ((Len J),x) <= len (Len J) by FINSEQ_3:25;
then (min ((Len J),x)) + x <= (len J) + (Sum (Len J)) by A147, XREAL_1:7;
then A150: ((min ((Len J),x)) + x) - 1 <= ((len J) + (Sum (Len J))) - 1 by XREAL_1:9;
set x1 = x -' 1;
A151: 1 <= x by A145, FINSEQ_3:25;
then A152: x -' 1 = x - 1 by XREAL_1:233;
1 <= min ((Len J),x) by A149, FINSEQ_3:25;
then 1 + 1 <= (min ((Len J),x)) + x by A151, XREAL_1:7;
then A153: 2 - 1 <= ((min ((Len J),x)) + x) - 1 by XREAL_1:9;
set mx = (min ((Len J),x)) + (x -' 1);
A154: ((min ((Len J),x)) + (x -' 1)) -' (min ((Len J),x)) = ((min ((Len J),x)) + (x -' 1)) - (min ((Len J),x)) by NAT_1:11, XREAL_1:233;
((len J) + (Sum (Len J))) - 1 <= ((len J) + (Sum (Len J))) - 0 by XREAL_1:10;
then (min ((Len J),x)) + (x -' 1) <= (len J) + (Sum (Len J)) by A152, A150, XXREAL_0:2;
then A155: (min ((Len J),x)) + (x -' 1) in Seg ((Sum (Len J)) + (len J)) by A152, A153;
then r . ((min ((Len J),x)) + (x -' 1)) = r /. ((min ((Len J),x)) + (x -' 1)) by A30, PARTFUN1:def 6;
then reconsider k = r . ((min ((Len J),x)) + (x -' 1)) as Element of NAT ;
A156: B . ((min ((Len J),x)) + (x -' 1)) in RNG by A59, A155, FUNCT_1:def 3;
A157: Sum ((Len J) | ((min ((Len J),x)) -' 1)) < (x -' 1) + 1 by A9, A145, A152, MATRIXJ1:7;
then ( min ((Len J),x) <= (min ((Len J),x)) + (x -' 1) & Sum ((Len J) | ((min ((Len J),x)) -' 1)) <= ((min ((Len J),x)) + (x -' 1)) -' (min ((Len J),x)) ) by A154, NAT_1:11, NAT_1:13;
then A158: min ((Len J),x) <= k by A29, A149, A155;
A159: min ((Len J),x) = k

proof

assume min ((Len J),x) <> k ; :: thesis:
then A160: min ((Len J),x) < k by A158, XXREAL_0:1;
then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
A161: k = k1 + 1 ;
then min ((Len J),x) <= k1 by A160, NAT_1:13;
then A162: Sum ((Len J) | (min ((Len J),x))) <= Sum ((Len J) | k1) by POLYNOM3:18;
A163: ((min ((Len J),x)) + (x -' 1)) -' k <= ((min ((Len J),x)) + (x -' 1)) -' (min ((Len J),x)) by A158, NAT_D:41;
k -' 1 = k1 by A161, NAT_D:34;
then Sum ((Len J) | k1) <= ((min ((Len J),x)) + (x -' 1)) -' k by A29, A155;
then Sum ((Len J) | (min ((Len J),x))) <= ((min ((Len J),x)) + (x -' 1)) -' k by A162, XXREAL_0:2;
then Sum ((Len J) | (min ((Len J),x))) <= x -' 1 by A154, A163, XXREAL_0:2;
hence contradiction by A152, A157, A148, NAT_1:13; :: thesis:

end;

A164: ( ((min ((Len J),x)) + (x -' 1)) -' (min ((Len J),x)) = Sum ((Len J) | ((min ((Len J),x)) -' 1)) or ((min ((Len J),x)) + (x -' 1)) -' (min ((Len J),x)) <> Sum ((Len J) | ((min ((Len J),x)) -' 1)) ) ;
((min ((Len J),x)) + (x -' 1)) -' (min ((Len J),x)) < Sum ((Len J) | (min ((Len J),x))) by A152, A154, A157, A148, NAT_1:13;
then F . (B . ((min ((Len J),x)) + (x -' 1))) = b1 . ((((min ((Len J),x)) + (x -' 1)) -' (min ((Len J),x))) + 1) by A57, A155, A159, A164;
hence y in F .: RNG by A146, A152, A154, A156, A144, FUNCT_1:def 6; :: thesis:

end;

( F . (f /. (n + 1)) in im F & F |^ 1 = F ) by RANKNULL:13, VECTSP11:19;
then F . (f /. (n + 1)) in Lin rngB1 by VECTSP_7:def 3;
then consider L being Linear_Combination of rngB1 such that
A165: F . (f /. (n + 1)) = Sum L by VECTSP_7:7;
consider K being Linear_Combination of V1 such that
A166: Carrier L = Carrier K and
A167: Sum L = Sum K by VECTSP_9:8;
Carrier L c= rngB1 by VECTSP_6:def 4;
then consider M being Linear_Combination of RNG such that
A168: F . (Sum M) = Sum K by A143, A166, VECTSP11:41, XBOOLE_1:1;
A169: f . (n + 1) in rng f by A141, FUNCT_1:def 3;
then A170: f /. (n + 1) in Rf by A142, XBOOLE_0:def 3;
A171: not f /. (n + 1) in RNG by A137, A142, A169, XBOOLE_0:3;
not f /. (n + 1) in RNG by A137, A142, A169, XBOOLE_0:3;
then A172: RNG c= Rf \ {(f /. (n + 1))} by XBOOLE_1:7, ZFMISC_1:34;
( Carrier M c= RNG & Carrier M = Carrier (- M) ) by VECTSP_6:38, VECTSP_6:def 4;
then Carrier (- M) c= Rf \ {(f /. (n + 1))} by A172;
then reconsider M9 = - M as Linear_Combination of Rf \ {(f /. (n + 1))} by VECTSP_6:def 4;
set fnM = (f /. (n + 1)) + (Sum M9);
A173: (f /. (n + 1)) + (Sum M9) <> f /. (n + 1)

proof

assume (f /. (n + 1)) + (Sum M9) = f /. (n + 1) ; :: thesis:
then 0. V1 = ((f /. (n + 1)) + (Sum M9)) - (f /. (n + 1)) by VECTSP_1:16
.= (Sum M9) + ((f /. (n + 1)) - (f /. (n + 1))) by RLVECT_1:def 3
.= (Sum M9) + (0. V1) by RLVECT_1:def 10
.= Sum M9 by RLVECT_1:def 4
.= - (Sum M) by VECTSP_6:46 ;
then 0. V1 = Sum M by VECTSP_1:28;
hence contradiction by A140, A142, A165, A167, A168, RANKNULL:9; :: thesis:

end;

take ff = f +* ((n + 1),((f /. (n + 1)) + (Sum M9))); :: thesis:
set fnS = (n + 1) .--> ((f /. (n + 1)) + (Sum M9));
A174: Rf is linearly-independent by A138, VECTSP_7:def 3;
A175: not (f /. (n + 1)) + (Sum M9) in Rf \ {(f /. (n + 1))}

proof

card Rf <> 0 by A169;
then reconsider c1 = (card Rf) - 1 as Element of NAT by NAT_1:20;
assume (f /. (n + 1)) + (Sum M9) in Rf \ {(f /. (n + 1))} ; :: thesis:
then A176: (Rf \ {(f /. (n + 1))}) \/ {((f /. (n + 1)) + (Sum M9))} = Rf \ {(f /. (n + 1))} by ZFMISC_1:40;
c1 + 1 = card Rf ;
then A177: card (Rf \ {(f /. (n + 1))}) = c1 by A170, STIRL2_1:55;
card ((Rf \ {(f /. (n + 1))}) \/ {((f /. (n + 1)) + (Sum M9))}) = c1 + 1 by A174, A170, VECTSP11:40;
hence contradiction by A177, A176; :: thesis:

end;

not (f /. (n + 1)) + (Sum M9) in rng f

proof

assume (f /. (n + 1)) + (Sum M9) in rng f ; :: thesis:
then (f /. (n + 1)) + (Sum M9) in Rf by XBOOLE_0:def 3;
hence contradiction by A175, A173, ZFMISC_1:56; :: thesis:

end;

then A178: rng f misses {((f /. (n + 1)) + (Sum M9))} by ZFMISC_1:50;
rng ((n + 1) .--> ((f /. (n + 1)) + (Sum M9))) = {((f /. (n + 1)) + (Sum M9))} by FUNCOP_1:8;
then f +* ((n + 1) .--> ((f /. (n + 1)) + (Sum M9))) is one-to-one by A135, A178, FUNCT_4:92;
hence ff is one-to-one by A141, FUNCT_7:def 3; :: thesis:
A179: dom ff = dom f by FUNCT_7:30;
hence len ff = card C by A136, FINSEQ_3:29; :: thesis:
A180: rng ff = ((rng f) \ {(f /. (n + 1))}) \/ {((f /. (n + 1)) + (Sum M9))} by A135, A141, A142, Lm1;
thus RNG misses rng ff :: thesis:

proof

assume RNG meets rng ff ; :: thesis:
then consider x being object such that
A181: x in RNG and
A182: x in rng ff by XBOOLE_0:3;
not x in (rng f) \ {(f /. (n + 1))} by A137, A181, XBOOLE_0:3;
then x in {((f /. (n + 1)) + (Sum M9))} by A180, A182, XBOOLE_0:def 3;
then A183: x = (f /. (n + 1)) + (Sum M9) by TARSKI:def 1;
not (f /. (n + 1)) + (Sum M9) in Rf by A175, A173, ZFMISC_1:56;
hence contradiction by A181, A183, XBOOLE_0:def 3; :: thesis:

end;

A184: (Rf \ {(f /. (n + 1))}) \/ {((f /. (n + 1)) + (Sum M9))} = ((RNG \ {(f /. (n + 1))}) \/ ((rng f) \ {(f /. (n + 1))})) \/ {((f /. (n + 1)) + (Sum M9))} by XBOOLE_1:42
.= (RNG \/ ((rng f) \ {(f /. (n + 1))})) \/ {((f /. (n + 1)) + (Sum M9))} by A171, ZFMISC_1:57
.= RNG \/ (rng ff) by A180, XBOOLE_1:4 ;
then reconsider Rff = RNG \/ (rng ff) as finite Subset of V1 ;
dim V1 = card Rf by A138, VECTSP_9:def 1
.= card (RNG \/ (rng ff)) by A174, A170, A184, VECTSP11:40 ;
then dim (Lin Rff) = dim V1 by A174, A170, A184, VECTSP11:40, VECTSP_9:26;
then A185: (Omega). V1 = (Omega). (Lin Rff) by VECTSP_9:28;
(Rf \ {(f /. (n + 1))}) \/ {((f /. (n + 1)) + (Sum M9))} is linearly-independent by A174, A170, VECTSP11:40;
hence RNG \/ (rng ff) is Basis of V1 by A184, A185, VECTSP_7:def 3; :: thesis:
let i be Nat; :: thesis:
assume that
A186: i in dom ff and
A187: i <= n + 1 ; :: thesis:

per cases by A187, XXREAL_0:1;

suppose i < n + 1 ; :: thesis:

then ( ff . i = f . i & i <= n ) by FUNCT_7:32, NAT_1:13;
hence F . (ff . i) = 0. V1 by A139, A179, A186; :: thesis:

end;

suppose i = n + 1 ; :: thesis:

then ff . i = (f /. (n + 1)) + (Sum M9) by A179, A186, FUNCT_7:31;
hence F . (ff . i) = F . ((f /. (n + 1)) - (Sum M)) by VECTSP_6:46
.= (F . (f /. (n + 1))) - (F . (Sum M)) by RANKNULL:8
.= 0. V1 by A165, A167, A168, RLVECT_1:def 10 ;
:: thesis:

end;

A188: card (RNG \/ C) = ((card RNG) + (card C)) - (card (RNG /\ C)) by CARD_2:45
.= (card BAS) - (card (RNG /\ C)) by A128 ;
then (card (RNG \/ C)) + (card (RNG /\ C)) = card BAS ;
then A189: card (RNG \/ C) <= card BAS by NAT_1:11;
A190: dim (Lin BAS) = card BAS by A4, VECTSP_9:26;
then A191: card (RNG \/ C) >= card BAS by A130, A129, MATRLIN2:6;
then A192: card (RNG \/ C) = card BAS by A189, XXREAL_0:1;
dim V1 = dim (Lin (RNG \/ C)) by A130, A129, VECTSP_9:28;
then A193: RNG \/ C is linearly-independent by A131, A190, A191, A189, MATRLIN2:5, XXREAL_0:1;
A194: S₅[ 0 ]

proof

assume 0 <= card C ; :: thesis:
card C = card (Seg (card C)) by FINSEQ_1:57;
then Seg (card C),C are_equipotent by CARD_1:5;
then consider f being Function such that
A195: f is one-to-one and
A196: dom f = Seg (card C) and
A197: rng f = C by WELLORD2:def 4;
reconsider f = f as FinSequence by A196, FINSEQ_1:def 2;
reconsider f = f as FinSequence of V1 by A197, FINSEQ_1:def 4;
take f ; :: thesis:
thus ( f is one-to-one & len f = card C ) by A195, A196, FINSEQ_1:def 3; :: thesis:
RNG /\ C = {} by A188, A192;
hence ( RNG misses rng f & RNG \/ (rng f) is Basis of V1 ) by A129, A193, A197, VECTSP_7:def 3, XBOOLE_0:def 7; :: thesis:
let i be Nat; :: thesis:
assume ( i in dom f & i <= 0 ) ; :: thesis:
hence F . (f . i) = 0. V1 by FINSEQ_3:25; :: thesis:

end;

for n being Nat holds S₅[n] from NAT_1:sch 2(A194, A132);
then consider f being FinSequence of V1 such that
A198: f is one-to-one and
A199: len f = card C and
A200: RNG misses rng f and
A201: RNG \/ (rng f) is Basis of V1 and
A202: for i being Nat st i in dom f & i <= card C holds
F . (f . i) = 0. V1 ;
A203: rng (B ^ f) = (rng B) \/ (rng f) by FINSEQ_1:31;

now :: thesis:

let x1, x2 be object ; :: thesis:
assume that
A204: x1 in dom B and
A205: x2 in dom B and
A206: B . x1 = B . x2 ; :: thesis:
reconsider i1 = x1, i2 = x2 as Nat by A204, A205;
( r /. i1 = r . i1 & r /. i2 = r . i2 ) by A30, A59, A204, A205, PARTFUN1:def 6;
then reconsider k1 = r . i1, k2 = r . i2 as Element of NAT ;
A207: ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) implies ( F . (B . x1) = b1 . ((i1 -' k1) + 1) & (i1 -' k1) + 1 in dom b1 ) ) by A57, A59, A204;
A208: S₂[i1,k1] by A29, A59, A204;
then A209: i1 -' k1 = i1 - k1 by XREAL_1:233;
A210: S₂[i2,k2] by A29, A59, A205;
then A211: i2 -' k2 = i2 - k2 by XREAL_1:233;
A212: k2 -' 1 <= k2 by NAT_D:35;
A213: ( i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) implies ( B . x1 = b1 . (i1 -' k1) & i1 -' k1 in dom b1 & min ((Len J),(i1 -' k1)) = k1 & ( i1 -' k1 < Sum ((Len J) | k1) implies ( F . (B . x1) = b1 . ((i1 -' k1) + 1) & (i1 -' k1) + 1 in dom b1 ) ) & ( i1 -' k1 = Sum ((Len J) | k1) implies F . (B . x1) = 0. V1 ) ) ) by A57, A59, A204;
k2 <= len (Len J) by A210, FINSEQ_3:25;
then A214: k2 -' 1 <= len (Len J) by A212, XXREAL_0:2;
1 <= k1 by A208, FINSEQ_3:25;
then A215: k1 -' 1 = k1 - 1 by XREAL_1:233;
A216: ( i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) implies ( B . x2 = b1 . (i2 -' k2) & i2 -' k2 in dom b1 & min ((Len J),(i2 -' k2)) = k2 & ( i2 -' k2 < Sum ((Len J) | k2) implies ( F . (B . x2) = b1 . ((i2 -' k2) + 1) & (i2 -' k2) + 1 in dom b1 ) ) & ( i2 -' k2 = Sum ((Len J) | k2) implies F . (B . x2) = 0. V1 ) ) ) by A57, A59, A205;
1 <= k2 by A210, FINSEQ_3:25;
then A217: k2 -' 1 = k2 - 1 by XREAL_1:233;
A218: ( i2 -' k2 = Sum ((Len J) | (k2 -' 1)) implies ( F . (B . x2) = b1 . ((i2 -' k2) + 1) & (i2 -' k2) + 1 in dom b1 ) ) by A57, A59, A205;
A219: k1 -' 1 <= k1 by NAT_D:35;
k1 <= len (Len J) by A208, FINSEQ_3:25;
then A220: k1 -' 1 <= len (Len J) by A219, XXREAL_0:2;
A221: dom (Len J) = dom J by MATRIXJ1:def 3;
rng b1 is Basis of (im (F |^ 1)) by MATRLIN:def 2;
then A222: rng b1 is linearly-independent Subset of (im (F |^ 1)) by VECTSP_7:def 3;
A223: b1 is one-to-one by MATRLIN:def 2;
A224: ( i1 -' k1 <= Sum ((Len J) | k1) & i2 -' k2 <= Sum ((Len J) | k2) ) by A29, A59, A204, A205;

now :: thesis:

per cases by A224, XXREAL_0:1;

suppose A225: ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 = Sum ((Len J) | (k2 -' 1)) ) ; :: thesis:

then A226: ( F . (B . x2) = b1 . ((i2 -' k2) + 1) & (i2 -' k2) + 1 in dom b1 ) by A57, A59, A205;
( F . (B . x1) = b1 . ((i1 -' k1) + 1) & (i1 -' k1) + 1 in dom b1 ) by A57, A59, A204, A225;
then A227: (i1 -' k1) + 1 = (i2 -' k2) + 1 by A206, A223, A226;
A228: ( k2 -' 1 in dom (Len J) implies (Len J) . (k2 -' 1) <> 0 ) by A7, A221;
( k1 -' 1 in dom (Len J) implies (Len J) . (k1 -' 1) <> 0 ) by A7, A221;
then k1 -' 1 = k2 -' 1 by A220, A214, A225, A227, A228, MATRIXJ1:11;
hence i1 = i2 by A215, A217, A209, A211, A227; :: thesis:

end;

suppose A229: ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) & i2 -' k2 < Sum ((Len J) | k2) ) ; :: thesis:

then A230: min ((Len J),(i2 -' k2)) = k2 by A57, A59, A205;
A231: ( F . (B . x2) = b1 . ((i2 -' k2) + 1) & (i2 -' k2) + 1 in dom b1 ) by A57, A59, A205, A229;
( F . (B . x1) = b1 . ((i1 -' k1) + 1) & (i1 -' k1) + 1 in dom b1 ) by A57, A59, A204, A229;
then A232: (i1 -' k1) + 1 = (i2 -' k2) + 1 by A206, A223, A231;
k1 -' 1 <> 0

proof

assume k1 -' 1 = 0 ; :: thesis:
then (Len J) | (k1 -' 1) = <*> REAL ;
hence contradiction by A29, A59, A205, A229, A232, RVSUM_1:72; :: thesis:

end;

then k1 -' 1 >= 1 by NAT_1:14;
then A233: k1 -' 1 in dom (Len J) by A220, FINSEQ_3:25;
then (Len J) . (k1 -' 1) <> 0 by A7, A221;
hence i1 = i2 by A229, A230, A232, A233, MATRIXJ1:6; :: thesis:

end;

suppose ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) & i2 -' k2 = Sum ((Len J) | k2) ) ; :: thesis:

then ( b1 . ((i1 -' k1) + 1) = 0. (im (F |^ 1)) & b1 . ((i1 -' k1) + 1) in rng b1 ) by A206, A207, A216, FUNCT_1:def 3, VECTSP_4:11;
hence i1 = i2 by A222, VECTSP_7:2; :: thesis:

end;

suppose A234: ( i2 -' k2 = Sum ((Len J) | (k2 -' 1)) & i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i1 -' k1 < Sum ((Len J) | k1) ) ; :: thesis:

then A235: min ((Len J),(i1 -' k1)) = k1 by A57, A59, A204;
A236: ( F . (B . x1) = b1 . ((i1 -' k1) + 1) & (i1 -' k1) + 1 in dom b1 ) by A57, A59, A204, A234;
( F . (B . x2) = b1 . ((i2 -' k2) + 1) & (i2 -' k2) + 1 in dom b1 ) by A57, A59, A205, A234;
then A237: (i2 -' k2) + 1 = (i1 -' k1) + 1 by A206, A223, A236;
k2 -' 1 <> 0

proof

assume k2 -' 1 = 0 ; :: thesis:
then i1 -' k1 = 0 by A234, A237, RVSUM_1:72;
hence contradiction by A29, A59, A204, A234; :: thesis:

end;

then k2 -' 1 >= 1 by NAT_1:14;
then A238: k2 -' 1 in dom (Len J) by A214, FINSEQ_3:25;
then (Len J) . (k2 -' 1) <> 0 by A7, A221;
hence i1 = i2 by A234, A235, A237, A238, MATRIXJ1:6; :: thesis:

end;

suppose ( i2 -' k2 = Sum ((Len J) | (k2 -' 1)) & i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i1 -' k1 = Sum ((Len J) | k1) ) ; :: thesis:

then ( b1 . ((i2 -' k2) + 1) = 0. (im (F |^ 1)) & b1 . ((i2 -' k2) + 1) in rng b1 ) by A206, A213, A218, FUNCT_1:def 3, VECTSP_4:11;
hence i1 = i2 by A222, VECTSP_7:2; :: thesis:

end;

suppose A239: ( i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) ) ; :: thesis:

then i2 -' k2 = i1 -' k1 by A206, A213, A216, A223;
then i2 - k1 = i1 - k1 by A57, A59, A205, A213, A209, A211, A239;
hence i1 = i2 ; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

then B is one-to-one ;
then B ^ f is one-to-one by A198, A200, FINSEQ_3:91;
then reconsider Bf = B ^ f as OrdBasis of V1 by A201, A203, MATRLIN:def 2;
for i being Nat holds
( not i in dom Bf or F . (Bf /. i) = (0. K) * (Bf /. i) or ( i + 1 in dom Bf & F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) )

proof

let i be Nat; :: thesis:
assume A240: i in dom Bf ; :: thesis:
A241: Bf /. i = Bf . i by A240, PARTFUN1:def 6;

per cases by A240, FINSEQ_1:25;

suppose A242: i in dom B ; :: thesis:

then r /. i = r . i by A30, A59, PARTFUN1:def 6;
then reconsider k = r . i as Element of NAT ;
A243: i -' k <= Sum ((Len J) | k) by A29, A59, A242;
A244: S₂[i,k] by A29, A59, A242;
then 1 <= k by FINSEQ_3:25;
then k -' 1 = k - 1 by XREAL_1:233;
then (k -' 1) + 1 = k ;
then (Len J) | k = ((Len J) | (k -' 1)) ^ <*((Len J) . k)*> by A244, FINSEQ_5:10;
then A245: ( dom (Len J) = dom J & Sum ((Len J) | k) = (Sum ((Len J) | (k -' 1))) + ((Len J) . k) ) by MATRIXJ1:def 3, RVSUM_1:74;

per cases by A243, XXREAL_0:1;

suppose A246: i -' k = Sum ((Len J) | k) ; :: thesis:

then A247: i -' k <> Sum ((Len J) | (k -' 1)) by A7, A244, A245;
F . (Bf /. i) = F . (B . i) by A241, A242, FINSEQ_1:def 7
.= 0. V1 by A57, A59, A242, A246, A247
.= (0. K) * (Bf /. i) by VECTSP_1:14 ;
hence ( F . (Bf /. i) = (0. K) * (Bf /. i) or ( i + 1 in dom Bf & F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) ) ; :: thesis:

end;

suppose A248: i -' k < Sum ((Len J) | k) ; :: thesis:

A249: ( i -' k = Sum ((Len J) | (k -' 1)) or i -' k <> Sum ((Len J) | (k -' 1)) ) ;
then A250: F . (B . i) = b1 . ((i -' k) + 1) by A57, A59, A242, A248;
dom J = dom (Len J) by MATRIXJ1:def 3;
then A251: k <= len J by A244, FINSEQ_3:25;
A252: (i -' k) + 1 <= Sum ((Len J) | k) by A248, NAT_1:13;
A253: i -' k = i - k by A244, XREAL_1:233;
A254: (i -' k) + 1 in dom b1 by A57, A59, A242, A248, A249;
then A255: 1 <= (i -' k) + 1 by FINSEQ_3:25;
then A256: 1 + 0 <= ((i - k) + 1) + k by A253, XREAL_1:7;
(i -' k) + 1 <= Sum (Len J) by A8, A254, FINSEQ_3:25;
then ((i - k) + 1) + k <= (Sum (Len J)) + (len J) by A251, A253, XREAL_1:7;
then A257: i + 1 in Seg ((Sum (Len J)) + (len J)) by A256;
then r /. (i + 1) = r . (i + 1) by A30, PARTFUN1:def 6;
then reconsider k1 = r . (i + 1) as Element of NAT ;
set i1 = i + 1;
A258: dom B c= dom Bf by FINSEQ_1:26;
1 + k <= ((i - k) + 1) + k by A255, A253, XREAL_1:7;
then A259: k <= i + 1 by NAT_1:13;
then A260: (i + 1) -' k = (i + 1) - k by XREAL_1:233;
Sum ((Len J) | (k -' 1)) <= (i -' k) + 1 by A244, NAT_1:12;
then A261: k <= k1 by A29, A244, A253, A257, A259, A260;
A262: S₂[i + 1,k1] by A29, A257;
A263: k = k1

proof

assume A264: k <> k1 ; :: thesis:
then A265: k < k1 by A261, XXREAL_0:1;
then reconsider K1 = k1 - 1 as Element of NAT by NAT_1:20;
A266: (i + 1) -' k1 <= (i + 1) -' k by A261, NAT_D:41;
(i + 1) - k1 = (i + 1) -' k1 by A262, XREAL_1:233;
then (i + 1) -' k1 <> (i + 1) -' k by A260, A264;
then A267: (i + 1) -' k1 < (i + 1) -' k by A266, XXREAL_0:1;
A268: k1 = K1 + 1 ;
then k <= K1 by A265, NAT_1:13;
then A269: Sum ((Len J) | k) <= Sum ((Len J) | K1) by POLYNOM3:18;
k1 -' 1 = K1 by A268, NAT_D:34;
then Sum ((Len J) | K1) <= (i + 1) -' k1 by A29, A257;
then Sum ((Len J) | k) <= (i + 1) -' k1 by A269, XXREAL_0:2;
hence contradiction by A252, A253, A260, A267, XXREAL_0:2; :: thesis:

end;

Sum ((Len J) | (k -' 1)) < (i -' k) + 1 by A244, NAT_1:13;
then B . (i + 1) = b1 . ((i -' k) + 1) by A57, A253, A257, A260, A263;
then Bf . (i + 1) = b1 . ((i -' k) + 1) by A59, A257, FINSEQ_1:def 7;
then Bf /. (i + 1) = b1 . ((i -' k) + 1) by A59, A257, A258, PARTFUN1:def 6;
then F . (Bf /. i) = Bf /. (i + 1) by A241, A242, A250, FINSEQ_1:def 7
.= (0. V1) + (Bf /. (i + 1)) by RLVECT_1:def 4
.= ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) by VECTSP_1:14 ;
hence ( F . (Bf /. i) = (0. K) * (Bf /. i) or ( i + 1 in dom Bf & F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) ) by A59, A257, A258; :: thesis:

end;

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

then consider j being Nat such that
A270: j in dom f and
A271: i = (len B) + j ;
A272: j <= len f by A270, FINSEQ_3:25;
F . (Bf /. i) = F . (f . j) by A241, A270, A271, FINSEQ_1:def 7
.= 0. V1 by A199, A202, A270, A272
.= (0. K) * (Bf /. i) by VECTSP_1:14 ;
hence ( F . (Bf /. i) = (0. K) * (Bf /. i) or ( i + 1 in dom Bf & F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) ) ; :: thesis:

end;

then consider J being non-empty FinSequence_of_Jordan_block of 0. K,K such that
A273: AutMt (F,Bf,Bf) = block_diagonal (J,(0. K)) by Th28;

now :: thesis:

A274: dom (Len J) = dom J by MATRIXJ1:def 3;
let i be Nat; :: thesis:
assume A275: i in dom J ; :: thesis:
J . i <> {} by A275, FUNCT_1:def 9;
hence (Len J) . i <> 0 by A275, A274, MATRIXJ1:def 3; :: thesis:

end;

hence ex J being FinSequence_of_Jordan_block of 0. K,K ex b1 being OrdBasis of V1 st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for i being Nat st i in dom J holds
(Len J) . i <> 0 ) ) by A273; :: thesis:

end;

A276: S₁[ 0 ]

proof

reconsider J = {} as FinSequence_of_Jordan_block of 0. K,K by Th10;
let V1 be finite-dimensional VectSp of K; :: thesis:
set b1 = the OrdBasis of V1;
let F be nilpotent linear-transformation of V1,V1; :: thesis:
assume deg F = 0 ; :: thesis:
then [#] V1 = {(0. V1)} by Th15
.= the carrier of ((0). V1) by VECTSP_4:def 3 ;
then (0). V1 = (Omega). V1 by VECTSP_4:29;
then A277: 0 = dim V1 by VECTSP_9:29
.= len the OrdBasis of V1 by MATRLIN2:21
.= len (AutMt (F, the OrdBasis of V1, the OrdBasis of V1)) by MATRIX_0:def 2 ;
take J ; :: thesis:
take the OrdBasis of V1 ; :: thesis:
thus AutMt (F, the OrdBasis of V1, the OrdBasis of V1) = {} by A277
.= block_diagonal (J,(0. K)) by MATRIXJ1:22 ; :: thesis:
thus for i being Nat st i in dom J holds
(Len J) . i <> 0 ; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A276, A1);
then S₁[ deg F] ;
then consider J being FinSequence_of_Jordan_block of 0. K,K, b1 being OrdBasis of V1 such that
A278: AutMt (F,b1,b1) = block_diagonal (J,(0. K)) and
A279: for i being Nat st i in dom J holds
(Len J) . i <> 0 ;

now :: thesis:

let x be object ; :: thesis:
assume A280: x in dom J ; :: thesis:
reconsider i = x as Element of NAT by A280;
( dom J = dom (Len J) & (Len J) . i <> 0 ) by A279, A280, MATRIXJ1:def 3;
then not J . i is empty by A280, MATRIXJ1:def 3;
hence not J . x is empty ; :: thesis:

end;

then J is non-empty ;
hence ex J being non-empty FinSequence_of_Jordan_block of 0. K,K ex b1 being OrdBasis of V1 st AutMt (F,b1,b1) = block_diagonal (J,(0. K)) by A278; :: thesis: