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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M & f a.e.cpfunc= g,M holds
( |.f.| a.e.= |.g.|,M & Integral (M,|.f.|) = Integral (M,|.g.|) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M & f a.e.cpfunc= g,M holds
( |.f.| a.e.= |.g.|,M & Integral (M,|.f.|) = Integral (M,|.g.|) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M & f a.e.cpfunc= g,M holds
( |.f.| a.e.= |.g.|,M & Integral (M,|.f.|) = Integral (M,|.g.|) )
let f, g be PartFunc of X,COMPLEX; :: thesis: ( f in L1_CFunctions M & g in L1_CFunctions M & f a.e.cpfunc= g,M implies ( |.f.| a.e.= |.g.|,M & Integral (M,|.f.|) = Integral (M,|.g.|) ) )
assume that
A1: f in L1_CFunctions M and
A2: g in L1_CFunctions M and
A3: f a.e.cpfunc= g,M ; :: thesis: ( |.f.| a.e.= |.g.|,M & Integral (M,|.f.|) = Integral (M,|.g.|) )
reconsider AF = |.f.|, AG = |.g.| as PartFunc of X,REAL ;
A4: ex f1 being PartFunc of X,COMPLEX 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: AF is_integrable_on M by A4, Th37;
consider EQ being Element of S such that
A8: M . EQ = 0 and
A9: f | (EQ `) = g | (EQ `) by A3;
A10: AF | (EQ `) = abs (g | (EQ `)) by A9, CFUNCT_1:54
.= AG | (EQ `) by CFUNCT_1:54 ;
A11: ex g1 being PartFunc of X,COMPLEX 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: AG is_integrable_on M by A11, Th37;
dom AG = NDg ` by A13, VALUED_1:def 11;
then A15: AG in L1_Functions M by A12, A14;
dom AF = NDf ` by A6, VALUED_1:def 11;
then AF in L1_Functions M by A5, A7;
hence ( |.f.| a.e.= |.g.|,M & Integral (M,|.f.|) = Integral (M,|.g.|) ) by A15, A8, A10, LPSPACE1:def 10, LPSPACE1:43; :: thesis: verum