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 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
A9: 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;
A10: 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
A11: 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;
set la = len a;
set lb = len b;
A12: ( dom f = union (rng F) & dom g = union (rng G) & dom F = dom a & dom G = dom b ) by A9, A11, MESFUNC3:def 1;
deffunc H1( Nat) -> set = (F . ((($1 -' 1) div (len b)) + 1)) /\ (G . ((($1 -' 1) mod (len b)) + 1));
consider FG being FinSequence such that
A13: len FG = (len a) * (len b) and
A14: for k being Nat st k in dom FG holds
FG . k = H1(k) from FINSEQ_1:sch 2();
 A15: dom FG = Seg ((len a) * (len b)) by A13, FINSEQ_1:def 3;
FG is FinSequence of S
proof
A16: now
let k be Element of NAT ; :: thesis: ( k in dom FG implies FG . k in S )
assume A17: k in dom FG ; :: thesis: FG . k in S
then A18: k in Seg ((len a) * (len b)) by A13, FINSEQ_1:def 3;
A19: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A17;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
A20: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
A21: ( 1 <= k & k <= (len a) * (len b) ) by A18, FINSEQ_1:3;
A22: len b <> 0 by A18;
len b >= 0 + 1 by A22, NAT_1:13;
then ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) & 1 <= len b ) by A21, NAT_D:def 3, XXREAL_0:2;
then A24: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A21, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:26;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A24, XREAL_1:21;
then A25: ((k -' 1) div (len b)) + 1 <= len a by A22, NAT_D:18;
(k -' 1) mod (len b) < len b by A22, NAT_D:1;
then ((k -' 1) mod (len b)) + 1 <= len b by NAT_1:13;
then ( ((k -' 1) div (len b)) + 1 in Seg (len a) & ((k -' 1) mod (len b)) + 1 in Seg (len b) ) by A20, A25;
then ( ((k -' 1) div (len b)) + 1 in dom F & ((k -' 1) mod (len b)) + 1 in dom G ) by A12, FINSEQ_1:def 3;
then ( F . (((k -' 1) div (len b)) + 1) in rng F & G . (((k -' 1) mod (len b)) + 1) in rng G ) by FUNCT_1:12;
hence FG . k in S by A19, MEASURE1:66; :: thesis: verum
end;
let b be set ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not b in rng FG or b in S )
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 A16; :: 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 A26: ( k in dom FG & l in dom FG & k <> l ) ; :: thesis: FG . k misses FG . l
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
set n = ((l -' 1) div (len b)) + 1;
set m = ((l -' 1) mod (len b)) + 1;
A27: ( k in Seg ((len a) * (len b)) & l in Seg ((len a) * (len b)) ) by A13, A26, FINSEQ_1:def 3;
then A28: ( 1 <= k & k <= (len a) * (len b) ) by FINSEQ_1:3;
A29: len b <> 0 by A27;
len b >= 0 + 1 by A29, NAT_1:13;
then ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) & 1 <= len b ) by A28, NAT_D:def 3, XXREAL_0:2;
then A31: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A28, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A31, NAT_2:26;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
then A32: ((k -' 1) div (len b)) + 1 <= len a by A29, NAT_D:18;
A33: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((l -' 1) div (len b)) + 1 >= 0 + 1 & ((l -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
( (k -' 1) mod (len b) < len b & (l -' 1) mod (len b) < len b ) by A29, NAT_D:1;
then ( ((k -' 1) mod (len b)) + 1 <= len b & ((l -' 1) mod (len b)) + 1 <= len b ) by NAT_1:13;
then ( ((k -' 1) div (len b)) + 1 in Seg (len a) & ((k -' 1) mod (len b)) + 1 in Seg (len b) & ((l -' 1) mod (len b)) + 1 in Seg (len b) ) by A32, A33;
then A34: ( ((k -' 1) div (len b)) + 1 in dom F & ((k -' 1) mod (len b)) + 1 in dom G & ((l -' 1) mod (len b)) + 1 in dom G ) by A12, FINSEQ_1:def 3;
A35: ( 1 <= l & l <= (len a) * (len b) ) by A27, 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 A31, NAT_2:26;
then ((l -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
then ((l -' 1) div (len b)) + 1 <= len a by A29, NAT_D:18;
then ((l -' 1) div (len b)) + 1 in Seg (len a) by A33;
then A36: ((l -' 1) div (len b)) + 1 in dom F by A12, FINSEQ_1:def 3;
A37: now
assume A38: ( ((k -' 1) div (len b)) + 1 = ((l -' 1) div (len b)) + 1 & ((k -' 1) mod (len b)) + 1 = ((l -' 1) mod (len b)) + 1 ) ; :: thesis: contradiction
( (k -' 1) + 1 = ((((((k -' 1) div (len b)) + 1) - 1) * (len b)) + ((((k -' 1) mod (len b)) + 1) - 1)) + 1 & (l -' 1) + 1 = ((((((l -' 1) div (len b)) + 1) - 1) * (len b)) + ((((l -' 1) mod (len b)) + 1) - 1)) + 1 ) by A29, NAT_D:2;
then ( (k - 1) + 1 = (((((k -' 1) div (len b)) + 1) - 1) * (len b)) + (((k -' 1) mod (len b)) + 1) & (l - 1) + 1 = (((((l -' 1) div (len b)) + 1) - 1) * (len b)) + (((l -' 1) mod (len b)) + 1) ) by A28, A35, XREAL_1:235;
hence contradiction by A26, A38; :: thesis: verum
end;
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A26;
then A39: (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 A14, A26
.= (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 ;
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 A37;
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 A34, A36, MESFUNC3:4;
then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A39, 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 A34, MESFUNC3:4;
then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len b)) + 1)) /\ (F . (((l -' 1) div (len b)) + 1))) /\ {} by A39, 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;
defpred S1[ 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) ) );
A40: for k being Nat st k in Seg (len FG) holds
ex v being Element of ExtREAL st S1[k,v]
proof
let k be Nat; :: thesis: ( k in Seg (len FG) implies ex v being Element of ExtREAL st S1[k,v] )
assume k in Seg (len FG) ; :: thesis: ex v being Element of ExtREAL st S1[k,v]
per cases ( F . (((k -' 1) div (len b)) + 1) = {} or F . (((k -' 1) div (len b)) + 1) <> {} ) ;
suppose A41: F . (((k -' 1) div (len b)) + 1) = {} ; :: thesis: ex v being Element of ExtREAL st S1[k,v]
take v = 0. ; :: thesis: S1[k,v]
thus S1[k,v] by A41; :: thesis: verum
end;
suppose A42: F . (((k -' 1) div (len b)) + 1) <> {} ; :: thesis: ex v being Element of ExtREAL st S1[k,v]
take v = a . (((k -' 1) div (len b)) + 1); :: thesis: S1[k,v]
thus S1[k,v] by A42; :: thesis: verum
end;
end;
end;
consider a1 being FinSequence of ExtREAL such that
A43: ( dom a1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds
S1[k,a1 . k] ) ) from FINSEQ_1:sch 5(A40);
 deffunc H2( Nat) -> Element of ExtREAL = (a1 . $1) * ((M * FG) . $1);
consider x1 being FinSequence of ExtREAL such that
A44: ( len x1 = len FG & ( for k being Nat st k in dom x1 holds
x1 . k = H2(k) ) ) from FINSEQ_2:sch 1();
 A45: dom x1 = dom FG by A44, FINSEQ_3:31;
defpred S2[ 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) ) );
A47: for k being Nat st k in Seg (len FG) holds
ex v being Element of ExtREAL st S2[k,v]
proof
let k be Nat; :: thesis: ( k in Seg (len FG) implies ex v being Element of ExtREAL st S2[k,v] )
assume k in Seg (len FG) ; :: thesis: ex v being Element of ExtREAL st S2[k,v]
per cases ( G . (((k -' 1) mod (len b)) + 1) = {} or G . (((k -' 1) mod (len b)) + 1) <> {} ) ;
suppose A48: G . (((k -' 1) mod (len b)) + 1) = {} ; :: thesis: ex v being Element of ExtREAL st S2[k,v]
take v = R_EAL 0 ; :: thesis: S2[k,v]
thus S2[k,v] by A48; :: thesis: verum
end;
suppose A49: G . (((k -' 1) mod (len b)) + 1) <> {} ; :: thesis: ex v being Element of ExtREAL st S2[k,v]
take v = b . (((k -' 1) mod (len b)) + 1); :: thesis: S2[k,v]
thus S2[k,v] by A49; :: thesis: verum
end;
end;
end;
consider b1 being FinSequence of ExtREAL such that
A50: ( dom b1 = Seg (len FG) & ( for k being Nat st k in Seg (len FG) holds
S2[k,b1 . k] ) ) from FINSEQ_1:sch 5(A47);
 deffunc H3( Nat) -> Element of ExtREAL = (b1 . $1) * ((M * FG) . $1);
consider y1 being FinSequence of ExtREAL such that
A51: ( len y1 = len FG & ( for k being Nat st k in dom y1 holds
y1 . k = H3(k) ) ) from FINSEQ_2:sch 1();
 A52: dom y1 = dom FG by A51, FINSEQ_3:31;
deffunc H4( Nat) -> Element of ExtREAL = (a1 . $1) - (b1 . $1);
consider c1 being FinSequence of ExtREAL such that
A54: len c1 = len FG and
A55: for k being Nat st k in dom c1 holds
c1 . k = H4(k) from FINSEQ_2:sch 1();
 A56: dom c1 = Seg (len FG) by A54, FINSEQ_1:def 3;
deffunc H5( Nat) -> Element of ExtREAL = (c1 . $1) * ((M * FG) . $1);
consider z1 being FinSequence of ExtREAL such that
A57: ( len z1 = len FG & ( for k being Nat st k in dom z1 holds
z1 . k = H5(k) ) ) from FINSEQ_2:sch 1();
 A58: dom z1 = dom FG by A57, FINSEQ_3:31;
A60: 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 A61: z in dom f ; :: thesis: z in union (rng FG)
then consider Y being set such that
A62: ( z in Y & Y in rng F ) by A12, TARSKI:def 4;
consider i being Nat such that
A63: ( i in dom F & Y = F . i ) by A62, FINSEQ_2:11;
consider Z being set such that
A64: ( z in Z & Z in rng G ) by A5, A12, A61, TARSKI:def 4;
consider j being Nat such that
A65: ( j in dom G & Z = G . j ) by A64, FINSEQ_2:11;
( i in Seg (len a) & j in Seg (len b) ) by A12, A63, A65, FINSEQ_1:def 3;
then A66: ( 1 <= i & i <= len a & 1 <= j & j <= len b ) by FINSEQ_1:3;
then consider i' being Nat such that
A67: i = 1 + i' by NAT_1:10;
(i' * (len b)) + j is Nat ;
then reconsider k = ((i - 1) * (len b)) + j as Element of NAT by A67;
consider j' being Nat such that
A68: j = 1 + j' by A66, NAT_1:10;
A69: k >= 0 + j by A67, XREAL_1:8;
then A70: k >= 1 by A66, XXREAL_0:2;
k -' 1 = k - 1 by A66, A69, XREAL_1:235, XXREAL_0:2;
then A71: k -' 1 = (i' * (len b)) + j' by A67, A68;
A72: j' < len b by A66, A68, NAT_1:13;
then A73: i = ((k -' 1) div (len b)) + 1 by A67, A71, NAT_D:def 1;
A74: j = ((k -' 1) mod (len b)) + 1 by A68, A71, A72, NAT_D:def 2;
i - 1 <= (len a) - 1 by A66, XREAL_1:11;
then (i - 1) * (len b) <= ((len a) - 1) * (len b) by XREAL_1:66;
then A75: k <= (((len a) - 1) * (len b)) + j by XREAL_1:8;
(((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b) by A66, XREAL_1:8;
then k <= (len a) * (len b) by A75, XXREAL_0:2;
then A76: k in Seg ((len a) * (len b)) by A70;
then k in dom FG by A13, FINSEQ_1:def 3;
then A77: FG . k in rng FG by FUNCT_1:def 5;
z in (F . i) /\ (G . j) by A62, A63, A64, A65, XBOOLE_0:def 4;
then z in FG . k by A14, A73, A74, A76, A15;
hence z in union (rng FG) by A77, 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 )
assume z in union (rng FG) ; :: thesis: z in dom f
then consider Y being set such that
A78: ( z in Y & Y in rng FG ) by TARSKI:def 4;
consider k being Nat such that
A79: ( k in dom FG & Y = FG . k ) by A78, FINSEQ_2:11;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A79;
then A80: z in F . (((k -' 1) div (len b)) + 1) by A78, A79, XBOOLE_0:def 4;
B81: k in Seg (len FG) by A79, FINSEQ_1:def 3;
then A81: ( 1 <= k & k <= (len a) * (len b) ) by A13, FINSEQ_1:3;
A82: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
A83: len b <> 0 by B81, A13;
then len b >= 0 + 1 by NAT_1:13;
then ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) & 1 <= len b ) by A81, NAT_D:def 3, XXREAL_0:2;
then A84: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A81, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A84, NAT_2:26;
then A85: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
((len a) * (len b)) div (len b) = len a by A83, NAT_D:18;
then ((k -' 1) div (len b)) + 1 in Seg (len a) by A82, A85;
then ((k -' 1) div (len b)) + 1 in dom F by A12, FINSEQ_1:def 3;
then F . (((k -' 1) div (len b)) + 1) in rng F by FUNCT_1:def 5;
hence z in dom f by A12, A80, TARSKI:def 4; :: thesis: verum
end;
g is real-valued by A4, MESFUNC2:def 5;
then A86: dom (f - g) = (dom f) /\ (dom g) by MESFUNC2:2;
A87: f - g is real-valued
proof
now
let x be Element of X; :: thesis: ( x in dom (f - g) implies |.((f - g) . x).| < +infty )
assume A88: x in dom (f - g) ; :: thesis: |.((f - g) . x).| < +infty
then A89: |.((f - g) . x).| = |.((f . x) - (g . x)).| by MESFUNC1:def 4;
B90: ( f is real-valued & g is real-valued ) by A1, A4, MESFUNC2:def 5;
then A90: ( |.(f . x).| < +infty & |.(g . x).| < +infty ) by A5, A86, A88, MESFUNC2:def 1;
A91: |.((f - g) . x).| <= |.(f . x).| + |.(g . x).| by A89, B90, EXTREAL2:69;
|.(f . x).| + |.(g . x).| <> +infty by A90, XXREAL_3:16;
hence |.((f - g) . x).| < +infty by A91, XXREAL_0:2, XXREAL_0:4; :: thesis: verum
end;
hence f - g is real-valued by MESFUNC2:def 1; :: thesis: verum
end;
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 A92: ( k in dom FG & x in FG . k & y in FG . k ) ; :: thesis: (f - g) . x = (f - g) . y
A93: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A92;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
B94: k in Seg (len FG) by A92, FINSEQ_1:def 3;
then A94: ( 1 <= k & k <= (len a) * (len b) ) by A13, FINSEQ_1:3;
A95: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
A96: len b <> 0 by B94, A13;
A97: len b > 0 by A94;
then len b >= 0 + 1 by NAT_1:13;
then ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) & 1 <= len b ) by A94, NAT_D:def 3, XXREAL_0:2;
then A98: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A94, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A98, NAT_2:26;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
then A99: ((k -' 1) div (len b)) + 1 <= len a by A96, NAT_D:18;
(k -' 1) mod (len b) < len b by A97, NAT_D:1;
then ((k -' 1) mod (len b)) + 1 <= len b by NAT_1:13;
then ( ((k -' 1) div (len b)) + 1 in Seg (len a) & ((k -' 1) mod (len b)) + 1 in Seg (len b) ) by A95, A99;
then A100: ( ((k -' 1) div (len b)) + 1 in dom F & ((k -' 1) mod (len b)) + 1 in dom G ) by A12, FINSEQ_1:def 3;
A101: ( x in F . (((k -' 1) div (len b)) + 1) & x in G . (((k -' 1) mod (len b)) + 1) & y in F . (((k -' 1) div (len b)) + 1) & y in G . (((k -' 1) mod (len b)) + 1) ) by A92, A93, XBOOLE_0:def 4;
then A102: ( f . x = a . (((k -' 1) div (len b)) + 1) & f . y = a . (((k -' 1) div (len b)) + 1) ) by A9, A100, MESFUNC3:def 1;
FG . k in rng FG by A92, FUNCT_1:def 5;
then A103: ( x in dom (f - g) & y in dom (f - g) ) by A5, A60, A86, A92, 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 A11, A100, A101, A102, MESFUNC3:def 1
.= (f . y) - (g . y) by A11, A100, A101, A102, MESFUNC3:def 1 ;
hence (f - g) . x = (f - g) . y by A103, MESFUNC1:def 4; :: thesis: verum
end;
hence A104: f - g is_simple_func_in S by A5, A60, A86, A87, 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) )
thus dom (f - g) <> {} by A2, A5, A86; :: thesis: ( f - g is nonnegative & integral X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,M,g) )
A105: 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 A106: x in dom (f - g) ; :: thesis: 0 <= (f - g) . x
0 <= (f . x) - (g . x) by A5, A7, A86, A106, XXREAL_3:43;
hence 0 <= (f - g) . x by A106, 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)
A107: 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 )
assume A108: k in dom FG ; :: thesis: for x being set st x in FG . k holds
f . x = a1 . k
let x be set ; :: thesis: ( x in FG . k implies f . x = a1 . k )
assume A109: x in FG . k ; :: thesis: f . x = a1 . k
A110: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A108;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
B111: k in Seg (len FG) by A108, FINSEQ_1:def 3;
then A111: ( 1 <= k & k <= (len a) * (len b) ) by A13, FINSEQ_1:3;
A112: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
A113: len b <> 0 by B111, A13;
then len b >= 0 + 1 by NAT_1:13;
then ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) & 1 <= len b ) by A111, NAT_D:def 3, XXREAL_0:2;
then A114: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A111, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:26;
then A115: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A114, XREAL_1:21;
((len a) * (len b)) div (len b) = len a by A113, NAT_D:18;
then ((k -' 1) div (len b)) + 1 in Seg (len a) by A112, A115;
then A116: ((k -' 1) div (len b)) + 1 in dom F by A12, FINSEQ_1:def 3;
A117: k in Seg (len FG) by A108, FINSEQ_1:def 3;
A118: x in F . (((k -' 1) div (len b)) + 1) by A109, A110, XBOOLE_0:def 4;
then f . x = a . (((k -' 1) div (len b)) + 1) by A9, A116, MESFUNC3:def 1;
hence f . x = a1 . k by A43, A117, A118; :: thesis: verum
end;
dom FG = dom a1 by A43, FINSEQ_1:def 3;
then FG,a1 are_Re-presentation_of f by A60, A107, MESFUNC3:def 1;
then A119: integral X,S,M,f = Sum x1 by A1, A2, A8, A45, A44, MESFUNC4:3;
A120: 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 )
assume A121: k in dom FG ; :: thesis: for x being set st x in FG . k holds
g . x = b1 . k
let x be set ; :: thesis: ( x in FG . k implies g . x = b1 . k )
assume A122: x in FG . k ; :: thesis: g . x = b1 . k
A123: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A14, A121;
set i = ((k -' 1) div (len b)) + 1;
set j = ((k -' 1) mod (len b)) + 1;
B124: k in Seg (len FG) by A121, FINSEQ_1:def 3;
A125: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
len b <> 0 by B124, A13;
then (k -' 1) mod (len b) < len b by 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 A125;
then A126: ((k -' 1) mod (len b)) + 1 in dom G by A12, FINSEQ_1:def 3;
A127: x in G . (((k -' 1) mod (len b)) + 1) by A122, A123, XBOOLE_0:def 4;
A128: k in Seg (len FG) by A121, FINSEQ_1:def 3;
thus g . x = b . (((k -' 1) mod (len b)) + 1) by A11, A126, A127, MESFUNC3:def 1
.= b1 . k by A50, A127, A128 ; :: thesis: verum
end;
dom FG = dom b1 by A50, FINSEQ_1:def 3;
then FG,b1 are_Re-presentation_of g by A5, A60, A120, MESFUNC3:def 1;
then A129: integral X,S,M,g = Sum y1 by A2, A4, A5, A10, A52, A51, MESFUNC4:3;
A130: 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 A131: 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 A132: x in FG . k ; :: thesis: (f - g) . x = c1 . k
FG . k in rng FG by A131, FUNCT_1:def 5;
then x in dom (f - g) by A5, A60, A86, A132, TARSKI:def 4;
then A133: (f - g) . x = (f . x) - (g . x) by MESFUNC1:def 4;
k in Seg (len FG) by A131, FINSEQ_1:def 3;
then (a1 . k) - (b1 . k) = c1 . k by A55, A56;
then (a1 . k) - (g . x) = c1 . k by A120, A131, A132;
hence (f - g) . x = c1 . k by A107, A131, A132, A133; :: thesis: verum
end;
dom FG = dom c1 by A54, FINSEQ_3:31;
then FG,c1 are_Re-presentation_of f - g by A5, A60, A86, A130, MESFUNC3:def 1;
then A134: integral X,S,M,(f - g) = Sum z1 by A2, A5, A58, A57, A86, A104, A105, MESFUNC4:3;
A135: 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 )
assume A136: i in dom y1 ; :: thesis: 0 <= y1 . i
then A137: y1 . i = (b1 . i) * ((M * FG) . i) by A51;
A138: i in Seg (len FG) by A51, A136, FINSEQ_1:def 3;
set i' = ((i -' 1) mod (len b)) + 1;
A140: ((i -' 1) mod (len b)) + 1 >= 0 + 1 by XREAL_1:8;
len b <> 0 by A13, A138;
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 A140;
then A141: ((i -' 1) mod (len b)) + 1 in dom G by A12, FINSEQ_1:def 3;
per cases ( G . (((i -' 1) mod (len b)) + 1) <> {} or G . (((i -' 1) mod (len b)) + 1) = {} ) ;
suppose A142: G . (((i -' 1) mod (len b)) + 1) <> {} ; :: thesis: 0 <= y1 . i
then consider x' being set such that
A143: x' in G . (((i -' 1) mod (len b)) + 1) by XBOOLE_0:def 1;
g . x' = b . (((i -' 1) mod (len b)) + 1) by A11, A141, A143, MESFUNC3:def 1
.= b1 . i by A50, A138, A142 ;
then A144: 0 <= b1 . i by A6, SUPINF_2:70;
FG . i in rng FG by A52, A136, 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 A145: M . {} <= M . FGi by MEASURE1:62;
M . {} = 0 by VALUED_0:def 19;
then 0 <= (M * FG) . i by A52, A136, A145, FUNCT_1:23;
hence 0 <= y1 . i by A137, A144; :: thesis: verum
end;
suppose A146: G . (((i -' 1) mod (len b)) + 1) = {} ; :: thesis: 0 <= y1 . i
FG . i = (F . (((i -' 1) div (len b)) + 1)) /\ (G . (((i -' 1) mod (len b)) + 1)) by A13, A14, A138, A15;
then M . (FG . i) = 0 by A146, VALUED_0:def 19;
then (M * FG) . i = 0 by A52, A136, FUNCT_1:23;
hence 0 <= y1 . i by A137; :: thesis: verum
end;
end;
end;
A147: for i being Nat st i in dom x1 holds
0 <= z1 . i
proof
let i be Nat; :: thesis: ( i in dom x1 implies 0 <= z1 . i )
assume A148: i in dom x1 ; :: thesis: 0 <= z1 . i
then A149: (M * FG) . i = M . (FG . i) by A45, FUNCT_1:23;
( FG . i in rng FG & rng FG c= S ) by A45, A148, FUNCT_1:12;
then reconsider V = FG . i as Element of S ;
reconsider EMPTY = {} as Element of S by PROB_1:42;
A150: i in Seg (len FG) by A44, A148, FINSEQ_1:def 3;
M . EMPTY <= M . V by MEASURE1:62, XBOOLE_1:2;
then A151: 0 <= (M * FG) . i by A149, VALUED_0:def 19;
per cases ( FG . i <> {} or FG . i = {} ) ;
suppose FG . i <> {} ; :: thesis: 0 <= z1 . i
then consider x being set such that
A152: x in FG . i by XBOOLE_0:def 1;
FG . i in rng FG by A45, A148, FUNCT_1:12;
then A153: x in union (rng FG) by A152, TARSKI:def 4;
then g . x <= f . x by A7, A60;
then g . x <= a1 . i by A45, A107, A148, A152;
then A154: b1 . i <= a1 . i by A45, A120, A148, A152;
reconsider x = x as Element of X by A60, A153;
0 <= (a1 . i) - (b1 . i) by A154, XXREAL_3:43;
then 0 <= c1 . i by A55, A150, A56;
then 0 <= (c1 . i) * ((M * FG) . i) by A151;
hence 0 <= z1 . i by A45, A58, A57, A148; :: thesis: verum
end;
suppose FG . i = {} ; :: thesis: 0 <= z1 . i
then (M * FG) . i = 0 by A149, VALUED_0:def 19;
then (c1 . i) * ((M * FG) . i) = 0 ;
hence 0 <= z1 . i by A45, A58, A57, A148; :: thesis: verum
end;
end;
end;
x1 = z1 + y1
proof
not -infty in rng y1
proof
assume -infty in rng y1 ; :: thesis: contradiction
then consider i being set such that
A156: i in dom y1 and
A157: y1 . i = -infty by FUNCT_1:def 5;
thus contradiction by A135, A156, A157; :: thesis: verum
end;
then A158: (z1 " {+infty }) /\ (y1 " {-infty }) = (z1 " {+infty }) /\ {} by FUNCT_1:142
.= {} ;
not -infty in rng z1
proof
assume -infty in rng z1 ; :: thesis: contradiction
then consider i being set such that
A159: i in dom z1 and
A160: z1 . i = -infty by FUNCT_1:def 5;
thus contradiction by A45, A58, A147, A159, A160; :: thesis: verum
end;
then (z1 " {-infty }) /\ (y1 " {+infty }) = {} /\ (y1 " {+infty }) by FUNCT_1:142
.= {} ;
then A161: dom (z1 + y1) = ((dom z1) /\ (dom y1)) \ ({} \/ {} ) by A158, MESFUNC1:def 3
.= dom x1 by A44, A52, A58, FINSEQ_3:31 ;
A162: for k being Nat st k in dom x1 holds
x1 . k = (z1 + y1) . k
proof
let k be Nat; :: thesis: ( k in dom x1 implies x1 . k = (z1 + y1) . k )
assume A163: k in dom x1 ; :: thesis: x1 . k = (z1 + y1) . k
then A164: k in Seg (len FG) by A44, FINSEQ_1:def 3;
set p = ((k -' 1) div (len b)) + 1;
set q = ((k -' 1) mod (len b)) + 1;
A165: ( 1 <= k & k <= (len a) * (len b) ) by A13, A164, FINSEQ_1:3;
A166: ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 >= 0 + 1 ) by XREAL_1:8;
A167: len b <> 0 by A13, A164;
A168: len b > 0 by A165;
then len b >= 0 + 1 by NAT_1:13;
then ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) & 1 <= len b ) by A165, NAT_D:def 3, XXREAL_0:2;
then A169: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by NAT_2:17;
k -' 1 <= ((len a) * (len b)) -' 1 by A165, NAT_D:42;
then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A169, NAT_2:26;
then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:21;
then ((k -' 1) div (len b)) + 1 <= len a by A167, NAT_D:18;
then A170: ((k -' 1) div (len b)) + 1 in Seg (len a) by A166;
(k -' 1) mod (len b) < len b by A168, 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 A166;
then A171: ( ((k -' 1) div (len b)) + 1 in dom F & ((k -' 1) mod (len b)) + 1 in dom G ) by A12, A170, FINSEQ_1:def 3;
A172: ((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 A13, A14, A164, A15;
then consider v being set such that
A173: v in (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by XBOOLE_0:def 1;
A174: ( v in F . (((k -' 1) div (len b)) + 1) & v in G . (((k -' 1) mod (len b)) + 1) ) by A173, XBOOLE_0:def 4;
then A175: ( a . (((k -' 1) div (len b)) + 1) = f . v & b . (((k -' 1) mod (len b)) + 1) = g . v ) by A9, A11, A171, MESFUNC3:def 1;
A176: ( F . (((k -' 1) div (len b)) + 1) <> {} & G . (((k -' 1) mod (len b)) + 1) <> {} ) by A173;
( F . (((k -' 1) div (len b)) + 1) in rng F & G . (((k -' 1) mod (len b)) + 1) in rng G ) by A171, FUNCT_1:12;
then A177: ( v in dom f & v in dom g ) by A12, A174, TARSKI:def 4;
0 <= b . (((k -' 1) mod (len b)) + 1) by A6, A175, SUPINF_2:70;
then A178: ( 0 = b1 . k or 0 < b1 . k ) by A50, A164, A173;
reconsider v = v as Element of X by A177;
b . (((k -' 1) mod (len b)) + 1) <= a . (((k -' 1) div (len b)) + 1) by A7, A175, A177;
then b1 . k <= a . (((k -' 1) div (len b)) + 1) by A50, A164, A176;
then b1 . k <= a1 . k by A43, A164, A176;
then 0 <= (a1 . k) - (b1 . k) by XXREAL_3:43;
then ( 0 = c1 . k or 0 < c1 . k ) by A55, A164, A56;
hence ((c1 . k) + (b1 . k)) * ((M * FG) . k) = ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A178, 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 X: (M * FG) . k = 0 by A45, A163, FUNCT_1:23;
hence ((c1 . k) + (b1 . k)) * ((M * FG) . k) = 0
.= ((c1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by X ;
:: thesis: verum
end;
end;
end;
A180: ( 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 A181: F . (((k -' 1) div (len b)) + 1) <> {} ; :: thesis: ( a1 . k <> +infty & -infty <> a1 . k )
then consider v being set such that
A182: v in F . (((k -' 1) div (len b)) + 1) by XBOOLE_0:def 1;
a1 . k = a . (((k -' 1) div (len b)) + 1) by A43, A164, A181;
then A183: a1 . k = f . v by A9, A171, A182, MESFUNC3:def 1;
F . (((k -' 1) div (len b)) + 1) in rng F by A171, FUNCT_1:12;
then A184: v in dom f by A12, A182, TARSKI:def 4;
then reconsider v = v as Element of X ;
f is real-valued by A1, MESFUNC2:def 5;
then |.(f . v).| < +infty by A184, MESFUNC2:def 1;
then ( - +infty < a1 . k & a1 . k < +infty ) by A183, EXTREAL2:58;
hence ( a1 . k <> +infty & -infty <> a1 . k ) by XXREAL_3:def 3; :: 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 A43, A164; :: 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 A185: G . (((k -' 1) mod (len b)) + 1) <> {} ; :: thesis: ( b1 . k <> +infty & b1 . k <> -infty )
then consider v being set such that
A186: v in G . (((k -' 1) mod (len b)) + 1) by XBOOLE_0:def 1;
b1 . k = b . (((k -' 1) mod (len b)) + 1) by A50, A164, A185;
then A187: b1 . k = g . v by A11, A171, A186, MESFUNC3:def 1;
G . (((k -' 1) mod (len b)) + 1) in rng G by A171, FUNCT_1:12;
then A188: v in dom g by A12, A186, TARSKI:def 4;
then reconsider v = v as Element of X ;
g is real-valued by A4, MESFUNC2:def 5;
then |.(g . v).| < +infty by A188, MESFUNC2:def 1;
then ( - +infty < b1 . k & b1 . k < +infty ) by A187, EXTREAL2:58;
hence ( b1 . k <> +infty & b1 . k <> -infty ) by XXREAL_3:def 3; :: 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 A50, A164; :: thesis: verum
end;
end;
end;
hence ( b1 . k <> +infty & b1 . k <> -infty ) ; :: thesis: verum
end;
X: (b1 . k) - (b1 . k) = - 0 by XXREAL_3:7;
c1 . k = (a1 . k) - (b1 . k) by A55, A164, A56;
then (c1 . k) + (b1 . k) = (a1 . k) - ((b1 . k) - (b1 . k)) by A180, XXREAL_3:33
.= (a1 . k) + (- 0 ) by X
.= a1 . k by XXREAL_3:4 ;
hence x1 . k = ((c1 . k) + (b1 . k)) * ((M * FG) . k) by A44, A163
.= (z1 . k) + ((b1 . k) * ((M * FG) . k)) by A45, A58, A57, A163, A172
.= (z1 . k) + (y1 . k) by A45, A52, A51, A163
.= (z1 + y1) . k by A161, A163, MESFUNC1:def 3 ;
:: thesis: verum
end;
dom (z1 + y1) = Seg (len x1) by A161, FINSEQ_1:def 3;
then z1 + y1 is FinSequence by FINSEQ_1:def 2;
hence x1 = z1 + y1 by A161, A162, FINSEQ_1:17; :: thesis: verum
end;
hence integral X,S,M,f = (integral X,S,M,(f - g)) + (integral X,S,M,g) by A45, A52, A58, A119, A129, A134, A135, A147, MESFUNC4:1; :: thesis: verum