let X be non empty set ; 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; 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; 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; ( 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 )
; f + g is A -measurable
for r being Real holds A /\ (less_dom ((f + g),r)) in S
proof
let r be
Real;
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 A2, Th6;
consider G being
sequence of
S such that A4:
rng F = rng G
by Th5, MESFUNC1:5;
A /\ (less_dom ((f + g),r)) = union (rng G)
by A1, A3, A4, Th3;
hence
A /\ (less_dom ((f + g),r)) in S
;
verum
end;
hence
f + g is A -measurable
; verum