let F be FinSequence of ExtREAL ; :: thesis: for k being Nat holds
( ( F is without-infty implies F /^ k is without-infty ) & ( F is without+infty implies F /^ k is without+infty ) )
let k be Nat; :: thesis: ( ( F is without-infty implies F /^ k is without-infty ) & ( F is without+infty implies F /^ k is without+infty ) )

hereby :: thesis: ( F is without+infty implies F /^ k is without+infty )

assume F is without-infty ; :: thesis: F /^ k is without-infty
then A1: not -infty in rng F by MESFUNC5:def 3;
rng (F /^ k) c= rng F by FINSEQ_5:33;
hence F /^ k is without-infty by A1, MESFUNC5:def 3; :: thesis: verum

end;

assume F is without+infty ; :: thesis: F /^ k is without+infty
then A2: not +infty in rng F by MESFUNC5:def 4;
rng (F /^ k) c= rng F by FINSEQ_5:33;
hence F /^ k is without+infty by A2, MESFUNC5:def 4; :: thesis: verum