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_{1}( set ) -> Event of = 0 ;

deffunc H_{2}( set ) -> Event of = 1;

defpred S_{1}[ set ] means p in $1;

ex f being Function st

( dom f = Sigma & ( for x being set st x in Sigma holds

( ( S_{1}[x] implies f . x = H_{2}(x) ) & ( not S_{1}[x] implies f . x = H_{1}(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_{1}[x] implies f . x = 1 ) & ( not S_{1}[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

( 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

deffunc H

defpred S

ex f being Function st

( dom f = Sigma & ( for x being set st x in Sigma holds

( ( S

then consider f being Function such that

A1: dom f = Sigma and

A2: for x being set st x in Sigma holds

( ( S

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