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:29; :: 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] & ( for n being Nat st S₁[n] holds
k <= n ) ) ;
ex m being Nat st dim (ker (f |^ m)) = k

proof

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

now

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

end;

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

end;

then consider m being Nat such that
A4: dim (ker (f |^ m)) = k ;
take m ; :: thesis: UnionKers f = ker (f |^ m)
A5: ker (f |^ m) is Subspace of UnionKers f by Th25;
assume UnionKers f <> ker (f |^ m) ; :: thesis: contradiction
then consider v being Element of (UnionKers f) such that
A6: not v in ker (f |^ m) by A5, VECTSP_4:40;
A7: v in UnionKers f by STRUCT_0:def 5;
reconsider v = v as Vector of V by VECTSP_4:18;
consider i being Nat such that
A8: (f |^ i) . v = 0. V by A7, 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 A8, Th23;
hence contradiction by A6, RANKNULL:10; :: thesis: verum

end;

then reconsider j = i - m as Element of NAT by NAT_1:21;
A9: ker (f |^ m) is Subspace of ker (f |^ (m + j)) by Th26;
(Omega). (ker (f |^ m)) <> (Omega). (ker (f |^ i)) by A6, A8, RANKNULL:10;
then ( k <> dim (ker (f |^ i)) & k <= dim (ker (f |^ i)) ) by A4, A9, VECTSP_9:29, VECTSP_9:32;
then k < dim (ker (f |^ i)) by XXREAL_0:1;
hence contradiction by A2; :: thesis: verum