let n be Nat; :: thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
let f be linear-transformation of V1,V1; :: thesis: f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))
set IM = im (f |^ n);
rng (f | (im (f |^ n))) c= the carrier of (im (f |^ n))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | (im (f |^ n))) or y in the carrier of (im (f |^ n)) )
assume y in rng (f | (im (f |^ n))) ; :: thesis: y in the carrier of (im (f |^ n))
then consider x being object such that
A1: x in dom (f | (im (f |^ n))) and
A2: (f | (im (f |^ n))) . x = y by FUNCT_1:def 3;
x in the carrier of (im (f |^ n)) by A1, FUNCT_2:def 1;
then A3: x in im (f |^ n) ;
then x in V1 by VECTSP_4:9;
then reconsider v = x as Vector of V1 ;
consider w being Vector of V1 such that
A4: (f |^ n) . w = v by A3, RANKNULL:13;
A5: the carrier of V1 = dom (f |^ 1) by FUNCT_2:def 1;
A6: the carrier of V1 = dom (f |^ n) by FUNCT_2:def 1;
y = f . x by A1, A2, FUNCT_1:47
.= (f * (f |^ n)) . w by A4, A6, FUNCT_1:13
.= ((f |^ 1) * (f |^ n)) . w by Th19
.= (f |^ (1 + n)) . w by Th20
.= ((f |^ n) * (f |^ 1)) . w by Th20
.= (f |^ n) . ((f |^ 1) . w) by A5, FUNCT_1:13 ;
then y in im (f |^ n) by RANKNULL:13;
hence y in the carrier of (im (f |^ n)) ; :: thesis: verum

end;

hence f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n)) by Lm1, FUNCT_2:6; :: thesis: verum