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 Th26;

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

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 Th26;

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