let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of 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 M being sigma_Measure of 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 M be sigma_Measure of S; :: 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
A4: g is_simple_func_in S ; :: thesis: f + g is_simple_func_in S
g is real-valued by A4, MESFUNC2:def 4;
then A8: dom (f + g) = (dom f) /\ (dom g) by MESFUNC2:2;
consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A10: F,a are_Re-presentation_of f by A1, MESFUNC3:12;
consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that
A9: G,b are_Re-presentation_of g by A4, MESFUNC3:12;
set la = len a;
set lb = len b;
A11: ( dom F = dom a & dom G = dom b ) by A9, A10, MESFUNC3:def 1;
deffunc H₁( Nat) -> M8(X,S) = (F . ((($1 -' 1) div (len b)) + 1)) /\ (G . ((($1 -' 1) mod (len b)) + 1));
consider FG being FinSequence such that
A12: len FG = (len a) * (len b) and
A13: for k being Nat st k in dom FG holds
FG . k = H₁(k) from FINSEQ_1:sch 2();
A14: dom FG = Seg ((len a) * (len b)) by A12, FINSEQ_1:def 3;

now :: thesis: for k being Nat st k in dom FG holds
FG . k in S

let k be Nat; :: thesis: ( k in dom FG implies FG . k in S )
assume k in dom FG ; :: thesis: FG . k in S
then FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13;
hence FG . k in S ; :: thesis: verum

end;

then reconsider FG = FG as FinSequence of S by FINSEQ_2:12;
for k, l being Nat st k in dom FG & l in dom FG & k <> l holds
FG . k misses FG . l

proof

let k, l be Nat; :: thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )
assume that
A25: k in dom FG and
A26: l in dom FG and
A27: k <> l ; :: thesis: FG . k misses FG . l
set m = ((l -' 1) mod (len b)) + 1;
set n = ((l -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
set i = ((k -' 1) div (len b)) + 1;
A29: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A25;
A30: k in Seg ((len a) * (len b)) by A12, A25, FINSEQ_1:def 3;
A31: ( 1 <= k & k <= (len a) * (len b) & 1 <= l & l <= (len a) * (len b) ) by A12, A25, A26, FINSEQ_3:25;
then A33: ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) ) by NAT_D:def 3, XXREAL_0:2;
A34: len b <> 0 by A30;
then len b >= 1 by NAT_1:14;
then A35: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A33, NAT_2:15;
k -' 1 <= ((len a) * (len b)) -' 1 by A31, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A35, NAT_2:24;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;
then ((k -' 1) div (len b)) + 1 <= len a by A34, NAT_D:18;
then A37: ((k -' 1) div (len b)) + 1 in dom F by A11, NAT_1:11, FINSEQ_3:25;
( ((l -' 1) mod (len b)) + 1 <= len b & ((k -' 1) mod (len b)) + 1 <= len b ) by A34, NAT_D:1, NAT_1:13;
then A42: ( ((l -' 1) mod (len b)) + 1 in dom G & ((k -' 1) mod (len b)) + 1 in dom G ) by A11, NAT_1:11, FINSEQ_3:25;
l -' 1 <= ((len a) * (len b)) -' 1 by A31, NAT_D:42;
then (l -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A35, NAT_2:24;
then ((l -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;
then ((l -' 1) div (len b)) + 1 <= len a by A34, NAT_D:18;
then A44: ((l -' 1) div (len b)) + 1 in dom F by A11, NAT_1:11, FINSEQ_3:25;
(l -' 1) + 1 = ((((((l -' 1) div (len b)) + 1) - 1) * (len b)) + ((((l -' 1) mod (len b)) + 1) - 1)) + 1 by A34, NAT_D:2;
then A40: (l - 1) + 1 = (((((l -' 1) div (len b)) + 1) - 1) * (len b)) + (((l -' 1) mod (len b)) + 1) by A31, XREAL_1:233;
(k -' 1) + 1 = ((((((k -' 1) div (len b)) + 1) - 1) * (len b)) + ((((k -' 1) mod (len b)) + 1) - 1)) + 1 by A34, NAT_D:2;
then A41: (k - 1) + 1 = (((((k -' 1) div (len b)) + 1) - 1) * (len b)) + (((k -' 1) mod (len b)) + 1) by A31, XREAL_1:233;

per cases ( ((k -' 1) div (len b)) + 1 <> ((l -' 1) div (len b)) + 1 or ((k -' 1) mod (len b)) + 1 <> ((l -' 1) mod (len b)) + 1 ) by A27, A40, A41;

suppose ((k -' 1) div (len b)) + 1 <> ((l -' 1) div (len b)) + 1 ; :: thesis: FG . k misses FG . l

then A45: F . (((k -' 1) div (len b)) + 1) misses F . (((l -' 1) div (len b)) + 1) by A37, A44, MESFUNC3:4;
(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A13, A26, A29
.= (F . (((k -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16
.= (F . (((k -' 1) div (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16
.= ((F . (((k -' 1) div (len b)) + 1)) /\ (F . (((l -' 1) div (len b)) + 1))) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by XBOOLE_1:16
.= {} by A45 ;
hence FG . k misses FG . l ; :: thesis: verum

end;

suppose ((k -' 1) mod (len b)) + 1 <> ((l -' 1) mod (len b)) + 1 ; :: thesis: FG . k misses FG . l

then A46: G . (((k -' 1) mod (len b)) + 1) misses G . (((l -' 1) mod (len b)) + 1) by A42, MESFUNC3:4;
(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A13, A26, A29
.= (F . (((k -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16
.= (F . (((k -' 1) div (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16
.= {} by A46 ;
hence FG . k misses FG . l ; :: thesis: verum

end;

end;

end;

then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A51: dom f = union (rng F) by A10, MESFUNC3:def 1;
A70: dom g = union (rng G) by A9, MESFUNC3:def 1;
A71: dom (f + g) = union (rng FG)

proof

thus dom (f + g) c= union (rng FG) :: according to XBOOLE_0:def 10 :: thesis: union (rng FG) c= dom (f + g)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom (f + g) or z in union (rng FG) )
assume z in dom (f + g) ; :: thesis: z in union (rng FG)
then A72: ( z in dom f & z in dom g ) by A8, XBOOLE_0:def 4;
then consider Y being set such that
A73: z in Y and
A74: Y in rng F by A51, TARSKI:def 4;
consider Z being set such that
A75: z in Z and
A76: Z in rng G by A70, A72, TARSKI:def 4;
consider j being object such that
A77: j in dom G and
A78: Z = G . j by A76, FUNCT_1:def 3;
reconsider j = j as Element of NAT by A77;
consider j9 being Nat such that
A81: j = 1 + j9 by A77, Lm2, FINSEQ_3:25;
consider i being object such that
A82: i in dom F and
A83: Y = F . i by A74, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A82;
consider i9 being Nat such that
A85: i = 1 + i9 by A82, Lm2, FINSEQ_3:25;
A80: ( 1 <= j & j <= len b ) by A11, A77, FINSEQ_3:25;
then A87: j9 < len b by A81, NAT_1:13;
reconsider k = ((i - 1) * (len b)) + j as Nat by A85;
A88: k >= 0 + j by A85, XREAL_1:6;
then A89: k -' 1 = k - 1 by A80, XREAL_1:233, XXREAL_0:2
.= (i9 * (len b)) + j9 by A85, A81 ;
then A90: i = ((k -' 1) div (len b)) + 1 by A85, A87, NAT_D:def 1;
i <= len a by A11, A82, FINSEQ_3:25;
then i - 1 <= (len a) - 1 by XREAL_1:9;
then (i - 1) * (len b) <= ((len a) - 1) * (len b) by XREAL_1:64;
then A91: k <= (((len a) - 1) * (len b)) + j by XREAL_1:6;
(((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b) by A80, XREAL_1:6;
then A92: k <= (len a) * (len b) by A91, XXREAL_0:2;
B1: k >= 1 by A80, A88, XXREAL_0:2;
then A93: k in Seg ((len a) * (len b)) by A92;
k in dom FG by A12, B1, A92, FINSEQ_3:25;
then A94: FG . k in rng FG by FUNCT_1:def 3;
A95: j = ((k -' 1) mod (len b)) + 1 by A81, A89, A87, NAT_D:def 2;
z in (F . i) /\ (G . j) by A73, A83, A75, A78, XBOOLE_0:def 4;
then z in FG . k by A13, A14, A90, A95, A93;
hence z in union (rng FG) by A94, TARSKI:def 4; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union (rng FG) or z in dom (f + g) )
assume z in union (rng FG) ; :: thesis: z in dom (f + g)
then consider Y being set such that
A96: z in Y and
A97: Y in rng FG by TARSKI:def 4;
consider k being object such that
A98: k in dom FG and
A99: Y = FG . k by A97, FUNCT_1:def 3;
reconsider k = k as Element of NAT by A98;
set j = ((k -' 1) mod (len b)) + 1;
set i = ((k -' 1) div (len b)) + 1;
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A98;
then A100: ( z in F . (((k -' 1) div (len b)) + 1) & z in G . (((k -' 1) mod (len b)) + 1) ) by A96, A99, XBOOLE_0:def 4;
A102: ( 1 <= k & k <= (len a) * (len b) ) by A12, A98, FINSEQ_3:25;
A103: len b <> 0 by A102;
then A104: len b >= 1 by NAT_1:14;
( len b divides (len a) * (len b) & 1 <= (len a) * (len b) ) by A102, NAT_D:def 3, XXREAL_0:2;
then A105: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A104, NAT_2:15;
A106: ((len a) * (len b)) div (len b) = len a by A103, NAT_D:18;
k -' 1 <= ((len a) * (len b)) -' 1 by A102, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A105, NAT_2:24;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;
then ((k -' 1) div (len b)) + 1 in dom F by A11, A106, NAT_1:11, FINSEQ_3:25;
then F . (((k -' 1) div (len b)) + 1) in rng F by FUNCT_1:def 3;
then a107: z in dom f by A51, A100, TARSKI:def 4;
( 1 <= ((k -' 1) mod (len b)) + 1 & ((k -' 1) mod (len b)) + 1 <= len b ) by A103, NAT_D:1, NAT_1:11, NAT_1:13;
then ((k -' 1) mod (len b)) + 1 in dom G by A11, FINSEQ_3:25;
then G . (((k -' 1) mod (len b)) + 1) in rng G by FUNCT_1:def 3;
then z in dom g by A70, A100, TARSKI:def 4;
hence z in dom (f + g) by A8, a107, XBOOLE_0:def 4; :: thesis: verum

end;

A107: for k being Nat
for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
(f + g) . x = (f + g) . y

proof

let k be Nat; :: thesis: for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
(f + g) . x = (f + g) . y
let x, y be Element of X; :: thesis: ( k in dom FG & x in FG . k & y in FG . k implies (f + g) . x = (f + g) . y )
assume that
A108: k in dom FG and
A109: ( x in FG . k & y in FG . k ) ; :: thesis: (f + g) . x = (f + g) . y
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
A110: ( ((k -' 1) div (len b)) + 1 >= 1 & ((k -' 1) mod (len b)) + 1 >= 1 ) by NAT_1:11;
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A108;
then A112: ( x in F . (((k -' 1) div (len b)) + 1) & x in G . (((k -' 1) mod (len b)) + 1) & y in F . (((k -' 1) div (len b)) + 1) & y in G . (((k -' 1) mod (len b)) + 1) ) by A109, XBOOLE_0:def 4;
A113: ( 1 <= k & k <= (len a) * (len b) ) by A12, A108, FINSEQ_3:25;
then A115: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;
A116: ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) ) by A113, NAT_D:def 3, XXREAL_0:2;
A117: len b <> 0 by A113;
then len b >= 1 by NAT_1:14;
then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A116, NAT_2:15;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A115, NAT_2:24;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;
then ((k -' 1) div (len b)) + 1 <= len a by A117, NAT_D:18;
then A119: ( f . x = a . (((k -' 1) div (len b)) + 1) & f . y = a . (((k -' 1) div (len b)) + 1) ) by A10, A11, A110, A112, FINSEQ_3:25, MESFUNC3:def 1;
A120: ((k -' 1) mod (len b)) + 1 <= len b by A117, NAT_D:1, NAT_1:13;
FG . k in rng FG by A108, FUNCT_1:def 3;
then A124: ( x in dom (f + g) & y in dom (f + g) ) by A71, A109, TARSKI:def 4;
hence (f + g) . x = (f . x) + (g . x) by MESFUNC1:def 3
.= (a . (((k -' 1) div (len b)) + 1)) + (b . (((k -' 1) mod (len b)) + 1)) by A9, A11, A110, A120, A112, A119, FINSEQ_3:25, MESFUNC3:def 1
.= (f . y) + (g . y) by A9, A11, A110, A120, A112, A119, FINSEQ_3:25, MESFUNC3:def 1
.= (f + g) . y by A124, MESFUNC1:def 3 ;
:: thesis: verum

end;

now :: thesis: for x being Element of X st x in dom (f + g) holds
|.((f + g) . x).| < +infty

let x be Element of X; :: thesis: ( x in dom (f + g) implies |.((f + g) . x).| < +infty )
assume A188: x in dom (f + g) ; :: thesis: |.((f + g) . x).| < +infty
then |.((f + g) . x).| = |.((f . x) + (g . x)).| by MESFUNC1:def 3;
then A189: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:24;
( x in dom f & x in dom g ) by A188, A8, XBOOLE_0:def 4;
then ( |.(f . x).| < +infty & |.(g . x).| < +infty ) by A1, A4, MESFUNC2:def 1, MESFUNC2:def 4;
then |.(f . x).| + |.(g . x).| <> +infty by XXREAL_3:16;
hence |.((f + g) . x).| < +infty by A189, XXREAL_0:2, XXREAL_0:4; :: thesis: verum

end;

hence f + g is_simple_func_in S by A71, A107, MESFUNC2:def 1, MESFUNC2:def 4; :: thesis: verum