let X be non empty set ; :: thesis: for F being without_+infty-valued FinSequence of Funcs (X,ExtREAL)
for n being Nat st n in dom F holds
(F /. n) " {+infty} = {}
let F be without_+infty-valued FinSequence of Funcs (X,ExtREAL); :: thesis: for n being Nat st n in dom F holds
(F /. n) " {+infty} = {}
let n be Nat; :: thesis: ( n in dom F implies (F /. n) " {+infty} = {} )
assume A1: n in dom F ; :: thesis: (F /. n) " {+infty} = {}
then F . n is without+infty by DEF10;
then not +infty in rng (F . n) by MESFUNC5:def 4;
then not +infty in rng (F /. n) by A1, PARTFUN1:def 6;
hence (F /. n) " {+infty} = {} by FUNCT_1:72; :: thesis: verum