theorem Th16: :: MATRIXJ2:16

for K being doubleLoopStr
for V being non empty ModuleStr over K
for f being nilpotent Function of V,V ex v being Vector of V st
for i being Nat st i < deg f holds
(f |^ i) . v <> 0. V