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 that
A1: f in x and
A2: g in x ; :: thesis: ( f a.e.= g,M & Integral M,f = Integral M,g & Integral M,(abs f) = Integral M,(abs g) )
A3: g in L1_Functions M by A2, Th46;
( f a.e.= g,M & f in L1_Functions M ) by A1, A2, Th46;
hence ( f a.e.= g,M & Integral M,f = Integral M,g & Integral M,(abs f) = Integral M,(abs g) ) by A3, Th43, Th45; :: thesis: verum