let X be set ; :: thesis: ex M being Function of bool X, ExtREAL st
for A being Subset of X holds M . A = 0.
consider M being Function of bool X, ExtREAL such that
A1: for A being Subset of X holds
( ( A = {} implies M . A = 0. ) & ( A <> {} implies M . A = 0. ) ) by Th7;
take M ; :: thesis: for A being Subset of X holds M . A = 0.
thus for A being Subset of X holds M . A = 0. by A1; :: thesis: verum