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₁( 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 object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not b in rng FG or b in S )

A18: now :: thesis: for k being Element of NAT st k in dom FG holds
FG . 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;

assume b in rng FG ; :: thesis: 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;

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

l <= (len a) * (len b) by A47, 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;

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

end;

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

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

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 0. ; :: thesis: S₂[k, 0. ]
thus S₂[k, 0. ] 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 a . (((k -' 1) div (len b)) + 1) ; :: thesis: S₂[k,a . (((k -' 1) div (len b)) + 1)]
thus S₂[k,a . (((k -' 1) div (len b)) + 1)] 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 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;

let z be object ; :: 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: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;

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

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 object st x in FG . k holds
f . x = a1 . k

proof

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;

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]

reconsider z = 0 as R_eal by XXREAL_0:def 1;
take z ; :: thesis: S₁[k,z]
thus S₁[k,z] 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 b . (((k -' 1) mod (len b)) + 1) ; :: thesis: S₁[k,b . (((k -' 1) mod (len b)) + 1)]
thus S₁[k,b . (((k -' 1) mod (len b)) + 1)] 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 object st x in FG . k holds
g . x = b1 . k

proof

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

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

proof

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

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

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;

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

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;

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;

then for i being object st i in dom z1 holds
0 <= z1 . i by A156, A155;
then cd: z1 is nonnegative by SUPINF_2:52;
not -infty in rng z1

proof

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 A163: (z1 " {-infty}) /\ (y1 " {+infty}) = {} /\ (y1 " {+infty}) by FUNCT_1:72
.= {} ;
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

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;

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

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;

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;

end;

end;

then for i being object st i in dom y1 holds
0 <= y1 . i ;
then ag: y1 is nonnegative by SUPINF_2:52;
not -infty in rng y1

proof

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

end;

then (z1 " {+infty}) /\ (y1 " {-infty}) = (z1 " {+infty}) /\ {} by FUNCT_1:72
.= {} ;
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))

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

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;

end;

end;

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

proof

now :: thesis: ( a1 . k <> +infty & -infty <> a1 . k )

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

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;

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

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

end;

end;

end;

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

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

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

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;

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

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

end;

end;

end;

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

end;

A207: (b1 . k) - (b1 . k) = - 0 by XXREAL_3:7;
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;

now :: thesis: for x being Element of X st x in dom (f - g) holds
|.((f - g) . x).| < +infty

let x be Element of X; :: thesis: ( x in dom (f - g) implies |.((f - g) . x).| < +infty )
assume 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;

then f - g is real-valued by MESFUNC2:def 1;
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

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;

hence aa: f - g is nonnegative by SUPINF_2:52; :: thesis: integral (M,f) = (integral (M,(f - g))) + (integral (M,g))
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