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

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

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;

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

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
j in dom <*EMPTY*> and
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 ; :: thesis: verum

end;

A9: for n being Nat st n in dom <*EMPTY*> holds
<*EMPTY*> . n = EMPTY

proof

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

end;

reconsider F = <*EMPTY*> as Finite_Sep_Sequence of S by A5, MESFUNC3:4;
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;

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

proof

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;

f | (dom (f + g)) is_simple_func_in S by A1, A22, Th34;
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;

end;