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 UpperBound of rng seq such that
A1: UB in REAL by SUPINF_1:def 11;

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) & r = (seq ^\ k) . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A2;
seq . (n + k) <= UB by FUNCT_2:6, XXREAL_2:def 1;
hence r <= UB by A2, 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 A1, SUPINF_1:def 11;
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 LowerBound of rng seq such that
A3: UB in REAL by SUPINF_1:def 12;

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
A4: ( n in dom (seq ^\ k) & r = (seq ^\ k) . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A4;
UB <= seq . (n + k) by FUNCT_2:6, XXREAL_2:def 2;
hence UB <= r by A4, 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 A3, SUPINF_1:def 12;
hence seq ^\ k is bounded_below by Def3; :: thesis: verum

end;