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

now :: thesis: for x being object st x in { (seq . m) where m is Nat : k <= m } holds
x in rng (seq ^\ k)

let x be object ; :: thesis: ( x in { (seq . m) where m is Nat : k <= m } implies x in rng (seq ^\ k) )
assume x in { (seq . m) where m is Nat : k <= m } ; :: thesis: x in rng (seq ^\ k)
then consider k1 being 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 Nat : k <= m } c= rng (seq ^\ k) ;
A5: dom (seq ^\ k) = NAT by FUNCT_2:def 1;

now :: thesis: for y being object st y in rng (seq ^\ k) holds
y in { (seq . m) where m is Nat : k <= m }

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

end;

then rng (seq ^\ k) c= { (seq . m) where m is Nat : k <= m } ;
hence rng (seq ^\ k) = { (seq . n) where n is Nat : k <= n } by A4; :: thesis: verum