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