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 ) )
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;
now :: thesis: for r being ExtReal st r in rng (seq ^\ k) holds
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;
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 ; :: thesis: verum
end;
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;
now :: thesis: for r being ExtReal st r in rng (seq ^\ k) holds
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;
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 ; :: thesis: verum
end;