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 <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative holds
( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being object st x in dom (f + g) holds
0. <= (f + g) . x ) & integral (M,(f + g)) = (integral (M,f)) + (integral (M,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 <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative holds
( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being object st x in dom (f + g) holds
0. <= (f + g) . x ) & integral (M,(f + g)) = (integral (M,f)) + (integral (M,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 <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative holds
( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being object st x in dom (f + g) holds
0. <= (f + g) . x ) & integral (M,(f + g)) = (integral (M,f)) + (integral (M,g)) )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & dom f <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative implies ( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being object st x in dom (f + g) holds
0. <= (f + g) . x ) & integral (M,(f + g)) = (integral (M,f)) + (integral (M,g)) ) )
assume that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: f is nonnegative and
A4: g is_simple_func_in S and
A5: dom g = dom f and
A6: g is nonnegative ; :: thesis: ( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being object st x in dom (f + g) holds
0. <= (f + g) . x ) & integral (M,(f + g)) = (integral (M,f)) + (integral (M,g)) )
A7: g is real-valued by A4, MESFUNC2:def 4;
then A8: dom (f + g) = (dom f) /\ (dom f) by A5, MESFUNC2:2
.= dom f ;
consider G being Finite_Sep_Sequence of S, b, y being FinSequence of ExtREAL such that
A9: 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 (M,g) = Sum y by A2, A4, A5, A6, Th4;
set lb = len b;
consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A10: 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 (M,f) = Sum x by A1, A2, A3, Th4;
deffunc H1( Nat) -> Element of ExtREAL = b . ((($1 -' 1) mod (len b)) + 1);
deffunc H2( Nat) -> Element of ExtREAL = a . ((($1 -' 1) div (len b)) + 1);
set la = len a;
A11: dom F = dom a by A10, MESFUNC3:def 1;
deffunc H3( Nat) -> set = (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 = H3(k) from FINSEQ_1:sch 2();
 A14: dom FG = Seg ((len a) * (len b)) by A12, FINSEQ_1:def 3;
A15: dom G = dom b by A9, MESFUNC3:def 1;
now :: thesis: for k being Nat st k in dom FG holds
FG . k in S
reconsider la9 = len a, lb9 = len b as Nat ;
let k be Nat; :: thesis: ( k in dom FG implies FG . k in S )
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
assume A16: k in dom FG ; :: thesis: FG . k in S
then A17: k in Seg ((len a) * (len b)) by A12, FINSEQ_1:def 3;
then A18: k <= (len a) * (len b) by FINSEQ_1:1;
then k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;
then A19: (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:24;
1 <= k by A17, FINSEQ_1:1;
then A20: ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A18, NAT_D:def 3, XXREAL_0:2;
A21: len b <> 0 by A17;
then len b >= 0 + 1 by NAT_1:13;
then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A20, NAT_2:15;
then A22: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A19, XREAL_1:19;
reconsider la = len a, lb = len b as Nat ;
( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= la ) by A21, A22, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len b)) + 1 in Seg la by FINSEQ_1:1;
then ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def 3;
then A23: F . (((k -' 1) div (len b)) + 1) in rng F by FUNCT_1:3;
(k -' 1) mod lb < lb by A21, NAT_D:1;
then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= lb ) by NAT_1:13;
then ((k -' 1) mod (len b)) + 1 in Seg lb by FINSEQ_1:1;
then ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def 3;
then A24: G . (((k -' 1) mod (len b)) + 1) in rng G by FUNCT_1:3;
( rng F c= S & rng G c= S ) by FINSEQ_1:def 4;
then (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) in S by A23, A24, MEASURE1:34;
hence FG . k in S by A13, A16; :: 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 a, lb9 = len b 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
A25: k in dom FG and
A26: l in dom FG and
A27: k <> l ; :: thesis: FG . k misses FG . l
A28: l in Seg ((len a) * (len b)) by A12, A26, FINSEQ_1:def 3;
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;
then A31: k <= (len a) * (len b) by FINSEQ_1:1;
A32: 1 <= k by A30, FINSEQ_1:1;
then A33: ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A31, NAT_D:def 3, XXREAL_0:2;
A34: len b <> 0 by A30;
then len b >= 0 + 1 by NAT_1:13;
then A35: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 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 A36: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;
reconsider la = len a, lb = len b as Nat ;
( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= la ) by A34, A36, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len b)) + 1 in Seg la by FINSEQ_1:1;
then A37: ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def 3;
A38: 1 <= l by A28, FINSEQ_1:1;
A39: ( ((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
(l -' 1) + 1 = ((((((l -' 1) div (len b)) + 1) - 1) * lb) + ((((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) * lb) + (((l -' 1) mod (len b)) + 1) by A38, XREAL_1:233;
(k -' 1) + 1 = ((((((k -' 1) div (len b)) + 1) - 1) * lb) + ((((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) * lb) + (((k -' 1) mod (len b)) + 1) by A32, XREAL_1:233;
assume ( ((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: contradiction
hence contradiction by A27, A41, A40; :: thesis: verum
end;
(l -' 1) mod lb < lb by A34, NAT_D:1;
then ( ((l -' 1) mod (len b)) + 1 >= 0 + 1 & ((l -' 1) mod (len b)) + 1 <= lb ) by NAT_1:13;
then ((l -' 1) mod (len b)) + 1 in Seg lb by FINSEQ_1:1;
then A42: ((l -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def 3;
(k -' 1) mod lb < lb by A34, NAT_D:1;
then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= lb ) by NAT_1:13;
then ((k -' 1) mod (len b)) + 1 in Seg lb by FINSEQ_1:1;
then A43: ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def 3;
l <= la * lb by A28, FINSEQ_1:1;
then l -' 1 <= (la * lb) -' 1 by NAT_D:42;
then (l -' 1) div lb <= ((la * lb) div lb) - 1 by A35, NAT_2:24;
then ((l -' 1) div lb) + 1 <= (la * lb) div lb by XREAL_1:19;
then ( ((l -' 1) div (len b)) + 1 >= 0 + 1 & ((l -' 1) div (len b)) + 1 <= la ) by A34, NAT_D:18, XREAL_1:6;
then ((l -' 1) div (len b)) + 1 in Seg la by FINSEQ_1:1;
then A44: ((l -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def 3;
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 A39;
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
.= {} /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) 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 A43, 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
.= ((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 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;
consider a1 being FinSequence of ExtREAL such that
A47: len a1 = len FG and
A48: for k being Nat st k in dom a1 holds
a1 . k = H2(k) from FINSEQ_2:sch 1();
 consider b1 being FinSequence of ExtREAL such that
A49: len b1 = len FG and
A50: for k being Nat st k in dom b1 holds
b1 . k = H1(k) from FINSEQ_2:sch 1();
 A51: dom f = union (rng F) by A10, MESFUNC3:def 1;
A52: dom a1 = Seg (len FG) by A47, FINSEQ_1:def 3;
A53: for k being Nat st k in dom FG holds
for x being object st x in FG . k holds
f . x = a1 . k
proof
reconsider la9 = len a, lb9 = len b as Nat ;
let k be Nat; :: thesis: ( k in dom FG implies for x being object st x in FG . k holds
f . x = a1 . k )
set i = ((k -' 1) div (len b)) + 1;
assume A54: k in dom FG ; :: thesis: for x being object st x in FG . k holds
f . x = a1 . k
then A55: k in Seg (len FG) by FINSEQ_1:def 3;
A56: k in Seg (len FG) by A54, FINSEQ_1:def 3;
then A57: k <= (len a) * (len b) by A12, FINSEQ_1:1;
A58: len b <> 0 by A12, A56;
then A59: len b >= 0 + 1 by NAT_1:13;
1 <= k by A56, FINSEQ_1:1;
then ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A57, NAT_D:def 3, XXREAL_0:2;
then A60: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A59, NAT_2:15;
A61: ((len a) * (len b)) div (len b) = len a by A58, NAT_D:18;
k -' 1 <= ((len a) * (len b)) -' 1 by A57, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:24;
then ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) ) by A60, XREAL_1:6, XREAL_1:19;
then ((k -' 1) div (len b)) + 1 in Seg (len a) by A61, FINSEQ_1:1;
then A62: ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def 3;
let x be object ; :: thesis: ( x in FG . k implies f . x = a1 . k )
assume A63: x in FG . k ; :: thesis: f . x = a1 . k
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A54;
then x in F . (((k -' 1) div (len b)) + 1) by A63, XBOOLE_0:def 4;
hence f . x = a . (((k -' 1) div (len b)) + 1) by A10, A62, MESFUNC3:def 1
.= a1 . k by A48, A52, A55 ;
:: thesis: verum
end;
A64: dom b1 = Seg (len FG) by A49, FINSEQ_1:def 3;
A65: for k being Nat st k in dom FG holds
for x being object st x in FG . k holds
g . x = b1 . k
proof
let k be Nat; :: thesis: ( k in dom FG implies for x being object st x in FG . k holds
g . x = b1 . k )
set j = ((k -' 1) mod (len b)) + 1;
assume A66: k in dom FG ; :: thesis: for x being object st x in FG . k holds
g . x = b1 . k
then A67: k in Seg (len FG) by FINSEQ_1:def 3;
k in Seg (len FG) by A66, FINSEQ_1:def 3;
then len b <> 0 by A12;
then (k -' 1) mod (len b) < len b by NAT_D:1;
then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= len b ) by NAT_1:13;
then ((k -' 1) mod (len b)) + 1 in Seg (len b) by FINSEQ_1:1;
then A68: ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def 3;
let x be object ; :: thesis: ( x in FG . k implies g . x = b1 . k )
assume A69: x in FG . k ; :: thesis: g . x = b1 . k
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A66;
then x in G . (((k -' 1) mod (len b)) + 1) by A69, XBOOLE_0:def 4;
hence g . x = b . (((k -' 1) mod (len b)) + 1) by A9, A68, MESFUNC3:def 1
.= b1 . k by A50, A64, A67 ;
:: thesis: verum
end;
A70: dom g = union (rng G) by A9, MESFUNC3:def 1;
A71: dom f = union (rng FG)
proof
thus dom f c= union (rng FG) :: according to XBOOLE_0:def 10 :: thesis: union (rng FG) c= dom f
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom f or z in union (rng FG) )
assume A72: z in dom f ; :: thesis: z in union (rng FG)
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 A5, 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;
A79: j in Seg (len b) by A15, A77, FINSEQ_1:def 3;
then A80: 1 <= j by FINSEQ_1:1;
then consider j9 being Nat such that
A81: j = 1 + j9 by NAT_1:10;
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;
A84: i in Seg (len a) by A11, A82, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then consider i9 being Nat such that
A85: i = 1 + i9 by NAT_1:10;
A86: j <= len b by A79, FINSEQ_1:1;
then A87: j9 < len b by A81, NAT_1:13;
set k = ((i - 1) * (len b)) + j;
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 A84, FINSEQ_1:1;
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 A86, XREAL_1:6;
then A92: k <= (len a) * (len b) by A91, XXREAL_0:2;
k >= 1 by A80, A88, XXREAL_0:2;
then A93: k in Seg ((len a) * (len b)) by A92, FINSEQ_1:1;
then k in dom FG by A12, FINSEQ_1:def 3;
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;
reconsider la9 = len a, lb9 = len b 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
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) by A96, A99, XBOOLE_0:def 4;
A101: k in Seg (len FG) by A98, FINSEQ_1:def 3;
then A102: k <= (len a) * (len b) by A12, FINSEQ_1:1;
A103: len b <> 0 by A12, A101;
then A104: len b >= 0 + 1 by NAT_1:13;
1 <= k by A101, FINSEQ_1:1;
then ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A102, NAT_D:def 3, XXREAL_0:2;
then A105: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A104, NAT_2:15;
reconsider i = ((k -' 1) div (len b)) + 1 as Nat ;
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 ( i >= 0 + 1 & i <= ((len a) * (len b)) div (len b) ) by XREAL_1:6, XREAL_1:19;
then i in Seg (len a) by A106, FINSEQ_1:1;
then i in dom F by A11, FINSEQ_1:def 3;
then F . i in rng F by FUNCT_1:def 3;
hence z in dom f by A51, A100, TARSKI: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
reconsider la9 = len a, lb9 = len b 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
A108: k in dom FG and
A109: x in FG . k and
A110: y in FG . k ; :: thesis: (f + g) . x = (f + g) . y
set j = ((k -' 1) mod (len b)) + 1;
A111: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A108;
then A112: x in G . (((k -' 1) mod (len b)) + 1) by A109, XBOOLE_0:def 4;
set i = ((k -' 1) div (len b)) + 1;
A113: k in Seg (len FG) by A108, FINSEQ_1:def 3;
then A114: k <= (len a) * (len b) by A12, FINSEQ_1:1;
then A115: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;
1 <= k by A113, FINSEQ_1:1;
then A116: ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A114, NAT_D:def 3, XXREAL_0:2;
A117: len b <> 0 by A12, A113;
then len b >= 0 + 1 by NAT_1:13;
then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 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 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= len a ) by A117, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len b)) + 1 in Seg (len a) by FINSEQ_1:1;
then A118: ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def 3;
x in F . (((k -' 1) div (len b)) + 1) by A109, A111, XBOOLE_0:def 4;
then A119: f . x = a . (((k -' 1) div (len b)) + 1) by A10, A118, MESFUNC3:def 1;
(k -' 1) mod (len b) < len b by A117, NAT_D:1;
then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= len b ) by NAT_1:13;
then ((k -' 1) mod (len b)) + 1 in Seg (len b) by FINSEQ_1:1;
then A120: ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def 3;
y in F . (((k -' 1) div (len b)) + 1) by A110, A111, XBOOLE_0:def 4;
then A121: f . y = a . (((k -' 1) div (len b)) + 1) by A10, A118, MESFUNC3:def 1;
A122: y in G . (((k -' 1) mod (len b)) + 1) by A110, A111, XBOOLE_0:def 4;
A123: FG . k in rng FG by A108, FUNCT_1:def 3;
then A124: y in dom (f + g) by A71, A8, A110, TARSKI:def 4;
x in dom (f + g) by A71, A8, A109, A123, 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, A120, A112, A119, MESFUNC3:def 1
.= (f . y) + (g . y) by A9, A120, A122, A121, MESFUNC3:def 1
.= (f + g) . y by A124, MESFUNC1:def 3 ;
:: thesis: verum
end;
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 H4( Nat) -> Element of ExtREAL = (b1 . $1) * ((M * FG) . $1);
consider y1 being FinSequence of ExtREAL such that
A125: ( len y1 = len FG & ( for k being Nat st k in dom y1 holds
y1 . k = H4(k) ) ) from FINSEQ_2:sch 1();
 take y1 ; :: thesis: ( dom y1 = dom FG & ( for n being Nat st n in dom y1 holds
y1 . n = (b1 . n) * ((M * FG) . n) ) )
dom y1 = Seg (len FG) by A125, 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 A125; :: thesis: verum
end;
then consider y1 being FinSequence of ExtREAL such that
A126: dom y1 = dom FG and
A127: for n being Nat st n in dom y1 holds
y1 . n = (b1 . n) * ((M * FG) . n) ;
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 H4( Nat) -> Element of ExtREAL = (a1 . $1) * ((M * FG) . $1);
consider x1 being FinSequence of ExtREAL such that
A128: ( len x1 = len FG & ( for k being Nat st k in dom x1 holds
x1 . k = H4(k) ) ) from FINSEQ_2:sch 1();
 take x1 ; :: thesis: ( dom x1 = dom FG & ( for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * FG) . n) ) )
thus ( dom x1 = dom FG & ( for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * FG) . n) ) ) by A128, FINSEQ_3:29; :: thesis: verum
end;
then consider x1 being FinSequence of ExtREAL such that
A129: dom x1 = dom FG and
A130: for n being Nat st n in dom x1 holds
x1 . n = (a1 . n) * ((M * FG) . n) ;
dom FG = Seg (len a1) by A47, FINSEQ_1:def 3
.= dom a1 by FINSEQ_1:def 3 ;
then FG,a1 are_Re-presentation_of f by A71, A53, MESFUNC3:def 1;
then A131: integral (M,f) = Sum x1 by A1, A2, A3, A129, A130, Th3;
deffunc H4( Nat) -> Element of ExtREAL = (a1 . $1) + (b1 . $1);
consider c1 being FinSequence of ExtREAL such that
A132: len c1 = len FG and
A133: for k being Nat st k in dom c1 holds
c1 . k = H4(k) from FINSEQ_2:sch 1();
 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 H5( Nat) -> Element of ExtREAL = (c1 . $1) * ((M * FG) . $1);
consider z1 being FinSequence of ExtREAL such that
A134: ( len z1 = len FG & ( for k being Nat st k in dom z1 holds
z1 . k = H5(k) ) ) from FINSEQ_2:sch 1();
 take z1 ; :: thesis: ( dom z1 = dom FG & ( for n being Nat st n in dom z1 holds
z1 . n = (c1 . n) * ((M * FG) . n) ) )
thus ( dom z1 = dom FG & ( for n being Nat st n in dom z1 holds
z1 . n = (c1 . n) * ((M * FG) . n) ) ) by A134, FINSEQ_3:29; :: thesis: verum
end;
then consider z1 being FinSequence of ExtREAL such that
A135: dom z1 = dom FG and
A136: for n being Nat st n in dom z1 holds
z1 . n = (c1 . n) * ((M * FG) . n) ;
A137: dom c1 = Seg (len FG) by A132, FINSEQ_1:def 3;
A138: for k being Nat st k in dom FG holds
for x being object st x in FG . k holds
(f + g) . x = c1 . k
proof
let k be Nat; :: thesis: ( k in dom FG implies for x being object st x in FG . k holds
(f + g) . x = c1 . k )
A139: dom (f + g) c= X by RELAT_1:def 18;
assume A140: k in dom FG ; :: thesis: for x being object st x in FG . k holds
(f + g) . x = c1 . k
then A141: k in Seg (len FG) by FINSEQ_1:def 3;
let x be object ; :: thesis: ( x in FG . k implies (f + g) . x = c1 . k )
assume A142: x in FG . k ; :: thesis: (f + g) . x = c1 . k
FG . k in rng FG by A140, FUNCT_1:def 3;
then x in dom (f + g) by A71, A8, A142, TARSKI:def 4;
hence (f + g) . x = (f . x) + (g . x) by A139, MESFUNC1:def 3
.= (a1 . k) + (g . x) by A53, A140, A142
.= (a1 . k) + (b1 . k) by A65, A140, A142
.= c1 . k by A133, A137, A141 ;
:: thesis: verum
end;
A143: for i being Nat st i in dom y1 holds
0. <= y1 . i
proof
let i be Nat; :: thesis: ( i in dom y1 implies 0. <= y1 . i )
set i9 = ((i -' 1) mod (len b)) + 1;
assume A144: i in dom y1 ; :: thesis: 0. <= y1 . i
then A145: y1 . i = (b1 . i) * ((M * FG) . i) by A127;
A146: i in Seg (len FG) by A126, A144, FINSEQ_1:def 3;
then len b <> 0 by A12;
then (i -' 1) mod (len b) < len b by NAT_D:1;
then ( ((i -' 1) mod (len b)) + 1 >= 0 + 1 & ((i -' 1) mod (len b)) + 1 <= len b ) by NAT_1:13;
then ((i -' 1) mod (len b)) + 1 in Seg (len b) by FINSEQ_1:1;
then A147: ((i -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def 3;
per cases ( G . (((i -' 1) mod (len b)) + 1) <> {} or G . (((i -' 1) mod (len b)) + 1) = {} ) ;
suppose G . (((i -' 1) mod (len b)) + 1) <> {} ; :: thesis: 0. <= y1 . i
then consider x9 being object such that
A148: x9 in G . (((i -' 1) mod (len b)) + 1) by XBOOLE_0:def 1;
( FG . i in rng FG & rng FG c= S ) by A126, A144, FINSEQ_1:def 4, FUNCT_1:3;
then reconsider FGi = FG . i as Element of S ;
reconsider EMPTY = {} as Element of S by MEASURE1:7;
EMPTY c= FGi ;
then A149: M . {} <= M . FGi by MEASURE1:31;
g . x9 = b . (((i -' 1) mod (len b)) + 1) by A9, A147, A148, MESFUNC3:def 1
.= b1 . i by A50, A64, A146 ;
then A151: 0. <= b1 . i by A6, SUPINF_2:51;
M . {} = 0. by VALUED_0:def 19;
then 0. <= (M * FG) . i by A126, A144, A149, FUNCT_1:13;
hence 0. <= y1 . i by A145, A151; :: thesis: verum
end;
suppose A152: G . (((i -' 1) mod (len b)) + 1) = {} ; :: thesis: 0. <= y1 . i
FG . i = (F . (((i -' 1) div (len b)) + 1)) /\ (G . (((i -' 1) mod (len b)) + 1)) by A13, A126, A144;
then M . (FG . i) = 0. by A152, VALUED_0:def 19;
then (M * FG) . i = 0. by A126, A144, FUNCT_1:13;
hence 0. <= y1 . i by A145; :: thesis: verum
end;
end;
end;
then for i being object st i in dom y1 holds
0. <= y1 . i ;
then Y: y1 is nonnegative by SUPINF_2:52;
not -infty in rng y1
proof
assume -infty in rng y1 ; :: thesis: contradiction
then ex i being object st
( i in dom y1 & y1 . i = -infty ) by FUNCT_1:def 3;
hence contradiction by A143; :: thesis: verum
end;
then A153: (x1 " {+infty}) /\ (y1 " {-infty}) = (x1 " {+infty}) /\ {} by FUNCT_1:72
.= {} ;
A154: for i being Nat st i in dom x1 holds
0. <= x1 . i
proof
reconsider la9 = len a, lb9 = len b as Nat ;
let i be Nat; :: thesis: ( i in dom x1 implies 0. <= x1 . i )
set i9 = ((i -' 1) div (len b)) + 1;
assume A155: i in dom x1 ; :: thesis: 0. <= x1 . i
then A156: x1 . i = (a1 . i) * ((M * FG) . i) by A130;
A157: i in Seg (len FG) by A129, A155, FINSEQ_1:def 3;
then A158: i <= (len a) * (len b) by A12, FINSEQ_1:1;
A159: len b <> 0 by A12, A157;
then A160: len b >= 0 + 1 by NAT_1:13;
1 <= i by A157, FINSEQ_1:1;
then ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A158, NAT_D:def 3, XXREAL_0:2;
then A161: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A160, NAT_2:15;
i -' 1 <= ((len a) * (len b)) -' 1 by A158, NAT_D:42;
then (i -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A161, NAT_2:24;
then A162: ( ((i -' 1) div (len b)) + 1 >= 0 + 1 & ((i -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) ) by XREAL_1:6, XREAL_1:19;
((len a) * (len b)) div (len b) = len a by A159, NAT_D:18;
then ((i -' 1) div (len b)) + 1 in Seg (len a) by A162, FINSEQ_1:1;
then A163: ((i -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def 3;
per cases ( F . (((i -' 1) div (len b)) + 1) <> {} or F . (((i -' 1) div (len b)) + 1) = {} ) ;
suppose F . (((i -' 1) div (len b)) + 1) <> {} ; :: thesis: 0. <= x1 . i
then consider x9 being object such that
A164: x9 in F . (((i -' 1) div (len b)) + 1) by XBOOLE_0:def 1;
( FG . i in rng FG & rng FG c= S ) by A129, A155, FINSEQ_1:def 4, FUNCT_1:3;
then reconsider FGi = FG . i as Element of S ;
reconsider EMPTY = {} as Element of S by MEASURE1:7;
EMPTY c= FGi ;
then A165: M . {} <= M . FGi by MEASURE1:31;
f . x9 = a . (((i -' 1) div (len b)) + 1) by A10, A163, A164, MESFUNC3:def 1
.= a1 . i by A48, A52, A157 ;
then A167: 0. <= a1 . i by A3, SUPINF_2:51;
M . {} = 0. by VALUED_0:def 19;
then 0. <= (M * FG) . i by A129, A155, A165, FUNCT_1:13;
hence 0. <= x1 . i by A156, A167; :: thesis: verum
end;
suppose A168: F . (((i -' 1) div (len b)) + 1) = {} ; :: thesis: 0. <= x1 . i
FG . i = (F . (((i -' 1) div (len b)) + 1)) /\ (G . (((i -' 1) mod (len b)) + 1)) by A13, A129, A155;
then M . (FG . i) = 0. by A168, VALUED_0:def 19;
then (M * FG) . i = 0. by A129, A155, FUNCT_1:13;
hence 0. <= x1 . i by A156; :: thesis: verum
end;
end;
end;
then for i being object st i in dom x1 holds
0. <= x1 . i ;
then Z: x1 is nonnegative by SUPINF_2:52;
not -infty in rng x1
proof
assume -infty in rng x1 ; :: thesis: contradiction
then ex i being object st
( i in dom x1 & x1 . i = -infty ) by FUNCT_1:def 3;
hence contradiction by A154; :: thesis: verum
end;
then (x1 " {-infty}) /\ (y1 " {+infty}) = {} /\ (y1 " {+infty}) by FUNCT_1:72
.= {} ;
then A169: dom (x1 + y1) = ((dom x1) /\ (dom y1)) \ ({} \/ {}) by A153, MESFUNC1:def 3
.= dom z1 by A129, A126, A135 ;
A170: for k being Nat st k in dom z1 holds
z1 . k = (x1 + y1) . k
proof
reconsider la9 = len a, lb9 = len b as Nat ;
let k be Nat; :: thesis: ( k in dom z1 implies z1 . k = (x1 + y1) . k )
set p = ((k -' 1) div (len b)) + 1;
set q = ((k -' 1) mod (len b)) + 1;
assume A171: k in dom z1 ; :: thesis: z1 . k = (x1 + y1) . k
then A172: k in Seg (len FG) by A135, FINSEQ_1:def 3;
then A173: k <= (len a) * (len b) by A12, FINSEQ_1:1;
then A174: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;
1 <= k by A172, FINSEQ_1:1;
then A175: ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A173, NAT_D:def 3, XXREAL_0:2;
A176: len b <> 0 by A12, A172;
then len b >= 0 + 1 by NAT_1:13;
then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A175, NAT_2:15;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A174, 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 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= len a ) by A176, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len b)) + 1 in Seg (len a) by FINSEQ_1:1;
then A177: ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def 3;
(k -' 1) mod (len b) < len b by A176, NAT_D:1;
then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= len b ) by NAT_1:13;
then ((k -' 1) mod (len b)) + 1 in Seg (len b) by FINSEQ_1:1;
then A178: ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def 3;
A179: ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))
proof
per cases ( FG . k <> {} or FG . k = {} ) ;
suppose FG . k <> {} ; :: thesis: ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))
then (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) <> {} by A13, A135, A171;
then consider v being object such that
A180: v in (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by XBOOLE_0:def 1;
A181: v in G . (((k -' 1) mod (len b)) + 1) by A180, XBOOLE_0:def 4;
b . (((k -' 1) mod (len b)) + 1) = g . v by A9, A178, A181, MESFUNC3:def 1;
then 0. <= b . (((k -' 1) mod (len b)) + 1) by A6, SUPINF_2:51;
then A183: ( 0. = b1 . k or 0. < b1 . k ) by A50, A64, A172;
A184: v in F . (((k -' 1) div (len b)) + 1) by A180, XBOOLE_0:def 4;
a . (((k -' 1) div (len b)) + 1) = f . v by A10, A177, A184, MESFUNC3:def 1;
then 0. <= a . (((k -' 1) div (len b)) + 1) by A3, SUPINF_2:51;
then ( 0. = a1 . k or 0. < a1 . k ) by A48, A52, A172;
hence ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A183, XXREAL_3:96; :: thesis: verum
end;
suppose FG . k = {} ; :: thesis: ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))
then M . (FG . k) = 0. by VALUED_0:def 19;
then A186: (M * FG) . k = 0. by A135, A171, FUNCT_1:13;
hence ((a1 . k) + (b1 . k)) * ((M * FG) . k) = 0
.= ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A186 ;
:: thesis: verum
end;
end;
end;
thus z1 . k = (c1 . k) * ((M * FG) . k) by A136, A171
.= ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A133, A137, A172, A179
.= (x1 . k) + ((b1 . k) * ((M * FG) . k)) by A129, A130, A135, A171
.= (x1 . k) + (y1 . k) by A126, A127, A135, A171
.= (x1 + y1) . k by A169, A171, MESFUNC1:def 3 ; :: thesis: verum
end;
A187: dom (f + g) = (dom g) /\ (dom g) by A5, A7, MESFUNC2:2
.= dom g ;
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;
g is real-valued by A4, MESFUNC2:def 4;
then A190: |.(g . x).| < +infty by A187, A188, MESFUNC2:def 1;
f is real-valued by A1, MESFUNC2:def 4;
then |.(f . x).| < +infty by A8, A188, MESFUNC2:def 1;
then |.(f . x).| + |.(g . x).| <> +infty by A190, XXREAL_3:16;
hence |.((f + g) . x).| < +infty by A189, XXREAL_0:2, XXREAL_0:4; :: thesis: verum
end;
then f + g is real-valued by MESFUNC2:def 1;
hence A191: f + g is_simple_func_in S by A71, A8, A107, MESFUNC2:def 4; :: thesis: ( dom (f + g) <> {} & ( for x being object st x in dom (f + g) holds
0. <= (f + g) . x ) & integral (M,(f + g)) = (integral (M,f)) + (integral (M,g)) )
thus dom (f + g) <> {} by A2, A8; :: thesis: ( ( for x being object st x in dom (f + g) holds
0. <= (f + g) . x ) & integral (M,(f + g)) = (integral (M,f)) + (integral (M,g)) )
thus for x being object st x in dom (f + g) holds
0. <= (f + g) . x :: thesis: integral (M,(f + g)) = (integral (M,f)) + (integral (M,g))
proof
let x be object ; :: thesis: ( x in dom (f + g) implies 0. <= (f + g) . x )
A193: dom f c= X by RELAT_1:def 18;
assume A194: x in dom (f + g) ; :: thesis: 0. <= (f + g) . x
( 0. <= f . x & 0. <= g . x ) by A3, A6, SUPINF_2:51;
then 0. <= (f . x) + (g . x) ;
hence 0. <= (f + g) . x by A8, A194, A193, MESFUNC1:def 3; :: thesis: verum
end;
then X: f + g is nonnegative by SUPINF_2:52;
dom FG = dom c1 by A132, FINSEQ_3:29;
then FG,c1 are_Re-presentation_of f + g by A71, A8, A138, MESFUNC3:def 1;
then A195: integral (M,(f + g)) = Sum z1 by X, A2, A135, A136, A8, A191, Th3;
dom (x1 + y1) = Seg (len z1) by A169, FINSEQ_1:def 3;
then x1 + y1 is FinSequence by FINSEQ_1:def 2;
then A196: z1 = x1 + y1 by A169, A170, FINSEQ_1:13;
dom FG = Seg (len b1) by A49, FINSEQ_1:def 3
.= dom b1 by FINSEQ_1:def 3 ;
then FG,b1 are_Re-presentation_of g by A5, A71, A65, MESFUNC3:def 1;
then integral (M,g) = Sum y1 by A2, A4, A5, A6, A126, A127, Th3;
hence integral (M,(f + g)) = (integral (M,f)) + (integral (M,g)) by A129, A126, A131, A195, A196, Th1, Y, Z; :: thesis: verum