reconsider f = X --> 0. as without+infty Function of X,ExtREAL by Lm2;
take f ; :: thesis: f is without-infty
thus f is without-infty by Lm2; :: thesis: verum