let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

( max+ f is_simple_func_in S & max- f is_simple_func_in S )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

( max+ f is_simple_func_in S & max- f is_simple_func_in S )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

( max+ f is_simple_func_in S & max- f is_simple_func_in S )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S implies ( max+ f is_simple_func_in S & max- f is_simple_func_in S ) )

assume A1: f is_simple_func_in S ; :: thesis: ( max+ f is_simple_func_in S & max- f is_simple_func_in S )

then A2: f is V55() by MESFUNC2:def 4;

consider F being Finite_Sep_Sequence of S such that

A3: dom f = union (rng F) and

A4: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y by A1, MESFUNC2:def 4;

A5: dom (max+ f) = union (rng F) by A3, MESFUNC2:def 2;

for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(max+ f) . x = (max+ f) . y

A9: dom (max- f) = union (rng F) by A3, MESFUNC2:def 3;

for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(max- f) . x = (max- f) . y

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

( max+ f is_simple_func_in S & max- f is_simple_func_in S )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

( max+ f is_simple_func_in S & max- f is_simple_func_in S )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

( max+ f is_simple_func_in S & max- f is_simple_func_in S )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S implies ( max+ f is_simple_func_in S & max- f is_simple_func_in S ) )

assume A1: f is_simple_func_in S ; :: thesis: ( max+ f is_simple_func_in S & max- f is_simple_func_in S )

then A2: f is V55() by MESFUNC2:def 4;

consider F being Finite_Sep_Sequence of S such that

A3: dom f = union (rng F) and

A4: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y by A1, MESFUNC2:def 4;

A5: dom (max+ f) = union (rng F) by A3, MESFUNC2:def 2;

for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(max+ f) . x = (max+ f) . y

proof

hence
max+ f is_simple_func_in S
by A2, A5, Th2, MESFUNC2:def 4; :: thesis: max- f is_simple_func_in S
let n be Nat; :: thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(max+ f) . x = (max+ f) . y

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies (max+ f) . x = (max+ f) . y )

assume that

A6: n in dom F and

A7: x in F . n and

A8: y in F . n ; :: thesis: (max+ f) . x = (max+ f) . y

F . n in rng F by A6, FUNCT_1:3;

then ( x in dom (max+ f) & y in dom (max+ f) ) by A5, A7, A8, TARSKI:def 4;

then ( (max+ f) . x = max ((f . x),0) & (max+ f) . y = max ((f . y),0) ) by MESFUNC2:def 2;

hence (max+ f) . x = (max+ f) . y by A4, A6, A7, A8; :: thesis: verum

end;(max+ f) . x = (max+ f) . y

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies (max+ f) . x = (max+ f) . y )

assume that

A6: n in dom F and

A7: x in F . n and

A8: y in F . n ; :: thesis: (max+ f) . x = (max+ f) . y

F . n in rng F by A6, FUNCT_1:3;

then ( x in dom (max+ f) & y in dom (max+ f) ) by A5, A7, A8, TARSKI:def 4;

then ( (max+ f) . x = max ((f . x),0) & (max+ f) . y = max ((f . y),0) ) by MESFUNC2:def 2;

hence (max+ f) . x = (max+ f) . y by A4, A6, A7, A8; :: thesis: verum

A9: dom (max- f) = union (rng F) by A3, MESFUNC2:def 3;

for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(max- f) . x = (max- f) . y

proof

hence
max- f is_simple_func_in S
by A2, A9, Th2, MESFUNC2:def 4; :: thesis: verum
let n be Nat; :: thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(max- f) . x = (max- f) . y

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies (max- f) . x = (max- f) . y )

assume that

A10: n in dom F and

A11: x in F . n and

A12: y in F . n ; :: thesis: (max- f) . x = (max- f) . y

F . n in rng F by A10, FUNCT_1:3;

then ( x in dom (max- f) & y in dom (max- f) ) by A9, A11, A12, TARSKI:def 4;

then ( (max- f) . x = max ((- (f . x)),0) & (max- f) . y = max ((- (f . y)),0) ) by MESFUNC2:def 3;

hence (max- f) . x = (max- f) . y by A4, A10, A11, A12; :: thesis: verum

end;(max- f) . x = (max- f) . y

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies (max- f) . x = (max- f) . y )

assume that

A10: n in dom F and

A11: x in F . n and

A12: y in F . n ; :: thesis: (max- f) . x = (max- f) . y

F . n in rng F by A10, FUNCT_1:3;

then ( x in dom (max- f) & y in dom (max- f) ) by A9, A11, A12, TARSKI:def 4;

then ( (max- f) . x = max ((- (f . x)),0) & (max- f) . y = max ((- (f . y)),0) ) by MESFUNC2:def 3;

hence (max- f) . x = (max- f) . y by A4, A10, A11, A12; :: thesis: verum