let F be FinSequence of ExtREAL ; :: thesis: for k being Nat holds
( ( F is V339() implies F /^ k is V339() ) & ( F is V340() implies F /^ k is V340() ) )
let k be Nat; :: thesis: ( ( F is V339() implies F /^ k is V339() ) & ( F is V340() implies F /^ k is V340() ) )
hereby :: thesis: ( F is V340() implies F /^ k is V340() )
assume F is V339() ; :: thesis: F /^ k is V339()
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 V339() by A1, MESFUNC5:def 3; :: thesis: verum
end;
assume F is V340() ; :: thesis: F /^ k is V340()
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 V340() by A2, MESFUNC5:def 4; :: thesis: verum