let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum