let n be 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))
let K be 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))
let V1 be 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))
let f be 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))
let L be Scalar of K; f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))
set fid = f + (L * (id V1));
set IM = im ((f + (L * (id V1))) |^ n);
reconsider fidI = (f + (L * (id V1))) | (im ((f + (L * (id V1))) |^ n)) as linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n)) by Th32;
rng (f | (im ((f + (L * (id V1))) |^ n))) c= the carrier of (im ((f + (L * (id V1))) |^ n))
hence
f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))
by Lm1, FUNCT_2:6; verum