theorem Th13: :: MATRIXJ2:13

for K being doubleLoopStr
for V being non empty ModuleStr over K
for f being Function of V,V holds
( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )