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
A1: f in Lp_Functions (M,k) and
A2: 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 ND -measurable & (abs h) to_power k is_integrable_on M ) ) by A1;
then consider NDf being Element of S such that
A3: ( M . (NDf `) = 0 & dom f = NDf & f is NDf -measurable & (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:34;
A4: dom t = dom (abs f) by MESFUN6C:def 4;
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 Th14;
then t a.e.= X --> 0,M by A2, A6, LPSPACE1:53;
then consider ND1 being Element of S such that
A7: ( M . ND1 = 0 & ((abs f) to_power k) | (ND1 `) = (X --> 0) | (ND1 `) ) ;
set ND2 = ND \/ ND1;
( ND is measure_zero of M & ND1 is measure_zero of M ) by A3, A7, MEASURE1:def 7;
then ND \/ ND1 is measure_zero of M by MEASURE1:37;
then A8: M . (ND \/ ND1) = 0 by MEASURE1:def 7;
A9: ( (ND \/ ND1) ` c= ND ` & (ND \/ ND1) ` c= ND1 ` ) by XBOOLE_1:7, XBOOLE_1:34;
dom (X --> 0) = X by FUNCOP_1:13;
then A10: dom ((X --> 0) | ((ND \/ ND1) `)) = (ND \/ ND1) ` by RELAT_1:62;
A11: dom (f | ((ND \/ ND1) `)) = (ND \/ ND1) ` by A3, A9, RELAT_1:62;
for x being object st x in dom (f | ((ND \/ ND1) `)) holds
(f | ((ND \/ ND1) `)) . x = ((X --> 0) | ((ND \/ ND1) `)) . x

proof

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

A13: now :: thesis: not f . x <> 0

assume f . x <> 0 ; :: thesis: contradiction
then |.(f . x).| > 0 by COMPLEX1:47;
then |.(f . x).| to_power k <> 0 by POWER:34;
then ((abs f) . x) to_power k <> 0 by VALUED_1:18;
then A14: ((abs f) to_power k) . x <> 0 by A5, A9, A12, A11, MESFUN6C:def 4;
((X --> 0) | (ND1 `)) . x = (X --> 0) . x by A9, A12, A11, FUNCT_1:49;
then ((X --> 0) | (ND1 `)) . x = 0 by A12, FUNCOP_1:7;
hence contradiction by A14, A7, A9, A12, A11, FUNCT_1:49; :: thesis: verum

end;

((X --> 0) | ((ND \/ ND1) `)) . x = (X --> 0) . x by A11, A12, FUNCT_1:49;
then ((X --> 0) | ((ND \/ ND1) `)) . x = 0 by A12, FUNCOP_1:7;
hence (f | ((ND \/ ND1) `)) . x = ((X --> 0) | ((ND \/ ND1) `)) . x by A11, A12, A13, FUNCT_1:49; :: thesis: verum

end;

then f | ((ND \/ ND1) `) = (X --> 0) | ((ND \/ ND1) `) by A10, A11, FUNCT_1:def 11;
hence f a.e.= X --> 0,M by A8; :: thesis: verum