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