let i, j be Nat; :: thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
let f be linear-transformation of V1,V1; :: thesis: for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1
let v1 be Vector of V1; :: thesis: ( (f |^ i) . v1 = 0. V1 implies (f |^ (i + j)) . v1 = 0. V1 )
assume A1: (f |^ i) . v1 = 0. V1 ; :: thesis: (f |^ (i + j)) . v1 = 0. V1
A2: dom (f |^ i) = the carrier of V1 by FUNCT_2:def 1;
thus (f |^ (i + j)) . v1 = ((f |^ j) * (f |^ i)) . v1 by Th20
.= (f |^ j) . (0. V1) by A1, A2, FUNCT_1:13
.= 0. V1 by RANKNULL:9 ; :: thesis: verum