let X be non empty set ; :: thesis: ( <*(X --> 0)*> is FinSequence of Funcs (X,ExtREAL) & ( for n being Nat st n in dom <*(X --> 0)*> holds
<*(X --> 0)*> . n is without+infty ) & ( for n being Nat st n in dom <*(X --> 0)*> holds
<*(X --> 0)*> . n is without-infty ) )
X --> 0 is Function of X,ExtREAL by XXREAL_0:def 1, FUNCOP_1:45;
then reconsider f = X --> 0 as Element of Funcs (X,ExtREAL) by FUNCT_2:8;
<*f*> is FinSequence of Funcs (X,ExtREAL) ;
hence <*(X --> 0)*> is FinSequence of Funcs (X,ExtREAL) ; :: thesis: ( ( for n being Nat st n in dom <*(X --> 0)*> holds
<*(X --> 0)*> . n is without+infty ) & ( for n being Nat st n in dom <*(X --> 0)*> holds
<*(X --> 0)*> . n is without-infty ) )

hereby :: thesis: for n being Nat st n in dom <*(X --> 0)*> holds
<*(X --> 0)*> . n is without-infty

let n be Nat; :: thesis: ( n in dom <*(X --> 0)*> implies <*(X --> 0)*> . n is without+infty )
assume n in dom <*(X --> 0)*> ; :: thesis: <*(X --> 0)*> . n is without+infty
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def 1;
then A1: <*(X --> 0)*> . n = X --> 0 ;
not +infty in rng (X --> 0) ;
hence <*(X --> 0)*> . n is without+infty by A1, MESFUNC5:def 4; :: thesis: verum

end;

let n be Nat; :: thesis: ( n in dom <*(X --> 0)*> implies <*(X --> 0)*> . n is without-infty )
assume n in dom <*(X --> 0)*> ; :: thesis: <*(X --> 0)*> . n is without-infty
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def 1;
then A2: <*(X --> 0)*> . n = X --> 0 ;
not -infty in rng (X --> 0) ;
hence <*(X --> 0)*> . n is without-infty by A2, MESFUNC5:def 3; :: thesis: verum