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 & 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,ExtREAL 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,ExtREAL 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,ExtREAL; :: 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) <> {} )

consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that

A5: F,a are_Re-presentation_of f by A1, MESFUNC3:12;

set la = len F;

A6: dom f = union (rng F) by A5, MESFUNC3:def 1;

consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that

A7: G,b are_Re-presentation_of g by A3, MESFUNC3:12;

set lb = len G;

deffunc H_{1}( Nat) -> set = (F . ((($1 -' 1) div (len G)) + 1)) /\ (G . ((($1 -' 1) mod (len G)) + 1));

consider FG being FinSequence such that

A8: len FG = (len F) * (len G) and

A9: for k being Nat st k in dom FG holds

FG . k = H_{1}(k)
from FINSEQ_1:sch 2();

A10: dom FG = Seg ((len F) * (len G)) by A8, FINSEQ_1:def 3;

A22: for k, l being Nat st k in dom FG & l in dom FG & k <> l holds

FG . k misses FG . l

then A53: dom (f + g) = (dom f) /\ (dom g) by MESFUNC2:2;

reconsider FG = FG as Finite_Sep_Sequence of S by A22, MESFUNC3:4;

A54: dom g = union (rng G) by A7, MESFUNC3:def 1;

A55: dom f = union (rng FG)

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

hence f + g is_simple_func_in S by A4, A55, A53, A93, MESFUNC2:def 4; :: thesis: dom (f + g) <> {}

thus dom (f + g) <> {} by A2, A4, A53; :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL 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,ExtREAL 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,ExtREAL 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,ExtREAL; :: 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) <> {} )

consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that

A5: F,a are_Re-presentation_of f by A1, MESFUNC3:12;

set la = len F;

A6: dom f = union (rng F) by A5, MESFUNC3:def 1;

consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that

A7: G,b are_Re-presentation_of g by A3, MESFUNC3:12;

set lb = len G;

deffunc H

consider FG being FinSequence such that

A8: len FG = (len F) * (len G) and

A9: for k being Nat st k in dom FG holds

FG . k = H

A10: dom FG = Seg ((len F) * (len G)) by A8, FINSEQ_1:def 3;

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

FG . k in S

then reconsider FG = FG as FinSequence of S by Lm2;FG . k in S

reconsider 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;

A11: lb9 divides (len F) * (len G) by NAT_D:def 3;

assume A12: k in dom FG ; :: thesis: FG . k in S

then A13: k in Seg ((len F) * (len G)) by A8, 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: 1 <= (len F) * (len G) by A14, XXREAL_0:2;

A17: len G <> 0 by A13;

then (k -' 1) mod (len G) < len G by NAT_D:1;

then A18: ((k -' 1) mod (len G)) + 1 <= len G by NAT_1:13;

len G >= 0 + 1 by A17, NAT_1:13;

then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A11, A16, NAT_2:15;

then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A15, XREAL_1:19;

then A19: ((k -' 1) div (len G)) + 1 <= len F by A17, NAT_D:18;

((k -' 1) div (len G)) + 1 >= 0 + 1 by XREAL_1:6;

then ((k -' 1) div (len G)) + 1 in Seg (len F) by A19;

then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

then A20: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:3;

((k -' 1) mod (len G)) + 1 >= 0 + 1 by XREAL_1:6;

then ((k -' 1) mod (len G)) + 1 in dom G by A18, FINSEQ_3:25;

then A21: G . (((k -' 1) mod (len G)) + 1) in rng G by FUNCT_1:3;

FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A9, A12;

hence FG . k in S by A20, A21, MEASURE1:34; :: thesis: verum

end;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;

A11: lb9 divides (len F) * (len G) by NAT_D:def 3;

assume A12: k in dom FG ; :: thesis: FG . k in S

then A13: k in Seg ((len F) * (len G)) by A8, 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: 1 <= (len F) * (len G) by A14, XXREAL_0:2;

A17: len G <> 0 by A13;

then (k -' 1) mod (len G) < len G by NAT_D:1;

then A18: ((k -' 1) mod (len G)) + 1 <= len G by NAT_1:13;

len G >= 0 + 1 by A17, NAT_1:13;

then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A11, A16, NAT_2:15;

then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A15, XREAL_1:19;

then A19: ((k -' 1) div (len G)) + 1 <= len F by A17, NAT_D:18;

((k -' 1) div (len G)) + 1 >= 0 + 1 by XREAL_1:6;

then ((k -' 1) div (len G)) + 1 in Seg (len F) by A19;

then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

then A20: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:3;

((k -' 1) mod (len G)) + 1 >= 0 + 1 by XREAL_1:6;

then ((k -' 1) mod (len G)) + 1 in dom G by A18, FINSEQ_3:25;

then A21: G . (((k -' 1) mod (len G)) + 1) in rng G by FUNCT_1:3;

FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A9, A12;

hence FG . k in S by A20, A21, MEASURE1:34; :: thesis: verum

A22: for k, l being Nat st k in dom FG & l in dom FG & k <> l holds

FG . k misses FG . l

proof

A52:
g is real-valued
by A3, MESFUNC2:def 4;
A23:
len G divides (len F) * (len G)
by NAT_D:def 3;

let k, l be Nat; :: thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )

assume that

A24: k in dom FG and

A25: l in dom FG and

A26: k <> l ; :: thesis: FG . k misses FG . l

A27: k in Seg ((len F) * (len G)) by A8, A24, FINSEQ_1:def 3;

then A28: 1 <= k by FINSEQ_1:1;

set m = ((l -' 1) mod (len G)) + 1;

set n = ((l -' 1) div (len G)) + 1;

set j = ((k -' 1) mod (len G)) + 1;

set i = ((k -' 1) div (len G)) + 1;

A29: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A9, A24;

A30: k <= (len F) * (len G) by A27, FINSEQ_1:1;

then A31: 1 <= (len F) * (len G) by A28, XXREAL_0:2;

A32: len G <> 0 by A27;

then len G >= 0 + 1 by NAT_1:13;

then A33: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A23, A31, NAT_2:15;

A34: l in Seg ((len F) * (len G)) by A8, A25, FINSEQ_1:def 3;

then A35: 1 <= l by FINSEQ_1:1;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A33, NAT_2:24;

then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;

then A40: ((k -' 1) div (len G)) + 1 <= len F by A32, NAT_D:18;

((k -' 1) div (len G)) + 1 >= 0 + 1 by XREAL_1:6;

then ((k -' 1) div (len G)) + 1 in Seg (len F) by A40;

then A41: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

A42: ((k -' 1) mod (len G)) + 1 >= 0 + 1 by XREAL_1:6;

(k -' 1) mod (len G) < len G by A32, NAT_D:1;

then ((k -' 1) mod (len G)) + 1 <= len G by NAT_1:13;

then A43: ((k -' 1) mod (len G)) + 1 in dom G by A42, FINSEQ_3:25;

A44: ((l -' 1) mod (len G)) + 1 >= 0 + 1 by XREAL_1:6;

(l -' 1) mod (len G) < len G by A32, NAT_D:1;

then ((l -' 1) mod (len G)) + 1 <= len G by NAT_1:13;

then A45: ((l -' 1) mod (len G)) + 1 in dom G by A44, FINSEQ_3:25;

A46: ((l -' 1) div (len G)) + 1 >= 0 + 1 by XREAL_1:6;

l <= (len F) * (len G) by A34, 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 A33, 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 <= len F by A32, NAT_D:18;

then ((l -' 1) div (len G)) + 1 in Seg (len F) by A46;

then A47: ((l -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

end;let k, l be Nat; :: thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )

assume that

A24: k in dom FG and

A25: l in dom FG and

A26: k <> l ; :: thesis: FG . k misses FG . l

A27: k in Seg ((len F) * (len G)) by A8, A24, FINSEQ_1:def 3;

then A28: 1 <= k by FINSEQ_1:1;

set m = ((l -' 1) mod (len G)) + 1;

set n = ((l -' 1) div (len G)) + 1;

set j = ((k -' 1) mod (len G)) + 1;

set i = ((k -' 1) div (len G)) + 1;

A29: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A9, A24;

A30: k <= (len F) * (len G) by A27, FINSEQ_1:1;

then A31: 1 <= (len F) * (len G) by A28, XXREAL_0:2;

A32: len G <> 0 by A27;

then len G >= 0 + 1 by NAT_1:13;

then A33: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A23, A31, NAT_2:15;

A34: l in Seg ((len F) * (len G)) by A8, A25, FINSEQ_1:def 3;

then A35: 1 <= l by FINSEQ_1:1;

A36: 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 )

k -' 1 <= ((len F) * (len G)) -' 1
by A30, NAT_D:42;
(l -' 1) + 1 = ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1
by A32, NAT_D:2;

then A37: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A35, XREAL_1:233;

assume that

A38: ((k -' 1) div (len G)) + 1 = ((l -' 1) div (len G)) + 1 and

A39: ((k -' 1) mod (len G)) + 1 = ((l -' 1) mod (len G)) + 1 ; :: thesis: contradiction

(k -' 1) + 1 = ((((((k -' 1) div (len G)) + 1) - 1) * (len G)) + ((((k -' 1) mod (len G)) + 1) - 1)) + 1 by A32, NAT_D:2;

then (k - 1) + 1 = (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1) by A28, XREAL_1:233;

hence contradiction by A26, A38, A39, A37; :: thesis: verum

end;then A37: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A35, XREAL_1:233;

assume that

A38: ((k -' 1) div (len G)) + 1 = ((l -' 1) div (len G)) + 1 and

A39: ((k -' 1) mod (len G)) + 1 = ((l -' 1) mod (len G)) + 1 ; :: thesis: contradiction

(k -' 1) + 1 = ((((((k -' 1) div (len G)) + 1) - 1) * (len G)) + ((((k -' 1) mod (len G)) + 1) - 1)) + 1 by A32, NAT_D:2;

then (k - 1) + 1 = (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1) by A28, XREAL_1:233;

hence contradiction by A26, A38, A39, A37; :: thesis: verum

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A33, NAT_2:24;

then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;

then A40: ((k -' 1) div (len G)) + 1 <= len F by A32, NAT_D:18;

((k -' 1) div (len G)) + 1 >= 0 + 1 by XREAL_1:6;

then ((k -' 1) div (len G)) + 1 in Seg (len F) by A40;

then A41: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

A42: ((k -' 1) mod (len G)) + 1 >= 0 + 1 by XREAL_1:6;

(k -' 1) mod (len G) < len G by A32, NAT_D:1;

then ((k -' 1) mod (len G)) + 1 <= len G by NAT_1:13;

then A43: ((k -' 1) mod (len G)) + 1 in dom G by A42, FINSEQ_3:25;

A44: ((l -' 1) mod (len G)) + 1 >= 0 + 1 by XREAL_1:6;

(l -' 1) mod (len G) < len G by A32, NAT_D:1;

then ((l -' 1) mod (len G)) + 1 <= len G by NAT_1:13;

then A45: ((l -' 1) mod (len G)) + 1 in dom G by A44, FINSEQ_3:25;

A46: ((l -' 1) div (len G)) + 1 >= 0 + 1 by XREAL_1:6;

l <= (len F) * (len G) by A34, 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 A33, 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 <= len F by A32, NAT_D:18;

then ((l -' 1) div (len G)) + 1 in Seg (len F) by A46;

then A47: ((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 A36;

end;

suppose A48:
((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 A9, A25, A29;

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 A49: (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 A41, A47, A48, MESFUNC3:4;

then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A49;

hence FG . k misses FG . l ; :: thesis: verum

end;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 A49: (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 A41, A47, A48, MESFUNC3:4;

then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A49;

hence FG . k misses FG . l ; :: thesis: verum

suppose A50:
((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 A9, A25, A29;

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 A51: (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 A43, A45, A50, MESFUNC3:4;

then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A51;

hence FG . k misses FG . l ; :: thesis: verum

end;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 A51: (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 A43, A45, A50, MESFUNC3:4;

then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A51;

hence FG . k misses FG . l ; :: thesis: verum

then A53: dom (f + g) = (dom f) /\ (dom g) by MESFUNC2:2;

reconsider FG = FG as Finite_Sep_Sequence of S by A22, MESFUNC3:4;

A54: dom g = union (rng G) by A7, MESFUNC3:def 1;

A55: dom f = union (rng FG)

proof

reconsider 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 )

A80: lb9 divides (len F) * (len G) by NAT_D:def 3;

assume z in union (rng FG) ; :: thesis: z in dom f

then consider Y being set such that

A81: z in Y and

A82: Y in rng FG by TARSKI:def 4;

consider k being Nat such that

A83: k in dom FG and

A84: Y = FG . k by A82, FINSEQ_2:10;

A85: k in Seg (len FG) by A83, FINSEQ_1:def 3;

then A86: k <= (len F) * (len G) by A8, FINSEQ_1:1;

then A87: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

set j = ((k -' 1) mod (len G)) + 1;

set i = ((k -' 1) div (len G)) + 1;

A88: ((k -' 1) div (len G)) + 1 >= 0 + 1 by NAT_1:13;

1 <= k by A85, FINSEQ_1:1;

then A89: 1 <= (len F) * (len G) by A86, XXREAL_0:2;

A90: len G <> 0 by A8, A85;

then len G >= 0 + 1 by NAT_1:13;

then (((len F) * (len G)) -' 1) div lb9 = (((len F) * (len G)) div (len G)) - 1 by A80, A89, NAT_2:15;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A87, NAT_2:24;

then A91: ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;

((len F) * (len G)) div (len G) = len F by A90, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in Seg (len F) by A91, A88;

then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

then A92: 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 A9, A83;

then z in F . (((k -' 1) div (len G)) + 1) by A81, A84, XBOOLE_0:def 4;

hence z in dom f by A6, A92, TARSKI:def 4; :: thesis: verum

end;

A93:
for k being Natnow :: thesis: for z being object st z in dom f holds

z in union (rng FG)

hence
dom f c= union (rng FG)
; :: according to XBOOLE_0:def 10 :: thesis: union (rng FG) c= dom fz in union (rng FG)

let z be object ; :: thesis: ( z in dom f implies z in union (rng FG) )

assume A56: z in dom f ; :: thesis: z in union (rng FG)

then consider Y being set such that

A57: z in Y and

A58: Y in rng F by A6, TARSKI:def 4;

consider i being Nat such that

A59: i in dom F and

A60: Y = F . i by A58, FINSEQ_2:10;

A61: i in Seg (len F) by A59, FINSEQ_1:def 3;

then 1 <= i by FINSEQ_1:1;

then consider i9 being Nat such that

A62: i = 1 + i9 by NAT_1:10;

consider Z being set such that

A63: z in Z and

A64: Z in rng G by A4, A54, A56, TARSKI:def 4;

consider j being Nat such that

A65: j in dom G and

A66: Z = G . j by A64, FINSEQ_2:10;

A67: j in Seg (len G) by A65, FINSEQ_1:def 3;

then A68: 1 <= j by FINSEQ_1:1;

then consider j9 being Nat such that

A69: j = 1 + j9 by NAT_1:10;

(i9 * (len G)) + j in NAT by ORDINAL1:def 12;

then reconsider k = ((i - 1) * (len G)) + j as Element of NAT by A62;

i <= len F by A61, 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 A70: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6;

A71: j <= len G by A67, FINSEQ_1:1;

then A72: j9 < len G by A69, NAT_1:13;

A73: k >= 0 + j by A62, XREAL_1:6;

then A74: k -' 1 = k - 1 by A68, XREAL_1:233, XXREAL_0:2

.= (i9 * (len G)) + j9 by A62, A69 ;

then A75: i = ((k -' 1) div (len G)) + 1 by A62, A72, NAT_D:def 1;

(((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by A71, XREAL_1:6;

then A76: k <= (len F) * (len G) by A70, XXREAL_0:2;

k >= 1 by A68, A73, XXREAL_0:2;

then A77: k in Seg ((len F) * (len G)) by A76;

then k in dom FG by A8, FINSEQ_1:def 3;

then A78: FG . k in rng FG by FUNCT_1:def 3;

A79: j = ((k -' 1) mod (len G)) + 1 by A69, A74, A72, NAT_D:def 2;

z in (F . i) /\ (G . j) by A57, A60, A63, A66, XBOOLE_0:def 4;

then z in FG . k by A9, A10, A75, A79, A77;

hence z in union (rng FG) by A78, TARSKI:def 4; :: thesis: verum

end;assume A56: z in dom f ; :: thesis: z in union (rng FG)

then consider Y being set such that

A57: z in Y and

A58: Y in rng F by A6, TARSKI:def 4;

consider i being Nat such that

A59: i in dom F and

A60: Y = F . i by A58, FINSEQ_2:10;

A61: i in Seg (len F) by A59, FINSEQ_1:def 3;

then 1 <= i by FINSEQ_1:1;

then consider i9 being Nat such that

A62: i = 1 + i9 by NAT_1:10;

consider Z being set such that

A63: z in Z and

A64: Z in rng G by A4, A54, A56, TARSKI:def 4;

consider j being Nat such that

A65: j in dom G and

A66: Z = G . j by A64, FINSEQ_2:10;

A67: j in Seg (len G) by A65, FINSEQ_1:def 3;

then A68: 1 <= j by FINSEQ_1:1;

then consider j9 being Nat such that

A69: j = 1 + j9 by NAT_1:10;

(i9 * (len G)) + j in NAT by ORDINAL1:def 12;

then reconsider k = ((i - 1) * (len G)) + j as Element of NAT by A62;

i <= len F by A61, 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 A70: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6;

A71: j <= len G by A67, FINSEQ_1:1;

then A72: j9 < len G by A69, NAT_1:13;

A73: k >= 0 + j by A62, XREAL_1:6;

then A74: k -' 1 = k - 1 by A68, XREAL_1:233, XXREAL_0:2

.= (i9 * (len G)) + j9 by A62, A69 ;

then A75: i = ((k -' 1) div (len G)) + 1 by A62, A72, NAT_D:def 1;

(((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by A71, XREAL_1:6;

then A76: k <= (len F) * (len G) by A70, XXREAL_0:2;

k >= 1 by A68, A73, XXREAL_0:2;

then A77: k in Seg ((len F) * (len G)) by A76;

then k in dom FG by A8, FINSEQ_1:def 3;

then A78: FG . k in rng FG by FUNCT_1:def 3;

A79: j = ((k -' 1) mod (len G)) + 1 by A69, A74, A72, NAT_D:def 2;

z in (F . i) /\ (G . j) by A57, A60, A63, A66, XBOOLE_0:def 4;

then z in FG . k by A9, A10, A75, A79, A77;

hence z in union (rng FG) by A78, TARSKI:def 4; :: thesis: verum

reconsider 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 )

A80: lb9 divides (len F) * (len G) by NAT_D:def 3;

assume z in union (rng FG) ; :: thesis: z in dom f

then consider Y being set such that

A81: z in Y and

A82: Y in rng FG by TARSKI:def 4;

consider k being Nat such that

A83: k in dom FG and

A84: Y = FG . k by A82, FINSEQ_2:10;

A85: k in Seg (len FG) by A83, FINSEQ_1:def 3;

then A86: k <= (len F) * (len G) by A8, FINSEQ_1:1;

then A87: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

set j = ((k -' 1) mod (len G)) + 1;

set i = ((k -' 1) div (len G)) + 1;

A88: ((k -' 1) div (len G)) + 1 >= 0 + 1 by NAT_1:13;

1 <= k by A85, FINSEQ_1:1;

then A89: 1 <= (len F) * (len G) by A86, XXREAL_0:2;

A90: len G <> 0 by A8, A85;

then len G >= 0 + 1 by NAT_1:13;

then (((len F) * (len G)) -' 1) div lb9 = (((len F) * (len G)) div (len G)) - 1 by A80, A89, NAT_2:15;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A87, NAT_2:24;

then A91: ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;

((len F) * (len G)) div (len G) = len F by A90, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in Seg (len F) by A91, A88;

then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

then A92: 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 A9, A83;

then z in F . (((k -' 1) div (len G)) + 1) by A81, A84, XBOOLE_0:def 4;

hence z in dom f by A6, A92, TARSKI:def 4; :: thesis: verum

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

A94:
len G divides (len F) * (len G)
by NAT_D:def 3;

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

A95: k in dom FG and

A96: x in FG . k and

A97: y in FG . k ; :: thesis: (f + g) . x = (f + g) . y

set j = ((k -' 1) mod (len G)) + 1;

A98: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A9, A95;

then A99: y in G . (((k -' 1) mod (len G)) + 1) by A97, XBOOLE_0:def 4;

set i = ((k -' 1) div (len G)) + 1;

A100: ((k -' 1) div (len G)) + 1 >= 0 + 1 by XREAL_1:6;

A101: k in Seg (len FG) by A95, FINSEQ_1:def 3;

then A102: 1 <= k by FINSEQ_1:1;

A103: len G > 0 by A8, A101;

then A104: len G >= 0 + 1 by NAT_1:13;

A105: k <= (len F) * (len G) by A8, A101, FINSEQ_1:1;

then A106: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

1 <= (len F) * (len G) by A102, A105, XXREAL_0:2;

then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A104, A94, NAT_2:15;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A106, NAT_2:24;

then A107: ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;

len G <> 0 by A8, A101;

then ((k -' 1) div (len G)) + 1 <= len F by A107, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in Seg (len F) by A100;

then A108: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

x in F . (((k -' 1) div (len G)) + 1) by A96, A98, XBOOLE_0:def 4;

then A109: f . x = a . (((k -' 1) div (len G)) + 1) by A5, A108, MESFUNC3:def 1;

A110: ((k -' 1) mod (len G)) + 1 >= 0 + 1 by XREAL_1:6;

(k -' 1) mod (len G) < len G by A103, NAT_D:1;

then ((k -' 1) mod (len G)) + 1 <= len G by NAT_1:13;

then ((k -' 1) mod (len G)) + 1 in Seg (len G) by A110;

then A111: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def 3;

y in F . (((k -' 1) div (len G)) + 1) by A97, A98, XBOOLE_0:def 4;

then A112: f . y = a . (((k -' 1) div (len G)) + 1) by A5, A108, MESFUNC3:def 1;

A113: FG . k in rng FG by A95, FUNCT_1:def 3;

then x in dom (f + g) by A4, A55, A53, A96, TARSKI:def 4;

then A114: (f + g) . x = (f . x) + (g . x) by MESFUNC1:def 3;

x in G . (((k -' 1) mod (len G)) + 1) by A96, A98, XBOOLE_0:def 4;

then (f + g) . x = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1)) by A7, A109, A111, A114, MESFUNC3:def 1;

then A115: (f + g) . x = (f . y) + (g . y) by A7, A99, A111, A112, MESFUNC3:def 1;

y in dom (f + g) by A4, A55, A53, A97, A113, TARSKI:def 4;

hence (f + g) . x = (f + g) . y by A115, MESFUNC1:def 3; :: thesis: verum

end;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

A95: k in dom FG and

A96: x in FG . k and

A97: y in FG . k ; :: thesis: (f + g) . x = (f + g) . y

set j = ((k -' 1) mod (len G)) + 1;

A98: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A9, A95;

then A99: y in G . (((k -' 1) mod (len G)) + 1) by A97, XBOOLE_0:def 4;

set i = ((k -' 1) div (len G)) + 1;

A100: ((k -' 1) div (len G)) + 1 >= 0 + 1 by XREAL_1:6;

A101: k in Seg (len FG) by A95, FINSEQ_1:def 3;

then A102: 1 <= k by FINSEQ_1:1;

A103: len G > 0 by A8, A101;

then A104: len G >= 0 + 1 by NAT_1:13;

A105: k <= (len F) * (len G) by A8, A101, FINSEQ_1:1;

then A106: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

1 <= (len F) * (len G) by A102, A105, XXREAL_0:2;

then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A104, A94, NAT_2:15;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A106, NAT_2:24;

then A107: ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;

len G <> 0 by A8, A101;

then ((k -' 1) div (len G)) + 1 <= len F by A107, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in Seg (len F) by A100;

then A108: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

x in F . (((k -' 1) div (len G)) + 1) by A96, A98, XBOOLE_0:def 4;

then A109: f . x = a . (((k -' 1) div (len G)) + 1) by A5, A108, MESFUNC3:def 1;

A110: ((k -' 1) mod (len G)) + 1 >= 0 + 1 by XREAL_1:6;

(k -' 1) mod (len G) < len G by A103, NAT_D:1;

then ((k -' 1) mod (len G)) + 1 <= len G by NAT_1:13;

then ((k -' 1) mod (len G)) + 1 in Seg (len G) by A110;

then A111: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def 3;

y in F . (((k -' 1) div (len G)) + 1) by A97, A98, XBOOLE_0:def 4;

then A112: f . y = a . (((k -' 1) div (len G)) + 1) by A5, A108, MESFUNC3:def 1;

A113: FG . k in rng FG by A95, FUNCT_1:def 3;

then x in dom (f + g) by A4, A55, A53, A96, TARSKI:def 4;

then A114: (f + g) . x = (f . x) + (g . x) by MESFUNC1:def 3;

x in G . (((k -' 1) mod (len G)) + 1) by A96, A98, XBOOLE_0:def 4;

then (f + g) . x = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1)) by A7, A109, A111, A114, MESFUNC3:def 1;

then A115: (f + g) . x = (f . y) + (g . y) by A7, A99, A111, A112, MESFUNC3:def 1;

y in dom (f + g) by A4, A55, A53, A97, A113, TARSKI:def 4;

hence (f + g) . x = (f + g) . y by A115, MESFUNC1:def 3; :: thesis: verum

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

|.((f + g) . x).| < +infty

then
f + g is real-valued
by MESFUNC2:def 1;|.((f + g) . x).| < +infty

let x be Element of X; :: thesis: ( x in dom (f + g) implies |.((f + g) . x).| < +infty )

assume A116: x in dom (f + g) ; :: thesis: |.((f + g) . x).| < +infty

then A117: |.(g . x).| < +infty by A4, A52, A53, MESFUNC2:def 1;

|.((f + g) . x).| = |.((f . x) + (g . x)).| by A116, MESFUNC1:def 3;

then A118: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:24;

f is real-valued by A1, MESFUNC2:def 4;

then |.(f . x).| < +infty by A4, A53, A116, MESFUNC2:def 1;

then |.(f . x).| + |.(g . x).| <> +infty by A117, XXREAL_3:16;

hence |.((f + g) . x).| < +infty by A118, XXREAL_0:2, XXREAL_0:4; :: thesis: verum

end;assume A116: x in dom (f + g) ; :: thesis: |.((f + g) . x).| < +infty

then A117: |.(g . x).| < +infty by A4, A52, A53, MESFUNC2:def 1;

|.((f + g) . x).| = |.((f . x) + (g . x)).| by A116, MESFUNC1:def 3;

then A118: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:24;

f is real-valued by A1, MESFUNC2:def 4;

then |.(f . x).| < +infty by A4, A53, A116, MESFUNC2:def 1;

then |.(f . x).| + |.(g . x).| <> +infty by A117, XXREAL_3:16;

hence |.((f + g) . x).| < +infty by A118, XXREAL_0:2, XXREAL_0:4; :: thesis: verum

hence f + g is_simple_func_in S by A4, A55, A53, A93, MESFUNC2:def 4; :: thesis: dom (f + g) <> {}

thus dom (f + g) <> {} by A2, A4, A53; :: thesis: verum