let k be Nat; :: thesis: for seq being ExtREAL_sequence holds

( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) )

let seq be ExtREAL_sequence; :: thesis: ( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) )

( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) )

let seq be ExtREAL_sequence; :: thesis: ( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) )

hereby :: thesis: ( seq is bounded_below implies seq ^\ k is bounded_below )

assume
seq is bounded_above
; :: thesis: seq ^\ k is bounded_above

then rng seq is bounded_above ;

then consider UB being Real such that

A1: UB is UpperBound of rng seq by XXREAL_2:def 10;

then rng (seq ^\ k) is bounded_above by XXREAL_2:def 10;

hence seq ^\ k is bounded_above ; :: thesis: verum

end;then rng seq is bounded_above ;

then consider UB being Real such that

A1: UB is UpperBound of rng seq by XXREAL_2:def 10;

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

r <= UB

then
UB is UpperBound of rng (seq ^\ k)
by XXREAL_2:def 1;r <= UB

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

assume r in rng (seq ^\ k) ; :: thesis: r <= UB

then consider n being object such that

A2: n in dom (seq ^\ k) and

A3: r = (seq ^\ k) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A2;

n + k in NAT by ORDINAL1:def 12;

then seq . (n + k) <= UB by A1, FUNCT_2:4, XXREAL_2:def 1;

hence r <= UB by A3, NAT_1:def 3; :: thesis: verum

end;assume r in rng (seq ^\ k) ; :: thesis: r <= UB

then consider n being object such that

A2: n in dom (seq ^\ k) and

A3: r = (seq ^\ k) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A2;

n + k in NAT by ORDINAL1:def 12;

then seq . (n + k) <= UB by A1, FUNCT_2:4, XXREAL_2:def 1;

hence r <= UB by A3, NAT_1:def 3; :: thesis: verum

then rng (seq ^\ k) is bounded_above by XXREAL_2:def 10;

hence seq ^\ k is bounded_above ; :: thesis: verum

hereby :: thesis: verum

assume
seq is bounded_below
; :: thesis: seq ^\ k is bounded_below

then rng seq is bounded_below ;

then consider UB being Real such that

A4: UB is LowerBound of rng seq by XXREAL_2:def 9;

then rng (seq ^\ k) is bounded_below by XXREAL_2:def 9;

hence seq ^\ k is bounded_below ; :: thesis: verum

end;then rng seq is bounded_below ;

then consider UB being Real such that

A4: UB is LowerBound of rng seq by XXREAL_2:def 9;

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

UB <= r

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

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

assume r in rng (seq ^\ k) ; :: thesis: UB <= r

then consider n being object such that

A5: n in dom (seq ^\ k) and

A6: r = (seq ^\ k) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A5;

n + k in NAT by ORDINAL1:def 12;

then seq . (n + k) in rng seq by FUNCT_2:4;

then UB <= seq . (n + k) by A4, XXREAL_2:def 2;

hence UB <= r by A6, NAT_1:def 3; :: thesis: verum

end;assume r in rng (seq ^\ k) ; :: thesis: UB <= r

then consider n being object such that

A5: n in dom (seq ^\ k) and

A6: r = (seq ^\ k) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A5;

n + k in NAT by ORDINAL1:def 12;

then seq . (n + k) in rng seq by FUNCT_2:4;

then UB <= seq . (n + k) by A4, XXREAL_2:def 2;

hence UB <= r by A6, NAT_1:def 3; :: thesis: verum

then rng (seq ^\ k) is bounded_below by XXREAL_2:def 9;

hence seq ^\ k is bounded_below ; :: thesis: verum