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 = dom f & f is E -measurable holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

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 = dom f & f is E -measurable holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for E being Element of S st E = dom f & f is E -measurable holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S st E = dom f & f is E -measurable holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

let E be Element of S; :: thesis: ( E = dom f & f is E -measurable implies Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) )

assume that

A1: E = dom f and

A2: f is E -measurable ; :: thesis: Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

A3: ( E = dom (max+ f) & E = dom (max- f) ) by A1, MESFUNC2:def 2, MESFUNC2:def 3;

( max+ f is E -measurable & max- f is E -measurable ) by A1, A2, Th10;

then ( Integral (M,(max+ f)) = integral+ (M,(max+ f)) & Integral (M,(max- f)) = integral+ (M,(max- f)) ) by A3, Th5, MESFUNC5:88;

hence Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) by MESFUNC5:def 16; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S st E = dom f & f is E -measurable holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

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 = dom f & f is E -measurable holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for E being Element of S st E = dom f & f is E -measurable holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S st E = dom f & f is E -measurable holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

let E be Element of S; :: thesis: ( E = dom f & f is E -measurable implies Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) )

assume that

A1: E = dom f and

A2: f is E -measurable ; :: thesis: Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

A3: ( E = dom (max+ f) & E = dom (max- f) ) by A1, MESFUNC2:def 2, MESFUNC2:def 3;

( max+ f is E -measurable & max- f is E -measurable ) by A1, A2, Th10;

then ( Integral (M,(max+ f)) = integral+ (M,(max+ f)) & Integral (M,(max- f)) = integral+ (M,(max- f)) ) by A3, Th5, MESFUNC5:88;

hence Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) by MESFUNC5:def 16; :: thesis: verum