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,COMPLEX
for x being Point of (Pre-L-CSpace M) st f in x & g in x holds
( f a.e.cpfunc= 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,COMPLEX
for x being Point of (Pre-L-CSpace M) st f in x & g in x holds
( f a.e.cpfunc= 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,COMPLEX
for x being Point of (Pre-L-CSpace M) st f in x & g in x holds
( f a.e.cpfunc= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
let f, g be PartFunc of X,COMPLEX; :: thesis: for x being Point of (Pre-L-CSpace M) st f in x & g in x holds
( f a.e.cpfunc= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
let x be Point of (Pre-L-CSpace M); :: thesis: ( f in x & g in x implies ( f a.e.cpfunc= 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.cpfunc= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
A3: g in L1_CFunctions M by A2, Th39;
( f a.e.cpfunc= g,M & f in L1_CFunctions M ) by A1, A2, Th39;
hence ( f a.e.cpfunc= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) ) by A3, Th36, Th38; :: thesis: verum