let K be Field; :: thesis: for V being VectSp of K
for W being Subspace of V
for f being nilpotent Function of V,V st f | W is Function of W,W holds
f | W is nilpotent Function of W,W
let V be VectSp of K; :: thesis: for W being Subspace of V
for f being nilpotent Function of V,V st f | W is Function of W,W holds
f | W is nilpotent Function of W,W
let W be Subspace of V; :: thesis: for f being nilpotent Function of V,V st f | W is Function of W,W holds
f | W is nilpotent Function of W,W
let f be nilpotent Function of V,V; :: thesis: ( f | W is Function of W,W implies f | W is nilpotent Function of W,W )
assume f | W is Function of W,W ; :: thesis: f | W is nilpotent Function of W,W
then reconsider fW = f | W as Function of W,W ;
consider n being Nat such that
A1: f |^ n = ZeroMap (V,V) by Th13;
[#] W c= [#] V by VECTSP_4:def 2;
then A2: [#] W = ([#] V) /\ ([#] W) by XBOOLE_1:28;
fW |^ n = (ZeroMap (V,V)) | W by A1, VECTSP11:22
.= ( the carrier of V --> (0. V)) | ([#] W) by GRCAT_1:def 7
.= ( the carrier of V /\ ([#] W)) --> (0. V) by FUNCOP_1:12
.= the carrier of W --> (0. W) by A2, VECTSP_4:11
.= ZeroMap (W,W) by GRCAT_1:def 7 ;
hence f | W is nilpotent Function of W,W by Th13; :: thesis: verum