let Omega be non empty set ; :: thesis: for p being set
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 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 ) ) ) )
defpred S₁[ set ] means p in $1;
deffunc H₁( set ) -> Element of NAT = 1;
deffunc H₂( set ) -> Element of NAT = 0 ;
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 1();
then consider f being Function such that
A1: ( dom f = Sigma & ( 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 A2: 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 A1; :: thesis: ( not p in D implies f . D = 0 )
assume not p in D ; :: thesis: f . D = 0
hence f . D = 0 by A1, A2; :: thesis: verum