let X be non empty set ; 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; 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; 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; 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); ( 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
; ( 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; verum