reconsider F = <*(X --> 0)*> as FinSequence of Funcs (X,ExtREAL) by Th52;
take F ; :: thesis: ( F is without_+infty-valued & F is without_-infty-valued )
thus ( F is without_+infty-valued & F is without_-infty-valued ) by Th52; :: thesis: verum