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

A3: 0 in REAL by XREAL_0:def 1;

rng f c= REAL

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

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

A3: 0 in REAL by XREAL_0:def 1;

rng f c= REAL

proof

then reconsider f = f as Function of Sigma,REAL by A1, FUNCT_2:def 1, RELSET_1:4;
let y be object ; :: 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 object such that

A4: x in dom f and

A5: y = f . x by FUNCT_1:def 3;

reconsider x = x as Subset of Omega by A1, A4;

reconsider j = 1 as Real ;

A6: 1 in REAL by XREAL_0:def 1;

A7: ( not p in x implies y = 0 ) by A1, A2, A4, A5;

( p in x implies y = j ) by A1, A2, A4, A5;

hence y in REAL by A7, A3, A6; :: thesis: verum

end;assume y in rng f ; :: thesis: y in REAL

then consider x being object such that

A4: x in dom f and

A5: y = f . x by FUNCT_1:def 3;

reconsider x = x as Subset of Omega by A1, A4;

reconsider j = 1 as Real ;

A6: 1 in REAL by XREAL_0:def 1;

A7: ( not p in x implies y = 0 ) by A1, A2, A4, A5;

( p in x implies y = j ) by A1, A2, A4, A5;

hence y in REAL by A7, A3, A6; :: thesis: verum

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