let X be non empty set ; :: thesis: ( X --> 0. is without-infty Function of X,ExtREAL & X --> 0. is without+infty Function of X,ExtREAL )
reconsider P = X --> 0. as Function of X,ExtREAL ;
for x being object holds -infty < P . x ;
hence X --> 0. is without-infty Function of X,ExtREAL by MESFUNC5:def 5; :: thesis: X --> 0. is without+infty Function of X,ExtREAL
reconsider M = X --> 0. as Function of X,ExtREAL ;
for x being object holds M . x < +infty by Lm1;
hence X --> 0. is without+infty Function of X,ExtREAL by MESFUNC5:def 6; :: thesis: verum