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 H1( set ) -> Event of = 0 ;
deffunc H2( set ) -> Event of = 1;
defpred S1[ set ] means p in \$1;
ex f being Function st
( dom f = Sigma & ( for x being set st x in Sigma holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) ) ) from then consider f being Function such that
A1: dom f = Sigma and
A2: for x being set st x in Sigma holds
( ( S1[x] implies f . x = 1 ) & ( not S1[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