theorem :: MESFUN11:22

for X being non empty set
for f being Function of X,ExtREAL holds
( 0 (#) f = X --> 0 & 0 (#) f is V120() & 0 (#) f is V121() )