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 f a.e.= g,M holds

a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,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 f a.e.= g,M holds

a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL

for k being positive Real st f a.e.= g,M holds

a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)

let f, g be PartFunc of X,REAL; :: thesis: for k being positive Real st f a.e.= g,M holds

a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)

let k be positive Real; :: thesis: ( f a.e.= g,M implies a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) )

assume A1: f a.e.= g,M ; :: thesis: a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)

hence a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) by A3; :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL

for k being positive Real st f a.e.= g,M holds

a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,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 f a.e.= g,M holds

a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL

for k being positive Real st f a.e.= g,M holds

a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)

let f, g be PartFunc of X,REAL; :: thesis: for k being positive Real st f a.e.= g,M holds

a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)

let k be positive Real; :: thesis: ( f a.e.= g,M implies a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) )

assume A1: f a.e.= g,M ; :: thesis: a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k)

now :: thesis: for x being object st x in a.e-eq-class_Lp (f,M,k) holds

x in a.e-eq-class_Lp (g,M,k)

then A3:
a.e-eq-class_Lp (f,M,k) c= a.e-eq-class_Lp (g,M,k)
;x in a.e-eq-class_Lp (g,M,k)

let x be object ; :: thesis: ( x in a.e-eq-class_Lp (f,M,k) implies x in a.e-eq-class_Lp (g,M,k) )

assume x in a.e-eq-class_Lp (f,M,k) ; :: thesis: x in a.e-eq-class_Lp (g,M,k)

then consider r being PartFunc of X,REAL such that

A2: ( x = r & r in Lp_Functions (M,k) & f a.e.= r,M ) ;

r a.e.= f,M by A2;

then r a.e.= g,M by A1, LPSPACE1:30;

then g a.e.= r,M ;

hence x in a.e-eq-class_Lp (g,M,k) by A2; :: thesis: verum

end;assume x in a.e-eq-class_Lp (f,M,k) ; :: thesis: x in a.e-eq-class_Lp (g,M,k)

then consider r being PartFunc of X,REAL such that

A2: ( x = r & r in Lp_Functions (M,k) & f a.e.= r,M ) ;

r a.e.= f,M by A2;

then r a.e.= g,M by A1, LPSPACE1:30;

then g a.e.= r,M ;

hence x in a.e-eq-class_Lp (g,M,k) by A2; :: thesis: verum

now :: thesis: for x being object st x in a.e-eq-class_Lp (g,M,k) holds

x in a.e-eq-class_Lp (f,M,k)

then
a.e-eq-class_Lp (g,M,k) c= a.e-eq-class_Lp (f,M,k)
;x in a.e-eq-class_Lp (f,M,k)

let x be object ; :: thesis: ( x in a.e-eq-class_Lp (g,M,k) implies x in a.e-eq-class_Lp (f,M,k) )

assume x in a.e-eq-class_Lp (g,M,k) ; :: thesis: x in a.e-eq-class_Lp (f,M,k)

then consider r being PartFunc of X,REAL such that

A4: ( x = r & r in Lp_Functions (M,k) & g a.e.= r,M ) ;

( r a.e.= g,M & g a.e.= f,M ) by A1, A4;

then r a.e.= f,M by LPSPACE1:30;

then f a.e.= r,M ;

hence x in a.e-eq-class_Lp (f,M,k) by A4; :: thesis: verum

end;assume x in a.e-eq-class_Lp (g,M,k) ; :: thesis: x in a.e-eq-class_Lp (f,M,k)

then consider r being PartFunc of X,REAL such that

A4: ( x = r & r in Lp_Functions (M,k) & g a.e.= r,M ) ;

( r a.e.= g,M & g a.e.= f,M ) by A1, A4;

then r a.e.= f,M by LPSPACE1:30;

then f a.e.= r,M ;

hence x in a.e-eq-class_Lp (f,M,k) by A4; :: thesis: verum

hence a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) by A3; :: thesis: verum