let k be Nat; :: thesis: for Y being non empty set
for f being sequence of Y holds rng (f ^\ k) = { (f . n) where n is Nat : k <= n }
let Y be non empty set ; :: thesis: for f being sequence of Y holds rng (f ^\ k) = { (f . n) where n is Nat : k <= n }
let f be sequence of Y; :: thesis: rng (f ^\ k) = { (f . n) where n is Nat : k <= n }
reconsider f1 = f ^\ k as sequence of Y ;
rng f1 = { (f . m) where m is Nat : k <= m }

proof

set Z = { (f . m) where m is Nat : k <= m } ;
A1: dom f1 = NAT by FUNCT_2:def 1;
A2: rng f1 c= { (f . m) where m is Nat : k <= m }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f1 or y in { (f . m) where m is Nat : k <= m } )
assume y in rng f1 ; :: thesis: y in { (f . m) where m is Nat : k <= m }
then consider m1 being object such that
A3: m1 in NAT and
A4: y = f1 . m1 by A1, FUNCT_1:def 3;
reconsider m1 = m1 as Element of NAT by A3;
y = f . (k + m1) by A4, NAT_1:def 3;
hence y in { (f . m) where m is Nat : k <= m } by Th1; :: thesis: verum

end;

{ (f . m) where m is Nat : k <= m } c= rng f1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . m) where m is Nat : k <= m } or x in rng f1 )
assume x in { (f . m) where m is Nat : k <= m } ; :: thesis: x in rng f1
then consider k1 being Nat such that
A5: x = f . k1 and
A6: k <= k1 ;
consider k2 being Nat such that
A7: k1 = k + k2 by A6, NAT_1:10;
( k2 in NAT & x = f1 . k2 ) by A5, A7, NAT_1:def 3, ORDINAL1:def 12;
hence x in rng f1 by FUNCT_2:4; :: thesis: verum

end;

hence rng f1 = { (f . m) where m is Nat : k <= m } by A2, XBOOLE_0:def 10; :: thesis: verum

end;

hence rng (f ^\ k) = { (f . n) where n is Nat : k <= n } ; :: thesis: verum