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 real-valued & g is real-valued & 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 real-valued & g is real-valued & 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 real-valued & g is real-valued & 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 real-valued & g is real-valued & f is_measurable_on A & g is_measurable_on A implies f + g is_measurable_on A )
assume that
A1: ( f is real-valued & g is real-valued ) and
A2: ( f is_measurable_on A & 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
A3: for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A2, Th6;
consider G being Function of NAT,S such that
A4: rng F = rng G by Th5, MESFUNC1:5;
A /\ (less_dom ((f + g),(R_EAL r))) = union (rng G) by A1, A3, A4, Th3;
hence A /\ (less_dom ((f + g),(R_EAL r))) in S ; :: thesis: verum

end;

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