let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S )
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S )
let f be PartFunc of X,ExtREAL ; :: thesis: for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S )
let A be Element of S; :: thesis: ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S )
A1: ( f is_measurable_on A implies for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S )

proof

assume A2: f is_measurable_on A ; :: thesis: for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S
A3: for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S

proof

let r be real number ; :: thesis: A /\ (less_eq_dom f,(R_EAL r)) in S
defpred S₁[ Element of NAT , set ] means A /\ (less_dom f,(R_EAL (r + (1 / ($1 + 1))))) = $2;
A4: for n being Element of NAT ex y being Element of S st S₁[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of S st S₁[n,y]
reconsider y = A /\ (less_dom f,(R_EAL (r + (1 / (n + 1))))) as Element of S by A2, Def17;
take y ; :: thesis: S₁[n,y]
thus S₁[n,y] ; :: thesis: verum

end;

consider F being Function of NAT ,S such that
A5: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A4);
A6: A /\ (less_eq_dom f,(R_EAL r)) = meet (rng F) by A5, Th24;
thus A /\ (less_eq_dom f,(R_EAL r)) in S by A6; :: thesis: verum

end;

thus for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S by A3; :: thesis: verum

end;

A7: ( ( for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S ) implies f is_measurable_on A )

proof

assume A8: for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S ; :: thesis: f is_measurable_on A
A9: for r being real number holds A /\ (less_dom f,(R_EAL r)) in S

proof

let r be real number ; :: thesis: A /\ (less_dom f,(R_EAL r)) in S
defpred S₁[ Element of NAT , set ] means A /\ (less_eq_dom f,(R_EAL (r - (1 / ($1 + 1))))) = $2;
A10: for n being Element of NAT ex y being Element of S st S₁[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of S st S₁[n,y]
reconsider y = A /\ (less_eq_dom f,(R_EAL (r - (1 / (n + 1))))) as Element of S by A8;
take y ; :: thesis: S₁[n,y]
thus S₁[n,y] ; :: thesis: verum

end;

consider F being Function of NAT ,S such that
A11: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A10);
A12: A /\ (less_dom f,(R_EAL r)) = union (rng F) by A11, Th25;
thus A /\ (less_dom f,(R_EAL r)) in S by A12; :: thesis: verum

end;

thus f is_measurable_on A by A9, Def17; :: thesis: verum

end;

thus ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom f,(R_EAL r)) in S ) by A1, A7; :: thesis: verum