let X be non empty set ; for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st f is A -measurable holds
A /\ (eq_dom (f,-infty)) in S
let S be SigmaField of X; for f being PartFunc of X,ExtREAL
for A being Element of S st f is A -measurable holds
A /\ (eq_dom (f,-infty)) in S
let f be PartFunc of X,ExtREAL; for A being Element of S st f is A -measurable holds
A /\ (eq_dom (f,-infty)) in S
let A be Element of S; ( f is A -measurable implies A /\ (eq_dom (f,-infty)) in S )
assume A1:
f is A -measurable
; A /\ (eq_dom (f,-infty)) in S
defpred S1[ Nat, set ] means A /\ (less_dom (f,(- $1))) = $2;
A2:
for n being Element of NAT ex y being Element of S st S1[n,y]
consider F being sequence of S such that
A3:
for n being Element of NAT holds S1[n,F . n]
from FUNCT_2:sch 3(A2);
for n being Nat holds S1[n,F . n]
then
A /\ (eq_dom (f,-infty)) = meet (rng F)
by Th25;
hence
A /\ (eq_dom (f,-infty)) in S
; verum