let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f, g be PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: for x being set st x in dom f holds
0. <= f . x and
A4: g is_simple_func_in S and
A5: dom g = dom f and
A6: for x being set st x in dom g holds
0. <= g . x ; :: thesis:
consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A7: F,a are_Re-presentation_of f and
dom x = dom F and
for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) and
integral X,S,M,f = Sum x by A1, A2, A3, Th4;
consider G being Finite_Sep_Sequence of S, b, y being FinSequence of ExtREAL such that
A8: G,b are_Re-presentation_of g and
dom y = dom G and
for n being Nat st n in dom y holds
y . n = (b . n) * ((M * G) . n) and
integral X,S,M,g = Sum y by A2, A4, A5, A6, Th4;
set la = len a;
set lb = len b;
A9: dom f = union (rng F) by A7, MESFUNC3:def 1;
A10: dom F = dom a by A7, MESFUNC3:def 1;
A11: dom g = union (rng G) by A8, MESFUNC3:def 1;
A12: dom G = dom b by A8, MESFUNC3:def 1;
deffunc H₁( Nat) -> set = (F . ((($1 -' 1) div (len b)) + 1)) /\ (G . ((($1 -' 1) mod (len b)) + 1));
consider FG being FinSequence such that
A13: len FG = (len a) * (len b) and
A14: for k being Nat st k in dom FG holds
FG . k = H₁(k) from FINSEQ_1:sch 2();
A15: dom FG = Seg ((len a) * (len b)) by A13, FINSEQ_1:def 3;
FG is FinSequence of S

proof

now

let k be Nat; :: thesis:
assume k in dom FG ; :: thesis:
then A16: k in Seg ((len a) * (len b)) by A13, FINSEQ_1:def 3;
then A17: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A15;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
A18: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
A19: ( 1 <= k & k <= (len a) * (len b) ) by A16, FINSEQ_1:3;
reconsider la' = len a, lb' = len b as natural number ;
A20: len b <> 0 by A19;
then A21: len b > 0 ;
then len b >= 0 + 1 by NAT_1:13;
then ( lb' divides la' * lb' & 1 <= (len a) * (len b) & 1 <= len b ) by A19, NAT_D:def 3, XXREAL_0:2;
then A22: ((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A19, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:26;
then A23: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A22, XREAL_1:21;
reconsider la = len a, lb = len b as Nat ;
((k -' 1) div (len b)) + 1 <= la by A20, A23, NAT_D:18;
then A24: ((k -' 1) div (len b)) + 1 in Seg la by A18, FINSEQ_1:3;
(k -' 1) mod lb < lb by A21, NAT_D:1;
then ((k -' 1) mod (len b)) + 1 <= lb by NAT_1:13;
then A25: ((k -' 1) mod (len b)) + 1 in Seg lb by A18, FINSEQ_1:3;
A26: ((k -' 1) div (len b)) + 1 in dom F by A10, A24, FINSEQ_1:def 3;
A27: ((k -' 1) mod (len b)) + 1 in dom G by A12, A25, FINSEQ_1:def 3;
A28: rng F c= S by FINSEQ_1:def 4;
A29: rng G c= S by FINSEQ_1:def 4;
A30: F . (((k -' 1) div (len b)) + 1) in rng F by A26, FUNCT_1:12;
A31: G . (((k -' 1) mod (len b)) + 1) in rng G by A27, FUNCT_1:12;
A32: F . (((k -' 1) div (len b)) + 1) in S by A28, A30;
G . (((k -' 1) mod (len b)) + 1) in S by A29, A31;
then (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) in S by A32, MEASURE1:66;
hence FG . k in S by A17; :: thesis:

end;

hence FG is FinSequence of S by FINSEQ_2:14; :: thesis:

end;

then reconsider FG = FG as FinSequence of S ;
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:
assume A33: ( k in dom FG & l in dom FG & k <> l ) ; :: thesis:
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
set n = ((l -' 1) div (len b)) + 1;
set m = ((l -' 1) mod (len b)) + 1;
A34: k in Seg ((len a) * (len b)) by A13, A33, FINSEQ_1:def 3;
then A35: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A15;
A36: l in Seg ((len a) * (len b)) by A13, A33, FINSEQ_1:def 3;
A37: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
A38: ( 1 <= k & k <= (len a) * (len b) ) by A34, FINSEQ_1:3;
reconsider la' = len a, lb' = len b as natural number ;
A39: len b <> 0 by A38;
then A40: len b > 0 ;
then len b >= 0 + 1 by NAT_1:13;
then ( lb' divides la' * lb' & 1 <= (len a) * (len b) & 1 <= len b ) by A38, NAT_D:def 3, XXREAL_0:2;
then A41: ((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A38, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A41, NAT_2:26;
then A42: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
reconsider la = len a, lb = len b as Nat ;
((k -' 1) div (len b)) + 1 <= la by A39, A42, NAT_D:18;
then A43: ((k -' 1) div (len b)) + 1 in Seg la by A37, FINSEQ_1:3;
(k -' 1) mod lb < lb by A40, NAT_D:1;
then ((k -' 1) mod (len b)) + 1 <= lb by NAT_1:13;
then A44: ((k -' 1) mod (len b)) + 1 in Seg lb by A37, FINSEQ_1:3;
A45: ((k -' 1) div (len b)) + 1 in dom F by A10, A43, FINSEQ_1:def 3;
A46: ((k -' 1) mod (len b)) + 1 in dom G by A12, A44, FINSEQ_1:def 3;
A47: ( ((l -' 1) div (len b)) + 1 >= 0 + 1 & ((l -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
A48: ( 1 <= l & l <= la * lb ) by A36, FINSEQ_1:3;
then l -' 1 <= (la * lb) -' 1 by NAT_D:42;
then (l -' 1) div lb <= ((la * lb) div lb) - 1 by A41, NAT_2:26;
then ((l -' 1) div lb) + 1 <= (la * lb) div lb by XREAL_1:21;
then ((l -' 1) div (len b)) + 1 <= la by A39, NAT_D:18;
then A49: ((l -' 1) div (len b)) + 1 in Seg la by A47, FINSEQ_1:3;
(l -' 1) mod lb < lb by A40, NAT_D:1;
then ((l -' 1) mod (len b)) + 1 <= lb by NAT_1:13;
then A50: ((l -' 1) mod (len b)) + 1 in Seg lb by A47, FINSEQ_1:3;
A51: ((l -' 1) div (len b)) + 1 in dom F by A10, A49, FINSEQ_1:def 3;
A52: ((l -' 1) mod (len b)) + 1 in dom G by A12, A50, FINSEQ_1:def 3;
A53: ( ((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 )

proof

assume A54: ( ((k -' 1) div (len b)) + 1 = ((l -' 1) div (len b)) + 1 & ((k -' 1) mod (len b)) + 1 = ((l -' 1) mod (len b)) + 1 ) ; :: thesis:
(k -' 1) + 1 = ((((((k -' 1) div (len b)) + 1) - 1) * lb) + ((((k -' 1) mod (len b)) + 1) - 1)) + 1 by A40, NAT_D:2;
then A55: (k - 1) + 1 = (((((k -' 1) div (len b)) + 1) - 1) * lb) + (((k -' 1) mod (len b)) + 1) by A38, XREAL_1:235;
(l -' 1) + 1 = ((((((l -' 1) div (len b)) + 1) - 1) * lb) + ((((l -' 1) mod (len b)) + 1) - 1)) + 1 by A40, NAT_D:2;
then (l - 1) + 1 = (((((l -' 1) div (len b)) + 1) - 1) * lb) + (((l -' 1) mod (len b)) + 1) by A48, XREAL_1:235;
hence contradiction by A33, A54, A55; :: thesis:

end;

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

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

then A56: F . (((k -' 1) div (len b)) + 1) misses F . (((l -' 1) div (len b)) + 1) by A45, A51, 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 A14, A35, A36, A15
.= (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
.= {} /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A56, XBOOLE_0:def 7
.= {} ;
hence FG . k misses FG . l by XBOOLE_0:def 7; :: thesis:

end;

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

then A57: G . (((k -' 1) mod (len b)) + 1) misses G . (((l -' 1) mod (len b)) + 1) by A46, A52, 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 A14, A35, A36, A15
.= (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
.= ((F . (((k -' 1) div (len b)) + 1)) /\ (F . (((l -' 1) div (len b)) + 1))) /\ {} by A57, XBOOLE_0:def 7
.= {} ;
hence FG . k misses FG . l by XBOOLE_0:def 7; :: thesis:

end;

then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
deffunc H₂( Nat) -> Element of ExtREAL = a . ((($1 -' 1) div (len b)) + 1);
consider a1 being FinSequence of ExtREAL such that
A58: len a1 = len FG and
A59: for k being Nat st k in dom a1 holds
a1 . k = H₂(k) from FINSEQ_2:sch 1();
A60: dom a1 = Seg (len FG) by A58, FINSEQ_1:def 3;
ex x1 being FinSequence of ExtREAL st
( dom x1 = dom FG & ( for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * FG) . n) ) )

proof

deffunc H₃( Nat) -> Element of ExtREAL = (a1 . $1) * ((M * FG) . $1);
consider x1 being FinSequence of ExtREAL such that
A61: ( len x1 = len FG & ( for k being Nat st k in dom x1 holds
x1 . k = H₃(k) ) ) from FINSEQ_2:sch 1();
take x1 ; :: thesis:
thus ( dom x1 = dom FG & ( for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * FG) . n) ) ) by A61, FINSEQ_3:31; :: thesis:

end;

then consider x1 being FinSequence of ExtREAL such that
A63: dom x1 = dom FG and
A64: for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * FG) . n) ;
deffunc H₃( Nat) -> Element of ExtREAL = b . ((($1 -' 1) mod (len b)) + 1);
consider b1 being FinSequence of ExtREAL such that
A65: len b1 = len FG and
A66: for k being Nat st k in dom b1 holds
b1 . k = H₃(k) from FINSEQ_2:sch 1();
A67: dom b1 = Seg (len FG) by A65, FINSEQ_1:def 3;
ex y1 being FinSequence of ExtREAL st
( dom y1 = dom FG & ( for n being Nat st n in dom y1 holds
y1 . n = (b1 . n) * ((M * FG) . n) ) )

proof

deffunc H₄( Nat) -> Element of ExtREAL = (b1 . $1) * ((M * FG) . $1);
consider y1 being FinSequence of ExtREAL such that
A68: ( len y1 = len FG & ( for k being Nat st k in dom y1 holds
y1 . k = H₄(k) ) ) from FINSEQ_2:sch 1();
take y1 ; :: thesis:
A70: for n being Nat st n in dom y1 holds
y1 . n = (b1 . n) * ((M * FG) . n) by A68;
dom y1 = Seg (len FG) by A68, FINSEQ_1:def 3
.= dom FG by FINSEQ_1:def 3 ;
hence ( dom y1 = dom FG & ( for n being Nat st n in dom y1 holds
y1 . n = (b1 . n) * ((M * FG) . n) ) ) by A70; :: thesis:

end;

then consider y1 being FinSequence of ExtREAL such that
A71: dom y1 = dom FG and
A72: for n being Nat st n in dom y1 holds
y1 . n = (b1 . n) * ((M * FG) . n) ;
deffunc H₄( Nat) -> Element of ExtREAL = (a1 . $1) + (b1 . $1);
consider c1 being FinSequence of ExtREAL such that
A73: len c1 = len FG and
A74: for k being Nat st k in dom c1 holds
c1 . k = H₄(k) from FINSEQ_2:sch 1();
A75: dom c1 = Seg (len FG) by A73, FINSEQ_1:def 3;
ex z1 being FinSequence of ExtREAL st
( dom z1 = dom FG & ( for n being Nat st n in dom z1 holds
z1 . n = (c1 . n) * ((M * FG) . n) ) )

proof

deffunc H₅( Nat) -> Element of ExtREAL = (c1 . $1) * ((M * FG) . $1);
consider z1 being FinSequence of ExtREAL such that
A76: ( len z1 = len FG & ( for k being Nat st k in dom z1 holds
z1 . k = H₅(k) ) ) from FINSEQ_2:sch 1();
take z1 ; :: thesis:
thus ( dom z1 = dom FG & ( for n being Nat st n in dom z1 holds
z1 . n = (c1 . n) * ((M * FG) . n) ) ) by A76, FINSEQ_3:31; :: thesis:

end;

then consider z1 being FinSequence of ExtREAL such that
A78: dom z1 = dom FG and
A79: for n being Nat st n in dom z1 holds
z1 . n = (c1 . n) * ((M * FG) . n) ;
A80: dom f = union (rng FG)

proof

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

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A81: z in dom f ; :: thesis:
then consider Y being set such that
A82: ( z in Y & Y in rng F ) by A9, TARSKI:def 4;
consider i being set such that
A83: ( i in dom F & Y = F . i ) by A82, FUNCT_1:def 5;
reconsider i = i as Element of NAT by A83;
consider Z being set such that
A84: ( z in Z & Z in rng G ) by A5, A11, A81, TARSKI:def 4;
consider j being set such that
A85: ( j in dom G & Z = G . j ) by A84, FUNCT_1:def 5;
reconsider j = j as Element of NAT by A85;
set k = ((i - 1) * (len b)) + j;
i in Seg (len a) by A10, A83, FINSEQ_1:def 3;
then A86: ( 1 <= i & i <= len a ) by FINSEQ_1:3;
then consider i' being Nat such that
A87: i = 1 + i' by NAT_1:10;
reconsider k = ((i - 1) * (len b)) + j as Nat by A87;
j in Seg (len b) by A12, A85, FINSEQ_1:def 3;
then A88: ( 1 <= j & j <= len b ) by FINSEQ_1:3;
then consider j' being Nat such that
A89: j = 1 + j' by NAT_1:10;
A90: k >= 0 + j by A87, XREAL_1:8;
then A91: k >= 1 by A88, XXREAL_0:2;
A92: k -' 1 = k - 1 by A88, A90, XREAL_1:235, XXREAL_0:2
.= (i' * (len b)) + j' by A87, A89 ;
A93: j' < len b by A88, A89, NAT_1:13;
then A94: i = ((k -' 1) div (len b)) + 1 by A87, A92, NAT_D:def 1;
A95: j = ((k -' 1) mod (len b)) + 1 by A89, A92, A93, NAT_D:def 2;
i - 1 <= (len a) - 1 by A86, XREAL_1:11;
then (i - 1) * (len b) <= ((len a) - 1) * (len b) by XREAL_1:66;
then A96: k <= (((len a) - 1) * (len b)) + j by XREAL_1:8;
(((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b) by A88, XREAL_1:8;
then k <= (len a) * (len b) by A96, XXREAL_0:2;
then A97: k in Seg ((len a) * (len b)) by A91, FINSEQ_1:3;
then A98: k in dom FG by A13, FINSEQ_1:def 3;
z in (F . i) /\ (G . j) by A82, A83, A84, A85, XBOOLE_0:def 4;
then A99: z in FG . k by A14, A94, A95, A97, A15;
FG . k in rng FG by A98, FUNCT_1:def 5;
hence z in union (rng FG) by A99, TARSKI:def 4; :: thesis:

end;

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in union (rng FG) ; :: thesis:
then consider Y being set such that
A100: ( z in Y & Y in rng FG ) by TARSKI:def 4;
consider k being set such that
A101: ( k in dom FG & Y = FG . k ) by A100, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A101;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
k in Seg ((len a) * (len b)) by A13, A101, FINSEQ_1:def 3;
then FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A15;
then A102: z in F . (((k -' 1) div (len b)) + 1) by A100, A101, XBOOLE_0:def 4;
reconsider i = ((k -' 1) div (len b)) + 1 as Nat ;
k in Seg (len FG) by A101, FINSEQ_1:def 3;
then A103: ( 1 <= k & k <= (len a) * (len b) ) by A13, FINSEQ_1:3;
A104: ( i >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
reconsider la' = len a, lb' = len b as natural number ;
A105: len b <> 0 by A103;
then len b > 0 ;
then len b >= 0 + 1 by NAT_1:13;
then ( lb' divides la' * lb' & 1 <= (len a) * (len b) & 1 <= len b ) by A103, NAT_D:def 3, XXREAL_0:2;
then A106: ((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A103, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A106, NAT_2:26;
then A107: i <= ((len a) * (len b)) div (len b) by XREAL_1:21;
((len a) * (len b)) div (len b) = len a by A105, NAT_D:18;
then i in Seg (len a) by A104, A107, FINSEQ_1:3;
then i in dom F by A10, FINSEQ_1:def 3;
then F . i in rng F by FUNCT_1:def 5;
hence z in dom f by A9, A102, TARSKI:def 4; :: thesis:

end;

A108: g is real-valued by A4, MESFUNC2:def 5;
then A109: dom (f + g) = (dom f) /\ (dom f) by A5, MESFUNC2:2
.= dom f ;
A110: dom (f + g) = (dom g) /\ (dom g) by A5, A108, MESFUNC2:2
.= dom g ;
A111: f + g is real-valued

proof

now

let x be Element of X; :: thesis:
assume A112: x in dom (f + g) ; :: thesis:
f is real-valued by A1, MESFUNC2:def 5;
then A113: |.(f . x).| < +infty by A109, A112, MESFUNC2:def 1;
g is real-valued by A4, MESFUNC2:def 5;
then A114: |.(g . x).| < +infty by A110, A112, MESFUNC2:def 1;
|.((f + g) . x).| = |.((f . x) + (g . x)).| by A112, MESFUNC1:def 3;
then A115: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by A113, EXTREAL2:61, EXTREAL2:67;
|.(f . x).| + |.(g . x).| <> +infty by A113, A114, XXREAL_3:16;
hence |.((f + g) . x).| < +infty by A115, XXREAL_0:2, XXREAL_0:4; :: thesis:

end;

hence f + g is real-valued by MESFUNC2:def 1; :: thesis:

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

let k be Nat; :: thesis:
let x, y be Element of X; :: thesis:
assume A116: ( k in dom FG & x in FG . k & y in FG . k ) ; :: thesis:
then k in Seg ((len a) * (len b)) by A13, FINSEQ_1:def 3;
then A117: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A15;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
k in Seg (len FG) by A116, FINSEQ_1:def 3;
then A118: ( 1 <= k & k <= (len a) * (len b) ) by A13, FINSEQ_1:3;
A119: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
reconsider la' = len a, lb' = len b as natural number ;
A120: len b <> 0 by A118;
then A121: len b > 0 ;
then len b >= 0 + 1 by NAT_1:13;
then ( lb' divides la' * lb' & 1 <= (len a) * (len b) & 1 <= len b ) by A118, NAT_D:def 3, XXREAL_0:2;
then A122: ((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A118, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A122, NAT_2:26;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
then ((k -' 1) div (len b)) + 1 <= len a by A120, NAT_D:18;
then A123: ((k -' 1) div (len b)) + 1 in Seg (len a) by A119, FINSEQ_1:3;
(k -' 1) mod (len b) < len b by A121, NAT_D:1;
then ((k -' 1) mod (len b)) + 1 <= len b by NAT_1:13;
then A124: ((k -' 1) mod (len b)) + 1 in Seg (len b) by A119, FINSEQ_1:3;
A125: ((k -' 1) div (len b)) + 1 in dom F by A10, A123, FINSEQ_1:def 3;
A126: ((k -' 1) mod (len b)) + 1 in dom G by A12, A124, FINSEQ_1:def 3;
A127: x in F . (((k -' 1) div (len b)) + 1) by A116, A117, XBOOLE_0:def 4;
A128: x in G . (((k -' 1) mod (len b)) + 1) by A116, A117, XBOOLE_0:def 4;
A129: f . x = a . (((k -' 1) div (len b)) + 1) by A7, A125, A127, MESFUNC3:def 1;
A130: y in F . (((k -' 1) div (len b)) + 1) by A116, A117, XBOOLE_0:def 4;
A131: y in G . (((k -' 1) mod (len b)) + 1) by A116, A117, XBOOLE_0:def 4;
A132: f . y = a . (((k -' 1) div (len b)) + 1) by A7, A125, A130, MESFUNC3:def 1;
A133: FG . k in rng FG by A116, FUNCT_1:def 5;
then A134: x in dom (f + g) by A80, A109, A116, TARSKI:def 4;
A135: y in dom (f + g) by A80, A109, A116, A133, TARSKI:def 4;
thus (f + g) . x = (f . x) + (g . x) by A134, MESFUNC1:def 3
.= (a . (((k -' 1) div (len b)) + 1)) + (b . (((k -' 1) mod (len b)) + 1)) by A8, A126, A128, A129, MESFUNC3:def 1
.= (f . y) + (g . y) by A8, A126, A131, A132, MESFUNC3:def 1
.= (f + g) . y by A135, MESFUNC1:def 3 ; :: thesis:

end;

hence A136: f + g is_simple_func_in S by A80, A109, A111, MESFUNC2:def 5; :: thesis:
thus dom (f + g) <> {} by A2, A109; :: thesis:
thus A137: for x being set st x in dom (f + g) holds
0. <= (f + g) . x :: thesis:

proof

let x be set ; :: thesis:
assume A138: x in dom (f + g) ; :: thesis:
then A139: 0. <= f . x by A3, A109;
0. <= g . x by A6, A110, A138;
then A140: 0. <= (f . x) + (g . x) by A139;
dom f c= X by RELAT_1:def 18;
hence 0. <= (f + g) . x by A109, A138, A140, MESFUNC1:def 3; :: thesis:

end;

A141: for k being Nat st k in dom FG holds
for x being set st x in FG . k holds
f . x = a1 . k

proof

let k be Nat; :: thesis:
assume A142: k in dom FG ; :: thesis:
let x be set ; :: thesis:
assume A143: x in FG . k ; :: thesis:
k in Seg ((len a) * (len b)) by A13, A142, FINSEQ_1:def 3;
then A144: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A15;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
k in Seg (len FG) by A142, FINSEQ_1:def 3;
then A145: ( 1 <= k & k <= (len a) * (len b) ) by A13, FINSEQ_1:3;
A146: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
reconsider la' = len a, lb' = len b as natural number ;
A147: len b <> 0 by A145;
then len b > 0 ;
then len b >= 0 + 1 by NAT_1:13;
then ( lb' divides la' * lb' & 1 <= (len a) * (len b) & 1 <= len b ) by A145, NAT_D:def 3, XXREAL_0:2;
then A148: ((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A145, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:26;
then A149: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A148, XREAL_1:21;
((len a) * (len b)) div (len b) = len a by A147, NAT_D:18;
then ((k -' 1) div (len b)) + 1 in Seg (len a) by A146, A149, FINSEQ_1:3;
then A150: ((k -' 1) div (len b)) + 1 in dom F by A10, FINSEQ_1:def 3;
A151: x in F . (((k -' 1) div (len b)) + 1) by A143, A144, XBOOLE_0:def 4;
A152: k in Seg (len FG) by A142, FINSEQ_1:def 3;
thus f . x = a . (((k -' 1) div (len b)) + 1) by A7, A150, A151, MESFUNC3:def 1
.= a1 . k by A59, A152, A60 ; :: thesis:

end;

A153: FG,a1 are_Re-presentation_of f

proof

thus dom f = union (rng FG) by A80; :: according to MESFUNC3:def 1 :: thesis:
thus dom FG = Seg (len a1) by A58, FINSEQ_1:def 3
.= dom a1 by FINSEQ_1:def 3 ; :: thesis:
thus for b₁ being set holds
( not b₁ in dom FG or for b₂ being set holds
( not b₂ in FG . b₁ or f . b₂ = a1 . b₁ ) ) by A141; :: thesis:

end;

A154: for k being Nat st k in dom FG holds
for x being set st x in FG . k holds
g . x = b1 . k

proof

let k be Nat; :: thesis:
assume A155: k in dom FG ; :: thesis:
let x be set ; :: thesis:
assume A156: x in FG . k ; :: thesis:
k in Seg ((len a) * (len b)) by A13, A155, FINSEQ_1:def 3;
then A157: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A15;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
k in Seg (len FG) by A155, FINSEQ_1:def 3;
then A158: ( 1 <= k & k <= (len a) * (len b) ) by A13, FINSEQ_1:3;
A159: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
len b <> 0 by A158;
then len b > 0 ;
then (k -' 1) mod (len b) < len b by NAT_D:1;
then ((k -' 1) mod (len b)) + 1 <= len b by NAT_1:13;
then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A159, FINSEQ_1:3;
then A160: ((k -' 1) mod (len b)) + 1 in dom G by A12, FINSEQ_1:def 3;
A161: x in G . (((k -' 1) mod (len b)) + 1) by A156, A157, XBOOLE_0:def 4;
A162: k in Seg (len FG) by A155, FINSEQ_1:def 3;
thus g . x = b . (((k -' 1) mod (len b)) + 1) by A8, A160, A161, MESFUNC3:def 1
.= b1 . k by A66, A162, A67 ; :: thesis:

end;

A163: FG,b1 are_Re-presentation_of g

proof

thus dom g = union (rng FG) by A5, A80; :: according to MESFUNC3:def 1 :: thesis:
thus dom FG = Seg (len b1) by A65, FINSEQ_1:def 3
.= dom b1 by FINSEQ_1:def 3 ; :: thesis:
thus for b₁ being set holds
( not b₁ in dom FG or for b₂ being set holds
( not b₂ in FG . b₁ or g . b₂ = b1 . b₁ ) ) by A154; :: thesis:

end;

A164: for k being Nat st k in dom FG holds
for x being set st x in FG . k holds
(f + g) . x = c1 . k

proof

let k be Nat; :: thesis:
assume A165: k in dom FG ; :: thesis:
let x be set ; :: thesis:
assume A166: x in FG . k ; :: thesis:
FG . k in rng FG by A165, FUNCT_1:def 5;
then A167: x in dom (f + g) by A80, A109, A166, TARSKI:def 4;
A168: k in Seg (len FG) by A165, FINSEQ_1:def 3;
dom (f + g) c= X by RELAT_1:def 18;
hence (f + g) . x = (f . x) + (g . x) by A167, MESFUNC1:def 3
.= (a1 . k) + (g . x) by A141, A165, A166
.= (a1 . k) + (b1 . k) by A154, A165, A166
.= c1 . k by A74, A168, A75 ;
:: thesis:

end;

A169: FG,c1 are_Re-presentation_of f + g

proof

thus dom (f + g) = union (rng FG) by A80, A109; :: according to MESFUNC3:def 1 :: thesis:
thus dom FG = dom c1 by A73, FINSEQ_3:31; :: thesis:
thus for b₁ being set holds
( not b₁ in dom FG or for b₂ being set holds
( not b₂ in FG . b₁ or (f + g) . b₂ = c1 . b₁ ) ) by A164; :: thesis:

end;

A170: integral X,S,M,f = Sum x1 by A1, A2, A3, A63, A64, A153, Th3;
A171: integral X,S,M,g = Sum y1 by A2, A4, A5, A6, A71, A72, A163, Th3;
A172: integral X,S,M,(f + g) = Sum z1 by A2, A78, A79, A109, A136, A137, A169, Th3;
A173: for i being Nat st i in dom x1 holds
0. <= x1 . i

proof

let i be Nat; :: thesis:
assume A174: i in dom x1 ; :: thesis:
then A175: x1 . i = (a1 . i) * ((M * FG) . i) by A64;
A176: i in Seg (len FG) by A63, A174, FINSEQ_1:def 3;
set i' = ((i -' 1) div (len b)) + 1;
A177: ( 1 <= i & i <= (len a) * (len b) ) by A13, A176, FINSEQ_1:3;
A178: ((i -' 1) div (len b)) + 1 >= 0 + 1 by XREAL_1:8;
reconsider la' = len a, lb' = len b as natural number ;
A179: len b <> 0 by A177;
then len b > 0 ;
then len b >= 0 + 1 by NAT_1:13;
then ( lb' divides la' * lb' & 1 <= (len a) * (len b) & 1 <= len b ) by A177, NAT_D:def 3, XXREAL_0:2;
then A180: ((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 1 by NAT_2:17;
i -' 1 <= ((len a) * (len b)) -' 1 by A177, NAT_D:42;
then (i -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A180, NAT_2:26;
then A181: ((i -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
((len a) * (len b)) div (len b) = len a by A179, NAT_D:18;
then ((i -' 1) div (len b)) + 1 in Seg (len a) by A178, A181, FINSEQ_1:3;
then A182: ((i -' 1) div (len b)) + 1 in dom F by A10, FINSEQ_1:def 3;

per cases ;

suppose F . (((i -' 1) div (len b)) + 1) <> {} ; :: thesis:

then consider x' being set such that
A183: x' in F . (((i -' 1) div (len b)) + 1) by XBOOLE_0:def 1;
A184: f . x' = a . (((i -' 1) div (len b)) + 1) by A7, A182, A183, MESFUNC3:def 1
.= a1 . i by A59, A176, A60 ;
F . (((i -' 1) div (len b)) + 1) c= dom f by A9, A182, FUNCT_1:12, ZFMISC_1:92;
then A185: 0. <= a1 . i by A3, A183, A184;
A186: FG . i in rng FG by A63, A174, FUNCT_1:12;
rng FG c= S by FINSEQ_1:def 4;
then reconsider FGi = FG . i as Element of S by A186;
reconsider EMPTY = {} as Element of S by MEASURE1:21;
EMPTY c= FGi by XBOOLE_1:2;
then A187: M . {} <= M . FGi by MEASURE1:62;
M . {} = 0. by VALUED_0:def 19;
then 0. <= (M * FG) . i by A63, A174, A187, FUNCT_1:23;
hence 0. <= x1 . i by A175, A185; :: thesis:

end;

suppose A188: F . (((i -' 1) div (len b)) + 1) = {} ; :: thesis:

FG . i = (F . (((i -' 1) div (len b)) + 1)) /\ (G . (((i -' 1) mod (len b)) + 1)) by A14, A63, A174;
then M . (FG . i) = 0. by A188, VALUED_0:def 19;
then (M * FG) . i = 0. by A63, A174, FUNCT_1:23;
hence 0. <= x1 . i by A175; :: thesis:

end;

A189: for i being Nat st i in dom y1 holds
0. <= y1 . i

proof

let i be Nat; :: thesis:
assume A190: i in dom y1 ; :: thesis:
then A191: y1 . i = (b1 . i) * ((M * FG) . i) by A72;
A192: i in Seg (len FG) by A71, A190, FINSEQ_1:def 3;
set i' = ((i -' 1) mod (len b)) + 1;
A193: ( 1 <= i & i <= (len a) * (len b) ) by A13, A192, FINSEQ_1:3;
A194: ((i -' 1) mod (len b)) + 1 >= 0 + 1 by XREAL_1:8;
len b <> 0 by A193;
then len b > 0 ;
then (i -' 1) mod (len b) < len b by NAT_D:1;
then ((i -' 1) mod (len b)) + 1 <= len b by NAT_1:13;
then ((i -' 1) mod (len b)) + 1 in Seg (len b) by A194, FINSEQ_1:3;
then A195: ((i -' 1) mod (len b)) + 1 in dom G by A12, FINSEQ_1:def 3;

per cases ;

suppose G . (((i -' 1) mod (len b)) + 1) <> {} ; :: thesis:

then consider x' being set such that
A196: x' in G . (((i -' 1) mod (len b)) + 1) by XBOOLE_0:def 1;
A197: g . x' = b . (((i -' 1) mod (len b)) + 1) by A8, A195, A196, MESFUNC3:def 1
.= b1 . i by A66, A192, A67 ;
G . (((i -' 1) mod (len b)) + 1) c= dom g by A11, A195, FUNCT_1:12, ZFMISC_1:92;
then A198: 0. <= b1 . i by A6, A196, A197;
A199: FG . i in rng FG by A71, A190, FUNCT_1:12;
rng FG c= S by FINSEQ_1:def 4;
then reconsider FGi = FG . i as Element of S by A199;
reconsider EMPTY = {} as Element of S by MEASURE1:21;
EMPTY c= FGi by XBOOLE_1:2;
then A200: M . {} <= M . FGi by MEASURE1:62;
M . {} = 0. by VALUED_0:def 19;
then 0. <= (M * FG) . i by A71, A190, A200, FUNCT_1:23;
hence 0. <= y1 . i by A191, A198; :: thesis:

end;

suppose A201: G . (((i -' 1) mod (len b)) + 1) = {} ; :: thesis:

FG . i = (F . (((i -' 1) div (len b)) + 1)) /\ (G . (((i -' 1) mod (len b)) + 1)) by A14, A71, A190;
then M . (FG . i) = 0. by A201, VALUED_0:def 19;
then (M * FG) . i = 0. by A71, A190, FUNCT_1:23;
hence 0. <= y1 . i by A191; :: thesis:

end;

z1 = x1 + y1

proof

not -infty in rng x1

proof

assume -infty in rng x1 ; :: thesis:
then consider i being set such that
A202: ( i in dom x1 & x1 . i = -infty ) by FUNCT_1:def 5;
thus contradiction by A173, A202; :: thesis:

end;

then A203: (x1 " {-infty }) /\ (y1 " {+infty }) = {} /\ (y1 " {+infty }) by FUNCT_1:142
.= {} ;
not -infty in rng y1

proof

assume -infty in rng y1 ; :: thesis:
then consider i being set such that
A204: ( i in dom y1 & y1 . i = -infty ) by FUNCT_1:def 5;
thus contradiction by A189, A204; :: thesis:

end;

then (x1 " {+infty }) /\ (y1 " {-infty }) = (x1 " {+infty }) /\ {} by FUNCT_1:142
.= {} ;
then A205: dom (x1 + y1) = ((dom x1) /\ (dom y1)) \ ({} \/ {} ) by A203, MESFUNC1:def 3
.= dom z1 by A63, A71, A78 ;
A206: for k being Nat st k in dom z1 holds
z1 . k = (x1 + y1) . k

proof

let k be Nat; :: thesis:
assume A207: k in dom z1 ; :: thesis:
then A208: k in Seg (len FG) by A78, FINSEQ_1:def 3;
set p = ((k -' 1) div (len b)) + 1;
set q = ((k -' 1) mod (len b)) + 1;
A209: ( 1 <= k & k <= (len a) * (len b) ) by A13, A208, FINSEQ_1:3;
A210: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
reconsider la' = len a, lb' = len b as natural number ;
A211: len b <> 0 by A209;
then A212: len b > 0 ;
then len b >= 0 + 1 by NAT_1:13;
then ( lb' divides la' * lb' & 1 <= (len a) * (len b) & 1 <= len b ) by A209, NAT_D:def 3, XXREAL_0:2;
then A213: ((la' * lb') -' 1) div lb' = ((la' * lb') div lb') - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A209, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A213, NAT_2:26;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
then ((k -' 1) div (len b)) + 1 <= len a by A211, NAT_D:18;
then A214: ((k -' 1) div (len b)) + 1 in Seg (len a) by A210, FINSEQ_1:3;
(k -' 1) mod (len b) < len b by A212, NAT_D:1;
then ((k -' 1) mod (len b)) + 1 <= len b by NAT_1:13;
then A215: ((k -' 1) mod (len b)) + 1 in Seg (len b) by A210, FINSEQ_1:3;
A216: ((k -' 1) div (len b)) + 1 in dom F by A10, A214, FINSEQ_1:def 3;
A217: ((k -' 1) mod (len b)) + 1 in dom G by A12, A215, FINSEQ_1:def 3;
A218: ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))

proof

per cases ;

suppose FG . k <> {} ; :: thesis:

then (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) <> {} by A14, A78, A207;
then consider v being set such that
A219: v in (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by XBOOLE_0:def 1;
A220: ( v in F . (((k -' 1) div (len b)) + 1) & v in G . (((k -' 1) mod (len b)) + 1) ) by A219, XBOOLE_0:def 4;
then A221: a . (((k -' 1) div (len b)) + 1) = f . v by A7, A216, MESFUNC3:def 1;
F . (((k -' 1) div (len b)) + 1) in rng F by A216, FUNCT_1:12;
then v in dom f by A9, A220, TARSKI:def 4;
then 0. <= a . (((k -' 1) div (len b)) + 1) by A3, A221;
then A222: ( 0. = a1 . k or 0. < a1 . k ) by A59, A208, A60;
A223: b . (((k -' 1) mod (len b)) + 1) = g . v by A8, A217, A220, MESFUNC3:def 1;
G . (((k -' 1) mod (len b)) + 1) in rng G by A217, FUNCT_1:12;
then v in dom g by A11, A220, TARSKI:def 4;
then 0. <= b . (((k -' 1) mod (len b)) + 1) by A6, A223;
then ( 0. = b1 . k or 0. < b1 . k ) by A66, A208, A67;
hence ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A222, XXREAL_3:107; :: thesis:

end;

suppose FG . k = {} ; :: thesis:

then M . (FG . k) = 0. by VALUED_0:def 19;
then X: (M * FG) . k = 0. by A78, A207, FUNCT_1:23;
hence ((a1 . k) + (b1 . k)) * ((M * FG) . k) = 0
.= ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by X ;
:: thesis:

end;

thus z1 . k = (c1 . k) * ((M * FG) . k) by A79, A207
.= ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A74, A208, A218, A75
.= (x1 . k) + ((b1 . k) * ((M * FG) . k)) by A63, A64, A78, A207
.= (x1 . k) + (y1 . k) by A71, A72, A78, A207
.= (x1 + y1) . k by A205, A207, MESFUNC1:def 3 ; :: thesis:

end;

dom (x1 + y1) = Seg (len z1) by A205, FINSEQ_1:def 3;
then x1 + y1 is FinSequence by FINSEQ_1:def 2;
hence z1 = x1 + y1 by A205, A206, FINSEQ_1:17; :: thesis:

end;

hence integral X,S,M,(f + g) = (integral X,S,M,f) + (integral X,S,M,g) by A63, A71, A170, A171, A172, A173, A189, Th1; :: thesis: