let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | (im ((f + (L * (id V1))) |^ n))) or y in the carrier of (im ((f + (L * (id V1))) |^ n)) )
assume y in rng (f | (im ((f + (L * (id V1))) |^ n))) ; :: thesis: y in the carrier of (im ((f + (L * (id V1))) |^ n))
then consider x being object such that
A1: x in dom (f | (im ((f + (L * (id V1))) |^ n))) and
A2: (f | (im ((f + (L * (id V1))) |^ n))) . x = y by FUNCT_1:def 3;
A3: x in the carrier of (im ((f + (L * (id V1))) |^ n)) by A1, FUNCT_2:def 1;
then A4: x in im ((f + (L * (id V1))) |^ n) ;
then x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 ;
A5: (f | (im ((f + (L * (id V1))) |^ n))) . v = f . v by A1, FUNCT_1:47;
dom fidI = the carrier of (im ((f + (L * (id V1))) |^ n)) by FUNCT_2:def 1;
then ( fidI . v = (f + (L * (id V1))) . v & fidI /. v = fidI . v ) by A3, FUNCT_1:47, PARTFUN1:def 6;
then A6: (f + (L * (id V1))) . v in im ((f + (L * (id V1))) |^ n) ;
(f + (L * (id V1))) . v = (f . v) + ((L * (id V1)) . v) by MATRLIN:def 3
.= (f . v) + (L * ((id V1) . v)) by MATRLIN:def 4
.= (f . v) + (L * v) ;
then A7: ((f + (L * (id V1))) . v) + ((- L) * v) = (f . v) + ((L * v) + ((- L) * v)) by RLVECT_1:def 3
.= (f . v) + ((L + (- L)) * v) by VECTSP_1:def 15
.= (f . v) + ((0. K) * v) by VECTSP_1:16
.= (f . v) + (0. V1) by VECTSP_1:14
.= f . v by RLVECT_1:def 4 ;
(- L) * v in im ((f + (L * (id V1))) |^ n) by A4, VECTSP_4:21;
then f . v in im ((f + (L * (id V1))) |^ n) by A7, A6, VECTSP_4:20;
hence y in the carrier of (im ((f + (L * (id V1))) |^ n)) by A2, A5; :: thesis: verum

end;

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; :: thesis: verum