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 () & g is () & f is A -measurable & g is A -measurable holds

f + g is A -measurable

let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is () & g is () & f is A -measurable & g is A -measurable holds

f + g is A -measurable

let f, g be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st f is () & g is () & f is A -measurable & g is A -measurable holds

f + g is A -measurable

let A be Element of S; :: thesis: ( f is () & g is () & f is A -measurable & g is A -measurable implies f + g is A -measurable )

assume that

A1: f is () and

A2: g is () and

A3: f is A -measurable and

A4: g is A -measurable ; :: thesis: f + g is A -measurable

for r being Real holds A /\ (less_dom ((f + g),r)) in S

for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is () & g is () & f is A -measurable & g is A -measurable holds

f + g is A -measurable

let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is () & g is () & f is A -measurable & g is A -measurable holds

f + g is A -measurable

let f, g be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st f is () & g is () & f is A -measurable & g is A -measurable holds

f + g is A -measurable

let A be Element of S; :: thesis: ( f is () & g is () & f is A -measurable & g is A -measurable implies f + g is A -measurable )

assume that

A1: f is () and

A2: g is () and

A3: f is A -measurable and

A4: g is A -measurable ; :: thesis: f + g is A -measurable

for r being Real holds A /\ (less_dom ((f + g),r)) in S

proof

hence
f + g is A -measurable
by MESFUNC1:def 16; :: thesis: verum
let r be Real; :: thesis: A /\ (less_dom ((f + g),r)) in S

consider F being Function of RAT,S such that

A5: for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) by A3, A4, MESFUNC2:6;

ex G being sequence of S st rng F = rng G by MESFUNC1:5, MESFUNC2:5;

then A6: rng F is N_Sub_set_fam of X by MEASURE1:23;

A /\ (less_dom ((f + g),r)) = union (rng F) by A1, A2, A5, Th18;

hence A /\ (less_dom ((f + g),r)) in S by A6, MEASURE1:def 5; :: thesis: verum

end;consider F being Function of RAT,S such that

A5: for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) by A3, A4, MESFUNC2:6;

ex G being sequence of S st rng F = rng G by MESFUNC1:5, MESFUNC2:5;

then A6: rng F is N_Sub_set_fam of X by MEASURE1:23;

A /\ (less_dom ((f + g),r)) = union (rng F) by A1, A2, A5, Th18;

hence A /\ (less_dom ((f + g),r)) in S by A6, MEASURE1:def 5; :: thesis: verum