let Omega, p be set ; :: thesis: for Sigma being SigmaField of Omega ex f being Function st
( 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 ) ) ) )
let Sigma be SigmaField of Omega; :: thesis: ex f being Function st
( 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 ) ) ) )
deffunc H₁( set ) -> Event of = 0 ;
deffunc H₂( set ) -> Event of = 1;
defpred S₁[ set ] means p in $1;
ex f being Function st
( dom f = Sigma & ( for x being set st x in Sigma holds
( ( S₁[x] implies f . x = H₂(x) ) & ( not S₁[x] implies f . x = H₁(x) ) ) ) ) from PARTFUN1:sch 5();
then consider f being Function such that
A1: dom f = Sigma and
A2: for x being set st x in Sigma holds
( ( S₁[x] implies f . x = 1 ) & ( not S₁[x] implies f . x = 0 ) ) ;
take f ; :: thesis: ( 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 ) ) ) )
thus dom f = Sigma by A1; :: 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 ) )
let D be Subset of Omega; :: thesis: ( D in Sigma implies ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) )
assume A3: D in Sigma ; :: thesis: ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) )
hence ( p in D implies f . D = 1 ) by A2; :: thesis: ( not p in D implies f . D = 0 )
assume not p in D ; :: thesis: f . D = 0
hence f . D = 0 by A2, A3; :: thesis: verum