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 DEF11;
then not -infty in rng (F . n) by MESFUNC5:def 3;
then not -infty in rng (F /. n) by A1, PARTFUN1:def 6;
hence (F /. n) " {-infty} = {} by FUNCT_1:72; :: thesis: verum