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

for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL

for A being Element of S

for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S

for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

let A be Element of S; :: thesis: for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

let r, s be Real; :: thesis: ( f is A -measurable & A c= dom f implies (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S )

assume that

A1: f is A -measurable and

A2: A c= dom f ; :: thesis: (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

A3: A /\ (less_dom (f,s)) in S by A1, MESFUNC1:def 16;

A4: (A /\ (great_eq_dom (f,r))) /\ (A /\ (less_dom (f,s))) = ((A /\ (great_eq_dom (f,r))) /\ A) /\ (less_dom (f,s)) by XBOOLE_1:16

.= ((great_eq_dom (f,r)) /\ (A /\ A)) /\ (less_dom (f,s)) by XBOOLE_1:16 ;

A /\ (great_eq_dom (f,r)) in S by A1, A2, MESFUNC1:27;

hence (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S by A3, A4, FINSUB_1:def 2; :: thesis: verum

for f being PartFunc of X,ExtREAL

for A being Element of S

for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL

for A being Element of S

for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S

for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

let A be Element of S; :: thesis: for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

let r, s be Real; :: thesis: ( f is A -measurable & A c= dom f implies (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S )

assume that

A1: f is A -measurable and

A2: A c= dom f ; :: thesis: (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

A3: A /\ (less_dom (f,s)) in S by A1, MESFUNC1:def 16;

A4: (A /\ (great_eq_dom (f,r))) /\ (A /\ (less_dom (f,s))) = ((A /\ (great_eq_dom (f,r))) /\ A) /\ (less_dom (f,s)) by XBOOLE_1:16

.= ((great_eq_dom (f,r)) /\ (A /\ A)) /\ (less_dom (f,s)) by XBOOLE_1:16 ;

A /\ (great_eq_dom (f,r)) in S by A1, A2, MESFUNC1:27;

hence (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S by A3, A4, FINSUB_1:def 2; :: thesis: verum