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,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
let f, g be PartFunc of X,REAL; :: thesis: ( f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f implies ( f + g is_simple_func_in S & dom (f + g) <> {} ) )
assume that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: g is_simple_func_in S and
A4: dom g = dom f ; :: thesis: ( f + g is_simple_func_in S & dom (f + g) <> {} )
R_EAL f is_simple_func_in S by A1, Th49;
then consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A5: F,a are_Re-presentation_of R_EAL f by MESFUNC3:12;
set la = len F;
A6: dom f = union (rng F) by A5, MESFUNC3:def 1;
R_EAL g is_simple_func_in S by A3, Th49;
then consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that
A7: G,b are_Re-presentation_of R_EAL g by MESFUNC3:12;
set lb = len G;
A8: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
deffunc H₁( Nat) -> set = (F . ((($1 -' 1) div (len G)) + 1)) /\ (G . ((($1 -' 1) mod (len G)) + 1));
consider FG being FinSequence such that
A9: len FG = (len F) * (len G) and
A10: for k being Nat st k in dom FG holds
FG . k = H₁(k) from FINSEQ_1:sch 2();
A11: dom FG = Seg ((len F) * (len G)) by A9, FINSEQ_1:def 3;

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

reconsider la9 = len F, lb9 = len G as Nat ;
let k be Nat; :: thesis: ( k in dom FG implies FG . k in S )
set i = ((k -' 1) div (len G)) + 1;
set j = ((k -' 1) mod (len G)) + 1;
assume A12: k in dom FG ; :: thesis: FG . k in S
then A13: k in Seg ((len F) * (len G)) by A9, FINSEQ_1:def 3;
then A14: k <= (len F) * (len G) by FINSEQ_1:1;
then k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
then A15: (k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G) by NAT_2:24;
1 <= k by A13, FINSEQ_1:1;
then A16: ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A14, NAT_D:def 3, XXREAL_0:2;
A17: len G <> 0 by A13, A14, FINSEQ_1:1;
then len G >= 0 + 1 by NAT_1:13;
then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A16, NAT_2:15;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A15, XREAL_1:19;
then ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A17, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len G)) + 1 in Seg (len F) ;
then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;
then A18: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:3;
(k -' 1) mod (len G) < len G by A17, NAT_D:1;
then ( ((k -' 1) mod (len G)) + 1 >= 0 + 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13;
then ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
then G . (((k -' 1) mod (len G)) + 1) in rng G by FUNCT_1:3;
then (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S by A18, MEASURE1:34;
hence FG . k in S by A10, A12; :: 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

reconsider la9 = len F, lb9 = len G as Nat ;
let k, l be Nat; :: thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )
assume that
A19: k in dom FG and
A20: l in dom FG and
A21: k <> l ; :: thesis: FG . k misses FG . l
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
A22: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A10, A19;
set m = ((l -' 1) mod (len G)) + 1;
set n = ((l -' 1) div (len G)) + 1;
A23: k in Seg ((len F) * (len G)) by A9, A19, FINSEQ_1:def 3;
then A24: 1 <= k by FINSEQ_1:1;
then A25: len G <> 0 by A23, FINSEQ_1:1;
then (k -' 1) mod (len G) < len G by NAT_D:1;
then ( ((k -' 1) mod (len G)) + 1 >= 0 + 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13;
then A26: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
A27: k <= (len F) * (len G) by A23, FINSEQ_1:1;
then A28: ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A24, NAT_D:def 3, XXREAL_0:2;
len G >= 0 + 1 by A25, NAT_1:13;
then A29: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A28, NAT_2:15;
A30: l in Seg ((len F) * (len G)) by A9, A20, FINSEQ_1:def 3;
then A31: 1 <= l by FINSEQ_1:1;

A32: now :: thesis: ( ((k -' 1) div (len G)) + 1 = ((l -' 1) div (len G)) + 1 implies not ((k -' 1) mod (len G)) + 1 = ((l -' 1) mod (len G)) + 1 )

(l -' 1) + 1 = ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1 by A25, NAT_D:2;
then A33: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A31, XREAL_1:233;
(k -' 1) + 1 = ((((((k -' 1) div (len G)) + 1) - 1) * (len G)) + ((((k -' 1) mod (len G)) + 1) - 1)) + 1 by A25, NAT_D:2;
then A34: (k - 1) + 1 = (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1) by A24, XREAL_1:233;
assume ( ((k -' 1) div (len G)) + 1 = ((l -' 1) div (len G)) + 1 & ((k -' 1) mod (len G)) + 1 = ((l -' 1) mod (len G)) + 1 ) ; :: thesis: contradiction
hence contradiction by A21, A34, A33; :: thesis: verum

end;

k -' 1 <= ((len F) * (len G)) -' 1 by A27, NAT_D:42;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A29, NAT_2:24;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A25, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len G)) + 1 in Seg (len F) ;
then A35: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;
(l -' 1) mod (len G) < len G by A25, NAT_D:1;
then ( ((l -' 1) mod (len G)) + 1 >= 0 + 1 & ((l -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13;
then A36: ((l -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
l <= (len F) * (len G) by A30, FINSEQ_1:1;
then l -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
then (l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A29, NAT_2:24;
then ((l -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then ( ((l -' 1) div (len G)) + 1 >= 0 + 1 & ((l -' 1) div (len G)) + 1 <= len F ) by A25, NAT_D:18, XREAL_1:6;
then ((l -' 1) div (len G)) + 1 in Seg (len F) ;
then A37: ((l -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

per cases ( ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 or ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ) by A32;

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

(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A10, A20, A22;
then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16;
then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16;
then A39: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by XBOOLE_1:16;
F . (((k -' 1) div (len G)) + 1) misses F . (((l -' 1) div (len G)) + 1) by A35, A37, A38, MESFUNC3:4;
then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A39;
hence FG . k misses FG . l ; :: thesis: verum

end;

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

(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A10, A20, A22;
then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16;
then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16;
then A41: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by XBOOLE_1:16;
G . (((k -' 1) mod (len G)) + 1) misses G . (((l -' 1) mod (len G)) + 1) by A26, A36, A40, MESFUNC3:4;
then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A41;
hence FG . k misses FG . l ; :: thesis: verum

end;

end;

end;

then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A42: dom g = union (rng G) by A7, MESFUNC3:def 1;
A43: dom f = union (rng FG)

proof

now :: thesis: for z being object st z in dom f holds
z in union (rng FG)

let z be object ; :: thesis: ( z in dom f implies z in union (rng FG) )
assume A44: z in dom f ; :: thesis: z in union (rng FG)
then consider Y being set such that
A45: z in Y and
A46: Y in rng F by A6, TARSKI:def 4;
consider i being Nat such that
A47: i in dom F and
A48: Y = F . i by A46, FINSEQ_2:10;
A49: i in Seg (len F) by A47, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then consider i9 being Nat such that
A50: i = 1 + i9 by NAT_1:10;
consider Z being set such that
A51: z in Z and
A52: Z in rng G by A4, A42, A44, TARSKI:def 4;
consider j being Nat such that
A53: j in dom G and
A54: Z = G . j by A52, FINSEQ_2:10;
A55: j in Seg (len G) by A53, FINSEQ_1:def 3;
then A56: 1 <= j by FINSEQ_1:1;
then consider j9 being Nat such that
A57: j = 1 + j9 by NAT_1:10;
A58: j <= len G by A55, FINSEQ_1:1;
then A59: j9 < len G by A57, NAT_1:13;
reconsider k = ((i - 1) * (len G)) + j as Nat by A50;
A60: k >= 0 + j by A50, XREAL_1:6;
then A61: k -' 1 = k - 1 by A56, XREAL_1:233, XXREAL_0:2
.= (i9 * (len G)) + j9 by A50, A57 ;
then A62: i = ((k -' 1) div (len G)) + 1 by A50, A59, NAT_D:def 1;
i <= len F by A49, FINSEQ_1:1;
then i - 1 <= (len F) - 1 by XREAL_1:9;
then (i - 1) * (len G) <= ((len F) - 1) * (len G) by XREAL_1:64;
then A63: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6;
(((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by A58, XREAL_1:6;
then A64: k <= (len F) * (len G) by A63, XXREAL_0:2;
k >= 1 by A56, A60, XXREAL_0:2;
then A65: k in Seg ((len F) * (len G)) by A64;
then k in dom FG by A9, FINSEQ_1:def 3;
then A66: FG . k in rng FG by FUNCT_1:def 3;
A67: j = ((k -' 1) mod (len G)) + 1 by A57, A61, A59, NAT_D:def 2;
z in (F . i) /\ (G . j) by A45, A48, A51, A54, XBOOLE_0:def 4;
then z in FG . k by A10, A11, A62, A67, A65;
hence z in union (rng FG) by A66, TARSKI:def 4; :: thesis: verum

end;

hence dom f c= union (rng FG) ; :: according to XBOOLE_0:def 10 :: thesis: union (rng FG) c= dom f
reconsider la9 = len F, lb9 = len G as Nat ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union (rng FG) or z in dom f )
assume z in union (rng FG) ; :: thesis: z in dom f
then consider Y being set such that
A68: z in Y and
A69: Y in rng FG by TARSKI:def 4;
consider k being Nat such that
A70: k in dom FG and
A71: Y = FG . k by A69, FINSEQ_2:10;
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
A72: k in Seg (len FG) by A70, FINSEQ_1:def 3;
then A73: k <= (len F) * (len G) by A9, FINSEQ_1:1;
then A74: len G <> 0 by A72, FINSEQ_1:1;
then A75: len G >= 0 + 1 by NAT_1:13;
1 <= k by A72, FINSEQ_1:1;
then ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A73, NAT_D:def 3, XXREAL_0:2;
then A76: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A75, NAT_2:15;
k -' 1 <= ((len F) * (len G)) -' 1 by A73, NAT_D:42;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A76, NAT_2:24;
then A77: ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((len F) * (len G)) div (len G) = len F ) by A74, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len G)) + 1 in Seg (len F) by A77;
then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;
then A78: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:def 3;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A10, A70;
then z in F . (((k -' 1) div (len G)) + 1) by A68, A71, XBOOLE_0:def 4;
hence z in dom f by A6, A78, TARSKI:def 4; :: thesis: verum

end;

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

reconsider la9 = len F, lb9 = len G as Nat ;
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
A79: k in dom FG and
A80: x in FG . k and
A81: y in FG . k ; :: thesis: (f + g) . x = (f + g) . y
set i = ((k -' 1) div (len G)) + 1;
set j = ((k -' 1) mod (len G)) + 1;
A82: k in Seg (len FG) by A79, FINSEQ_1:def 3;
then A83: k <= (len F) * (len G) by A9, FINSEQ_1:1;
then A84: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
A85: len G <> 0 by A82, A83, FINSEQ_1:1;
then (k -' 1) mod (len G) < len G by NAT_D:1;
then ( ((k -' 1) mod (len G)) + 1 >= 0 + 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13;
then ((k -' 1) mod (len G)) + 1 in Seg (len G) ;
then A86: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def 3;
1 <= k by A82, FINSEQ_1:1;
then A87: ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A83, NAT_D:def 3, XXREAL_0:2;
len G >= 0 + 1 by A85, NAT_1:13;
then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A87, NAT_2:15;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A84, NAT_2:24;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A85, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len G)) + 1 in Seg (len F) ;
then A88: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;
A89: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A10, A79;
then x in G . (((k -' 1) mod (len G)) + 1) by A80, XBOOLE_0:def 4;
then A90: g . x = b . (((k -' 1) mod (len G)) + 1) by A7, A86, MESFUNC3:def 1;
y in G . (((k -' 1) mod (len G)) + 1) by A81, A89, XBOOLE_0:def 4;
then A91: g . y = b . (((k -' 1) mod (len G)) + 1) by A7, A86, MESFUNC3:def 1;
x in F . (((k -' 1) div (len G)) + 1) by A80, A89, XBOOLE_0:def 4;
then f . x = a . (((k -' 1) div (len G)) + 1) by A5, A88, MESFUNC3:def 1;
then A92: (f . x) + (g . x) = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1)) by A90, SUPINF_2:1;
y in F . (((k -' 1) div (len G)) + 1) by A81, A89, XBOOLE_0:def 4;
then A93: f . y = a . (((k -' 1) div (len G)) + 1) by A5, A88, MESFUNC3:def 1;
A94: FG . k in rng FG by A79, FUNCT_1:def 3;
then x in dom (f + g) by A4, A43, A8, A80, TARSKI:def 4;
then (f + g) . x = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1)) by A92, VALUED_1:def 1;
then A95: (f + g) . x = (f . y) + (g . y) by A93, A91, SUPINF_2:1;
y in dom (f + g) by A4, A43, A8, A81, A94, TARSKI:def 4;
hence (f + g) . x = (f + g) . y by A95, VALUED_1:def 1; :: thesis: verum

end;

hence f + g is_simple_func_in S by A4, A43, A8; :: thesis: dom (f + g) <> {}
thus dom (f + g) <> {} by A2, A4, A8; :: thesis: verum