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) )

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

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

( 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

hence
seq ^\ k is non-decreasing
; :: thesis: sup seq = sup (seq ^\ k)(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;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

now :: thesis: for y being ExtReal st y in rng seq holds

y <= sup (rng (seq ^\ k))

then
sup (rng (seq ^\ k)) is UpperBound of rng seq
by XXREAL_2:def 1;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;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

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)

then
sup (rng seq) is UpperBound of rng (seq ^\ k)
by XXREAL_2:def 1;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;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

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