let k be Nat; :: thesis: for seq being ExtREAL_sequence st seq is non-decreasing holds
( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) )
let seq be ExtREAL_sequence; :: thesis: ( seq is non-decreasing implies ( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) ) )
set seq0 = seq ^\ k;
assume A1: seq is non-decreasing ; :: thesis: ( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) )

now :: thesis: for n, m being Nat st m <= n holds
(seq ^\ k) . m <= (seq ^\ k) . n

let n, m be Nat; :: thesis: ( m <= n implies (seq ^\ k) . m <= (seq ^\ k) . n )
assume m <= n ; :: thesis: (seq ^\ k) . m <= (seq ^\ k) . n
then k + m <= k + n by XREAL_1:6;
then seq . (k + m) <= seq . (k + n) by A1, Th7;
then (seq ^\ k) . m <= seq . (k + n) by NAT_1:def 3;
hence (seq ^\ k) . m <= (seq ^\ k) . n by NAT_1:def 3; :: thesis: verum

end;

hence seq ^\ k is non-decreasing ; :: thesis: sup seq = sup (seq ^\ k)

now :: thesis: for y being ExtReal st y in rng seq holds
y <= sup (rng (seq ^\ k))

let y be ExtReal; :: thesis: ( y in rng seq implies y <= sup (rng (seq ^\ k)) )
assume y in rng seq ; :: thesis: y <= sup (rng (seq ^\ k))
then consider n being object such that
A2: n in dom seq and
A3: y = seq . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A2;
(seq ^\ k) . n = seq . (n + k) by NAT_1:def 3;
then A4: seq . (n + k) <= sup (seq ^\ k) by Th23;
n <= n + k by NAT_1:11;
then seq . n <= seq . (n + k) by A1, Th7;
hence y <= sup (rng (seq ^\ k)) by A3, A4, XXREAL_0:2; :: thesis: verum

end;

then sup (rng (seq ^\ k)) is UpperBound of rng seq by XXREAL_2:def 1;
then A5: sup (rng seq) <= sup (rng (seq ^\ k)) by XXREAL_2:def 3;

now :: thesis: for y being ExtReal st y in rng (seq ^\ k) holds
y <= sup (rng seq)

let y be ExtReal; :: thesis: ( y in rng (seq ^\ k) implies y <= sup (rng seq) )
assume y in rng (seq ^\ k) ; :: thesis: y <= sup (rng seq)
then consider n being object such that
A6: n in dom (seq ^\ k) and
A7: y = (seq ^\ k) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A6;
(seq ^\ k) . n = seq . (n + k) by NAT_1:def 3;
then (seq ^\ k) . n <= sup seq by Th23;
hence y <= sup (rng seq) by A7; :: thesis: verum

end;

then sup (rng seq) is UpperBound of rng (seq ^\ k) by XXREAL_2:def 1;
then sup (rng (seq ^\ k)) <= sup (rng seq) by XXREAL_2:def 3;
hence sup seq = sup (seq ^\ k) by A5, XXREAL_0:1; :: thesis: verum