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 x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral M,f = Integral M,g & Integral M,(abs f) = Integral M,(abs g) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral M,f = Integral M,g & Integral M,(abs f) = Integral M,(abs g) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral M,f = Integral M,g & Integral M,(abs f) = Integral M,(abs g) )
let f, g be PartFunc of X,REAL ; :: thesis: for x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral M,f = Integral M,g & Integral M,(abs f) = Integral M,(abs g) )
let x be Point of (Pre-L-Space M); :: thesis: ( f in x & g in x implies ( f a.e.= g,M & Integral M,f = Integral M,g & Integral M,(abs f) = Integral M,(abs g) ) )
assume ( f in x & g in x ) ; :: thesis: ( f a.e.= g,M & Integral M,f = Integral M,g & Integral M,(abs f) = Integral M,(abs g) )
then ( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M ) by Lm10;
hence ( f a.e.= g,M & Integral M,f = Integral M,g & Integral M,(abs f) = Integral M,(abs g) ) by Th14, Th14a; :: thesis: verum