let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds
f - g is_simple_func_in S
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds
f - g is_simple_func_in S
let M be sigma_Measure of S; for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds
f - g is_simple_func_in S
let f, g be PartFunc of X,ExtREAL; ( f is_simple_func_in S & g is_simple_func_in S implies f - g is_simple_func_in S )
assume that
A1:
f is_simple_func_in S
and
A4:
g is_simple_func_in S
; f - g is_simple_func_in S
(- 1) (#) g is_simple_func_in S
by A4, MESFUNC5:39;
then
- g is_simple_func_in S
by MESFUNC2:9;
then
f + (- g) is_simple_func_in S
by A1, Th28;
then
- (g - f) is_simple_func_in S
by MEASUR11:64;
hence
f - g is_simple_func_in S
by MEASUR11:64; verum