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
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;
A3: 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
A4: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A3);
A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) by A4, Th24;
hence A /\ (less_eq_dom (f,(R_EAL r))) in S ; :: thesis: verum

end;

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

end;

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

proof

assume A5: for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ; :: thesis: f is_measurable_on A
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;
A6: 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 A5;
take y ; :: thesis: S₁[n,y]
thus S₁[n,y] ; :: thesis: verum

end;

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

end;

hence f is_measurable_on A by Def17; :: thesis: verum

end;

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