let X be non empty set ; :: thesis: ( X --> 0. is V183() Function of X,ExtREAL & X --> 0. is V184() 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 V183() Function of X,ExtREAL by MESFUNC5:def 5; :: thesis: X --> 0. is V184() 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 V184() Function of X,ExtREAL by MESFUNC5:def 6; :: thesis: verum