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 number holds A /\ (less_dom f,(R_EAL r)) = less_dom (f | A),(R_EAL 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 number holds A /\ (less_dom f,(R_EAL r)) = less_dom (f | A),(R_EAL r)
let A be Element of S; :: thesis: for f being PartFunc of X,ExtREAL
for r being real number holds A /\ (less_dom f,(R_EAL r)) = less_dom (f | A),(R_EAL r)
let f be PartFunc of X,ExtREAL ; :: thesis: for r being real number holds A /\ (less_dom f,(R_EAL r)) = less_dom (f | A),(R_EAL r)
let r be real number ; :: thesis: A /\ (less_dom f,(R_EAL r)) = less_dom (f | A),(R_EAL r)

now

let v be set ; :: thesis: ( v in A /\ (less_dom f,(R_EAL r)) implies v in less_dom (f | A),(R_EAL r) )
assume A1: v in A /\ (less_dom f,(R_EAL r)) ; :: thesis: v in less_dom (f | A),(R_EAL r)
then A2: v in less_dom f,(R_EAL 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:72;
v in dom f by A2, MESFUNC1:def 12;
then v in A /\ (dom f) by A3, XBOOLE_0:def 4;
then A5: v in dom (f | A) by RELAT_1:90;
f . v < R_EAL r by A2, MESFUNC1:def 12;
hence v in less_dom (f | A),(R_EAL r) by A5, A4, MESFUNC1:def 12; :: thesis: verum

end;

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