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
for x being Point of (Pre-Lp-Space M,k) st f in x & g in x holds
( f a.e.= g,M & 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
for x being Point of (Pre-Lp-Space M,k) st f in x & g in x holds
( f a.e.= g,M & 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
for x being Point of (Pre-Lp-Space M,k) st f in x & g in x holds
( f a.e.= g,M & 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
for x being Point of (Pre-Lp-Space M,k) st f in x & g in x holds
( f a.e.= g,M & Integral M,((abs f) to_power k) = Integral M,((abs g) to_power k) )
let k be positive Real; :: thesis: for x being Point of (Pre-Lp-Space M,k) st f in x & g in x holds
( f a.e.= g,M & Integral M,((abs f) to_power k) = Integral M,((abs g) to_power k) )
let x be Point of (Pre-Lp-Space M,k); :: thesis: ( f in x & g in x implies ( f a.e.= g,M & Integral M,((abs f) to_power k) = Integral M,((abs g) to_power k) ) )
assume ( f in x & g in x ) ; :: thesis: ( f a.e.= g,M & Integral M,((abs f) to_power k) = Integral M,((abs g) to_power k) )
then ( f a.e.= g,M & f in Lp_Functions M,k & g in Lp_Functions M,k ) by Lm10;
hence ( f a.e.= g,M & Integral M,((abs f) to_power k) = Integral M,((abs g) to_power k) ) by Th14; :: thesis: verum