let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions M,k & Integral M,((abs f) to_power k) = 0 holds
f a.e.= X --> 0 ,M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions M,k & Integral M,((abs f) to_power k) = 0 holds
f a.e.= X --> 0 ,M
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions M,k & Integral M,((abs f) to_power k) = 0 holds
f a.e.= X --> 0 ,M
let f be PartFunc of X,REAL ; :: thesis: for k being positive Real st f in Lp_Functions M,k & Integral M,((abs f) to_power k) = 0 holds
f a.e.= X --> 0 ,M
let k be positive Real; :: thesis: ( f in Lp_Functions M,k & Integral M,((abs f) to_power k) = 0 implies f a.e.= X --> 0 ,M )
assume that
AS1: f in Lp_Functions M,k and
AS2: Integral M,((abs f) to_power k) = 0 ; :: thesis: f a.e.= X --> 0 ,M
ex h being PartFunc of X,REAL st
( f = h & ex ND being Element of S st
( M . (ND ` ) = 0 & dom h = ND & h is_measurable_on ND & (abs h) to_power k is_integrable_on M ) ) by AS1;
then consider NDf being Element of S such that
A3: ( M . (NDf ` ) = 0 & dom f = NDf & f is_measurable_on NDf & (abs f) to_power k is_integrable_on M ) ;
reconsider t = (abs f) to_power k as PartFunc of X,REAL ;
reconsider ND = NDf ` as Element of S by MEASURE1:66;
A4: dom t = dom (abs f) by MESFUN6C:def 6;
then A5: dom t = NDf by A3, VALUED_1:def 11;
dom t = ND ` by A4, A3, VALUED_1:def 11;
then A6: t in L1_Functions M by A3;
abs t = t by Lm002b;
then t a.e.= X --> 0 ,M by AS2, A6, LPSPACE1:54;
then consider ND1 being Element of S such that
A7: ( M . ND1 = 0 & ((abs f) to_power k) | (ND1 ` ) = (X --> 0 ) | (ND1 ` ) ) by LPSPACE1:def 10;
set ND2 = ND \/ ND1;
( ND is measure_zero of M & ND1 is measure_zero of M ) by A3, A7, MEASURE1:def 13;
then ND \/ ND1 is measure_zero of M by MEASURE1:70;
then A8: M . (ND \/ ND1) = 0 by MEASURE1:def 13;
A9: ( (ND \/ ND1) ` c= ND ` & (ND \/ ND1) ` c= ND1 ` ) by XBOOLE_1:7, XBOOLE_1:34;
dom (X --> 0 ) = X by FUNCOP_1:19;
then B1: dom ((X --> 0 ) | ((ND \/ ND1) ` )) = (ND \/ ND1) ` by RELAT_1:91;
B2: dom (f | ((ND \/ ND1) ` )) = (ND \/ ND1) ` by A3, A9, RELAT_1:91;
for x being set st x in dom (f | ((ND \/ ND1) ` )) holds
(f | ((ND \/ ND1) ` )) . x = ((X --> 0 ) | ((ND \/ ND1) ` )) . x

proof

let x be set ; :: thesis: ( x in dom (f | ((ND \/ ND1) ` )) implies (f | ((ND \/ ND1) ` )) . x = ((X --> 0 ) | ((ND \/ ND1) ` )) . x )
assume B3: x in dom (f | ((ND \/ ND1) ` )) ; :: thesis: (f | ((ND \/ ND1) ` )) . x = ((X --> 0 ) | ((ND \/ ND1) ` )) . x

B4: now

assume f . x <> 0 ; :: thesis: contradiction
then abs (f . x) > 0 by COMPLEX1:133;
then (abs (f . x)) to_power k <> 0 by POWER:39;
then ((abs f) . x) to_power k <> 0 by VALUED_1:18;
then K1: ((abs f) to_power k) . x <> 0 by A5, A9, B3, B2, MESFUN6C:def 6;
((X --> 0 ) | (ND1 ` )) . x = (X --> 0 ) . x by A9, B3, B2, FUNCT_1:72;
then ((X --> 0 ) | (ND1 ` )) . x = 0 by B3, FUNCOP_1:13;
hence contradiction by K1, A7, A9, B3, B2, FUNCT_1:72; :: thesis: verum

end;

((X --> 0 ) | ((ND \/ ND1) ` )) . x = (X --> 0 ) . x by B2, B3, FUNCT_1:72;
then ((X --> 0 ) | ((ND \/ ND1) ` )) . x = 0 by B3, FUNCOP_1:13;
hence (f | ((ND \/ ND1) ` )) . x = ((X --> 0 ) | ((ND \/ ND1) ` )) . x by B2, B3, B4, FUNCT_1:72; :: thesis: verum

end;

then f | ((ND \/ ND1) ` ) = (X --> 0 ) | ((ND \/ ND1) ` ) by B1, B2, FUNCT_1:def 17;
hence f a.e.= X --> 0 ,M by A8, LPSPACE1:def 10; :: thesis: verum