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