let X be non empty set ; for S being SigmaField of X
for A being Element of S
for f being V176() PartFunc of X,ExtREAL
for g being V175() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds
f - g is A -measurable
let S be SigmaField of X; for A being Element of S
for f being V176() PartFunc of X,ExtREAL
for g being V175() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds
f - g is A -measurable
let A be Element of S; for f being V176() PartFunc of X,ExtREAL
for g being V175() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds
f - g is A -measurable
let f be V176() PartFunc of X,ExtREAL; for g being V175() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds
f - g is A -measurable
let g be V175() PartFunc of X,ExtREAL; ( f is A -measurable & g is A -measurable & A c= dom (f - g) implies f - g is A -measurable )
assume that
A1:
f is A -measurable
and
A2:
g is A -measurable
and
A3:
A c= dom (f - g)
; f - g is A -measurable
A4:
dom (f - g) = (dom f) /\ (dom g)
by MESFUNC9:2;
( (dom f) /\ (dom g) c= dom f & (dom f) /\ (dom g) c= dom g )
by XBOOLE_1:17;
then
( A c= dom f & A c= dom g )
by A3, A4;
then
- f is A -measurable
by A1, Th59;
then A5:
(- f) + g is A -measurable
by A2, MESFUNC5:31;
( dom f = dom (- f) & dom g = dom (- g) )
by MESFUNC1:def 7;
then
dom ((- f) + g) = (dom f) /\ (dom g)
by MESFUNC5:16;
then
dom ((- f) + g) = dom (f - g)
by MESFUNC9:2;
then
- ((- f) + g) is A -measurable
by A3, A5, Th59;
hence
f - g is A -measurable
by Th60; verum