let n be Nat; :: thesis: for K being Field
for V being VectSp of K
for W being Subspace of V
for f being nilpotent linear-transformation of V,V
for fI being nilpotent Function of (im (f |^ n)),(im (f |^ n)) st fI = f | (im (f |^ n)) & n <= deg f holds
(deg fI) + n = deg f
let K be Field; :: thesis: for V being VectSp of K
for W being Subspace of V
for f being nilpotent linear-transformation of V,V
for fI being nilpotent Function of (im (f |^ n)),(im (f |^ n)) st fI = f | (im (f |^ n)) & n <= deg f holds
(deg fI) + n = deg f
let V be VectSp of K; :: thesis: for W being Subspace of V
for f being nilpotent linear-transformation of V,V
for fI being nilpotent Function of (im (f |^ n)),(im (f |^ n)) st fI = f | (im (f |^ n)) & n <= deg f holds
(deg fI) + n = deg f
let W be Subspace of V; :: thesis: for f being nilpotent linear-transformation of V,V
for fI being nilpotent Function of (im (f |^ n)),(im (f |^ n)) st fI = f | (im (f |^ n)) & n <= deg f holds
(deg fI) + n = deg f
let f be nilpotent linear-transformation of V,V; :: thesis: for fI being nilpotent Function of (im (f |^ n)),(im (f |^ n)) st fI = f | (im (f |^ n)) & n <= deg f holds
(deg fI) + n = deg f
set IM = im (f |^ n);
let fI be nilpotent Function of (im (f |^ n)),(im (f |^ n)); :: thesis: ( fI = f | (im (f |^ n)) & n <= deg f implies (deg fI) + n = deg f )
assume A1: fI = f | (im (f |^ n)) ; :: thesis: ( not n <= deg f or (deg fI) + n = deg f )
set D = deg f;
assume n <= deg f ; :: thesis: (deg fI) + n = deg f
then reconsider Dn = (deg f) - n as Element of NAT by NAT_1:21;

A2: now :: thesis: for x being object st x in dom (fI |^ Dn) holds
0. (im (f |^ n)) = (fI |^ Dn) . x

let x be object ; :: thesis: ( x in dom (fI |^ Dn) implies 0. (im (f |^ n)) = (fI |^ Dn) . x )
assume x in dom (fI |^ Dn) ; :: thesis: 0. (im (f |^ n)) = (fI |^ Dn) . x
then reconsider X = x as Vector of (im (f |^ n)) by FUNCT_2:def 1;
reconsider v = X as Vector of V by VECTSP_4:10;
A3: dom (f |^ n) = the carrier of V by FUNCT_2:def 1;
X in im (f |^ n) ;
then consider w being Element of V such that
A4: v = (f |^ n) . w by RANKNULL:13;
(f |^ (deg f)) . w = (ZeroMap (V,V)) . w by Def5
.= ( the carrier of V --> (0. V)) . w by GRCAT_1:def 7
.= 0. V ;
hence 0. (im (f |^ n)) = (f |^ (Dn + n)) . w by VECTSP_4:11
.= ((f |^ Dn) * (f |^ n)) . w by VECTSP11:20
.= (f |^ Dn) . v by A4, A3, FUNCT_1:13
.= ((f |^ Dn) | (im (f |^ n))) . X by FUNCT_1:49
.= (fI |^ Dn) . x by A1, VECTSP11:22 ;
:: thesis: verum

end;

dom (fI |^ Dn) = [#] (im (f |^ n)) by FUNCT_2:def 1;
then fI |^ Dn = the carrier of (im (f |^ n)) --> (0. (im (f |^ n))) by A2, FUNCOP_1:11
.= ZeroMap ((im (f |^ n)),(im (f |^ n))) by GRCAT_1:def 7 ;
then A5: deg fI <= Dn by Def5;
deg fI = Dn

proof

set DI = deg fI;
A6: dom (f |^ n) = the carrier of V by FUNCT_2:def 1;
assume deg fI <> Dn ; :: thesis: contradiction
then deg fI < Dn by A5, XXREAL_0:1;
then A7: (deg fI) + n < Dn + n by XREAL_1:6;
consider v being Vector of V such that
A8: for i being Nat st i < deg f holds
(f |^ i) . v <> 0. V by Th16;
(f |^ n) . v in im (f |^ n) by RANKNULL:13;
then A9: (f |^ n) . v in the carrier of (im (f |^ n)) ;
fI |^ (deg fI) = ZeroMap ((im (f |^ n)),(im (f |^ n))) by Def5
.= the carrier of (im (f |^ n)) --> (0. (im (f |^ n))) by GRCAT_1:def 7 ;
then 0. (im (f |^ n)) = (fI |^ (deg fI)) . ((f |^ n) . v) by A9, FUNCOP_1:7
.= ((f |^ (deg fI)) | (im (f |^ n))) . ((f |^ n) . v) by A1, VECTSP11:22
.= (f |^ (deg fI)) . ((f |^ n) . v) by A9, FUNCT_1:49
.= ((f |^ (deg fI)) * (f |^ n)) . v by A6, FUNCT_1:13
.= (f |^ ((deg fI) + n)) . v by VECTSP11:20 ;
hence contradiction by A7, A8, VECTSP_4:11; :: thesis: verum

end;

hence (deg fI) + n = deg f ; :: thesis: verum