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 A1: ( f is_simple_func_in S & g is_simple_func_in S ) ; :: thesis: f + g is_simple_func_in S

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

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

then for x being Element of X st x in dom (f + g) holds
|.((f + g) . x).| < +infty ;
then A3: f + g is real-valued by MESFUNC2:def 1;
reconsider EMPTY = {} as Element of S by PROB_1:42;
set F = <*EMPTY*>;
A5: dom <*EMPTY*> = Seg 1 by FINSEQ_1:55;
B4: 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 A5, FINSEQ_1:4, TARSKI:def 1;
hence <*EMPTY*> . n = EMPTY by FINSEQ_1:57; :: thesis: verum

end;

now

let i, j be Nat; :: thesis: ( i in dom <*EMPTY*> & j in dom <*EMPTY*> & i <> j implies <*EMPTY*> . i misses <*EMPTY*> . j )
assume A6: ( i in dom <*EMPTY*> & j in dom <*EMPTY*> & i <> j ) ; :: thesis: <*EMPTY*> . i misses <*EMPTY*> . j
then ( i = 1 & j = 1 ) by A5, FINSEQ_1:4, TARSKI:def 1;
hence <*EMPTY*> . i misses <*EMPTY*> . j by A6; :: thesis: verum

end;

then reconsider F = <*EMPTY*> as Finite_Sep_Sequence of S by MESFUNC3:4;
union (rng F) = union (bool {} ) by FINSEQ_1:56, ZFMISC_1:1;
then X: dom (f + g) = union (rng F) by A2, ZFMISC_1:99;
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 B4;
hence f + g is_simple_func_in S by A3, X, MESFUNC2:def 5; :: thesis: verum

end;

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

( f is without+infty & g is without+infty ) by A1, Th20;
then ( not +infty in rng f & not +infty in rng g ) by Def4;
then A9: ( f " {+infty } = {} & g " {+infty } = {} ) by FUNCT_1:142;
then A10: ((dom f) /\ (dom g)) \ (((f " {+infty }) /\ (g " {-infty })) \/ ((f " {-infty }) /\ (g " {+infty }))) = (dom f) /\ (dom g) ;
then A11: dom (f + g) = (dom f) /\ (dom g) by MESFUNC1:def 3;
( dom f is Element of S & dom g is Element of S ) by A1, Th43;
then dom (f + g) in S by A11, FINSUB_1:def 2;
then A12: ( f | (dom (f + g)) is_simple_func_in S & g | (dom (f + g)) is_simple_func_in S ) by A1, Th40;
( dom (f | (dom (f + g))) = (dom f) /\ (dom (f + g)) & dom (g | (dom (f + g))) = (dom g) /\ (dom (f + g)) ) by RELAT_1:90;
then A13: ( dom (f | (dom (f + g))) = ((dom f) /\ (dom f)) /\ (dom g) & dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) ) by A11, XBOOLE_1:16;
then ( dom (f | (dom (f + g))) = dom (f + g) & dom (g | (dom (f + g))) = dom (f + g) ) by A10, MESFUNC1:def 3;
then A14: (f | (dom (f + g))) + (g | (dom (f + g))) is_simple_func_in S by A8, A12, Lm4;
A15: ( (f | (dom (f + g))) " {+infty } = (dom (f + g)) /\ (f " {+infty }) & (g | (dom (f + g))) " {+infty } = (dom (f + g)) /\ (g " {+infty }) ) by FUNCT_1:139;
A16: 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 A9, A10, A13, A15, MESFUNC1:def 3 ;
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 A17: 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 A16, A17, FUNCT_1:72
.= (f . x) + (g . x) by A16, A17, FUNCT_1:72 ;
hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A16, A17, MESFUNC1:def 3; :: thesis: verum

end;

hence f + g is_simple_func_in S by A14, A16, PARTFUN1:34; :: thesis: verum

end;

end;