let n be Nat; :: thesis:
let seq be ExtREAL_sequence; :: thesis:
set rseq = seq ^\ n;
A1: ex Z being non empty Subset of ExtREAL st
( Z = { (seq . k) where k is Nat : n <= k } & (inferior_realsequence seq) . n = inf Z ) by Def6;

let x be object ; :: thesis:
assume x in { (seq . k) where k is Nat : n <= k } ; :: thesis:
then consider k being Nat such that
A2: x = seq . k and
A3: n <= k ;
reconsider k1 = k - n as Element of NAT by A3, INT_1:5;
x = seq . (n + k1) by A2;
then x = (seq ^\ n) . k1 by NAT_1:def 3;
hence x in rng (seq ^\ n) by FUNCT_2:4; :: thesis:

end;

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

let x be object ; :: thesis:
assume x in rng (seq ^\ n) ; :: thesis:
then consider z being object such that
A5: z in dom (seq ^\ n) and
A6: x = (seq ^\ n) . z by FUNCT_1:def 3;
reconsider k0 = z as Element of NAT by A5;
A7: n <= n + k0 by NAT_1:11;
x = seq . (n + k0) by A6, NAT_1:def 3;
hence x in { (seq . k) where k is Nat : n <= k } by A7; :: thesis:

end;

then A8: rng (seq ^\ n) c= { (seq . k) where k is Nat : n <= k } ;
ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : n <= k } & (superior_realsequence seq) . n = sup Y ) by Def7;
hence ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) ) by A1, A4, A8, XBOOLE_0:def 10; :: thesis: