let k be Element of 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 ) )

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 by Def4;
then consider UB being real number such that
A1: UB is UpperBound of rng seq by XXREAL_2:def 10;

now

let r be ext-real number ; :: thesis: ( r in rng (seq ^\ k) implies r <= UB )
assume r in rng (seq ^\ k) ; :: thesis: r <= UB
then consider n being set such that
A2: n in dom (seq ^\ k) and
A3: r = (seq ^\ k) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A2;
seq . (n + k) <= UB by A1, FUNCT_2:6, XXREAL_2:def 1;
hence r <= UB by A3, NAT_1:def 3; :: thesis: verum

end;

then UB is UpperBound of rng (seq ^\ k) by XXREAL_2:def 1;
then rng (seq ^\ k) is bounded_above by XXREAL_2:def 10;
hence seq ^\ k is bounded_above by Def4; :: thesis: verum

end;

hereby :: thesis: verum

assume seq is bounded_below ; :: thesis: seq ^\ k is bounded_below
then rng seq is bounded_below by Def3;
then consider UB being real number such that
A4: UB is LowerBound of rng seq by XXREAL_2:def 9;

now

let r be ext-real number ; :: thesis: ( r in rng (seq ^\ k) implies UB <= r )
assume r in rng (seq ^\ k) ; :: thesis: UB <= r
then consider n being set such that
A5: n in dom (seq ^\ k) and
A6: r = (seq ^\ k) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A5;
seq . (n + k) in rng seq by FUNCT_2:6;
then UB <= seq . (n + k) by A4, XXREAL_2:def 2;
hence UB <= r by A6, NAT_1:def 3; :: thesis: verum

end;

then UB is LowerBound of rng (seq ^\ k) by XXREAL_2:def 2;
then rng (seq ^\ k) is bounded_below by XXREAL_2:def 9;
hence seq ^\ k is bounded_below by Def3; :: thesis: verum

end;