let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E c= dom f & f is E -measurable holds
Integral (M,((- f) | E)) = - (Integral (M,(f | E)))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E c= dom f & f is E -measurable holds
Integral (M,((- f) | E)) = - (Integral (M,(f | E)))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for E being Element of S st E c= dom f & f is E -measurable holds
Integral (M,((- f) | E)) = - (Integral (M,(f | E)))
let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S st E c= dom f & f is E -measurable holds
Integral (M,((- f) | E)) = - (Integral (M,(f | E)))
let E be Element of S; :: thesis: ( E c= dom f & f is E -measurable implies Integral (M,((- f) | E)) = - (Integral (M,(f | E))) )
assume that
A1: E c= dom f and
A2: f is E -measurable ; :: thesis: Integral (M,((- f) | E)) = - (Integral (M,(f | E)))
A3: E = dom (f | E) by A1, RELAT_1:62;
then A4: E = (dom f) /\ E by RELAT_1:61;
(- f) | E = - (f | E) by Th3;
hence Integral (M,((- f) | E)) = - (Integral (M,(f | E))) by A3, A4, A2, MESFUNC5:42, Th52; :: thesis: verum