reconsider M = X --> 0 as Function of X,REAL by FUNCOP_1:45, XREAL_0:def 1;
take M ; :: thesis: ( M is nonnegative & M is nonpositive )
A1: M is Function of X,ExtREAL by FUNCOP_1:45, XXREAL_0:def 1;
for x being object holds 0 <= M . x ;
hence M is nonnegative by A1, SUPINF_2:51; :: thesis: M is nonpositive
for x being object holds M . x <= 0 by Lm1;
hence M is nonpositive by A1, MESFUNC5:8; :: thesis: verum