let k be Element of NAT ; :: thesis: for seq being Real_Sequence holds rng (seq ^\ k) = { (seq . n) where n is Element of NAT : k <= n }
let seq be Real_Sequence; :: thesis: rng (seq ^\ k) = { (seq . n) where n is Element of NAT : k <= n }
set seq1 = seq ^\ k;
set Z = { (seq . m) where m is Element of NAT : k <= m } ;

now

let x be set ; :: thesis: ( x in { (seq . m) where m is Element of NAT : k <= m } implies x in rng (seq ^\ k) )
assume x in { (seq . m) where m is Element of NAT : k <= m } ; :: thesis: x in rng (seq ^\ k)
then consider k1 being Element of NAT such that
A1: x = seq . k1 and
A2: k <= k1 ;
consider k2 being Nat such that
A3: k1 = k + k2 by A2, NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 12;
x = (seq ^\ k) . k2 by A1, A3, NAT_1:def 3;
hence x in rng (seq ^\ k) by FUNCT_2:4; :: thesis: verum

end;

then A4: { (seq . m) where m is Element of NAT : k <= m } c= rng (seq ^\ k) by TARSKI:def 3;
A5: dom (seq ^\ k) = NAT by FUNCT_2:def 1;

now

let y be set ; :: thesis: ( y in rng (seq ^\ k) implies y in { (seq . m) where m is Element of NAT : k <= m } )
assume y in rng (seq ^\ k) ; :: thesis: y in { (seq . m) where m is Element of NAT : k <= m }
then consider m1 being set such that
A6: m1 in NAT and
A7: y = (seq ^\ k) . m1 by A5, FUNCT_1:def 3;
reconsider m1 = m1 as Element of NAT by A6;
y = seq . (k + m1) by A7, NAT_1:def 3;
hence y in { (seq . m) where m is Element of NAT : k <= m } by SETLIM_1:1; :: thesis: verum

end;

then rng (seq ^\ k) c= { (seq . m) where m is Element of NAT : k <= m } by TARSKI:def 3;
hence rng (seq ^\ k) = { (seq . n) where n is Element of NAT : k <= n } by A4, XBOOLE_0:def 10; :: thesis: verum