reconsider f = X --> 0. as V184() Function of X,ExtREAL by Lm2;
take f ; :: thesis: f is V183()
thus f is V183() by Lm2; :: thesis: verum