let k be Element of 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) ) )
assume A1: seq is non-decreasing ; :: thesis: ( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) )
set seq0 = seq ^\ k;

now

let n, m be Element of 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:8;
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 by Th7; :: thesis: sup seq = sup (seq ^\ k)

now

let y be ext-real number ; :: 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 set such that
A2: ( n in dom (seq ^\ k) & y = (seq ^\ k) . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A2;
(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 A2; :: thesis: verum

end;

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

now

let y be ext-real number ; :: 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 set such that
A4: ( n in dom seq & y = seq . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A4;
n <= n + k by NAT_1:11;
then A5: seq . n <= seq . (n + k) by A1, Th7;
(seq ^\ k) . n = seq . (n + k) by NAT_1:def 3;
then seq . (n + k) <= sup (seq ^\ k) by Th23;
hence y <= sup (rng (seq ^\ k)) by A4, A5, XXREAL_0:2; :: thesis: verum

end;

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