let Omega, p be 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 Sigma be 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 ) ) ) )
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 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
( ( S1[x] implies f . x = 1 ) & ( not S1[x] implies f . x = 0 ) )
;
take
f
; ( 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; 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; ( D in Sigma implies ( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) )
assume A3:
D in Sigma
; ( ( 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; ( not p in D implies f . D = 0 )
assume
not p in D
; f . D = 0
hence
f . D = 0
by A2, A3; verum