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 v in A /\ (less_dom f,(R_EAL r)) ; :: thesis: v in less_dom (f | A),(R_EAL r)
then A1: ( v in A & v in less_dom f,(R_EAL r) ) by XBOOLE_0:def 4;
then ( v in dom f & f . v < R_EAL r ) by MESFUNC1:def 12;
then v in A /\ (dom f) by A1, XBOOLE_0:def 4;
then A2: v in dom (f | A) by RELAT_1:90;
A3: f . v < R_EAL r by A1, MESFUNC1:def 12;
f . v = (f | A) . v by A1, FUNCT_1:72;
hence v in less_dom (f | A),(R_EAL r) by A2, A3, 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 A4: v in less_dom (f | A),(R_EAL r) ; :: thesis: v in A /\ (less_dom f,(R_EAL r))
then A5: v in dom (f | A) by MESFUNC1:def 12;
A6: (f | A) . v < R_EAL r by A4, MESFUNC1:def 12;
( v in (dom f) /\ A & (f | A) . v = f . v ) by A5, FUNCT_1:70, RELAT_1:90;
then ( v in dom f & v in A & ex w being R_eal st
( w = f . v & w < R_EAL r ) ) by A6, XBOOLE_0:def 4;
then ( v in A & v in less_dom f,(R_EAL r) ) by MESFUNC1:def 12;
hence v in A /\ (less_dom f,(R_EAL r)) by XBOOLE_0:def 4; :: thesis: verum