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 V70() 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 H_{1}( Nat) -> Element of ExtREAL = b . ((($1 -' 1) mod (len b)) + 1);

deffunc H_{2}( 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 H_{3}( 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 = H_{3}(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;

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

FG . k misses FG . l

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 = H_{2}(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 = H_{1}(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

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

A71: 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

( dom y1 = dom FG & ( for n being Nat st n in dom y1 holds

y1 . n = (b1 . n) * ((M * FG) . n) ) )

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

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 H_{4}( 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 = H_{4}(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) ) )

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

0. <= y1 . i

0. <= y1 . i ;

then Y: y1 is nonnegative by SUPINF_2:52;

not -infty in rng y1

.= {} ;

A154: for i being Nat st i in dom x1 holds

0. <= x1 . i

0. <= x1 . i ;

then Z: x1 is nonnegative by SUPINF_2:52;

not -infty in rng x1

.= {} ;

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

.= dom g ;

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

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

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 V70() 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 H

deffunc H

set la = len a;

A11: dom F = dom a by A10, MESFUNC3:def 1;

deffunc H

consider FG being FinSequence such that

A12: len FG = (len a) * (len b) and

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

FG . k = H

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

then reconsider FG = FG as FinSequence of S by FINSEQ_2:12;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;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

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

FG . k misses FG . l

proof

then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
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 )

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;

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

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) mod lb < lb
by A34, NAT_D:1;
(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;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

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;

end;

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

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

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 = H

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 = H

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

A64:
dom b1 = Seg (len FG)
by A49, FINSEQ_1:def 3;
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;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

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

A70:
dom g = union (rng G)
by A9, MESFUNC3:def 1;
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;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

A71: dom f = union (rng FG)

proof

A107:
for k being Nat
thus
dom f c= union (rng FG)
:: according to XBOOLE_0:def 10 :: thesis: union (rng FG) c= dom f

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

reconsider la9 = len a, lb9 = len b as Nat ;
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;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

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

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

ex y1 being FinSequence of ExtREAL st
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;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

( dom y1 = dom FG & ( for n being Nat st n in dom y1 holds

y1 . n = (b1 . n) * ((M * FG) . n) ) )

proof

then consider y1 being FinSequence of ExtREAL such that
deffunc H_{4}( 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 = H_{4}(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;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 = H

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

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

then consider x1 being FinSequence of ExtREAL such that
deffunc H_{4}( 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 = H_{4}(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;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 = H

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

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 H

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 = H

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

then consider z1 being FinSequence of ExtREAL such that
deffunc H_{5}( 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 = H_{5}(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;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 = H

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

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

A143:
for i being Nat st i in dom y1 holds
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;(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

0. <= y1 . i

proof

then
for i being object st i in dom y1 holds
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;

end;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) = {} )
;

end;

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

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

0. <= y1 . i ;

then Y: y1 is nonnegative by SUPINF_2:52;

not -infty in rng y1

proof

then A153: (x1 " {+infty}) /\ (y1 " {-infty}) =
(x1 " {+infty}) /\ {}
by FUNCT_1:72
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 ex i being object st

( i in dom y1 & y1 . i = -infty ) by FUNCT_1:def 3;

hence contradiction by A143; :: thesis: verum

.= {} ;

A154: for i being Nat st i in dom x1 holds

0. <= x1 . i

proof

then
for i being object st i in dom x1 holds
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;

end;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) = {} )
;

end;

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

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

0. <= x1 . i ;

then Z: x1 is nonnegative by SUPINF_2:52;

not -infty in rng x1

proof

then (x1 " {-infty}) /\ (y1 " {+infty}) =
{} /\ (y1 " {+infty})
by FUNCT_1:72
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 ex i being object st

( i in dom x1 & x1 . i = -infty ) by FUNCT_1:def 3;

hence contradiction by A154; :: thesis: verum

.= {} ;

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

A187: dom (f + g) =
(dom g) /\ (dom g)
by A5, A7, MESFUNC2:2
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))

.= ((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;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
end;

thus z1 . k =
(c1 . k) * ((M * FG) . k)
by A136, A171
per cases
( FG . k <> {} or FG . k = {} )
;

end;

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

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

.= ((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

.= dom g ;

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

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

then
f + g is V70()
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 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 V70() by A4, MESFUNC2:def 4;

then A190: |.(g . x).| < +infty by A187, A188, MESFUNC2:def 1;

f is V70() 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;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 V70() by A4, MESFUNC2:def 4;

then A190: |.(g . x).| < +infty by A187, A188, MESFUNC2:def 1;

f is V70() 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

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

then X:
f + g is nonnegative
by SUPINF_2:52;
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;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

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