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 & A c= dom g 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 & A c= dom g 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 & A c= dom g 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 & A c= dom g implies f - g is A -measurable )
assume that
A1:
f is V82()
and
A2:
g is V82()
and
A3:
f is A -measurable
and
A4:
( g is A -measurable & A c= dom g )
; f - g is A -measurable
A5:
(- 1) (#) g is V82()
by A2, Th10;
A6:
(- 1) (#) g is A -measurable
by A4, MESFUNC1:37;
A7:
- g is V82()
by A5, Th9;
- g is A -measurable
by A6, Th9;
then
f + (- g) is A -measurable
by A1, A3, A7, Th7;
hence
f - g is A -measurable
by Th8; verum