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:4;
set F = <*EMPTY*>;
A3: dom <*EMPTY*> = Seg 1 by FINSEQ_1:38;

A4: 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
A5: i in dom <*EMPTY*> and
A6: ( j in dom <*EMPTY*> & i <> j ) ; :: thesis: <*EMPTY*> . i misses <*EMPTY*> . j
i = 1 by A3, A5, FINSEQ_1:2, TARSKI:def 1;
hence <*EMPTY*> . i misses <*EMPTY*> . j by A3, A6, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;

A7: 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 A3, FINSEQ_1:2, TARSKI:def 1;
hence <*EMPTY*> . n = EMPTY by FINSEQ_1:40; :: thesis: verum

end;

reconsider F = <*EMPTY*> as Finite_Sep_Sequence of S by A4, 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 ) )
union (rng F) = union (bool {}) by FINSEQ_1:39, ZFMISC_1:1;
hence dom (f + g) = union (rng F) by A2; :: 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 A7; :: thesis: verum

end;

hence f + g is_simple_func_in S ; :: 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)) by RELAT_1:61;
then A11: dom (f | (dom (f + g))) = ((dom f) /\ (dom f)) /\ (dom g) by A9, XBOOLE_1:16;
dom (g | (dom (f + g))) = (dom g) /\ (dom (f + g)) by RELAT_1:61;
then A12: dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) by A9, XBOOLE_1:16;
then A13: dom (g | (dom (f + g))) = dom (f + g) by VALUED_1:def 1;
A14: 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, A12, VALUED_1:def 1 ;
A15: 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 A16: 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 A14, A16, FUNCT_1:49
.= (f . x) + (g . x) by A14, A16, FUNCT_1:49 ;
hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A14, A16, VALUED_1:def 1; :: thesis: verum

end;

dom (f | (dom (f + g))) = dom (f + g) by A11, VALUED_1:def 1;
then (f | (dom (f + g))) + (g | (dom (f + g))) is_simple_func_in S by A8, A10, A13, Lm1;
hence f + g is_simple_func_in S by A14, A15, PARTFUN1:5; :: thesis: verum

end;

end;