let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )
let f, g be PartFunc of X,REAL; :: thesis: ( f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies ( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) ) )
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M and
A3: f a.e.= g,M ; :: thesis: ( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )
A4: ex f1 being PartFunc of X,REAL st
( f = f1 & ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) ) by A1;
then consider NDf being Element of S such that
A5: M . NDf = 0 and
A6: dom f = NDf ` and
f is_integrable_on M ;
A7: abs f is_integrable_on M by A4, Th44;
consider EQ being Element of S such that
A8: M . EQ = 0 and
A9: f | (EQ `) = g | (EQ `) by A3;
(abs f) | (EQ `) = abs (g | (EQ `)) by A9, RFUNCT_1:46
.= (abs g) | (EQ `) by RFUNCT_1:46 ;
then A10: abs f a.e.= abs g,M by A8;
A11: ex g1 being PartFunc of X,REAL st
( g = g1 & ex ND being Element of S st
( M . ND = 0 & dom g1 = ND ` & g1 is_integrable_on M ) ) by A2;
then consider NDg being Element of S such that
A12: M . NDg = 0 and
A13: dom g = NDg ` and
g is_integrable_on M ;
A14: abs g is_integrable_on M by A11, Th44;
dom (abs g) = NDg ` by A13, VALUED_1:def 11;
then A15: abs g in L1_Functions M by A12, A14;
dom (abs f) = NDf ` by A6, VALUED_1:def 11;
then abs f in L1_Functions M by A5, A7;
hence ( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) ) by A15, A10, Th43; :: thesis: verum