:: deftheorem defines zeroed VALUED_0:def 19 :
for f being ext-real-valued Function holds
( f is zeroed iff f . {} = 0 );