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,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) holds

ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) holds

ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) holds

ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable )

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) implies ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable ) )

assume that

A1: ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) and

A2: ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) ; :: thesis: ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable )

consider E1 being Element of S such that

A3: E1 = dom f and

A4: f is E1 -measurable by A1;

consider E2 being Element of S such that

A5: E2 = dom g and

A6: g is E2 -measurable by A2;

set E3 = E1 /\ E2;

set g1 = g | (E1 /\ E2);

A7: (g | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (g " {-infty}) by FUNCT_1:70;

set f1 = f | (E1 /\ E2);

dom (f | (E1 /\ E2)) = (dom f) /\ (E1 /\ E2) by RELAT_1:61;

then A8: dom (f | (E1 /\ E2)) = E1 /\ E2 by A3, XBOOLE_1:17, XBOOLE_1:28;

g is E1 /\ E2 -measurable by A6, MESFUNC1:30, XBOOLE_1:17;

then A9: g | (E1 /\ E2) is E1 /\ E2 -measurable by Lm6;

A10: (g | (E1 /\ E2)) " {+infty} = (E1 /\ E2) /\ (g " {+infty}) by FUNCT_1:70;

dom (g | (E1 /\ E2)) = (dom g) /\ (E1 /\ E2) by RELAT_1:61;

then A11: dom (g | (E1 /\ E2)) = E1 /\ E2 by A5, XBOOLE_1:17, XBOOLE_1:28;

(f | (E1 /\ E2)) " {+infty} = (E1 /\ E2) /\ (f " {+infty}) by FUNCT_1:70;

then A12: ((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty}) = (f " {+infty}) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {-infty}))) by A7, XBOOLE_1:16

.= (f " {+infty}) /\ (((E1 /\ E2) /\ (E1 /\ E2)) /\ (g " {-infty})) by XBOOLE_1:16

.= ((f " {+infty}) /\ (g " {-infty})) /\ (E1 /\ E2) by XBOOLE_1:16 ;

A13: dom ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) = ((dom (f | (E1 /\ E2))) /\ (dom (g | (E1 /\ E2)))) \ ((((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty})) \/ (((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty}))) by MESFUNC1:def 3;

f is E1 /\ E2 -measurable by A4, MESFUNC1:30, XBOOLE_1:17;

then f | (E1 /\ E2) is E1 /\ E2 -measurable by Lm6;

then consider E being Element of S such that

A14: E = dom ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) and

A15: (f | (E1 /\ E2)) + (g | (E1 /\ E2)) is E -measurable by A9, A8, A11, Lm7;

take E ; :: thesis: ( E = dom (f + g) & f + g is E -measurable )

A16: dom ((f + g) | E) = (dom (f + g)) /\ E by RELAT_1:61;

(f | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (f " {-infty}) by FUNCT_1:70;

then ((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty}) = (f " {-infty}) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {+infty}))) by A10, XBOOLE_1:16

.= (f " {-infty}) /\ (((E1 /\ E2) /\ (E1 /\ E2)) /\ (g " {+infty})) by XBOOLE_1:16

.= ((f " {-infty}) /\ (g " {+infty})) /\ (E1 /\ E2) by XBOOLE_1:16 ;

then A17: (((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty})) \/ (((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty})) = (E1 /\ E2) /\ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by A12, XBOOLE_1:23;

A18: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;

then A19: dom (f + g) = E by A3, A5, A8, A11, A14, A13, A17, XBOOLE_1:47;

hence ( E = dom (f + g) & f + g is E -measurable ) by A3, A5, A8, A11, A14, A15, A13, A17, A18, Lm6, XBOOLE_1:47; :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) holds

ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) holds

ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) holds

ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable )

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) implies ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable ) )

assume that

A1: ex E1 being Element of S st

( E1 = dom f & f is E1 -measurable ) and

A2: ex E2 being Element of S st

( E2 = dom g & g is E2 -measurable ) ; :: thesis: ex E being Element of S st

( E = dom (f + g) & f + g is E -measurable )

consider E1 being Element of S such that

A3: E1 = dom f and

A4: f is E1 -measurable by A1;

consider E2 being Element of S such that

A5: E2 = dom g and

A6: g is E2 -measurable by A2;

set E3 = E1 /\ E2;

set g1 = g | (E1 /\ E2);

A7: (g | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (g " {-infty}) by FUNCT_1:70;

set f1 = f | (E1 /\ E2);

dom (f | (E1 /\ E2)) = (dom f) /\ (E1 /\ E2) by RELAT_1:61;

then A8: dom (f | (E1 /\ E2)) = E1 /\ E2 by A3, XBOOLE_1:17, XBOOLE_1:28;

g is E1 /\ E2 -measurable by A6, MESFUNC1:30, XBOOLE_1:17;

then A9: g | (E1 /\ E2) is E1 /\ E2 -measurable by Lm6;

A10: (g | (E1 /\ E2)) " {+infty} = (E1 /\ E2) /\ (g " {+infty}) by FUNCT_1:70;

dom (g | (E1 /\ E2)) = (dom g) /\ (E1 /\ E2) by RELAT_1:61;

then A11: dom (g | (E1 /\ E2)) = E1 /\ E2 by A5, XBOOLE_1:17, XBOOLE_1:28;

(f | (E1 /\ E2)) " {+infty} = (E1 /\ E2) /\ (f " {+infty}) by FUNCT_1:70;

then A12: ((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty}) = (f " {+infty}) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {-infty}))) by A7, XBOOLE_1:16

.= (f " {+infty}) /\ (((E1 /\ E2) /\ (E1 /\ E2)) /\ (g " {-infty})) by XBOOLE_1:16

.= ((f " {+infty}) /\ (g " {-infty})) /\ (E1 /\ E2) by XBOOLE_1:16 ;

A13: dom ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) = ((dom (f | (E1 /\ E2))) /\ (dom (g | (E1 /\ E2)))) \ ((((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty})) \/ (((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty}))) by MESFUNC1:def 3;

f is E1 /\ E2 -measurable by A4, MESFUNC1:30, XBOOLE_1:17;

then f | (E1 /\ E2) is E1 /\ E2 -measurable by Lm6;

then consider E being Element of S such that

A14: E = dom ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) and

A15: (f | (E1 /\ E2)) + (g | (E1 /\ E2)) is E -measurable by A9, A8, A11, Lm7;

take E ; :: thesis: ( E = dom (f + g) & f + g is E -measurable )

A16: dom ((f + g) | E) = (dom (f + g)) /\ E by RELAT_1:61;

(f | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (f " {-infty}) by FUNCT_1:70;

then ((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty}) = (f " {-infty}) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {+infty}))) by A10, XBOOLE_1:16

.= (f " {-infty}) /\ (((E1 /\ E2) /\ (E1 /\ E2)) /\ (g " {+infty})) by XBOOLE_1:16

.= ((f " {-infty}) /\ (g " {+infty})) /\ (E1 /\ E2) by XBOOLE_1:16 ;

then A17: (((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty})) \/ (((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty})) = (E1 /\ E2) /\ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by A12, XBOOLE_1:23;

A18: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;

then A19: dom (f + g) = E by A3, A5, A8, A11, A14, A13, A17, XBOOLE_1:47;

now :: thesis: for v being Element of X st v in dom ((f + g) | E) holds

((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v

then
(f + g) | E = (f | (E1 /\ E2)) + (g | (E1 /\ E2))
by A14, A19, A16, PARTFUN1:5;((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v

let v be Element of X; :: thesis: ( v in dom ((f + g) | E) implies ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v )

assume A20: v in dom ((f + g) | E) ; :: thesis: ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v

then A21: v in (dom (f + g)) /\ E by RELAT_1:61;

then A22: v in dom (f + g) by XBOOLE_0:def 4;

A23: ((f + g) | E) . v = (f + g) . v by A20, FUNCT_1:47

.= (f . v) + (g . v) by A22, MESFUNC1:def 3 ;

A24: v in E by A21, XBOOLE_0:def 4;

A25: E c= E1 /\ E2 by A8, A11, A14, A13, XBOOLE_1:36;

((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v = ((f | (E1 /\ E2)) . v) + ((g | (E1 /\ E2)) . v) by A14, A19, A16, A20, MESFUNC1:def 3

.= (f . v) + ((g | (E1 /\ E2)) . v) by A8, A24, A25, FUNCT_1:47 ;

hence ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v by A11, A24, A25, A23, FUNCT_1:47; :: thesis: verum

end;assume A20: v in dom ((f + g) | E) ; :: thesis: ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v

then A21: v in (dom (f + g)) /\ E by RELAT_1:61;

then A22: v in dom (f + g) by XBOOLE_0:def 4;

A23: ((f + g) | E) . v = (f + g) . v by A20, FUNCT_1:47

.= (f . v) + (g . v) by A22, MESFUNC1:def 3 ;

A24: v in E by A21, XBOOLE_0:def 4;

A25: E c= E1 /\ E2 by A8, A11, A14, A13, XBOOLE_1:36;

((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v = ((f | (E1 /\ E2)) . v) + ((g | (E1 /\ E2)) . v) by A14, A19, A16, A20, MESFUNC1:def 3

.= (f . v) + ((g | (E1 /\ E2)) . v) by A8, A24, A25, FUNCT_1:47 ;

hence ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v by A11, A24, A25, A23, FUNCT_1:47; :: thesis: verum

hence ( E = dom (f + g) & f + g is E -measurable ) by A3, A5, A8, A11, A14, A15, A13, A17, A18, Lm6, XBOOLE_1:47; :: thesis: verum