for X being non empty set holds
( <*(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 ) )