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 X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,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 X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,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 X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,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 X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,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 X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,M,g) )
A8: for x being set st x in dom g holds
0 <= g . x by A6, SUPINF_2:70;
then 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 X,S,M,g = Sum y by A2, A4, A5, MESFUNC4:4;
g is V61() by A4, MESFUNC2:def 5;
then A10: dom (f - g) = (dom f) /\ (dom g) by MESFUNC2:2;
A11: for x being set st x in dom f holds
0 <= f . x by A3, SUPINF_2:70;
then 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 X,S,M,f = Sum x by A1, A2, MESFUNC4:4;
set la = len a;
A13: dom F = dom a by A12, MESFUNC3:def 1;
set lb = len b;
deffunc H₁( 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₁(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

proof

let b be set ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not b in proj2 FG or b in S )

A18: now

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:3;
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:26;
1 <= k by A21, FINSEQ_1:3;
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:17;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A23, XREAL_1:21;
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:8;
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:12;
((k -' 1) mod (len b)) + 1 >= 0 + 1 by XREAL_1:8;
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:12;
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:66; :: thesis: verum

end;

assume b in rng FG ; :: thesis: b in S
then ex a being set st
( a in dom FG & b = FG . a ) by FUNCT_1:def 5;
hence b in S by A18; :: thesis: verum

end;

then reconsider FG = FG as FinSequence of S ;
for k, l being Nat st k in dom FG & l in dom FG & k <> l holds
FG . k misses FG . l

proof

let k, l be Nat; :: thesis: ( 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: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;
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:3;
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:17;
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:26;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
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:8;
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:8;
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:8;
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:3;

A49: now

(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:235;
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:235;
hence contradiction by A32, A51, A52, A50; :: thesis: verum

end;

l <= (len a) * (len b) by A47, FINSEQ_1:3;
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:26;
then ((l -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
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:8;
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;

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, XBOOLE_0:def 7;
hence FG . k misses FG . l by XBOOLE_0:def 7; :: thesis: verum

end;

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, XBOOLE_0:def 7;
hence FG . k misses FG . l by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A55: dom f = union (rng F) by A12, MESFUNC3:def 1;
defpred S₁[ 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₂[ 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₂[k,v]

proof

let k be Nat; :: thesis: ( k in Seg (len FG) implies ex v being Element of ExtREAL st S₂[k,v] )
assume k in Seg (len FG) ; :: thesis: ex v being Element of ExtREAL st S₂[k,v]

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

suppose A57: F . (((k -' 1) div (len b)) + 1) = {} ; :: thesis: ex v being Element of ExtREAL st S₂[k,v]

take v = 0. ; :: thesis: S₂[k,v]
thus S₂[k,v] by A57; :: thesis: verum

end;

suppose A58: F . (((k -' 1) div (len b)) + 1) <> {} ; :: thesis: ex v being Element of ExtREAL st S₂[k,v]

take v = a . (((k -' 1) div (len b)) + 1); :: thesis: S₂[k,v]
thus S₂[k,v] by A58; :: thesis: verum

end;

end;

end;

consider a1 being FinSequence of ExtREAL such that
A59: ( dom a1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds
S₂[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)

proof

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

proof

let z be set ; :: 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:11;
A67: i in Seg (len a) by A13, A65, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:3;
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:11;
A73: j in Seg (len b) by A17, A71, FINSEQ_1:def 3;
then A74: 1 <= j by FINSEQ_1:3;
then consider j9 being Nat such that
A75: j = 1 + j9 by NAT_1:10;
(i9 * (len b)) + j is Nat ;
then reconsider k = ((i - 1) * (len b)) + j as Element of NAT by A68;
i <= len a by A67, FINSEQ_1:3;
then i - 1 <= (len a) - 1 by XREAL_1:11;
then (i - 1) * (len b) <= ((len a) - 1) * (len b) by XREAL_1:66;
then A76: k <= (((len a) - 1) * (len b)) + j by XREAL_1:8;
A77: k >= 0 + j by A68, XREAL_1:8;
then k -' 1 = k - 1 by A74, XREAL_1:235, XXREAL_0:2;
then A78: k -' 1 = (i9 * (len b)) + j9 by A68, A75;
A79: j <= len b by A73, FINSEQ_1:3;
then (((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b) by XREAL_1:8;
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 5;
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;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in union (rng FG) or z in 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:11;
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:3;
then A93: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;
1 <= k by A91, FINSEQ_1:3;
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:17;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A93, NAT_2:26;
then A96: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
set j = ((k -' 1) mod (len b)) + 1;
A97: ((k -' 1) div (len b)) + 1 >= 0 + 1 by XREAL_1:8;
((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 5;
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;

A99: for k being Nat
for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
(f - g) . x = (f - g) . y

proof

let k be Nat; :: thesis: 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:8;
A106: k in Seg (len FG) by A100, FINSEQ_1:def 3;
then A107: 1 <= k by FINSEQ_1:3;
then A108: len b > 0 by A14, A106, FINSEQ_1:3;
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:3;
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:17;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A113, NAT_2:26;
then A114: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
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:8;
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 5;
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;

deffunc H₂( 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₂(k) ) ) from FINSEQ_2:sch 1();
A123: for k being Nat st k in dom FG holds
for x being set st x in FG . k holds
f . x = a1 . k

proof

let k be Nat; :: thesis: ( k in dom FG implies for x being set st x in FG . k holds
f . x = a1 . k )
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
A124: ((k -' 1) div (len b)) + 1 >= 0 + 1 by XREAL_1:8;
assume A125: k in dom FG ; :: thesis: for x being set 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 set ; :: 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:3;
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:26;
A132: len b divides (len a) * (len b) by NAT_D:def 3;
1 <= k by A129, FINSEQ_1:3;
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:17;
then A135: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A131, XREAL_1:21;
((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;

A136: for k being Nat st k in Seg (len FG) holds
ex v being Element of ExtREAL st S₁[k,v]

proof

let k be Nat; :: thesis: ( k in Seg (len FG) implies ex v being Element of ExtREAL st S₁[k,v] )
assume k in Seg (len FG) ; :: thesis: ex v being Element of ExtREAL st S₁[k,v]

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

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

take v = R_EAL 0 ; :: thesis: S₁[k,v]
thus S₁[k,v] by A137; :: thesis: verum

end;

suppose A138: G . (((k -' 1) mod (len b)) + 1) <> {} ; :: thesis: ex v being Element of ExtREAL st S₁[k,v]

take v = b . (((k -' 1) mod (len b)) + 1); :: thesis: S₁[k,v]
thus S₁[k,v] by A138; :: thesis: verum

end;

end;

end;

consider b1 being FinSequence of ExtREAL such that
A139: ( dom b1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds
S₁[k,b1 . k] ) ) from FINSEQ_1:sch 5(A136);
deffunc H₃( 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₃(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 set st x in FG . k holds
g . x = b1 . k

proof

let k be Nat; :: thesis: ( k in dom FG implies for x being set st x in FG . k holds
g . x = b1 . k )
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
assume A144: k in dom FG ; :: thesis: for x being set 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 set ; :: 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:8;
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;

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

proof

let k be Nat; :: thesis: ( k in dom FG implies for x being set st x in FG . k holds
(f - g) . x = c1 . k )
assume A150: k in dom FG ; :: thesis: for x being set st x in FG . k holds
(f - g) . x = c1 . k
let x be set ; :: 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 5;
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;

deffunc H₄( 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₄(k) ) ) from FINSEQ_2:sch 1();
deffunc H₅( 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₅(k) ) ) from FINSEQ_2:sch 1();
A155: dom x1 = dom FG by A122, FINSEQ_3:31;
A156: dom z1 = dom FG by A153, FINSEQ_3:31;
A157: for i being Nat st i in dom x1 holds
0 <= z1 . i

proof

reconsider EMPTY = {} as Element of S by PROB_1:10;
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:23;
FG . i in rng FG by A155, A158, FUNCT_1:12;
then reconsider V = FG . i as Element of S ;
M . EMPTY <= M . V by MEASURE1:62, 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 = {} ) ;

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

then consider x being set such that
A162: x in FG . i by XBOOLE_0:def 1;
FG . i in rng FG by A155, A158, FUNCT_1:12;
then A163: 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:43;
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
reconsider x = x as Element of X by A61, A163;

end;

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

then (M * FG) . i = 0 by A159, VALUED_0:def 19;
then (c1 . i) * ((M * FG) . i) = 0 ;
hence 0 <= z1 . i by A155, A153, A156, A158; :: thesis: verum

end;

end;

end;

not -infty in rng z1

proof

assume -infty in rng z1 ; :: thesis: contradiction
then ex i being set st
( i in dom z1 & z1 . i = -infty ) by FUNCT_1:def 5;
hence contradiction by A155, A156, A157; :: thesis: verum

end;

then A164: (z1 " {-infty }) /\ (y1 " {+infty }) = {} /\ (y1 " {+infty }) by FUNCT_1:142
.= {} ;
A165: dom y1 = dom FG by A154, FINSEQ_3:31;
A166: for i being Nat st i in dom y1 holds
0 <= y1 . i

proof

let i be Nat; :: thesis: ( i in dom y1 implies 0 <= y1 . i )
set i9 = ((i -' 1) mod (len b)) + 1;
A167: ((i -' 1) mod (len b)) + 1 >= 0 + 1 by XREAL_1:8;
assume A168: i in dom y1 ; :: thesis: 0 <= y1 . i
then A169: y1 . i = (b1 . i) * ((M * FG) . i) by A154;
A170: i in Seg (len FG) by A154, A168, 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 A167;
then A171: ((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) = {} ) ;

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

FG . i in rng FG by A165, A168, FUNCT_1:12;
then reconsider FGi = FG . i as Element of S ;
reconsider EMPTY = {} as Element of S by MEASURE1:21;
EMPTY c= FGi by XBOOLE_1:2;
then A173: M . {} <= M . FGi by MEASURE1:62;
consider x9 being set such that
A174: x9 in G . (((i -' 1) mod (len b)) + 1) by A172, XBOOLE_0:def 1;
g . x9 = b . (((i -' 1) mod (len b)) + 1) by A9, A171, A174, MESFUNC3:def 1
.= b1 . i by A139, A170, A172 ;
then A175: 0 <= b1 . i by A6, SUPINF_2:70;
M . {} = 0 by VALUED_0:def 19;
then 0 <= (M * FG) . i by A165, A168, A173, FUNCT_1:23;
hence 0 <= y1 . i by A169, A175; :: thesis: verum

end;

suppose A176: 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, A170;
then M . (FG . i) = 0 by A176, VALUED_0:def 19;
then (M * FG) . i = 0 by A165, A168, FUNCT_1:23;
hence 0 <= y1 . i by A169; :: thesis: verum

end;

end;

end;

not -infty in rng y1

proof

assume -infty in rng y1 ; :: thesis: contradiction
then ex i being set st
( i in dom y1 & y1 . i = -infty ) by FUNCT_1:def 5;
hence contradiction by A166; :: thesis: verum

end;

then (z1 " {+infty }) /\ (y1 " {-infty }) = (z1 " {+infty }) /\ {} by FUNCT_1:142
.= {} ;
then A177: dom (z1 + y1) = ((dom z1) /\ (dom y1)) \ ({} \/ {} ) by A164, MESFUNC1:def 3
.= dom x1 by A122, A165, A156, FINSEQ_3:31 ;
A178: for k being Nat st k in dom x1 holds
x1 . k = (z1 + y1) . k

proof

A179: 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;
A180: ((k -' 1) div (len b)) + 1 >= 0 + 1 by XREAL_1:8;
assume A181: k in dom x1 ; :: thesis: x1 . k = (z1 + y1) . k
then A182: k in Seg (len FG) by A122, FINSEQ_1:def 3;
then A183: 1 <= k by FINSEQ_1:3;
then A184: len b > 0 by A14, A182, FINSEQ_1:3;
then A185: len b >= 0 + 1 by NAT_1:13;
A186: k <= (len a) * (len b) by A14, A182, FINSEQ_1:3;
then A187: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;
1 <= (len a) * (len b) by A183, A186, XXREAL_0:2;
then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A185, A179, NAT_2:17;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A187, NAT_2:26;
then A188: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
len b <> 0 by A14, A182;
then ((k -' 1) div (len b)) + 1 <= len a by A188, NAT_D:18;
then ((k -' 1) div (len b)) + 1 in Seg (len a) by A180;
then A189: ((k -' 1) div (len b)) + 1 in dom F by A13, FINSEQ_1:def 3;
A190: ((k -' 1) mod (len b)) + 1 >= 0 + 1 by XREAL_1:8;
(k -' 1) mod (len b) < len b by A184, 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 A190;
then A191: ((k -' 1) mod (len b)) + 1 in dom G by A17, FINSEQ_1:def 3;
A192: ((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))

proof

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

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, A182;
then consider v being set such that
A193: v in (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by XBOOLE_0:def 1;
A194: G . (((k -' 1) mod (len b)) + 1) <> {} by A193;
A195: v in F . (((k -' 1) div (len b)) + 1) by A193, XBOOLE_0:def 4;
v in G . (((k -' 1) mod (len b)) + 1) by A193, XBOOLE_0:def 4;
then A196: b . (((k -' 1) mod (len b)) + 1) = g . v by A9, A191, MESFUNC3:def 1;
F . (((k -' 1) div (len b)) + 1) in rng F by A189, FUNCT_1:12;
then A197: v in dom f by A55, A195, TARSKI:def 4;
a . (((k -' 1) div (len b)) + 1) = f . v by A12, A189, A195, MESFUNC3:def 1;
then b . (((k -' 1) mod (len b)) + 1) <= a . (((k -' 1) div (len b)) + 1) by A7, A196, A197;
then A198: b1 . k <= a . (((k -' 1) div (len b)) + 1) by A139, A182, A194;
F . (((k -' 1) div (len b)) + 1) <> {} by A193;
then b1 . k <= a1 . k by A59, A182, A198;
then 0 <= (a1 . k) - (b1 . k) by XXREAL_3:43;
then A199: ( 0 = c1 . k or 0 < c1 . k ) by A141, A142, A182;
reconsider v = v as Element of X by A197;
0 <= b . (((k -' 1) mod (len b)) + 1) by A6, A196, SUPINF_2:70;
then ( 0 = b1 . k or 0 < b1 . k ) by A139, A182, A193;
hence ((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A199, XXREAL_3:107; :: thesis: verum

end;

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 A200: (M * FG) . k = 0 by A155, A181, FUNCT_1:23;
hence ((c1 . k) + (b1 . k)) * ((M * FG) . k) = 0
.= ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A200 ;
:: thesis: verum

end;

end;

end;

A201: ( a1 . k <> +infty & a1 . k <> -infty & b1 . k <> +infty & b1 . k <> -infty )

proof

now

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

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

then consider v being set such that
A203: v in F . (((k -' 1) div (len b)) + 1) by XBOOLE_0:def 1;
F . (((k -' 1) div (len b)) + 1) in rng F by A189, FUNCT_1:12;
then A204: v in dom f by A55, A203, TARSKI:def 4;
A205: f is V61() by A1, MESFUNC2:def 5;
a1 . k = a . (((k -' 1) div (len b)) + 1) by A59, A182, A202;
then a1 . k = f . v by A12, A189, A203, MESFUNC3:def 1;
hence ( a1 . k <> +infty & -infty <> a1 . k ) by A205; :: thesis: verum
reconsider v = v as Element of X by A204;

end;

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

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

end;

end;

end;

hence ( +infty <> a1 . k & a1 . k <> -infty ) ; :: thesis: ( b1 . k <> +infty & b1 . k <> -infty )

now

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

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

then consider v being set such that
A207: v in G . (((k -' 1) mod (len b)) + 1) by XBOOLE_0:def 1;
G . (((k -' 1) mod (len b)) + 1) in rng G by A191, FUNCT_1:12;
then A208: v in dom g by A60, A207, TARSKI:def 4;
A209: g is V61() by A4, MESFUNC2:def 5;
b1 . k = b . (((k -' 1) mod (len b)) + 1) by A139, A182, A206;
then b1 . k = g . v by A9, A191, A207, MESFUNC3:def 1;
hence ( b1 . k <> +infty & b1 . k <> -infty ) by A209; :: thesis: verum
reconsider v = v as Element of X by A208;

end;

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

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

end;

end;

end;

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

end;

A210: (b1 . k) - (b1 . k) = - 0 by XXREAL_3:7;
c1 . k = (a1 . k) - (b1 . k) by A141, A142, A182;
then (c1 . k) + (b1 . k) = (a1 . k) - ((b1 . k) - (b1 . k)) by A201, XXREAL_3:33
.= (a1 . k) + (- 0 ) by A210
.= a1 . k by XXREAL_3:4 ;
hence x1 . k = ((c1 . k) + (b1 . k)) * ((M * FG) . k) by A122, A181
.= (z1 . k) + ((b1 . k) * ((M * FG) . k)) by A155, A153, A156, A181, A192
.= (z1 . k) + (y1 . k) by A155, A154, A165, A181
.= (z1 + y1) . k by A177, A181, MESFUNC1:def 3 ;
:: thesis: verum

end;

now

let x be Element of X; :: thesis: ( x in dom (f - g) implies |.((f - g) . x).| < +infty )
assume A211: x in dom (f - g) ; :: thesis: |.((f - g) . x).| < +infty
g is V61() by A4, MESFUNC2:def 5;
then A212: |.(g . x).| < +infty by A5, A10, A211, MESFUNC2:def 1;
A213: f is V61() by A1, MESFUNC2:def 5;
then |.(f . x).| < +infty by A5, A10, A211, MESFUNC2:def 1;
then A214: |.(f . x).| + |.(g . x).| <> +infty by A212, XXREAL_3:16;
|.((f - g) . x).| = |.((f . x) - (g . x)).| by A211, MESFUNC1:def 4;
then |.((f - g) . x).| <= |.(f . x).| + |.(g . x).| by A213, EXTREAL2:69;
hence |.((f - g) . x).| < +infty by A214, XXREAL_0:2, XXREAL_0:4; :: thesis: verum

end;

then f - g is V61() by MESFUNC2:def 1;
hence A215: f - g is_simple_func_in S by A5, A61, A10, A99, MESFUNC2:def 5; :: thesis: ( dom (f - g) <> {} & f - g is nonnegative & integral X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,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 A216: integral X,S,M,f = Sum x1 by A1, A2, A11, A122, A155, MESFUNC4:3;
dom (z1 + y1) = Seg (len x1) by A177, FINSEQ_1:def 3;
then z1 + y1 is FinSequence by FINSEQ_1:def 2;
then A217: x1 = z1 + y1 by A177, A178, FINSEQ_1:17;
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 A218: integral X,S,M,g = Sum y1 by A2, A4, A5, A8, A154, A165, MESFUNC4:3;
thus dom (f - g) <> {} by A2, A5, A10; :: thesis: ( f - g is nonnegative & integral X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,M,g) )
A219: for x being set st x in dom (f - g) holds
0 <= (f - g) . x

proof

let x be set ; :: thesis: ( x in dom (f - g) implies 0 <= (f - g) . x )
assume A220: x in dom (f - g) ; :: thesis: 0 <= (f - g) . x
then 0 <= (f . x) - (g . x) by A5, A7, A10, XXREAL_3:43;
hence 0 <= (f - g) . x by A220, MESFUNC1:def 4; :: thesis: verum

end;

hence f - g is nonnegative by SUPINF_2:71; :: thesis: integral X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,M,g)
dom FG = dom c1 by A140, FINSEQ_3:31;
then FG,c1 are_Re-presentation_of f - g by A5, A61, A10, A149, MESFUNC3:def 1;
then integral X,S,M,(f - g) = Sum z1 by A2, A5, A153, A156, A10, A215, A219, MESFUNC4:3;
hence integral X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,M,g) by A155, A165, A156, A216, A218, A166, A157, A217, MESFUNC4:1; :: thesis: verum