theorem :: VECTSP11:33
for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))