reconsider M = X --> 0. as Function of X,ExtREAL ;
take M ; :: thesis: ( M is V183() & M is V184() & M is nonnegative & M is nonpositive )
for x being object holds -infty < M . x ;
hence M is V183() by MESFUNC5:def 5; :: thesis: ( M is V184() & M is nonnegative & M is nonpositive )
for x being object holds M . x < +infty by Lm1;
hence M is V184() by MESFUNC5:def 6; :: thesis: ( M is nonnegative & M is nonpositive )
for x being object holds 0 <= M . x ;
hence M is nonnegative by SUPINF_2:51; :: thesis: M is nonpositive
for x being object holds M . x <= 0 by Lm1;
hence M is nonpositive by MESFUNC5:8; :: thesis: verum