let k be Nat; :: thesis: for seq being ExtREAL_sequence st seq is non-increasing holds

( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )

let seq be ExtREAL_sequence; :: thesis: ( seq is non-increasing implies ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) ) )

set seq0 = seq ^\ k;

assume A1: seq is non-increasing ; :: thesis: ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )

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

then inf (rng seq) <= inf (rng (seq ^\ k)) by XXREAL_2:def 4;

hence inf seq = inf (seq ^\ k) by A5, XXREAL_0:1; :: thesis: verum

( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )

let seq be ExtREAL_sequence; :: thesis: ( seq is non-increasing implies ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) ) )

set seq0 = seq ^\ k;

assume A1: seq is non-increasing ; :: thesis: ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )

now :: thesis: for n, m being Nat st m <= n holds

(seq ^\ k) . n <= (seq ^\ k) . m

hence
seq ^\ k is non-increasing
; :: thesis: inf seq = inf (seq ^\ k)(seq ^\ k) . n <= (seq ^\ k) . m

let n, m be Nat; :: thesis: ( m <= n implies (seq ^\ k) . n <= (seq ^\ k) . m )

assume m <= n ; :: thesis: (seq ^\ k) . n <= (seq ^\ k) . m

then k + m <= k + n by XREAL_1:6;

then seq . (k + n) <= seq . (k + m) by A1, Th7;

then (seq ^\ k) . n <= seq . (k + m) by NAT_1:def 3;

hence (seq ^\ k) . n <= (seq ^\ k) . m by NAT_1:def 3; :: thesis: verum

end;assume m <= n ; :: thesis: (seq ^\ k) . n <= (seq ^\ k) . m

then k + m <= k + n by XREAL_1:6;

then seq . (k + n) <= seq . (k + m) by A1, Th7;

then (seq ^\ k) . n <= seq . (k + m) by NAT_1:def 3;

hence (seq ^\ k) . n <= (seq ^\ k) . m by NAT_1:def 3; :: thesis: verum

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

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

then
inf (rng (seq ^\ k)) is LowerBound of rng seq
by XXREAL_2:def 2;inf (rng (seq ^\ k)) <= y

let y be ExtReal; :: thesis: ( y in rng seq implies inf (rng (seq ^\ k)) <= y )

assume y in rng seq ; :: thesis: inf (rng (seq ^\ k)) <= y

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: inf (seq ^\ k) <= seq . (n + k) by Th23;

n <= n + k by NAT_1:11;

then seq . (n + k) <= seq . n by A1, Th7;

hence inf (rng (seq ^\ k)) <= y by A3, A4, XXREAL_0:2; :: thesis: verum

end;assume y in rng seq ; :: thesis: inf (rng (seq ^\ k)) <= y

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: inf (seq ^\ k) <= seq . (n + k) by Th23;

n <= n + k by NAT_1:11;

then seq . (n + k) <= seq . n by A1, Th7;

hence inf (rng (seq ^\ k)) <= y by A3, A4, XXREAL_0:2; :: thesis: verum

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

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

inf (rng seq) <= y

then
inf (rng seq) is LowerBound of rng (seq ^\ k)
by XXREAL_2:def 2;inf (rng seq) <= y

let y be ExtReal; :: thesis: ( y in rng (seq ^\ k) implies inf (rng seq) <= y )

assume y in rng (seq ^\ k) ; :: thesis: inf (rng seq) <= y

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 inf seq <= (seq ^\ k) . n by Th23;

hence inf (rng seq) <= y by A7; :: thesis: verum

end;assume y in rng (seq ^\ k) ; :: thesis: inf (rng seq) <= y

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 inf seq <= (seq ^\ k) . n by Th23;

hence inf (rng seq) <= y by A7; :: thesis: verum

then inf (rng seq) <= inf (rng (seq ^\ k)) by XXREAL_2:def 4;

hence inf seq = inf (seq ^\ k) by A5, XXREAL_0:1; :: thesis: verum