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 A1: F is without-infty ; :: thesis: F | k is without-infty

now :: thesis: not -infty in rng (F | k)

assume -infty in rng (F | k) ; :: thesis: contradiction
then consider i being Element of NAT such that
A2: ( i in dom (F | k) & -infty = (F | k) . i ) by PARTFUN1:3;
dom (F | k) c= dom F by RELAT_1:60;
then ( i in dom F & (F | k) . i = F . i ) by A2, FUNCT_1:47;
then -infty in rng F by A2, FUNCT_1:3;
hence contradiction by A1, MESFUNC5:def 3; :: thesis: verum

end;

hence F | k is without-infty by MESFUNC5:def 3; :: thesis: verum

end;

assume A3: F is without+infty ; :: thesis: F | k is without+infty

now :: thesis: not +infty in rng (F | k)

assume +infty in rng (F | k) ; :: thesis: contradiction
then consider i being Element of NAT such that
A4: ( i in dom (F | k) & +infty = (F | k) . i ) by PARTFUN1:3;
dom (F | k) c= dom F by RELAT_1:60;
then ( i in dom F & (F | k) . i = F . i ) by A4, FUNCT_1:47;
then +infty in rng F by A4, FUNCT_1:3;
hence contradiction by A3, MESFUNC5:def 4; :: thesis: verum

end;

hence F | k is without+infty by MESFUNC5:def 4; :: thesis: verum