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

let A be Element of S; :: thesis: ( f is V82() & g is V82() & f is A -measurable & g is A -measurable implies f + g is A -measurable )
assume that
A1: ( f is V82() & g is V82() ) and
A2: ( f is A -measurable & g is A -measurable ) ; :: thesis: f + g is A -measurable
for r being Real holds A /\ (less_dom ((f + g),r)) in S
proof
let r be Real; :: thesis: A /\ (less_dom ((f + g),r)) in S
reconsider r = r as Real ;
consider F being Function of RAT,S such that
A3: for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) by ;
consider G being sequence of S such that
A4: rng F = rng G by ;
A /\ (less_dom ((f + g),r)) = union (rng G) by A1, A3, A4, Th3;
hence A /\ (less_dom ((f + g),r)) in S ; :: thesis: verum
end;
hence f + g is A -measurable ; :: thesis: verum