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

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 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

A2: g is_simple_func_in S ; :: thesis: f + g is_simple_func_in 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 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

A2: g is_simple_func_in S ; :: thesis: f + g is_simple_func_in S

per cases
( dom (f + g) = {} or dom (f + g) <> {} )
;

end;

suppose A3:
dom (f + g) = {}
; :: thesis: f + g is_simple_func_in S

reconsider EMPTY = {} as Element of S by PROB_1:4;

set F = <*EMPTY*>;

A4: dom <*EMPTY*> = Seg 1 by FINSEQ_1:38;

<*EMPTY*> . n = EMPTY

union (rng F) = union (bool {}) by FINSEQ_1:39, ZFMISC_1:1;

then A10: dom (f + g) = union (rng F) by A3, ZFMISC_1:81;

for x being Element of X st x in dom (f + g) holds

|.((f + g) . x).| < +infty by A3;

then A11: f + g is real-valued by MESFUNC2:def 1;

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 + g) . x = (f + g) . y by A9;

hence f + g is_simple_func_in S by A11, A10, MESFUNC2:def 4; :: thesis: verum

end;set F = <*EMPTY*>;

A4: dom <*EMPTY*> = Seg 1 by FINSEQ_1:38;

A5: now :: thesis: for i, j being Nat st i in dom <*EMPTY*> & j in dom <*EMPTY*> & i <> j holds

<*EMPTY*> . i misses <*EMPTY*> . j

A9:
for n being Nat st n in dom <*EMPTY*> holds <*EMPTY*> . i misses <*EMPTY*> . j

let i, j be Nat; :: thesis: ( i in dom <*EMPTY*> & j in dom <*EMPTY*> & i <> j implies <*EMPTY*> . i misses <*EMPTY*> . j )

assume that

A6: i in dom <*EMPTY*> and

A7: j in dom <*EMPTY*> and

A8: i <> j ; :: thesis: <*EMPTY*> . i misses <*EMPTY*> . j

i = 1 by A4, A6, FINSEQ_1:2, TARSKI:def 1;

hence <*EMPTY*> . i misses <*EMPTY*> . j by A4, A7, A8, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;assume that

A6: i in dom <*EMPTY*> and

A7: j in dom <*EMPTY*> and

A8: i <> j ; :: thesis: <*EMPTY*> . i misses <*EMPTY*> . j

i = 1 by A4, A6, FINSEQ_1:2, TARSKI:def 1;

hence <*EMPTY*> . i misses <*EMPTY*> . j by A4, A7, A8, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

<*EMPTY*> . n = EMPTY

proof

reconsider F = <*EMPTY*> as Finite_Sep_Sequence of S by A5, MESFUNC3:4;
let n be Nat; :: thesis: ( n in dom <*EMPTY*> implies <*EMPTY*> . n = EMPTY )

assume n in dom <*EMPTY*> ; :: thesis: <*EMPTY*> . n = EMPTY

then n = 1 by A4, FINSEQ_1:2, TARSKI:def 1;

hence <*EMPTY*> . n = EMPTY by FINSEQ_1:40; :: thesis: verum

end;assume n in dom <*EMPTY*> ; :: thesis: <*EMPTY*> . n = EMPTY

then n = 1 by A4, FINSEQ_1:2, TARSKI:def 1;

hence <*EMPTY*> . n = EMPTY by FINSEQ_1:40; :: thesis: verum

union (rng F) = union (bool {}) by FINSEQ_1:39, ZFMISC_1:1;

then A10: dom (f + g) = union (rng F) by A3, ZFMISC_1:81;

for x being Element of X st x in dom (f + g) holds

|.((f + g) . x).| < +infty by A3;

then A11: f + g is real-valued by MESFUNC2:def 1;

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 + g) . x = (f + g) . y by A9;

hence f + g is_simple_func_in S by A11, A10, MESFUNC2:def 4; :: thesis: verum

suppose A12:
dom (f + g) <> {}
; :: thesis: f + g is_simple_func_in S

A13:
(f | (dom (f + g))) " {+infty} = (dom (f + g)) /\ (f " {+infty})
by FUNCT_1:70;

g is () by A2, Th14;

then not +infty in rng g ;

then A14: g " {+infty} = {} by FUNCT_1:72;

A15: (g | (dom (f + g))) " {+infty} = (dom (f + g)) /\ (g " {+infty}) by FUNCT_1:70;

f is () by A1, Th14;

then not +infty in rng f ;

then A16: f " {+infty} = {} by FUNCT_1:72;

then A17: ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty}))) = (dom f) /\ (dom g) by A14;

then A18: dom (f + g) = (dom f) /\ (dom g) by MESFUNC1:def 3;

dom (f | (dom (f + g))) = (dom f) /\ (dom (f + g)) by RELAT_1:61;

then A19: dom (f | (dom (f + g))) = ((dom f) /\ (dom f)) /\ (dom g) by A18, XBOOLE_1:16;

then A20: dom (f | (dom (f + g))) = dom (f + g) by A17, MESFUNC1:def 3;

A21: dom g is Element of S by A2, Th37;

dom f is Element of S by A1, Th37;

then A22: dom (f + g) in S by A18, A21, FINSUB_1:def 2;

then A23: g | (dom (f + g)) is_simple_func_in S by A2, Th34;

dom (g | (dom (f + g))) = (dom g) /\ (dom (f + g)) by RELAT_1:61;

then A24: dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) by A18, XBOOLE_1:16;

then A25: dom (g | (dom (f + g))) = dom (f + g) by A17, MESFUNC1:def 3;

A26: dom ((f | (dom (f + g))) + (g | (dom (f + g)))) = ((dom (f | (dom (f + g)))) /\ (dom (g | (dom (f + g))))) \ ((((f | (dom (f + g))) " {+infty}) /\ ((g | (dom (f + g))) " {-infty})) \/ (((f | (dom (f + g))) " {-infty}) /\ ((g | (dom (f + g))) " {+infty}))) by MESFUNC1:def 3

.= dom (f + g) by A16, A14, A17, A19, A24, A13, A15, MESFUNC1:def 3 ;

A27: for x being Element of X st x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) holds

((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x

then (f | (dom (f + g))) + (g | (dom (f + g))) is_simple_func_in S by A12, A23, A20, A25, Lm3;

hence f + g is_simple_func_in S by A26, A27, PARTFUN1:5; :: thesis: verum

end;g is () by A2, Th14;

then not +infty in rng g ;

then A14: g " {+infty} = {} by FUNCT_1:72;

A15: (g | (dom (f + g))) " {+infty} = (dom (f + g)) /\ (g " {+infty}) by FUNCT_1:70;

f is () by A1, Th14;

then not +infty in rng f ;

then A16: f " {+infty} = {} by FUNCT_1:72;

then A17: ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty}))) = (dom f) /\ (dom g) by A14;

then A18: dom (f + g) = (dom f) /\ (dom g) by MESFUNC1:def 3;

dom (f | (dom (f + g))) = (dom f) /\ (dom (f + g)) by RELAT_1:61;

then A19: dom (f | (dom (f + g))) = ((dom f) /\ (dom f)) /\ (dom g) by A18, XBOOLE_1:16;

then A20: dom (f | (dom (f + g))) = dom (f + g) by A17, MESFUNC1:def 3;

A21: dom g is Element of S by A2, Th37;

dom f is Element of S by A1, Th37;

then A22: dom (f + g) in S by A18, A21, FINSUB_1:def 2;

then A23: g | (dom (f + g)) is_simple_func_in S by A2, Th34;

dom (g | (dom (f + g))) = (dom g) /\ (dom (f + g)) by RELAT_1:61;

then A24: dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) by A18, XBOOLE_1:16;

then A25: dom (g | (dom (f + g))) = dom (f + g) by A17, MESFUNC1:def 3;

A26: dom ((f | (dom (f + g))) + (g | (dom (f + g)))) = ((dom (f | (dom (f + g)))) /\ (dom (g | (dom (f + g))))) \ ((((f | (dom (f + g))) " {+infty}) /\ ((g | (dom (f + g))) " {-infty})) \/ (((f | (dom (f + g))) " {-infty}) /\ ((g | (dom (f + g))) " {+infty}))) by MESFUNC1:def 3

.= dom (f + g) by A16, A14, A17, A19, A24, A13, A15, MESFUNC1:def 3 ;

A27: for x being Element of X st x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) holds

((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x

proof

f | (dom (f + g)) is_simple_func_in S
by A1, A22, Th34;
let x be Element of X; :: thesis: ( x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) implies ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x )

assume A28: x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) ; :: thesis: ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x

then ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = ((f | (dom (f + g))) . x) + ((g | (dom (f + g))) . x) by MESFUNC1:def 3

.= (f . x) + ((g | (dom (f + g))) . x) by A26, A28, FUNCT_1:49

.= (f . x) + (g . x) by A26, A28, FUNCT_1:49 ;

hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A26, A28, MESFUNC1:def 3; :: thesis: verum

end;assume A28: x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) ; :: thesis: ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x

then ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = ((f | (dom (f + g))) . x) + ((g | (dom (f + g))) . x) by MESFUNC1:def 3

.= (f . x) + ((g | (dom (f + g))) . x) by A26, A28, FUNCT_1:49

.= (f . x) + (g . x) by A26, A28, FUNCT_1:49 ;

hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A26, A28, MESFUNC1:def 3; :: thesis: verum

then (f | (dom (f + g))) + (g | (dom (f + g))) is_simple_func_in S by A12, A23, A20, A25, Lm3;

hence f + g is_simple_func_in S by A26, A27, PARTFUN1:5; :: thesis: verum