let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is without-infty & g is without-infty & f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is without-infty & g is without-infty & f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let f, g be PartFunc of X,ExtREAL ; :: thesis: for A being Element of S st f is without-infty & g is without-infty & f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let A be Element of S; :: thesis: ( f is without-infty & g is without-infty & f is_measurable_on A & g is_measurable_on A implies f + g is_measurable_on A )
assume that
A1: f is without-infty and
A2: g is without-infty and
A3: f is_measurable_on A and
A4: g is_measurable_on A ; :: thesis: f + g is_measurable_on A
for r being real number holds A /\ (less_dom (f + g),(R_EAL r)) in S

proof

let r be real number ; :: thesis: A /\ (less_dom (f + g),(R_EAL r)) in S
reconsider r = r as Real by XREAL_0:def 1;
consider F being Function of RAT ,S such that
A5: for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) by A3, A4, MESFUNC2:6;
ex G being Function of NAT ,S st rng F = rng G by MESFUNC1:5, MESFUNC2:5;
then A6: rng F is N_Sub_set_fam of X by MEASURE1:52;
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F) by A1, A2, A5, Th24;
hence A /\ (less_dom (f + g),(R_EAL r)) in S by A6, MEASURE1:def 9; :: thesis: verum

end;

hence f + g is_measurable_on A by MESFUNC1:def 17; :: thesis: verum