let X be non empty set ; 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; 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; 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; ( 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
; ( |.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; verum