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

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