let K be doubleLoopStr ; :: thesis: for V being non empty VectSpStr of K
for f being Function of V,V holds
( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )
let V be non empty VectSpStr of K; :: thesis: for f being Function of V,V holds
( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )
let f be Function of V,V; :: thesis: ( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )

hereby :: thesis: ( ex n being Nat st f |^ n = ZeroMap (V,V) implies f is nilpotent )

assume f is nilpotent ; :: thesis: ex n being Nat st f |^ n = ZeroMap (V,V)
then consider n being Nat such that
A1: for v being Vector of V holds (f |^ n) . v = 0. V by Def4;

now

let x be set ; :: thesis: ( x in dom (f |^ n) implies (f |^ n) . x = 0. V )
assume x in dom (f |^ n) ; :: thesis: (f |^ n) . x = 0. V
then reconsider v = x as Vector of V by FUNCT_2:def 1;
thus (f |^ n) . x = (f |^ n) . v
.= 0. V by A1 ; :: thesis: verum

end;

then f |^ n = (dom (f |^ n)) --> (0. V) by FUNCOP_1:17
.= the carrier of V --> (0. V) by FUNCT_2:def 1
.= ZeroMap (V,V) by GRCAT_1:def 12 ;
hence ex n being Nat st f |^ n = ZeroMap (V,V) ; :: thesis: verum

end;

given n being Nat such that A2: f |^ n = ZeroMap (V,V) ; :: thesis: f is nilpotent
take n ; :: according to MATRIXJ2:def 4 :: thesis: for v being Vector of V holds (f |^ n) . v = 0. V
let v be Vector of V; :: thesis: (f |^ n) . v = 0. V
thus (f |^ n) . v = ( the carrier of V --> (0. V)) . v by A2, GRCAT_1:def 12
.= 0. V by FUNCOP_1:13 ; :: thesis: verum