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 A1: ( f in L1_Functions M & g in L1_Functions M & f a.e.= g,M ) ; :: thesis: ( abs f a.e.= abs g,M & Integral M,(abs f) = Integral M,(abs g) )
A2: 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
A3: ( M . NDf = 0 & dom f = NDf ` & f is_integrable_on M ) ;
A4: 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 A1;
then consider NDg being Element of S such that
A5: ( M . NDg = 0 & dom g = NDg ` & g is_integrable_on M ) ;
consider EQ being Element of S such that
A6: ( M . EQ = 0 & f | (EQ ` ) = g | (EQ ` ) ) by A1, Def2;
A8: ( abs f is_integrable_on M & abs g is_integrable_on M ) by A2, A4, Lm15;
( dom (abs f) = NDf ` & dom (abs g) = NDg ` ) by A3, A5, VALUED_1:def 11;
then A9: ( abs f in L1_Functions M & abs g in L1_Functions M ) by A3, A5, A8;
(abs f) | (EQ ` ) = abs (g | (EQ ` )) by A6, RFUNCT_1:62
.= (abs g) | (EQ ` ) by RFUNCT_1:62 ;
then abs f a.e.= abs g,M by Def2, A6;
hence ( abs f a.e.= abs g,M & Integral M,(abs f) = Integral M,(abs g) ) by A9, Th14a; :: thesis: verum