let Omega, 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 and
A2: 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
A3: x in dom f and
A4: y = f . x by FUNCT_1:def 3;
reconsider x = x as Subset of Omega by A1, A3;
A5: ( not p in x implies y = 0 ) by A1, A2, A3, A4;
( p in x implies y = 1 ) by A1, A2, A3, A4;
hence y in REAL by A5; :: thesis: verum

end;

then reconsider f = f as Function of Sigma,REAL by A1, FUNCT_2:def 1, RELSET_1:4;
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 A2; :: thesis: verum