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
for r, s being Real st f is A -measurable & A c= dom f holds
(A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
let S be 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_dom (f,r))) /\ (less_dom (f,s)) in S
let f be 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_dom (f,r))) /\ (less_dom (f,s)) in S
let A be Element of S; for r, s being Real st f is A -measurable & A c= dom f holds
(A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
let r, s be Real; ( f is A -measurable & A c= dom f implies (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S )
assume that
A1:
f is A -measurable
and
A2:
A c= dom f
; (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
A3:
A /\ (less_dom (f,s)) in S
by A1;
A4:
for r1 being Real holds A /\ (great_eq_dom (f,r1)) in S
for r1 being Real holds A /\ (great_dom (f,r1)) in S
then A7:
A /\ (great_dom (f,r)) in S
;
(A /\ (great_dom (f,r))) /\ (A /\ (less_dom (f,s))) =
((A /\ (great_dom (f,r))) /\ A) /\ (less_dom (f,s))
by XBOOLE_1:16
.=
((great_dom (f,r)) /\ (A /\ A)) /\ (less_dom (f,s))
by XBOOLE_1:16
;
hence
(A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
by A3, A7, FINSUB_1:def 2; verum