let X be non empty set ; :: thesis: for f being Function of X,ExtREAL holds
( 0 (#) f = X --> 0 & 0 (#) f is without-infty & 0 (#) f is without+infty )
let f be Function of X,ExtREAL; :: thesis: ( 0 (#) f = X --> 0 & 0 (#) f is without-infty & 0 (#) f is without+infty )
A1: X --> 0 is Function of X,ExtREAL by FUNCOP_1:45, XXREAL_0:def 1;
for x being Element of X holds (0 (#) f) . x = (X --> 0) . x

proof

let x be Element of X; :: thesis: (0 (#) f) . x = (X --> 0) . x
x in X ;
then x in dom (0 (#) f) by FUNCT_2:def 1;
then (0 (#) f) . x = 0 * (f . x) by MESFUNC1:def 6;
hence (0 (#) f) . x = (X --> 0) . x by FUNCOP_1:7; :: thesis: verum

end;

hence 0 (#) f = X --> 0 by A1, FUNCT_2:def 8; :: thesis: ( 0 (#) f is without-infty & 0 (#) f is without+infty )
hence ( 0 (#) f is without-infty & 0 (#) f is without+infty ) by Th21; :: thesis: verum