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
for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) & f a.e.= g,M holds
Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) & f a.e.= g,M holds
Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k))
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) & f a.e.= g,M holds
Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k))
let f, g be PartFunc of X,REAL; :: thesis: for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) & f a.e.= g,M holds
Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k))
let k be positive Real; :: thesis: ( f in Lp_Functions (M,k) & g in Lp_Functions (M,k) & f a.e.= g,M implies Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k)) )
set t = (abs f) to_power k;
set s = (abs g) to_power k;
assume A1: ( f in Lp_Functions (M,k) & g in Lp_Functions (M,k) & f a.e.= g,M ) ; :: thesis: Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k))
then ex f1 being PartFunc of X,REAL st
( f = f1 & ex E being Element of S st
( M . (E `) = 0 & dom f1 = E & f1 is E -measurable & (abs f1) to_power k is_integrable_on M ) ) ;
then consider Df being Element of S such that
A2: ( M . (Df `) = 0 & dom f = Df & f is Df -measurable & (abs f) to_power k is_integrable_on M ) ;
ex g1 being PartFunc of X,REAL st
( g = g1 & ex E being Element of S st
( M . (E `) = 0 & dom g1 = E & g1 is E -measurable & (abs g1) to_power k is_integrable_on M ) ) by A1;
then consider Dg being Element of S such that
A3: ( M . (Dg `) = 0 & dom g = Dg & g is Dg -measurable & (abs g) to_power k is_integrable_on M ) ;
A4: ( dom (abs f) = dom f & dom (abs g) = dom g ) by VALUED_1:def 11;
consider E1 being Element of S such that
A5: ( M . E1 = 0 & f | (E1 `) = g | (E1 `) ) by A1;
reconsider NDf = Df ` , NDg = Dg ` as Element of S by MEASURE1:34;
set Ef = Df \ (NDg \/ E1);
set Eg = Dg \ (NDf \/ E1);
set E2 = (NDf \/ NDg) \/ E1;
( NDf is measure_zero of M & NDg is measure_zero of M & E1 is measure_zero of M ) by A2, A3, A5, MEASURE1:def 7;
then ( NDf \/ E1 is measure_zero of M & NDg \/ E1 is measure_zero of M ) by MEASURE1:37;
then A6: ( M . (NDf \/ E1) = 0 & M . (NDg \/ E1) = 0 ) by MEASURE1:def 7;
( X \ NDf = X /\ Df & X \ NDg = X /\ Dg ) by XBOOLE_1:48;
then A7: ( X \ NDf = Df & X \ NDg = Dg ) by XBOOLE_1:28;
( Df \ (NDg \/ E1) = (Df \ NDg) \ E1 & Dg \ (NDf \/ E1) = (Dg \ NDf) \ E1 ) by XBOOLE_1:41;
then A8: ( Df \ (NDg \/ E1) = (X \ (NDf \/ NDg)) \ E1 & Dg \ (NDf \/ E1) = (X \ (NDf \/ NDg)) \ E1 ) by A7, XBOOLE_1:41;
then A9: ( Df \ (NDg \/ E1) = X \ ((NDf \/ NDg) \/ E1) & Dg \ (NDf \/ E1) = X \ ((NDf \/ NDg) \/ E1) ) by XBOOLE_1:41;
( abs f is Df -measurable & abs g is Dg -measurable ) by A2, A3, MESFUNC6:48;
then A10: ( (abs f) to_power k is Df -measurable & (abs g) to_power k is Dg -measurable ) by A2, A3, A4, MESFUN6C:29;
A11: ( dom ((abs f) to_power k) = Df & dom ((abs g) to_power k) = Dg ) by A2, A3, A4, MESFUN6C:def 4;
then A12: ( Integral (M,(((abs f) to_power k) | (Df \ (NDg \/ E1)))) = Integral (M,((abs f) to_power k)) & Integral (M,(((abs g) to_power k) | (Dg \ (NDf \/ E1)))) = Integral (M,((abs g) to_power k)) ) by A6, A10, MESFUNC6:89;
( dom (((abs f) to_power k) | (Df \ (NDg \/ E1))) = (dom ((abs f) to_power k)) /\ (Df \ (NDg \/ E1)) & dom (((abs g) to_power k) | (Df \ (NDg \/ E1))) = (dom ((abs g) to_power k)) /\ (Df \ (NDg \/ E1)) ) by RELAT_1:61;
then A13: ( dom (((abs f) to_power k) | (Df \ (NDg \/ E1))) = (Df /\ Df) \ (NDg \/ E1) & dom (((abs g) to_power k) | (Df \ (NDg \/ E1))) = (Dg /\ Dg) \ (NDf \/ E1) ) by A11, A8, XBOOLE_1:49;

now :: thesis: for x being Element of X st x in dom (((abs f) to_power k) | (Df \ (NDg \/ E1))) holds
(((abs f) to_power k) | (Df \ (NDg \/ E1))) . x = (((abs g) to_power k) | (Df \ (NDg \/ E1))) . x

let x be Element of X; :: thesis: ( x in dom (((abs f) to_power k) | (Df \ (NDg \/ E1))) implies (((abs f) to_power k) | (Df \ (NDg \/ E1))) . x = (((abs g) to_power k) | (Df \ (NDg \/ E1))) . x )
assume A14: x in dom (((abs f) to_power k) | (Df \ (NDg \/ E1))) ; :: thesis: (((abs f) to_power k) | (Df \ (NDg \/ E1))) . x = (((abs g) to_power k) | (Df \ (NDg \/ E1))) . x
A15: ( dom (((abs f) to_power k) | (Df \ (NDg \/ E1))) c= dom ((abs f) to_power k) & dom (((abs g) to_power k) | (Df \ (NDg \/ E1))) c= dom ((abs g) to_power k) ) by RELAT_1:60;
((NDf \/ NDg) \/ E1) ` c= E1 ` by XBOOLE_1:7, XBOOLE_1:34;
then A16: ( f . x = (f | (E1 `)) . x & g . x = (g | (E1 `)) . x ) by A14, A13, A9, FUNCT_1:49;
( (((abs f) to_power k) | (Df \ (NDg \/ E1))) . x = ((abs f) to_power k) . x & (((abs g) to_power k) | (Df \ (NDg \/ E1))) . x = ((abs g) to_power k) . x ) by A14, A13, FUNCT_1:49;
then ( (((abs f) to_power k) | (Df \ (NDg \/ E1))) . x = ((abs f) . x) to_power k & (((abs g) to_power k) | (Df \ (NDg \/ E1))) . x = ((abs g) . x) to_power k ) by A8, A13, A14, A15, MESFUN6C:def 4;
then ( (((abs f) to_power k) | (Df \ (NDg \/ E1))) . x = |.(f . x).| to_power k & (((abs g) to_power k) | (Df \ (NDg \/ E1))) . x = |.(g . x).| to_power k ) by VALUED_1:18;
hence (((abs f) to_power k) | (Df \ (NDg \/ E1))) . x = (((abs g) to_power k) | (Df \ (NDg \/ E1))) . x by A5, A16; :: thesis: verum

end;

hence Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k)) by A12, A13, A8, PARTFUN1:5; :: thesis: verum