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