let seq be ExtREAL_sequence; :: thesis:
let j be Element of NAT ; :: thesis:
set rseq = seq ^\ j;

let n be Element of NAT ; :: thesis:
A1: ex Y2 being non empty Subset of ExtREAL st
( Y2 = { ((seq ^\ j) . k) where k is Nat : n <= k } & (superior_realsequence (seq ^\ j)) . n = sup Y2 ) by Def7;
A2: ex Y3 being non empty Subset of ExtREAL st
( Y3 = { (seq . k) where k is Nat : j + n <= k } & (superior_realsequence seq) . (j + n) = sup Y3 ) by Def7;

let x be object ; :: thesis:
assume x in { (seq . k) where k is Nat : j + n <= k } ; :: thesis:
then consider k being Nat such that
A3: x = seq . k and
A4: j + n <= k ;
j <= j + n by NAT_1:11;
then reconsider k1 = k - j as Element of NAT by A4, INT_1:5, XXREAL_0:2;
A5: x = seq . (j + k1) by A3;
(j + n) - j <= k - j by A4, XREAL_1:9;
hence x in { (seq . (j + k2)) where k2 is Nat : n <= k2 } by A5; :: thesis:

end;

then A6: { (seq . k) where k is Nat : j + n <= k } c= { (seq . (j + k)) where k is Nat : n <= k } ;

let x be object ; :: thesis:
assume x in { (seq . (j + k)) where k is Nat : n <= k } ; :: thesis:
then consider k being Nat such that
A7: x = seq . (j + k) and
A8: n <= k ;
j + n <= j + k by A8, XREAL_1:6;
hence x in { (seq . k1) where k1 is Nat : j + n <= k1 } by A7; :: thesis:

end;

then { (seq . (j + k)) where k is Nat : n <= k } c= { (seq . k) where k is Nat : j + n <= k } ;
then A9: { (seq . (j + k)) where k is Nat : n <= k } = { (seq . k) where k is Nat : j + n <= k } by A6, XBOOLE_0:def 10;

let x be object ; :: thesis:
assume x in { (seq . (j + k)) where k is Nat : n <= k } ; :: thesis:
then consider k being Nat such that
A10: x = seq . (j + k) and
A11: n <= k ;
x = (seq ^\ j) . k by A10, NAT_1:def 3;
hence x in { ((seq ^\ j) . k1) where k1 is Nat : n <= k1 } by A11; :: thesis:

end;

then A12: { (seq . (j + k)) where k is Nat : n <= k } c= { ((seq ^\ j) . k) where k is Nat : n <= k } ;

let x be object ; :: thesis:
assume x in { ((seq ^\ j) . k) where k is Nat : n <= k } ; :: thesis:
then consider k being Nat such that
A13: x = (seq ^\ j) . k and
A14: n <= k ;
x = seq . (j + k) by A13, NAT_1:def 3;
hence x in { (seq . (j + k1)) where k1 is Nat : n <= k1 } by A14; :: thesis:

end;

then { ((seq ^\ j) . k) where k is Nat : n <= k } c= { (seq . (j + k)) where k is Nat : n <= k } ;
then { ((seq ^\ j) . k) where k is Nat : n <= k } = { (seq . (j + k)) where k is Nat : n <= k } by A12, XBOOLE_0:def 10;
hence (superior_realsequence (seq ^\ j)) . n = ((superior_realsequence seq) ^\ j) . n by A1, A2, A9, NAT_1:def 3; :: thesis:

end;