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

f a.e.= g, COM M

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f a.e.= g,M holds

f a.e.= g, COM M

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

f a.e.= g, COM M

let f, g be PartFunc of X,REAL; :: thesis: ( f a.e.= g,M implies f a.e.= g, COM M )

assume f a.e.= g,M ; :: thesis: f a.e.= g, COM M

then consider E being Element of S such that

A1: ( M . E = 0 & f | (E `) = g | (E `) ) by LPSPACE1:def 10;

reconsider E0 = {} as Element of S by MEASURE1:7;

M . E0 = 0 by VALUED_0:def 19;

then A2: E0 is thin of M by MEASURE3:def 2;

A3: E = E \/ E0 ;

reconsider E1 = E as Element of COM (S,M) by Th27;

(COM M) . E1 = 0 by A1, A2, A3, MEASURE3:def 5;

hence f a.e.= g, COM M by A1, LPSPACE1:def 10; :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f a.e.= g,M holds

f a.e.= g, COM M

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f a.e.= g,M holds

f a.e.= g, COM M

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

f a.e.= g, COM M

let f, g be PartFunc of X,REAL; :: thesis: ( f a.e.= g,M implies f a.e.= g, COM M )

assume f a.e.= g,M ; :: thesis: f a.e.= g, COM M

then consider E being Element of S such that

A1: ( M . E = 0 & f | (E `) = g | (E `) ) by LPSPACE1:def 10;

reconsider E0 = {} as Element of S by MEASURE1:7;

M . E0 = 0 by VALUED_0:def 19;

then A2: E0 is thin of M by MEASURE3:def 2;

A3: E = E \/ E0 ;

reconsider E1 = E as Element of COM (S,M) by Th27;

(COM M) . E1 = 0 by A1, A2, A3, MEASURE3:def 5;

hence f a.e.= g, COM M by A1, LPSPACE1:def 10; :: thesis: verum