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 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum