let K be Field; :: thesis: for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V ex n being Nat st UnionKers f = ker (f |^ n)
let V be finite-dimensional VectSp of K; :: thesis: for f being linear-transformation of V,V ex n being Nat st UnionKers f = ker (f |^ n)
let f be linear-transformation of V,V; :: thesis: ex n being Nat st UnionKers f = ker (f |^ n)
defpred S₁[ Nat] means for n being Nat holds dim (ker (f |^ n)) <= $1;
S₁[ dim (UnionKers f)]

proof

let n be Nat; :: thesis: dim (ker (f |^ n)) <= dim (UnionKers f)
ker (f |^ n) is Subspace of UnionKers f by Th25;
hence dim (ker (f |^ n)) <= dim (UnionKers f) by VECTSP_9:25; :: thesis: verum

end;

then A1: ex k being Nat st S₁[k] ;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A1);
then consider k being Nat such that
A2: S₁[k] and
A3: for n being Nat st S₁[n] holds
k <= n ;
ex m being Nat st dim (ker (f |^ m)) = k

proof

assume A4: for m being Nat holds dim (ker (f |^ m)) <> k ; :: thesis: contradiction
dim (ker (f |^ 0)) <= k by A2;
then dim (ker (f |^ 0)) < k by A4, XXREAL_0:1;
then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;

now :: thesis: for n being Nat holds dim (ker (f |^ n)) <= k1

let n be Nat; :: thesis: dim (ker (f |^ n)) <= k1
dim (ker (f |^ n)) <= k by A2;
then dim (ker (f |^ n)) < k1 + 1 by A4, XXREAL_0:1;
hence dim (ker (f |^ n)) <= k1 by NAT_1:13; :: thesis: verum

end;

then k1 + 1 <= k1 by A3;
hence contradiction by NAT_1:16; :: thesis: verum

end;

then consider m being Nat such that
A5: dim (ker (f |^ m)) = k ;
take m ; :: thesis: UnionKers f = ker (f |^ m)
assume A6: UnionKers f <> ker (f |^ m) ; :: thesis: contradiction
ker (f |^ m) is Subspace of UnionKers f by Th25;
then consider v being Element of (UnionKers f) such that
A7: not v in ker (f |^ m) by A6, VECTSP_4:32;
A8: v in UnionKers f ;
reconsider v = v as Vector of V by VECTSP_4:10;
consider i being Nat such that
A9: (f |^ i) . v = 0. V by A8, Th24;
i > m

proof

assume i <= m ; :: thesis: contradiction
then reconsider j = m - i as Element of NAT by NAT_1:21;
(f |^ (j + i)) . v = 0. V by A9, Th23;
hence contradiction by A7, RANKNULL:10; :: thesis: verum

end;

then reconsider j = i - m as Element of NAT by NAT_1:21;
A10: ker (f |^ m) is Subspace of ker (f |^ (m + j)) by Th26;
then A11: k <= dim (ker (f |^ i)) by A5, VECTSP_9:25;
(Omega). (ker (f |^ m)) <> (Omega). (ker (f |^ i)) by A7, A9, RANKNULL:10;
then k <> dim (ker (f |^ i)) by A5, A10, VECTSP_9:28;
then k < dim (ker (f |^ i)) by A11, XXREAL_0:1;
hence contradiction by A2; :: thesis: verum