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 & ( for x being set st x in dom f holds

g . x <= f . x ) holds

( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (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 & ( for x being set st x in dom f holds

g . x <= f . x ) holds

( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (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 & ( for x being set st x in dom f holds

g . x <= f . x ) holds

( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (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 & ( for x being set st x in dom f holds

g . x <= f . x ) implies ( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (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 and

A7: for x being set st x in dom f holds

g . x <= f . x ; :: thesis: ( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )

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, MESFUNC4:4;

g is real-valued by A4, MESFUNC2:def 4;

then A10: dom (f - g) = (dom f) /\ (dom g) by MESFUNC2:2;

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

A12: 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, MESFUNC4:4, A3;

set la = len a;

A13: dom F = dom a by A12, MESFUNC3:def 1;

set lb = len b;

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

consider FG being FinSequence such that

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

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

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

A16: dom FG = Seg ((len a) * (len b)) by A14, FINSEQ_1:def 3;

A17: dom G = dom b by A9, MESFUNC3:def 1;

FG is FinSequence of S

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

FG . k misses FG . l

A55: dom f = union (rng F) by A12, MESFUNC3:def 1;

defpred S_{1}[ Nat, set ] means ( ( G . ((($1 -' 1) mod (len b)) + 1) = {} implies $2 = 0 ) & ( G . ((($1 -' 1) mod (len b)) + 1) <> {} implies $2 = b . ((($1 -' 1) mod (len b)) + 1) ) );

defpred S_{2}[ Nat, set ] means ( ( F . ((($1 -' 1) div (len b)) + 1) = {} implies $2 = 0 ) & ( F . ((($1 -' 1) div (len b)) + 1) <> {} implies $2 = a . ((($1 -' 1) div (len b)) + 1) ) );

A56: for k being Nat st k in Seg (len FG) holds

ex v being Element of ExtREAL st S_{2}[k,v]

A59: ( dom a1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds

S_{2}[k,a1 . k] ) )
from FINSEQ_1:sch 5(A56);

A60: dom g = union (rng G) by A9, MESFUNC3:def 1;

A61: 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_{2}( Nat) -> Element of ExtREAL = (a1 . $1) * ((M * FG) . $1);

consider x1 being FinSequence of ExtREAL such that

A122: ( len x1 = len FG & ( for k being Nat st k in dom x1 holds

x1 . k = H_{2}(k) ) )
from FINSEQ_2:sch 1();

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

for x being object st x in FG . k holds

f . x = a1 . k

ex v being Element of ExtREAL st S_{1}[k,v]

A139: ( dom b1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds

S_{1}[k,b1 . k] ) )
from FINSEQ_1:sch 5(A136);

deffunc H_{3}( Nat) -> Element of ExtREAL = (a1 . $1) - (b1 . $1);

consider c1 being FinSequence of ExtREAL such that

A140: len c1 = len FG and

A141: for k being Nat st k in dom c1 holds

c1 . k = H_{3}(k)
from FINSEQ_2:sch 1();

A142: dom c1 = Seg (len FG) by A140, FINSEQ_1:def 3;

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

for x being object st x in FG . k holds

g . x = b1 . k

for x being object st x in FG . k holds

(f - g) . x = c1 . k_{4}( Nat) -> Element of ExtREAL = (c1 . $1) * ((M * FG) . $1);

consider z1 being FinSequence of ExtREAL such that

A153: ( len z1 = len FG & ( for k being Nat st k in dom z1 holds

z1 . k = H_{4}(k) ) )
from FINSEQ_2:sch 1();

deffunc H_{5}( Nat) -> Element of ExtREAL = (b1 . $1) * ((M * FG) . $1);

consider y1 being FinSequence of ExtREAL such that

A154: ( len y1 = len FG & ( for k being Nat st k in dom y1 holds

y1 . k = H_{5}(k) ) )
from FINSEQ_2:sch 1();

A155: dom x1 = dom FG by A122, FINSEQ_3:29;

A156: dom z1 = dom FG by A153, FINSEQ_3:29;

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

0 <= z1 . i

0 <= z1 . i by A156, A155;

then cd: z1 is nonnegative by SUPINF_2:52;

not -infty in rng z1

.= {} ;

A164: dom y1 = dom FG by A154, FINSEQ_3:29;

A165: for i being Nat st i in dom y1 holds

0 <= y1 . i

0 <= y1 . i ;

then ag: y1 is nonnegative by SUPINF_2:52;

not -infty in rng y1

.= {} ;

then A176: dom (z1 + y1) = ((dom z1) /\ (dom y1)) \ ({} \/ {}) by A163, MESFUNC1:def 3

.= dom x1 by A122, A164, A156, FINSEQ_3:29 ;

A177: for k being Nat st k in dom x1 holds

x1 . k = (z1 + y1) . k

hence A211: f - g is_simple_func_in S by A5, A61, A10, A99, MESFUNC2:def 4; :: thesis: ( dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )

dom FG = dom a1 by A59, FINSEQ_1:def 3;

then FG,a1 are_Re-presentation_of f by A61, A123, MESFUNC3:def 1;

then A212: integral (M,f) = Sum x1 by A1, A2, A3, A122, A155, MESFUNC4:3;

dom (z1 + y1) = Seg (len x1) by A176, FINSEQ_1:def 3;

then z1 + y1 is FinSequence by FINSEQ_1:def 2;

then A213: x1 = z1 + y1 by A176, A177, FINSEQ_1:13;

dom FG = dom b1 by A139, FINSEQ_1:def 3;

then FG,b1 are_Re-presentation_of g by A5, A61, A143, MESFUNC3:def 1;

then A214: integral (M,g) = Sum y1 by A2, A4, A5, A6, A154, A164, MESFUNC4:3;

thus dom (f - g) <> {} by A2, A5, A10; :: thesis: ( f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )

for x being object st x in dom (f - g) holds

0 <= (f - g) . x

dom FG = dom c1 by A140, FINSEQ_3:29;

then FG,c1 are_Re-presentation_of f - g by A5, A61, A10, A149, MESFUNC3:def 1;

then integral (M,(f - g)) = Sum z1 by aa, A2, A5, A153, A156, A10, A211, MESFUNC4:3;

hence integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) by A164, A156, A212, A214, A213, MESFUNC4:1, ag, cd; :: 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 & ( for x being set st x in dom f holds

g . x <= f . x ) holds

( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (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 & ( for x being set st x in dom f holds

g . x <= f . x ) holds

( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (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 & ( for x being set st x in dom f holds

g . x <= f . x ) holds

( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (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 & ( for x being set st x in dom f holds

g . x <= f . x ) implies ( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (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 and

A7: for x being set st x in dom f holds

g . x <= f . x ; :: thesis: ( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )

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, MESFUNC4:4;

g is real-valued by A4, MESFUNC2:def 4;

then A10: dom (f - g) = (dom f) /\ (dom g) by MESFUNC2:2;

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

A12: 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, MESFUNC4:4, A3;

set la = len a;

A13: dom F = dom a by A12, MESFUNC3:def 1;

set lb = len b;

deffunc H

consider FG being FinSequence such that

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

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

FG . k = H

A16: dom FG = Seg ((len a) * (len b)) by A14, FINSEQ_1:def 3;

A17: dom G = dom b by A9, MESFUNC3:def 1;

FG is FinSequence of S

proof

then reconsider FG = FG as FinSequence of S ;
let b be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not b in rng FG or b in S )

then ex a being object st

( a in dom FG & b = FG . a ) by FUNCT_1:def 3;

hence b in S by A18; :: thesis: verum

end;A18: now :: thesis: for k being Element of NAT st k in dom FG holds

FG . k in S

assume
b in rng FG
; :: thesis: b in SFG . k in S

let k be Element of 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;

A19: len b divides (len a) * (len b) by NAT_D:def 3;

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

then A21: k in Seg ((len a) * (len b)) by A14, FINSEQ_1:def 3;

then A22: k <= (len a) * (len b) by FINSEQ_1:1;

then k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

then A23: (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:24;

1 <= k by A21, FINSEQ_1:1;

then A24: 1 <= (len a) * (len b) by A22, XXREAL_0:2;

A25: len b <> 0 by A21;

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

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

len b >= 0 + 1 by A25, NAT_1:13;

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A19, A24, NAT_2:15;

then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A23, XREAL_1:19;

then A27: ((k -' 1) div (len b)) + 1 <= len a by A25, NAT_D:18;

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

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A27;

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

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

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A26;

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

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

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

hence FG . k in S by A28, A29, MEASURE1:34; :: thesis: verum

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

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

A19: len b divides (len a) * (len b) by NAT_D:def 3;

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

then A21: k in Seg ((len a) * (len b)) by A14, FINSEQ_1:def 3;

then A22: k <= (len a) * (len b) by FINSEQ_1:1;

then k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

then A23: (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:24;

1 <= k by A21, FINSEQ_1:1;

then A24: 1 <= (len a) * (len b) by A22, XXREAL_0:2;

A25: len b <> 0 by A21;

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

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

len b >= 0 + 1 by A25, NAT_1:13;

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A19, A24, NAT_2:15;

then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A23, XREAL_1:19;

then A27: ((k -' 1) div (len b)) + 1 <= len a by A25, NAT_D:18;

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

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A27;

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

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

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A26;

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

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

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

hence FG . k in S by A28, A29, MEASURE1:34; :: thesis: verum

then ex a being object st

( a in dom FG & b = FG . a ) by FUNCT_1:def 3;

hence b in S by A18; :: 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;
let k, l be Nat; :: thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )

assume that

A30: k in dom FG and

A31: l in dom FG and

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

A33: k in Seg ((len a) * (len b)) by A14, A30, FINSEQ_1:def 3;

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

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;

A35: len b divides (len a) * (len b) by NAT_D:def 3;

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

then A36: (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 A15, A31

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

A37: k <= (len a) * (len b) by A33, FINSEQ_1:1;

then A38: 1 <= (len a) * (len b) by A34, XXREAL_0:2;

A39: len b <> 0 by A33;

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

then A40: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A35, A38, NAT_2:15;

k -' 1 <= ((len a) * (len b)) -' 1 by A37, NAT_D:42;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A40, NAT_2:24;

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

then A41: ((k -' 1) div (len b)) + 1 <= len a by A39, NAT_D:18;

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

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A41;

then A42: ((k -' 1) div (len b)) + 1 in dom F by A13, FINSEQ_1:def 3;

(l -' 1) mod (len b) < len b by A39, NAT_D:1;

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

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

then ((l -' 1) mod (len b)) + 1 in Seg (len b) by A43;

then A44: ((l -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

(k -' 1) mod (len b) < len b by A39, NAT_D:1;

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

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A45;

then A46: ((k -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

A47: l in Seg ((len a) * (len b)) by A14, A31, FINSEQ_1:def 3;

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

then l -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

then (l -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A40, NAT_2:24;

then ((l -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then A53: ((l -' 1) div (len b)) + 1 <= len a by A39, NAT_D:18;

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

then ((l -' 1) div (len b)) + 1 in Seg (len a) by A53;

then A54: ((l -' 1) div (len b)) + 1 in dom F by A13, FINSEQ_1:def 3;

end;assume that

A30: k in dom FG and

A31: l in dom FG and

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

A33: k in Seg ((len a) * (len b)) by A14, A30, FINSEQ_1:def 3;

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

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;

A35: len b divides (len a) * (len b) by NAT_D:def 3;

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

then A36: (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 A15, A31

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

A37: k <= (len a) * (len b) by A33, FINSEQ_1:1;

then A38: 1 <= (len a) * (len b) by A34, XXREAL_0:2;

A39: len b <> 0 by A33;

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

then A40: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A35, A38, NAT_2:15;

k -' 1 <= ((len a) * (len b)) -' 1 by A37, NAT_D:42;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A40, NAT_2:24;

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

then A41: ((k -' 1) div (len b)) + 1 <= len a by A39, NAT_D:18;

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

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A41;

then A42: ((k -' 1) div (len b)) + 1 in dom F by A13, FINSEQ_1:def 3;

(l -' 1) mod (len b) < len b by A39, NAT_D:1;

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

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

then ((l -' 1) mod (len b)) + 1 in Seg (len b) by A43;

then A44: ((l -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

(k -' 1) mod (len b) < len b by A39, NAT_D:1;

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

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A45;

then A46: ((k -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

A47: l in Seg ((len a) * (len b)) by A14, A31, FINSEQ_1:def 3;

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

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

l <= (len a) * (len b)
by A47, FINSEQ_1:1;
(l -' 1) + 1 = ((((((l -' 1) div (len b)) + 1) - 1) * (len b)) + ((((l -' 1) mod (len b)) + 1) - 1)) + 1
by A39, NAT_D:2;

then A50: (l - 1) + 1 = (((((l -' 1) div (len b)) + 1) - 1) * (len b)) + (((l -' 1) mod (len b)) + 1) by A48, XREAL_1:233;

assume that

A51: ((k -' 1) div (len b)) + 1 = ((l -' 1) div (len b)) + 1 and

A52: ((k -' 1) mod (len b)) + 1 = ((l -' 1) mod (len b)) + 1 ; :: thesis: contradiction

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

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

hence contradiction by A32, A51, A52, A50; :: thesis: verum

end;then A50: (l - 1) + 1 = (((((l -' 1) div (len b)) + 1) - 1) * (len b)) + (((l -' 1) mod (len b)) + 1) by A48, XREAL_1:233;

assume that

A51: ((k -' 1) div (len b)) + 1 = ((l -' 1) div (len b)) + 1 and

A52: ((k -' 1) mod (len b)) + 1 = ((l -' 1) mod (len b)) + 1 ; :: thesis: contradiction

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

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

hence contradiction by A32, A51, A52, A50; :: thesis: verum

then l -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

then (l -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A40, NAT_2:24;

then ((l -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then A53: ((l -' 1) div (len b)) + 1 <= len a by A39, NAT_D:18;

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

then ((l -' 1) div (len b)) + 1 in Seg (len a) by A53;

then A54: ((l -' 1) div (len b)) + 1 in dom F by A13, 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 A49;

end;

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

then
F . (((k -' 1) div (len b)) + 1) misses F . (((l -' 1) div (len b)) + 1)
by A42, A54, MESFUNC3:4;

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

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

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

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
G . (((k -' 1) mod (len b)) + 1) misses G . (((l -' 1) mod (len b)) + 1)
by A46, A44, MESFUNC3:4;

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

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

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

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

A55: dom f = union (rng F) by A12, MESFUNC3:def 1;

defpred S

defpred S

A56: for k being Nat st k in Seg (len FG) holds

ex v being Element of ExtREAL st S

proof

consider a1 being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg (len FG) implies ex v being Element of ExtREAL st S_{2}[k,v] )

assume k in Seg (len FG) ; :: thesis: ex v being Element of ExtREAL st S_{2}[k,v]

end;assume k in Seg (len FG) ; :: thesis: ex v being Element of ExtREAL st S

A59: ( dom a1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds

S

A60: dom g = union (rng G) by A9, MESFUNC3:def 1;

A61: dom f = union (rng FG)

proof

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

A86: len b divides (len a) * (len b) by NAT_D:def 3;

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

then consider Y being set such that

A87: z in Y and

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

consider k being Nat such that

A89: k in dom FG and

A90: Y = FG . k by A88, FINSEQ_2:10;

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

A91: k in Seg (len FG) by A89, FINSEQ_1:def 3;

then A92: k <= (len a) * (len b) by A14, FINSEQ_1:1;

then A93: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

1 <= k by A91, FINSEQ_1:1;

then A94: 1 <= (len a) * (len b) by A92, XXREAL_0:2;

A95: len b <> 0 by A14, A91;

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

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A86, A94, NAT_2:15;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A93, NAT_2:24;

then A96: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

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

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

((len a) * (len b)) div (len b) = len a by A95, NAT_D:18;

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A97, A96;

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

then A98: F . (((k -' 1) div (len b)) + 1) in rng F by FUNCT_1:def 3;

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

then z in F . (((k -' 1) div (len b)) + 1) by A87, A90, XBOOLE_0:def 4;

hence z in dom f by A55, A98, TARSKI:def 4; :: thesis: verum

end;proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union (rng FG) or z in dom f )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom f or z in union (rng FG) )

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

then consider Y being set such that

A63: z in Y and

A64: Y in rng F by A55, TARSKI:def 4;

consider i being Nat such that

A65: i in dom F and

A66: Y = F . i by A64, FINSEQ_2:10;

A67: i in Seg (len a) by A13, A65, FINSEQ_1:def 3;

then 1 <= i by FINSEQ_1:1;

then consider i9 being Nat such that

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

consider Z being set such that

A69: z in Z and

A70: Z in rng G by A5, A60, A62, TARSKI:def 4;

consider j being Nat such that

A71: j in dom G and

A72: Z = G . j by A70, FINSEQ_2:10;

A73: j in Seg (len b) by A17, A71, FINSEQ_1:def 3;

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

then consider j9 being Nat such that

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

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

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

i <= len a by A67, 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 A76: k <= (((len a) - 1) * (len b)) + j by XREAL_1:6;

A77: k >= 0 + j by A68, XREAL_1:6;

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

then A78: k -' 1 = (i9 * (len b)) + j9 by A68, A75;

A79: j <= len b by A73, FINSEQ_1:1;

then (((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b) by XREAL_1:6;

then A80: k <= (len a) * (len b) by A76, XXREAL_0:2;

k >= 1 by A74, A77, XXREAL_0:2;

then A81: k in Seg ((len a) * (len b)) by A80;

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

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

A83: j9 < len b by A79, A75, NAT_1:13;

then A84: j = ((k -' 1) mod (len b)) + 1 by A75, A78, NAT_D:def 2;

A85: i = ((k -' 1) div (len b)) + 1 by A68, A78, A83, NAT_D:def 1;

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

then z in FG . k by A15, A16, A85, A84, A81;

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

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

then consider Y being set such that

A63: z in Y and

A64: Y in rng F by A55, TARSKI:def 4;

consider i being Nat such that

A65: i in dom F and

A66: Y = F . i by A64, FINSEQ_2:10;

A67: i in Seg (len a) by A13, A65, FINSEQ_1:def 3;

then 1 <= i by FINSEQ_1:1;

then consider i9 being Nat such that

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

consider Z being set such that

A69: z in Z and

A70: Z in rng G by A5, A60, A62, TARSKI:def 4;

consider j being Nat such that

A71: j in dom G and

A72: Z = G . j by A70, FINSEQ_2:10;

A73: j in Seg (len b) by A17, A71, FINSEQ_1:def 3;

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

then consider j9 being Nat such that

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

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

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

i <= len a by A67, 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 A76: k <= (((len a) - 1) * (len b)) + j by XREAL_1:6;

A77: k >= 0 + j by A68, XREAL_1:6;

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

then A78: k -' 1 = (i9 * (len b)) + j9 by A68, A75;

A79: j <= len b by A73, FINSEQ_1:1;

then (((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b) by XREAL_1:6;

then A80: k <= (len a) * (len b) by A76, XXREAL_0:2;

k >= 1 by A74, A77, XXREAL_0:2;

then A81: k in Seg ((len a) * (len b)) by A80;

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

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

A83: j9 < len b by A79, A75, NAT_1:13;

then A84: j = ((k -' 1) mod (len b)) + 1 by A75, A78, NAT_D:def 2;

A85: i = ((k -' 1) div (len b)) + 1 by A68, A78, A83, NAT_D:def 1;

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

then z in FG . k by A15, A16, A85, A84, A81;

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

A86: len b divides (len a) * (len b) by NAT_D:def 3;

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

then consider Y being set such that

A87: z in Y and

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

consider k being Nat such that

A89: k in dom FG and

A90: Y = FG . k by A88, FINSEQ_2:10;

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

A91: k in Seg (len FG) by A89, FINSEQ_1:def 3;

then A92: k <= (len a) * (len b) by A14, FINSEQ_1:1;

then A93: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

1 <= k by A91, FINSEQ_1:1;

then A94: 1 <= (len a) * (len b) by A92, XXREAL_0:2;

A95: len b <> 0 by A14, A91;

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

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A86, A94, NAT_2:15;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A93, NAT_2:24;

then A96: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

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

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

((len a) * (len b)) div (len b) = len a by A95, NAT_D:18;

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A97, A96;

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

then A98: F . (((k -' 1) div (len b)) + 1) in rng F by FUNCT_1:def 3;

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

then z in F . (((k -' 1) div (len b)) + 1) by A87, A90, XBOOLE_0:def 4;

hence z in dom f by A55, A98, 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

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

A100: k in dom FG and

A101: x in FG . k and

A102: y in FG . k ; :: thesis: (f - g) . x = (f - g) . y

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

A103: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A15, A100;

then A104: x in G . (((k -' 1) mod (len b)) + 1) by A101, XBOOLE_0:def 4;

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

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

A106: k in Seg (len FG) by A100, FINSEQ_1:def 3;

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

A108: len b > 0 by A14, A106;

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

A110: y in G . (((k -' 1) mod (len b)) + 1) by A102, A103, XBOOLE_0:def 4;

A111: len b divides (len a) * (len b) by NAT_D:def 3;

A112: k <= (len a) * (len b) by A14, A106, FINSEQ_1:1;

then A113: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

1 <= (len a) * (len b) by A107, A112, XXREAL_0:2;

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A109, A111, NAT_2:15;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A113, NAT_2:24;

then A114: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

len b <> 0 by A14, A106;

then ((k -' 1) div (len b)) + 1 <= len a by A114, NAT_D:18;

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A105;

then A115: ((k -' 1) div (len b)) + 1 in dom F by A13, FINSEQ_1:def 3;

(k -' 1) mod (len b) < len b by A108, NAT_D:1;

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

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A116;

then A117: ((k -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

y in F . (((k -' 1) div (len b)) + 1) by A102, A103, XBOOLE_0:def 4;

then A118: f . y = a . (((k -' 1) div (len b)) + 1) by A12, A115, MESFUNC3:def 1;

x in F . (((k -' 1) div (len b)) + 1) by A101, A103, XBOOLE_0:def 4;

then A119: f . x = a . (((k -' 1) div (len b)) + 1) by A12, A115, MESFUNC3:def 1;

A120: FG . k in rng FG by A100, FUNCT_1:def 3;

then A121: y in dom (f - g) by A5, A61, A10, A102, TARSKI:def 4;

x in dom (f - g) by A5, A61, A10, A101, A120, TARSKI:def 4;

then (f - g) . x = (f . x) - (g . x) by MESFUNC1:def 4

.= (a . (((k -' 1) div (len b)) + 1)) - (b . (((k -' 1) mod (len b)) + 1)) by A9, A117, A104, A119, MESFUNC3:def 1

.= (f . y) - (g . y) by A9, A117, A110, A118, MESFUNC3:def 1 ;

hence (f - g) . x = (f - g) . y by A121, MESFUNC1:def 4; :: thesis: verum

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

A100: k in dom FG and

A101: x in FG . k and

A102: y in FG . k ; :: thesis: (f - g) . x = (f - g) . y

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

A103: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A15, A100;

then A104: x in G . (((k -' 1) mod (len b)) + 1) by A101, XBOOLE_0:def 4;

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

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

A106: k in Seg (len FG) by A100, FINSEQ_1:def 3;

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

A108: len b > 0 by A14, A106;

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

A110: y in G . (((k -' 1) mod (len b)) + 1) by A102, A103, XBOOLE_0:def 4;

A111: len b divides (len a) * (len b) by NAT_D:def 3;

A112: k <= (len a) * (len b) by A14, A106, FINSEQ_1:1;

then A113: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

1 <= (len a) * (len b) by A107, A112, XXREAL_0:2;

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A109, A111, NAT_2:15;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A113, NAT_2:24;

then A114: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

len b <> 0 by A14, A106;

then ((k -' 1) div (len b)) + 1 <= len a by A114, NAT_D:18;

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A105;

then A115: ((k -' 1) div (len b)) + 1 in dom F by A13, FINSEQ_1:def 3;

(k -' 1) mod (len b) < len b by A108, NAT_D:1;

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

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A116;

then A117: ((k -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

y in F . (((k -' 1) div (len b)) + 1) by A102, A103, XBOOLE_0:def 4;

then A118: f . y = a . (((k -' 1) div (len b)) + 1) by A12, A115, MESFUNC3:def 1;

x in F . (((k -' 1) div (len b)) + 1) by A101, A103, XBOOLE_0:def 4;

then A119: f . x = a . (((k -' 1) div (len b)) + 1) by A12, A115, MESFUNC3:def 1;

A120: FG . k in rng FG by A100, FUNCT_1:def 3;

then A121: y in dom (f - g) by A5, A61, A10, A102, TARSKI:def 4;

x in dom (f - g) by A5, A61, A10, A101, A120, TARSKI:def 4;

then (f - g) . x = (f . x) - (g . x) by MESFUNC1:def 4

.= (a . (((k -' 1) div (len b)) + 1)) - (b . (((k -' 1) mod (len b)) + 1)) by A9, A117, A104, A119, MESFUNC3:def 1

.= (f . y) - (g . y) by A9, A117, A110, A118, MESFUNC3:def 1 ;

hence (f - g) . x = (f - g) . y by A121, MESFUNC1:def 4; :: thesis: verum

consider x1 being FinSequence of ExtREAL such that

A122: ( len x1 = len FG & ( for k being Nat st k in dom x1 holds

x1 . k = H

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

A136:
for k being Nat st k in Seg (len FG) holds
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;

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

assume A125: k in dom FG ; :: thesis: for x being object st x in FG . k holds

f . x = a1 . k

then A126: k in Seg (len FG) by FINSEQ_1:def 3;

let x be object ; :: thesis: ( x in FG . k implies f . x = a1 . k )

assume A127: 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 A15, A125;

then A128: x in F . (((k -' 1) div (len b)) + 1) by A127, XBOOLE_0:def 4;

A129: k in Seg (len FG) by A125, FINSEQ_1:def 3;

then A130: k <= (len a) * (len b) by A14, FINSEQ_1:1;

then k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

then A131: (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:24;

A132: len b divides (len a) * (len b) by NAT_D:def 3;

1 <= k by A129, FINSEQ_1:1;

then A133: 1 <= (len a) * (len b) by A130, XXREAL_0:2;

A134: len b <> 0 by A14, A129;

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

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A132, A133, NAT_2:15;

then A135: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A131, XREAL_1:19;

((len a) * (len b)) div (len b) = len a by A134, NAT_D:18;

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A124, A135;

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

then f . x = a . (((k -' 1) div (len b)) + 1) by A12, A128, MESFUNC3:def 1;

hence f . x = a1 . k by A59, A126, A128; :: thesis: verum

end;f . x = a1 . k )

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

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

assume A125: k in dom FG ; :: thesis: for x being object st x in FG . k holds

f . x = a1 . k

then A126: k in Seg (len FG) by FINSEQ_1:def 3;

let x be object ; :: thesis: ( x in FG . k implies f . x = a1 . k )

assume A127: 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 A15, A125;

then A128: x in F . (((k -' 1) div (len b)) + 1) by A127, XBOOLE_0:def 4;

A129: k in Seg (len FG) by A125, FINSEQ_1:def 3;

then A130: k <= (len a) * (len b) by A14, FINSEQ_1:1;

then k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

then A131: (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:24;

A132: len b divides (len a) * (len b) by NAT_D:def 3;

1 <= k by A129, FINSEQ_1:1;

then A133: 1 <= (len a) * (len b) by A130, XXREAL_0:2;

A134: len b <> 0 by A14, A129;

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

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A132, A133, NAT_2:15;

then A135: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A131, XREAL_1:19;

((len a) * (len b)) div (len b) = len a by A134, NAT_D:18;

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A124, A135;

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

then f . x = a . (((k -' 1) div (len b)) + 1) by A12, A128, MESFUNC3:def 1;

hence f . x = a1 . k by A59, A126, A128; :: thesis: verum

ex v being Element of ExtREAL st S

proof

consider b1 being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg (len FG) implies ex v being Element of ExtREAL st S_{1}[k,v] )

assume k in Seg (len FG) ; :: thesis: ex v being Element of ExtREAL st S_{1}[k,v]

end;assume k in Seg (len FG) ; :: thesis: ex v being Element of ExtREAL st S

per cases
( G . (((k -' 1) mod (len b)) + 1) = {} or G . (((k -' 1) mod (len b)) + 1) <> {} )
;

end;

suppose A137:
G . (((k -' 1) mod (len b)) + 1) = {}
; :: thesis: ex v being Element of ExtREAL st S_{1}[k,v]

reconsider z = 0 as R_eal by XXREAL_0:def 1;

take z ; :: thesis: S_{1}[k,z]

thus S_{1}[k,z]
by A137; :: thesis: verum

end;take z ; :: thesis: S

thus S

A139: ( dom b1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds

S

deffunc H

consider c1 being FinSequence of ExtREAL such that

A140: len c1 = len FG and

A141: for k being Nat st k in dom c1 holds

c1 . k = H

A142: dom c1 = Seg (len FG) by A140, FINSEQ_1:def 3;

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

A149:
for k being Nat st k in dom FG holds
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 A144: k in dom FG ; :: thesis: for x being object st x in FG . k holds

g . x = b1 . k

then A145: k in Seg (len FG) by FINSEQ_1:def 3;

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

then len b <> 0 by A14;

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

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

let x be object ; :: thesis: ( x in FG . k implies g . x = b1 . k )

assume A147: 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 A15, A144;

then A148: x in G . (((k -' 1) mod (len b)) + 1) by A147, XBOOLE_0:def 4;

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A146;

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

hence g . x = b . (((k -' 1) mod (len b)) + 1) by A9, A148, MESFUNC3:def 1

.= b1 . k by A139, A148, A145 ;

:: thesis: verum

end;g . x = b1 . k )

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

assume A144: k in dom FG ; :: thesis: for x being object st x in FG . k holds

g . x = b1 . k

then A145: k in Seg (len FG) by FINSEQ_1:def 3;

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

then len b <> 0 by A14;

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

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

let x be object ; :: thesis: ( x in FG . k implies g . x = b1 . k )

assume A147: 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 A15, A144;

then A148: x in G . (((k -' 1) mod (len b)) + 1) by A147, XBOOLE_0:def 4;

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A146;

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

hence g . x = b . (((k -' 1) mod (len b)) + 1) by A9, A148, MESFUNC3:def 1

.= b1 . k by A139, A148, A145 ;

:: thesis: verum

for x being object st x in FG . k holds

(f - g) . x = c1 . k

proof

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

assume A150: k in dom FG ; :: thesis: for x being object st x in FG . k holds

(f - g) . x = c1 . k

let x be object ; :: thesis: ( x in FG . k implies (f - g) . x = c1 . k )

assume A151: x in FG . k ; :: thesis: (f - g) . x = c1 . k

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

then x in dom (f - g) by A5, A61, A10, A151, TARSKI:def 4;

then A152: (f - g) . x = (f . x) - (g . x) by MESFUNC1:def 4;

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

then (a1 . k) - (b1 . k) = c1 . k by A141, A142;

then (a1 . k) - (g . x) = c1 . k by A143, A150, A151;

hence (f - g) . x = c1 . k by A123, A150, A151, A152; :: thesis: verum

end;(f - g) . x = c1 . k )

assume A150: k in dom FG ; :: thesis: for x being object st x in FG . k holds

(f - g) . x = c1 . k

let x be object ; :: thesis: ( x in FG . k implies (f - g) . x = c1 . k )

assume A151: x in FG . k ; :: thesis: (f - g) . x = c1 . k

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

then x in dom (f - g) by A5, A61, A10, A151, TARSKI:def 4;

then A152: (f - g) . x = (f . x) - (g . x) by MESFUNC1:def 4;

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

then (a1 . k) - (b1 . k) = c1 . k by A141, A142;

then (a1 . k) - (g . x) = c1 . k by A143, A150, A151;

hence (f - g) . x = c1 . k by A123, A150, A151, A152; :: thesis: verum

consider z1 being FinSequence of ExtREAL such that

A153: ( len z1 = len FG & ( for k being Nat st k in dom z1 holds

z1 . k = H

deffunc H

consider y1 being FinSequence of ExtREAL such that

A154: ( len y1 = len FG & ( for k being Nat st k in dom y1 holds

y1 . k = H

A155: dom x1 = dom FG by A122, FINSEQ_3:29;

A156: dom z1 = dom FG by A153, FINSEQ_3:29;

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

0 <= z1 . i

proof

then
for i being object st i in dom z1 holds
reconsider EMPTY = {} as Element of S by PROB_1:4;

let i be Nat; :: thesis: ( i in dom x1 implies 0 <= z1 . i )

assume A158: i in dom x1 ; :: thesis: 0 <= z1 . i

then A159: (M * FG) . i = M . (FG . i) by A155, FUNCT_1:13;

FG . i in rng FG by A155, A158, FUNCT_1:3;

then reconsider V = FG . i as Element of S ;

M . EMPTY <= M . V by MEASURE1:31, XBOOLE_1:2;

then A160: 0 <= (M * FG) . i by A159, VALUED_0:def 19;

A161: i in Seg (len FG) by A122, A158, FINSEQ_1:def 3;

end;let i be Nat; :: thesis: ( i in dom x1 implies 0 <= z1 . i )

assume A158: i in dom x1 ; :: thesis: 0 <= z1 . i

then A159: (M * FG) . i = M . (FG . i) by A155, FUNCT_1:13;

FG . i in rng FG by A155, A158, FUNCT_1:3;

then reconsider V = FG . i as Element of S ;

M . EMPTY <= M . V by MEASURE1:31, XBOOLE_1:2;

then A160: 0 <= (M * FG) . i by A159, VALUED_0:def 19;

A161: i in Seg (len FG) by A122, A158, FINSEQ_1:def 3;

per cases
( FG . i <> {} or FG . i = {} )
;

end;

suppose
FG . i <> {}
; :: thesis: 0 <= z1 . i

then consider x being object such that

A162: x in FG . i by XBOOLE_0:def 1;

FG . i in rng FG by A155, A158, FUNCT_1:3;

then x in union (rng FG) by A162, TARSKI:def 4;

then g . x <= f . x by A7, A61;

then g . x <= a1 . i by A155, A123, A158, A162;

then b1 . i <= a1 . i by A155, A143, A158, A162;

then 0 <= (a1 . i) - (b1 . i) by XXREAL_3:40;

then 0 <= c1 . i by A141, A142, A161;

then 0 <= (c1 . i) * ((M * FG) . i) by A160;

hence 0 <= z1 . i by A155, A153, A156, A158; :: thesis: verum

end;A162: x in FG . i by XBOOLE_0:def 1;

FG . i in rng FG by A155, A158, FUNCT_1:3;

then x in union (rng FG) by A162, TARSKI:def 4;

then g . x <= f . x by A7, A61;

then g . x <= a1 . i by A155, A123, A158, A162;

then b1 . i <= a1 . i by A155, A143, A158, A162;

then 0 <= (a1 . i) - (b1 . i) by XXREAL_3:40;

then 0 <= c1 . i by A141, A142, A161;

then 0 <= (c1 . i) * ((M * FG) . i) by A160;

hence 0 <= z1 . i by A155, A153, A156, A158; :: thesis: verum

0 <= z1 . i by A156, A155;

then cd: z1 is nonnegative by SUPINF_2:52;

not -infty in rng z1

proof

then A163: (z1 " {-infty}) /\ (y1 " {+infty}) =
{} /\ (y1 " {+infty})
by FUNCT_1:72
assume
-infty in rng z1
; :: thesis: contradiction

then ex i being object st

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

hence contradiction by A155, A156, A157; :: thesis: verum

end;then ex i being object st

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

hence contradiction by A155, A156, A157; :: thesis: verum

.= {} ;

A164: dom y1 = dom FG by A154, FINSEQ_3:29;

A165: for i being Nat st i in dom y1 holds

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;

A166: ((i -' 1) mod (len b)) + 1 >= 0 + 1 by XREAL_1:6;

assume A167: i in dom y1 ; :: thesis: 0 <= y1 . i

then A168: y1 . i = (b1 . i) * ((M * FG) . i) by A154;

A169: i in Seg (len FG) by A154, A167, FINSEQ_1:def 3;

then len b <> 0 by A14;

then (i -' 1) mod (len b) < len b by NAT_D:1;

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

then ((i -' 1) mod (len b)) + 1 in Seg (len b) by A166;

then A170: ((i -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

end;set i9 = ((i -' 1) mod (len b)) + 1;

A166: ((i -' 1) mod (len b)) + 1 >= 0 + 1 by XREAL_1:6;

assume A167: i in dom y1 ; :: thesis: 0 <= y1 . i

then A168: y1 . i = (b1 . i) * ((M * FG) . i) by A154;

A169: i in Seg (len FG) by A154, A167, FINSEQ_1:def 3;

then len b <> 0 by A14;

then (i -' 1) mod (len b) < len b by NAT_D:1;

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

then ((i -' 1) mod (len b)) + 1 in Seg (len b) by A166;

then A170: ((i -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

per cases
( G . (((i -' 1) mod (len b)) + 1) <> {} or G . (((i -' 1) mod (len b)) + 1) = {} )
;

end;

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

FG . i in rng FG
by A164, A167, 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 A172: M . {} <= M . FGi by MEASURE1:31;

consider x9 being object such that

A173: x9 in G . (((i -' 1) mod (len b)) + 1) by A171, XBOOLE_0:def 1;

g . x9 = b . (((i -' 1) mod (len b)) + 1) by A9, A170, A173, MESFUNC3:def 1

.= b1 . i by A139, A169, A171 ;

then A174: 0 <= b1 . i by A6, SUPINF_2:51;

M . {} = 0 by VALUED_0:def 19;

then 0 <= (M * FG) . i by A164, A167, A172, FUNCT_1:13;

hence 0 <= y1 . i by A168, A174; :: thesis: verum

end;then reconsider FGi = FG . i as Element of S ;

reconsider EMPTY = {} as Element of S by MEASURE1:7;

EMPTY c= FGi ;

then A172: M . {} <= M . FGi by MEASURE1:31;

consider x9 being object such that

A173: x9 in G . (((i -' 1) mod (len b)) + 1) by A171, XBOOLE_0:def 1;

g . x9 = b . (((i -' 1) mod (len b)) + 1) by A9, A170, A173, MESFUNC3:def 1

.= b1 . i by A139, A169, A171 ;

then A174: 0 <= b1 . i by A6, SUPINF_2:51;

M . {} = 0 by VALUED_0:def 19;

then 0 <= (M * FG) . i by A164, A167, A172, FUNCT_1:13;

hence 0 <= y1 . i by A168, A174; :: thesis: verum

suppose A175:
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 A14, A15, A16, A169;

then M . (FG . i) = 0 by A175, VALUED_0:def 19;

then (M * FG) . i = 0 by A164, A167, FUNCT_1:13;

hence 0 <= y1 . i by A168; :: thesis: verum

end;then M . (FG . i) = 0 by A175, VALUED_0:def 19;

then (M * FG) . i = 0 by A164, A167, FUNCT_1:13;

hence 0 <= y1 . i by A168; :: thesis: verum

0 <= y1 . i ;

then ag: y1 is nonnegative by SUPINF_2:52;

not -infty in rng y1

proof

then (z1 " {+infty}) /\ (y1 " {-infty}) =
(z1 " {+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 A165; :: thesis: verum

end;then ex i being object st

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

hence contradiction by A165; :: thesis: verum

.= {} ;

then A176: dom (z1 + y1) = ((dom z1) /\ (dom y1)) \ ({} \/ {}) by A163, MESFUNC1:def 3

.= dom x1 by A122, A164, A156, FINSEQ_3:29 ;

A177: for k being Nat st k in dom x1 holds

x1 . k = (z1 + y1) . k

proof

A178:
len b divides (len a) * (len b)
by NAT_D:def 3;

let k be Nat; :: thesis: ( k in dom x1 implies x1 . k = (z1 + y1) . k )

set p = ((k -' 1) div (len b)) + 1;

set q = ((k -' 1) mod (len b)) + 1;

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

assume A180: k in dom x1 ; :: thesis: x1 . k = (z1 + y1) . k

then A181: k in Seg (len FG) by A122, FINSEQ_1:def 3;

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

A183: len b > 0 by A14, A181;

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

A185: k <= (len a) * (len b) by A14, A181, FINSEQ_1:1;

then A186: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

1 <= (len a) * (len b) by A182, A185, XXREAL_0:2;

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A184, A178, NAT_2:15;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A186, NAT_2:24;

then A187: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

len b <> 0 by A14, A181;

then ((k -' 1) div (len b)) + 1 <= len a by A187, NAT_D:18;

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A179;

then A188: ((k -' 1) div (len b)) + 1 in dom F by A13, FINSEQ_1:def 3;

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

(k -' 1) mod (len b) < len b by A183, NAT_D:1;

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A189;

then A190: ((k -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

A191: ((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))

c1 . k = (a1 . k) - (b1 . k) by A141, A142, A181;

then (c1 . k) + (b1 . k) = (a1 . k) - ((b1 . k) - (b1 . k)) by A200, XXREAL_3:32

.= (a1 . k) + (- 0) by A207

.= a1 . k by XXREAL_3:4 ;

hence x1 . k = ((c1 . k) + (b1 . k)) * ((M * FG) . k) by A122, A180

.= (z1 . k) + ((b1 . k) * ((M * FG) . k)) by A155, A153, A156, A180, A191

.= (z1 . k) + (y1 . k) by A155, A154, A164, A180

.= (z1 + y1) . k by A176, A180, MESFUNC1:def 3 ;

:: thesis: verum

end;let k be Nat; :: thesis: ( k in dom x1 implies x1 . k = (z1 + y1) . k )

set p = ((k -' 1) div (len b)) + 1;

set q = ((k -' 1) mod (len b)) + 1;

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

assume A180: k in dom x1 ; :: thesis: x1 . k = (z1 + y1) . k

then A181: k in Seg (len FG) by A122, FINSEQ_1:def 3;

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

A183: len b > 0 by A14, A181;

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

A185: k <= (len a) * (len b) by A14, A181, FINSEQ_1:1;

then A186: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

1 <= (len a) * (len b) by A182, A185, XXREAL_0:2;

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A184, A178, NAT_2:15;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A186, NAT_2:24;

then A187: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

len b <> 0 by A14, A181;

then ((k -' 1) div (len b)) + 1 <= len a by A187, NAT_D:18;

then ((k -' 1) div (len b)) + 1 in Seg (len a) by A179;

then A188: ((k -' 1) div (len b)) + 1 in dom F by A13, FINSEQ_1:def 3;

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

(k -' 1) mod (len b) < len b by A183, NAT_D:1;

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

then ((k -' 1) mod (len b)) + 1 in Seg (len b) by A189;

then A190: ((k -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;

A191: ((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))

proof
end;

A200:
( a1 . k <> +infty & a1 . k <> -infty & b1 . k <> +infty & b1 . k <> -infty )
per cases
( FG . k <> {} or FG . k = {} )
;

end;

suppose
FG . k <> {}
; :: thesis: ((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . 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 A14, A15, A16, A181;

then consider v being object such that

A192: v in (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by XBOOLE_0:def 1;

A193: G . (((k -' 1) mod (len b)) + 1) <> {} by A192;

A194: v in F . (((k -' 1) div (len b)) + 1) by A192, XBOOLE_0:def 4;

v in G . (((k -' 1) mod (len b)) + 1) by A192, XBOOLE_0:def 4;

then A195: b . (((k -' 1) mod (len b)) + 1) = g . v by A9, A190, MESFUNC3:def 1;

F . (((k -' 1) div (len b)) + 1) in rng F by A188, FUNCT_1:3;

then A196: v in dom f by A55, A194, TARSKI:def 4;

a . (((k -' 1) div (len b)) + 1) = f . v by A12, A188, A194, MESFUNC3:def 1;

then b . (((k -' 1) mod (len b)) + 1) <= a . (((k -' 1) div (len b)) + 1) by A7, A195, A196;

then A197: b1 . k <= a . (((k -' 1) div (len b)) + 1) by A139, A181, A193;

F . (((k -' 1) div (len b)) + 1) <> {} by A192;

then b1 . k <= a1 . k by A59, A181, A197;

then 0 <= (a1 . k) - (b1 . k) by XXREAL_3:40;

then A198: ( 0 = c1 . k or 0 < c1 . k ) by A141, A142, A181;

0 <= b . (((k -' 1) mod (len b)) + 1) by A6, A195, SUPINF_2:51;

then ( 0 = b1 . k or 0 < b1 . k ) by A139, A181, A192;

hence ((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A198, XXREAL_3:96; :: thesis: verum

end;then consider v being object such that

A192: v in (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by XBOOLE_0:def 1;

A193: G . (((k -' 1) mod (len b)) + 1) <> {} by A192;

A194: v in F . (((k -' 1) div (len b)) + 1) by A192, XBOOLE_0:def 4;

v in G . (((k -' 1) mod (len b)) + 1) by A192, XBOOLE_0:def 4;

then A195: b . (((k -' 1) mod (len b)) + 1) = g . v by A9, A190, MESFUNC3:def 1;

F . (((k -' 1) div (len b)) + 1) in rng F by A188, FUNCT_1:3;

then A196: v in dom f by A55, A194, TARSKI:def 4;

a . (((k -' 1) div (len b)) + 1) = f . v by A12, A188, A194, MESFUNC3:def 1;

then b . (((k -' 1) mod (len b)) + 1) <= a . (((k -' 1) div (len b)) + 1) by A7, A195, A196;

then A197: b1 . k <= a . (((k -' 1) div (len b)) + 1) by A139, A181, A193;

F . (((k -' 1) div (len b)) + 1) <> {} by A192;

then b1 . k <= a1 . k by A59, A181, A197;

then 0 <= (a1 . k) - (b1 . k) by XXREAL_3:40;

then A198: ( 0 = c1 . k or 0 < c1 . k ) by A141, A142, A181;

0 <= b . (((k -' 1) mod (len b)) + 1) by A6, A195, SUPINF_2:51;

then ( 0 = b1 . k or 0 < b1 . k ) by A139, A181, A192;

hence ((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A198, XXREAL_3:96; :: thesis: verum

suppose
FG . k = {}
; :: thesis: ((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))

then
M . (FG . k) = 0
by VALUED_0:def 19;

then A199: (M * FG) . k = 0 by A155, A180, FUNCT_1:13;

hence ((c1 . k) + (b1 . k)) * ((M * FG) . k) = 0

.= ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A199 ;

:: thesis: verum

end;then A199: (M * FG) . k = 0 by A155, A180, FUNCT_1:13;

hence ((c1 . k) + (b1 . k)) * ((M * FG) . k) = 0

.= ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A199 ;

:: thesis: verum

proof

end;

A207:
(b1 . k) - (b1 . k) = - 0
by XXREAL_3:7;now :: thesis: ( a1 . k <> +infty & -infty <> a1 . k )end;

hence
( +infty <> a1 . k & a1 . k <> -infty )
; :: thesis: ( b1 . k <> +infty & b1 . k <> -infty )per cases
( F . (((k -' 1) div (len b)) + 1) <> {} or F . (((k -' 1) div (len b)) + 1) = {} )
;

end;

suppose A201:
F . (((k -' 1) div (len b)) + 1) <> {}
; :: thesis: ( a1 . k <> +infty & -infty <> a1 . k )

then consider v being object such that

A202: v in F . (((k -' 1) div (len b)) + 1) by XBOOLE_0:def 1;

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

a1 . k = a . (((k -' 1) div (len b)) + 1) by A59, A181, A201;

then a1 . k = f . v by A12, A188, A202, MESFUNC3:def 1;

hence ( a1 . k <> +infty & -infty <> a1 . k ) by A203; :: thesis: verum

end;A202: v in F . (((k -' 1) div (len b)) + 1) by XBOOLE_0:def 1;

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

a1 . k = a . (((k -' 1) div (len b)) + 1) by A59, A181, A201;

then a1 . k = f . v by A12, A188, A202, MESFUNC3:def 1;

hence ( a1 . k <> +infty & -infty <> a1 . k ) by A203; :: thesis: verum

now :: thesis: ( b1 . k <> +infty & b1 . k <> -infty )end;

hence
( b1 . k <> +infty & b1 . k <> -infty )
; :: thesis: verumper cases
( G . (((k -' 1) mod (len b)) + 1) <> {} or G . (((k -' 1) mod (len b)) + 1) = {} )
;

end;

suppose A204:
G . (((k -' 1) mod (len b)) + 1) <> {}
; :: thesis: ( b1 . k <> +infty & b1 . k <> -infty )

then consider v being object such that

A205: v in G . (((k -' 1) mod (len b)) + 1) by XBOOLE_0:def 1;

A206: g is real-valued by A4, MESFUNC2:def 4;

b1 . k = b . (((k -' 1) mod (len b)) + 1) by A139, A181, A204;

then b1 . k = g . v by A9, A190, A205, MESFUNC3:def 1;

hence ( b1 . k <> +infty & b1 . k <> -infty ) by A206; :: thesis: verum

end;A205: v in G . (((k -' 1) mod (len b)) + 1) by XBOOLE_0:def 1;

A206: g is real-valued by A4, MESFUNC2:def 4;

b1 . k = b . (((k -' 1) mod (len b)) + 1) by A139, A181, A204;

then b1 . k = g . v by A9, A190, A205, MESFUNC3:def 1;

hence ( b1 . k <> +infty & b1 . k <> -infty ) by A206; :: thesis: verum

c1 . k = (a1 . k) - (b1 . k) by A141, A142, A181;

then (c1 . k) + (b1 . k) = (a1 . k) - ((b1 . k) - (b1 . k)) by A200, XXREAL_3:32

.= (a1 . k) + (- 0) by A207

.= a1 . k by XXREAL_3:4 ;

hence x1 . k = ((c1 . k) + (b1 . k)) * ((M * FG) . k) by A122, A180

.= (z1 . k) + ((b1 . k) * ((M * FG) . k)) by A155, A153, A156, A180, A191

.= (z1 . k) + (y1 . k) by A155, A154, A164, A180

.= (z1 + y1) . k by A176, A180, MESFUNC1:def 3 ;

:: thesis: verum

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

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

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

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

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

g is real-valued by A4, MESFUNC2:def 4;

then A209: |.(g . x).| < +infty by A5, A10, A208, MESFUNC2:def 1;

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

then |.(f . x).| < +infty by A5, A10, A208, MESFUNC2:def 1;

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

|.((f - g) . x).| = |.((f . x) - (g . x)).| by A208, MESFUNC1:def 4;

then |.((f - g) . x).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:32;

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

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

g is real-valued by A4, MESFUNC2:def 4;

then A209: |.(g . x).| < +infty by A5, A10, A208, MESFUNC2:def 1;

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

then |.(f . x).| < +infty by A5, A10, A208, MESFUNC2:def 1;

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

|.((f - g) . x).| = |.((f . x) - (g . x)).| by A208, MESFUNC1:def 4;

then |.((f - g) . x).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:32;

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

hence A211: f - g is_simple_func_in S by A5, A61, A10, A99, MESFUNC2:def 4; :: thesis: ( dom (f - g) <> {} & f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )

dom FG = dom a1 by A59, FINSEQ_1:def 3;

then FG,a1 are_Re-presentation_of f by A61, A123, MESFUNC3:def 1;

then A212: integral (M,f) = Sum x1 by A1, A2, A3, A122, A155, MESFUNC4:3;

dom (z1 + y1) = Seg (len x1) by A176, FINSEQ_1:def 3;

then z1 + y1 is FinSequence by FINSEQ_1:def 2;

then A213: x1 = z1 + y1 by A176, A177, FINSEQ_1:13;

dom FG = dom b1 by A139, FINSEQ_1:def 3;

then FG,b1 are_Re-presentation_of g by A5, A61, A143, MESFUNC3:def 1;

then A214: integral (M,g) = Sum y1 by A2, A4, A5, A6, A154, A164, MESFUNC4:3;

thus dom (f - g) <> {} by A2, A5, A10; :: thesis: ( f - g is nonnegative & integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) )

for x being object st x in dom (f - g) holds

0 <= (f - g) . x

proof

hence aa:
f - g is nonnegative
by SUPINF_2:52; :: thesis: integral (M,f) = (integral (M,(f - g))) + (integral (M,g))
let x be object ; :: thesis: ( x in dom (f - g) implies 0 <= (f - g) . x )

assume A216: x in dom (f - g) ; :: thesis: 0 <= (f - g) . x

then 0 <= (f . x) - (g . x) by A5, A7, A10, XXREAL_3:40;

hence 0 <= (f - g) . x by A216, MESFUNC1:def 4; :: thesis: verum

end;assume A216: x in dom (f - g) ; :: thesis: 0 <= (f - g) . x

then 0 <= (f . x) - (g . x) by A5, A7, A10, XXREAL_3:40;

hence 0 <= (f - g) . x by A216, MESFUNC1:def 4; :: thesis: verum

dom FG = dom c1 by A140, FINSEQ_3:29;

then FG,c1 are_Re-presentation_of f - g by A5, A61, A10, A149, MESFUNC3:def 1;

then integral (M,(f - g)) = Sum z1 by aa, A2, A5, A153, A156, A10, A211, MESFUNC4:3;

hence integral (M,f) = (integral (M,(f - g))) + (integral (M,g)) by A164, A156, A212, A214, A213, MESFUNC4:1, ag, cd; :: thesis: verum