let Omega be non empty set ; :: thesis: for p being set
for Sigma being SigmaField of Omega ex P being Function of Sigma,REAL st
for D being Subset of Omega st D in Sigma holds
( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) )
let p be set ; :: thesis: for Sigma being SigmaField of Omega ex P being Function of Sigma,REAL st
for D being Subset of Omega st D in Sigma holds
( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) )
let Sigma be SigmaField of Omega; :: thesis: ex P being Function of Sigma,REAL st
for D being Subset of Omega st D in Sigma holds
( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) )
consider f being Function such that
A1: ( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) ) by Th59;
rng f c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in REAL )
assume y in rng f ; :: thesis: y in REAL
then consider x being set such that
A2: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
reconsider x = x as Subset of Omega by A1, A2;
A3: ( p in x implies y = 1 ) by A1, A2;
( not p in x implies y = 0 ) by A1, A2;
hence y in REAL by A3; :: thesis: verum

end;

then reconsider f = f as Function of Sigma,REAL by A1, FUNCT_2:def 1, RELSET_1:11;
take f ; :: thesis: for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) )
thus for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) by A1; :: thesis: verum