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 Th50;

hence ( f a.e.= g,M & Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k)) ) by Th48; :: thesis: verum

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 Th50;

hence ( f a.e.= g,M & Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k)) ) by Th48; :: thesis: verum