let X be non empty set ; :: thesis: for f being Function of X,ExtREAL holds

( 0 (#) f = X --> 0 & 0 (#) f is V120() & 0 (#) f is V121() )

let f be Function of X,ExtREAL; :: thesis: ( 0 (#) f = X --> 0 & 0 (#) f is V120() & 0 (#) f is V121() )

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

hence ( 0 (#) f is V120() & 0 (#) f is V121() ) by Th21; :: thesis: verum

( 0 (#) f = X --> 0 & 0 (#) f is V120() & 0 (#) f is V121() )

let f be Function of X,ExtREAL; :: thesis: ( 0 (#) f = X --> 0 & 0 (#) f is V120() & 0 (#) f is V121() )

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

hence
0 (#) f = X --> 0
by A1, FUNCT_2:def 8; :: thesis: ( 0 (#) f is V120() & 0 (#) f is V121() )
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;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

hence ( 0 (#) f is V120() & 0 (#) f is V121() ) by Th21; :: thesis: verum