let X be non empty set ; :: thesis: for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,ExtREAL
for r being Real holds A /\ (less_dom (f,r)) = less_dom ((f | A),r)
let S be SigmaField of X; :: thesis: for A being Element of S
for f being PartFunc of X,ExtREAL
for r being Real holds A /\ (less_dom (f,r)) = less_dom ((f | A),r)
let A be Element of S; :: thesis: for f being PartFunc of X,ExtREAL
for r being Real holds A /\ (less_dom (f,r)) = less_dom ((f | A),r)
let f be PartFunc of X,ExtREAL; :: thesis: for r being Real holds A /\ (less_dom (f,r)) = less_dom ((f | A),r)
let r be Real; :: thesis: A /\ (less_dom (f,r)) = less_dom ((f | A),r)

now :: thesis: for v being object st v in A /\ (less_dom (f,r)) holds
v in less_dom ((f | A),r)

let v be object ; :: thesis: ( v in A /\ (less_dom (f,r)) implies v in less_dom ((f | A),r) )
assume A1: v in A /\ (less_dom (f,r)) ; :: thesis: v in less_dom ((f | A),r)
then A2: v in less_dom (f,r) by XBOOLE_0:def 4;
A3: v in A by A1, XBOOLE_0:def 4;
then A4: f . v = (f | A) . v by FUNCT_1:49;
v in dom f by A2, MESFUNC1:def 11;
then v in A /\ (dom f) by A3, XBOOLE_0:def 4;
then A5: v in dom (f | A) by RELAT_1:61;
f . v < r by A2, MESFUNC1:def 11;
hence v in less_dom ((f | A),r) by A5, A4, MESFUNC1:def 11; :: thesis: verum

end;

hence A /\ (less_dom (f,r)) c= less_dom ((f | A),r) ; :: according to XBOOLE_0:def 10 :: thesis: less_dom ((f | A),r) c= A /\ (less_dom (f,r))
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in less_dom ((f | A),r) or v in A /\ (less_dom (f,r)) )
reconsider vv = v as set by TARSKI:1;
assume A6: v in less_dom ((f | A),r) ; :: thesis: v in A /\ (less_dom (f,r))
then A7: v in dom (f | A) by MESFUNC1:def 11;
then A8: v in (dom f) /\ A by RELAT_1:61;
then A9: v in dom f by XBOOLE_0:def 4;
(f | A) . vv < r by A6, MESFUNC1:def 11;
then ex w being R_eal st
( w = f . vv & w < r ) by A7, FUNCT_1:47;
then A10: v in less_dom (f,r) by A9, MESFUNC1:def 11;
v in A by A8, XBOOLE_0:def 4;
hence v in A /\ (less_dom (f,r)) by A10, XBOOLE_0:def 4; :: thesis: verum