let X be non empty set ; 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 ex x being VECTOR of (Pre-Lp-Space (M,k)) st
( f in x & g in x ) holds
( f a.e.= g,M & f in Lp_Functions (M,k) & g in Lp_Functions (M,k) )
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st ex x being VECTOR of (Pre-Lp-Space (M,k)) st
( f in x & g in x ) holds
( f a.e.= g,M & f in Lp_Functions (M,k) & g in Lp_Functions (M,k) )
let M be sigma_Measure of S; for f, g being PartFunc of X,REAL
for k being positive Real st ex x being VECTOR of (Pre-Lp-Space (M,k)) st
( f in x & g in x ) holds
( f a.e.= g,M & f in Lp_Functions (M,k) & g in Lp_Functions (M,k) )
let f, g be PartFunc of X,REAL; for k being positive Real st ex x being VECTOR of (Pre-Lp-Space (M,k)) st
( f in x & g in x ) holds
( f a.e.= g,M & f in Lp_Functions (M,k) & g in Lp_Functions (M,k) )
let k be positive Real; ( ex x being VECTOR of (Pre-Lp-Space (M,k)) st
( f in x & g in x ) implies ( f a.e.= g,M & f in Lp_Functions (M,k) & g in Lp_Functions (M,k) ) )
assume
ex x being VECTOR of (Pre-Lp-Space (M,k)) st
( f in x & g in x )
; ( f a.e.= g,M & f in Lp_Functions (M,k) & g in Lp_Functions (M,k) )
then consider x being VECTOR of (Pre-Lp-Space (M,k)) such that
A1:
( f in x & g in x )
;
x in the carrier of (Pre-Lp-Space (M,k))
;
then
x in CosetSet (M,k)
by Def11;
then consider h being PartFunc of X,REAL such that
A2:
( x = a.e-eq-class_Lp (h,M,k) & h in Lp_Functions (M,k) )
;
( ex i being PartFunc of X,REAL st
( f = i & i in Lp_Functions (M,k) & h a.e.= i,M ) & ex j being PartFunc of X,REAL st
( g = j & j in Lp_Functions (M,k) & h a.e.= j,M ) )
by A1, A2;
then
( f a.e.= h,M & h a.e.= g,M )
;
hence
( f a.e.= g,M & f in Lp_Functions (M,k) & g in Lp_Functions (M,k) )
by A1, A2, LPSPACE1:30; verum