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

proof

C1: dom f1 = NAT by FUNCT_2:def 1;
set Z = { (f . m) where m is Element of NAT : k <= m } ;
C00: { (f . m) where m is Element of NAT : k <= m } c= rng f1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . m) where m is Element of NAT : k <= m } or x in rng f1 )
assume x in { (f . m) where m is Element of NAT : k <= m } ; :: thesis: x in rng f1
then consider k1 being Element of NAT such that
CC0: ( x = f . k1 & k <= k1 ) ;
consider k2 being Nat such that
CC1: k1 = k + k2 by CC0, NAT_1:10;
AA: k2 in NAT by ORDINAL1:def 13;
x = f1 . k2 by CC0, CC1, NAT_1:def 3;
hence x in rng f1 by AA, FUNCT_2:6; :: thesis: verum

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f1 or y in { (f . m) where m is Element of NAT : k <= m } )
assume y in rng f1 ; :: thesis: y in { (f . m) where m is Element of NAT : k <= m }
then consider m1 being set such that
DD1: ( m1 in NAT & y = f1 . m1 ) by C1, FUNCT_1:def 5;
reconsider m1 = m1 as Element of NAT by DD1;
y = f . (k + m1) by DD1, NAT_1:def 3;
hence y in { (f . m) where m is Element of NAT : k <= m } by Th5; :: thesis: verum

end;

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

end;

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