let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL 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,REAL 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,REAL ; :: 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

ex F being Finite_Sep_Sequence of S st
( dom (f + g) = union (rng F) & ( 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 ) )

proof

reconsider EMPTY = {} as Element of S by PROB_1:42;
set F = <*EMPTY*>;
A4: dom <*EMPTY*> = Seg 1 by FINSEQ_1:55;
A3: 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: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 A5: ( i in dom <*EMPTY*> & j in dom <*EMPTY*> & i <> j ) ; :: thesis: <*EMPTY*> . i misses <*EMPTY*> . j
then ( i = 1 & j = 1 ) by A4, FINSEQ_1:4, TARSKI:def 1;
hence <*EMPTY*> . i misses <*EMPTY*> . j by A5; :: thesis: verum

end;

then reconsider F = <*EMPTY*> as Finite_Sep_Sequence of S by MESFUNC3:4;
take F ; :: thesis: ( dom (f + g) = union (rng F) & ( 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 ) )
F = <*(F . 1)*> by FINSEQ_1:57;
then A6: rng F = {(F . 1)} by FINSEQ_1:56;
1 in Seg 1 ;
then union (rng F) = union (bool {} ) by A3, A6, A4, ZFMISC_1:1;
hence dom (f + g) = union (rng F) by A2, ZFMISC_1:99; :: thesis: 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
thus 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 A3; :: thesis: verum

end;

hence f + g is_simple_func_in S by Def7; :: thesis: verum

end;

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

A9: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
( dom f is Element of S & dom g is Element of S ) by A1, Th71;
then dom (f + g) in S by A9, FINSUB_1:def 2;
then A10: ( f | (dom (f + g)) is_simple_func_in S & g | (dom (f + g)) is_simple_func_in S ) by A1, Th70;
( 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 A11: ( dom (f | (dom (f + g))) = ((dom f) /\ (dom f)) /\ (dom g) & dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) ) by A9, XBOOLE_1:16;
then ( dom (f | (dom (f + g))) = dom (f + g) & dom (g | (dom (f + g))) = dom (f + g) ) by VALUED_1:def 1;
then A12: (f | (dom (f + g))) + (g | (dom (f + g))) is_simple_func_in S by A8, A10, Lm1;
A13: dom ((f | (dom (f + g))) + (g | (dom (f + g)))) = (dom (f | (dom (f + g)))) /\ (dom (g | (dom (f + g)))) by VALUED_1:def 1
.= dom (f + g) by A11, VALUED_1:def 1 ;
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 A14: 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 VALUED_1:def 1
.= (f . x) + ((g | (dom (f + g))) . x) by A13, A14, FUNCT_1:72
.= (f . x) + (g . x) by A13, A14, FUNCT_1:72 ;
hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A13, A14, VALUED_1:def 1; :: thesis: verum

end;

hence f + g is_simple_func_in S by A12, A13, PARTFUN1:34; :: thesis: verum

end;

end;