let X be non empty set ; 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; 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; 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; for r being Real holds A /\ (less_dom (f,r)) = less_dom ((f | A),r)
let r be Real; A /\ (less_dom (f,r)) = less_dom ((f | A),r)
now for v being object st v in A /\ (less_dom (f,r)) holds
v in less_dom ((f | A),r)let v be
object ;
( v in A /\ (less_dom (f,r)) implies v in less_dom ((f | A),r) )assume A1:
v in A /\ (less_dom (f,r))
;
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;
verum end;
hence
A /\ (less_dom (f,r)) c= less_dom ((f | A),r)
; XBOOLE_0:def 10 less_dom ((f | A),r) c= A /\ (less_dom (f,r))
let v be object ; TARSKI:def 3 ( 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)
; 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; verum