theorem
for
X being non
empty set for
S being
SigmaField of
X for
M being
sigma_Measure of
S for
f,
g,
f1,
g1 being
PartFunc of
X,
REAL for
k being
positive Real st ex
E being
Element of
S st
(
M . (E `) = 0 &
E = dom f &
f is
E -measurable ) & ex
E being
Element of
S st
(
M . (E `) = 0 &
E = dom f1 &
f1 is
E -measurable ) & ex
E being
Element of
S st
(
M . (E `) = 0 &
E = dom g &
g is
E -measurable ) & ex
E being
Element of
S st
(
M . (E `) = 0 &
E = dom g1 &
g1 is
E -measurable ) & not
a.e-eq-class_Lp (
f,
M,
k) is
empty & not
a.e-eq-class_Lp (
g,
M,
k) is
empty &
a.e-eq-class_Lp (
f,
M,
k)
= a.e-eq-class_Lp (
f1,
M,
k) &
a.e-eq-class_Lp (
g,
M,
k)
= a.e-eq-class_Lp (
g1,
M,
k) holds
a.e-eq-class_Lp (
(f + g),
M,
k)
= a.e-eq-class_Lp (
(f1 + g1),
M,
k)