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)

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

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)

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))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;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

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