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