:: Linearity of {L}ebesgue Integral of Simple Valued Function
:: by Noboru Endou and Yasunari Shidama
::
:: Received September 14, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, NAT_1, RELAT_1, SUPINF_2, XXREAL_0, FUNCT_1,
ARYTM_3, CARD_3, SUBSET_1, XBOOLE_0, CARD_1, PROB_1, MEASURE1, PARTFUN1,
MESFUNC2, MESFUNC3, INTEGRA1, VALUED_0, TARSKI, COMPLEX1, MESFUNC1,
ORDINAL4, ARYTM_1, INT_1, SUPINF_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, XXREAL_3, EXTREAL1, XCMPLX_0,
XREAL_0, NAT_1, NAT_D, PROB_1, SUPINF_1, SUPINF_2, MEASURE1, MESFUNC1,
MESFUNC2, MESFUNC3;
constructors PARTFUN1, REAL_1, NAT_1, NAT_D, FINSEQOP, EXTREAL1, MESFUNC1,
BINARITH, MESFUNC2, MESFUNC3, SUPINF_1, RELSET_1, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
MEASURE1, VALUED_0, MEMBERED, CARD_1, XXREAL_3;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, SUPINF_2;
expansions TARSKI, XBOOLE_0;
theorems MEASURE1, TARSKI, FUNCT_1, NAT_1, MESFUNC1, ZFMISC_1, FINSEQ_1,
FINSEQ_2, FINSEQ_5, PROB_2, XBOOLE_0, XBOOLE_1, RELAT_1, MESFUNC2,
EXTREAL1, MESFUNC3, XREAL_1, NAT_2, FINSEQ_3, XXREAL_0, PROB_1, FINSUB_1,
ORDINAL1, NAT_D, VALUED_0, XXREAL_3, NUMBERS, SUPINF_2;
schemes FINSEQ_1, FINSEQ_2, NAT_1;
begin :: Linearity of Lebesgue Integral of Simple Valued Function
theorem Th1:
for F,G,H be FinSequence of ExtREAL st F is nonnegative &
G is nonnegative &
dom F = dom
G & H = F + G holds Sum(H)=Sum(F)+Sum(G)
proof
let F,G,H be FinSequence of ExtREAL;
assume that
A1: F is nonnegative and
A2: G is nonnegative and
A3: dom F = dom G and
A4: H = F + G;
for y be object st y in rng F holds not y in {-infty}
proof
let y be object;
assume y in rng F;
then consider x be object such that
A5: x in dom F and
A6: y = F.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A5;
0. <= F.x by A1,SUPINF_2:39;
hence thesis by A6,TARSKI:def 1;
end;
then rng F misses {-infty} by XBOOLE_0:3;
then
A7: F"{-infty} = {} by RELAT_1:138;
for y be object st y in rng G holds not y in {-infty}
proof
let y be object;
assume y in rng G;
then consider x be object such that
A8: x in dom G and
A9: y = G.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A8;
0. <= G.x by A2,SUPINF_2:39;
hence thesis by A9,TARSKI:def 1;
end;
then rng G misses {-infty} by XBOOLE_0:3;
then
A10: G"{-infty} = {} by RELAT_1:138;
A11: dom H = (dom F /\ dom G)\((F"{-infty}/\G"{+infty})\/(F"{+infty}/\G"{
-infty})) by A4,MESFUNC1:def 3
.= dom F by A3,A7,A10;
then
A12: len H = len F by FINSEQ_3:29;
consider h be sequence of ExtREAL such that
A13: Sum(H) = h.(len H) and
A14: h.0 = 0. and
A15: for i be Nat st i < len H holds h.(i+1) = h.i + H.(i+1)
by EXTREAL1:def 2;
consider f be sequence of ExtREAL such that
A16: Sum(F) = f.(len F) and
A17: f.0 = 0. and
A18: for i be Nat st i < len F holds f.(i+1) = f.i + F.(i+1)
by EXTREAL1:def 2;
consider g be sequence of ExtREAL such that
A19: Sum(G) = g.(len G) and
A20: g.0 = 0. and
A21: for i be Nat st i < len G holds g.(i+1) = g.i + G.(i+1)
by EXTREAL1:def 2;
defpred P[Nat] means $1 <= len H implies h.$1 = f.$1 + g.$1;
A22: len H = len G by A3,A11,FINSEQ_3:29;
A23: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A24: P[k];
assume
A25: k+1 <= len H;
reconsider k as Element of NAT by ORDINAL1:def 12;
A26: k < len H by A25,NAT_1:13;
then
A27: f.(k+1) = f.k + F.(k+1) & g.(k+1) = g.k + G.(k+1) by A18,A21,A12,A22;
1 <= k+1 by NAT_1:11;
then
A28: k+1 in dom H by A25,FINSEQ_3:25;
A29: f.k <> -infty & g.k <> -infty & F.(k+1) <> -infty & G.(k+1) <> -infty
proof
defpred Pg[Nat] means $1 <= len H implies g.$1 <> -infty;
defpred Pf[Nat] means $1 <= len H implies f.$1 <> -infty;
A30: for m be Nat st Pf[m] holds Pf[m+1]
proof
let m be Nat;
assume
A31: Pf[m];
assume
A32: m+1 <= len H;
reconsider m as Element of NAT by ORDINAL1:def 12;
A33: 0. <= F.(m+1) by A1,SUPINF_2:39;
m < len H by A32,NAT_1:13;
then f.(m+1) = f.m + F.(m+1) by A18,A12;
hence thesis by A31,A32,A33,NAT_1:13,XXREAL_3:17;
end;
A34: Pf[0] by A17;
for i be Nat holds Pf[i] from NAT_1:sch 2(A34,A30);
hence f.k <> -infty by A26;
A35: for m be Nat st Pg[m] holds Pg[m+1]
proof
let m be Nat;
assume
A36: Pg[m];
assume
A37: m+1 <= len H;
reconsider m as Element of NAT by ORDINAL1:def 12;
A38: 0. <= G.(m+1) by A2,SUPINF_2:39;
m < len H by A37,NAT_1:13;
then g.(m+1) = g.m + G.(m+1) by A21,A22;
hence thesis by A36,A37,A38,NAT_1:13,XXREAL_3:17;
end;
A39: Pg[0] by A20;
for i be Nat holds Pg[i] from NAT_1:sch 2(A39,A35);
hence g.k <> -infty by A26;
thus F.(k+1) <> -infty by A1,SUPINF_2:51;
thus thesis by A2,SUPINF_2:51;
end;
then
A40: f.k + F.(k+1) <> -infty by XXREAL_3:17;
A41: h.(k+1) = (f.k + g.k) + H.(k+1) by A15,A24,A26
.= (f.k + g.k) + (F.(k+1) + G.(k+1)) by A4,A28,MESFUNC1:def 3;
f.k + g.k <> -infty by A29,XXREAL_3:17;
then h.(k+1) = ((f.k + g.k) + F.(k+1)) + G.(k+1) by A41,A29,XXREAL_3:29
.= (f.k + F.(k+1) + g.k) + G.(k+1) by A29,XXREAL_3:29
.= f.(k+1) + g.(k+1) by A27,A29,A40,XXREAL_3:29;
hence thesis;
end;
A42: P[0] by A17,A20,A14;
for i be Nat holds P[i] from NAT_1:sch 2(A42,A23);
hence thesis by A16,A19,A13,A12,A22;
end;
theorem Th2:
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S holds for n be Nat, f be PartFunc of X,ExtREAL, F be Finite_Sep_Sequence
of S, a,x be FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} &
f is nonnegative &
F,a are_Re-presentation_of f &
dom x = dom F & (for i be Nat st i in dom x holds x.i=a.i*(M*F).i) & len F = n
holds integral(M,f)=Sum(x)
proof
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
defpred P[Nat] means for f be PartFunc of X,ExtREAL, F be
Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL st f is_simple_func_in
S & dom f <> {} & f is nonnegative &
F,a
are_Re-presentation_of f & dom x = dom F & (for i be Nat st i in dom x holds x.
i=a.i*(M*F).i) & len F = $1 holds integral(M,f)=Sum(x);
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
let f be PartFunc of X,ExtREAL, F be Finite_Sep_Sequence of S, a,x be
FinSequence of ExtREAL such that
A3: f is_simple_func_in S and
A4: dom f <> {} and
A5: f is nonnegative and
A6: F,a are_Re-presentation_of f and
A7: dom x = dom F and
A8: for i be Nat st i in dom x holds x.i=a.i*(M*F).i and
A9: len F = n+1;
A10: f is real-valued by A3,MESFUNC2:def 4;
a5: for x be object st x in dom f holds 0. <= f.x
by A5,SUPINF_2:51;
reconsider n as Element of NAT by ORDINAL1:def 12;
set F1=F|(Seg n);
set f1=f|(union rng F1);
reconsider F1 as Finite_Sep_Sequence of S by MESFUNC2:33;
A11: dom f1 = (dom f) /\ (union rng F1) by RELAT_1:61
.= (union rng F) /\ (union rng F1) by A6,MESFUNC3:def 1;
for x be object st x in dom f1 holds 0. <= f1.x
proof
let x be object;
assume x in dom f1;
then
X: dom f1 c= dom f & f1.x = f.x by FUNCT_1:47,RELAT_1:60;
0. <= f.x by A5,SUPINF_2:51;
hence thesis by X;
end; then
a12: f1 is nonnegative by SUPINF_2:52;
set a1=a|(Seg n);
reconsider a1 as FinSequence of ExtREAL by FINSEQ_1:18;
set x1=x|(Seg n);
reconsider x1 as FinSequence of ExtREAL by FINSEQ_1:18;
A14: dom x1 = dom F /\ Seg n by A7,RELAT_1:61
.= dom F1 by RELAT_1:61;
A15: union rng F1 c= union rng F by RELAT_1:70,ZFMISC_1:77;
then
A16: dom f1 = union rng F1 by A11,XBOOLE_1:28;
ex F19 be Finite_Sep_Sequence of S st (dom f1 = union rng F19 & for n
be Nat, x,y be Element of X st n in dom F19 & x in F19.n & y in F19.n holds f1.
x = f1.y)
proof
take F1;
for n be Nat, x,y be Element of X st n in dom F1 & x in F1.n & y in
F1.n holds f1.x = f1.y
proof
let n be Nat;
let x,y be Element of X;
assume that
A17: n in dom F1 and
A18: x in F1.n and
A19: y in F1.n;
F1.n c= dom f1 by A16,A17,FUNCT_1:3,ZFMISC_1:74;
then
A20: f1.x = f.x & f1.y = f.y by A18,A19,FUNCT_1:47;
A21: dom F1 c= dom F by RELAT_1:60;
A22: F1.n = F.n by A17,FUNCT_1:47;
then f.x = a.n by A6,A17,A18,A21,MESFUNC3:def 1;
hence thesis by A6,A17,A19,A20,A22,A21,MESFUNC3:def 1;
end;
hence thesis by A11,A15,XBOOLE_1:28;
end;
then
A23: f1 is_simple_func_in S by A10,MESFUNC2:def 4;
A24: dom F1 = dom F /\ Seg n by RELAT_1:61
.= dom a /\ Seg n by A6,MESFUNC3:def 1
.= dom a1 by RELAT_1:61;
for n be Nat st n in dom F1 for x be object st x in F1.n holds f1.x = a1 .n
proof
let n be Nat;
assume
A25: n in dom F1;
then
A26: F1.n = F.n & a1.n = a.n by A24,FUNCT_1:47;
let x be object;
assume
A27: x in F1.n;
F1.n c= dom f1 by A16,A25,FUNCT_1:3,ZFMISC_1:74;
then dom F1 c= dom F & f1.x = f.x by A27,FUNCT_1:47,RELAT_1:60;
hence thesis by A6,A25,A26,A27,MESFUNC3:def 1;
end;
then
A28: F1,a1 are_Re-presentation_of f1 by A16,A24,MESFUNC3:def 1;
now
per cases;
suppose
A29: dom f1 = {};
1 <= n+1 by NAT_1:11;
then
A30: n+1 in dom F by A9,FINSEQ_3:25;
A31: union rng F = (union rng F1) \/ F.(n+1)
proof
thus union rng F c= (union rng F1) \/ F.(n+1)
proof
let v be object;
assume v in union rng F;
then consider A be set such that
A32: v in A and
A33: A in rng F by TARSKI:def 4;
consider i be object such that
A34: i in dom F and
A35: A = F.i by A33,FUNCT_1:def 3;
reconsider i as Element of NAT by A34;
A36: i in Seg len F by A34,FINSEQ_1:def 3;
then
A37: 1 <= i by FINSEQ_1:1;
A38: i <= n+1 by A9,A36,FINSEQ_1:1;
per cases;
suppose
i = n+1;
hence thesis by A32,A35,XBOOLE_0:def 3;
end;
suppose
i <> n+1;
then i < n+1 by A38,XXREAL_0:1;
then i <= n by NAT_1:13;
then i in Seg n by A37,FINSEQ_1:1;
then i in dom F /\ Seg n by A34,XBOOLE_0:def 4;
then i in dom F1 by RELAT_1:61;
then F1.i = A & F1.i in rng F1 by A35,FUNCT_1:3,47;
then v in union rng F1 by A32,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
let v be object;
assume
A39: v in (union rng F1) \/ F.(n+1);
per cases by A39,XBOOLE_0:def 3;
suppose
v in union rng F1;
then consider A be set such that
A40: v in A and
A41: A in rng F1 by TARSKI:def 4;
consider i be object such that
A42: i in dom F1 and
A43: A = F1.i by A41,FUNCT_1:def 3;
i in dom F /\ Seg n by A42,RELAT_1:61;
then
A44: i in dom F by XBOOLE_0:def 4;
F.i = A by A42,A43,FUNCT_1:47;
then A in rng F by A44,FUNCT_1:3;
hence thesis by A40,TARSKI:def 4;
end;
suppose
A45: v in F.(n+1);
F.(n+1) in rng F by A30,FUNCT_1:3;
hence thesis by A45,TARSKI:def 4;
end;
end;
A46: Seg len x = dom F by A7,FINSEQ_1:def 3
.= Seg(n+1) by A9,FINSEQ_1:def 3;
then
A47: len x = n+1 by FINSEQ_1:6;
then
A48: n < len x by NAT_1:13;
consider sumx be sequence of ExtREAL such that
A49: Sum x = sumx.(len x) and
A50: sumx.0 = 0. and
A51: for m be Nat st m < len x holds sumx.(m+1) = sumx.
m + x. (m+1) by EXTREAL1:def 2;
defpred PSumx[Nat] means $1 < len x implies sumx.$1 = 0.;
A52: for m be Nat st m in dom F1 holds F1.m = {}
proof
let m be Nat;
assume m in dom F1;
then F1.m in rng F1 by FUNCT_1:3;
hence thesis by A16,A29,XBOOLE_1:3,ZFMISC_1:74;
end;
A53: for m be Nat st m in dom F1 holds x.m = 0.
proof
reconsider EMPTY = {} as Element of S by PROB_1:4;
let m be Nat;
assume
A54: m in dom F1;
then F1.m = {} by A52;
then
A55: F.m = {} by A54,FUNCT_1:47;
m in dom F /\ (Seg n) by A54,RELAT_1:61;
then
A56: m in dom x by A7,XBOOLE_0:def 4;
then
A57: x.m = a.m*(M*F).m by A8;
M.EMPTY = 0. by VALUED_0:def 19;
then (M*F).m = 0. by A7,A56,A55,FUNCT_1:13;
hence thesis by A57;
end;
A58: for m be Nat st PSumx[m] holds PSumx[m+1]
proof
let m be Nat;
assume
A59: PSumx[m];
A60: 1 <= m+1 by NAT_1:11;
assume
A61: m+1 < len x;
then m+1 <= n by A47,NAT_1:13;
then
A62: m+1 in Seg n by A60,FINSEQ_1:1;
m+1 in Seg len x by A61,A60,FINSEQ_1:1;
then m+1 in dom F by A7,FINSEQ_1:def 3;
then m+1 in dom F /\ Seg n by A62,XBOOLE_0:def 4;
then
A63: m+1 in dom F1 by RELAT_1:61;
m <= m+1 by NAT_1:11;
then m < len x by A61,XXREAL_0:2;
then sumx.(m+1) = 0. + x.(m+1) by A51,A59
.= x.(m+1) by XXREAL_3:4;
hence thesis by A53,A63;
end;
A64: PSumx[0] by A50;
A65: for m be Nat holds PSumx[m] from NAT_1:sch 2(A64,A58);
A66: Sum x = sumx.(n+1) by A49,A46,FINSEQ_1:6
.= sumx.n + x.(n+1) by A51,A48
.= 0. + x.(n+1) by A65,A48
.= x.(n+1) by XXREAL_3:4;
now
per cases;
case
A67: a.(n+1) <> 0.;
defpred Pb[Nat,set] means ($1 = 1 implies $2 = 0.) & ($1 = 2
implies $2 = a.(n+1));
defpred PG[Nat,set] means ($1 = 1 implies $2 = union rng F1) & ($1
= 2 implies $2 = F.(n+1));
A68: for k be Nat st k in Seg 2 ex x being Element of ExtREAL st Pb[k,x]
proof
let k be Nat;
assume
A69: k in Seg 2;
per cases by A69,FINSEQ_1:2,TARSKI:def 2;
suppose
A70: k = 1;
set x = 0.;
reconsider x as Element of ExtREAL;
take x;
thus thesis by A70;
end;
suppose
A71: k = 2;
set x = a.(n+1);
reconsider x as Element of ExtREAL;
take x;
thus thesis by A71;
end;
end;
consider b be FinSequence of ExtREAL such that
A72: dom b = Seg 2 & for k be Nat st k in Seg 2 holds Pb[k,b.
k] from FINSEQ_1:sch 5(A68);
A73: for k be Nat st k in Seg 2 ex x being Element of S st PG[k,x ]
proof
let k be Nat;
assume
A74: k in Seg 2;
per cases by A74,FINSEQ_1:2,TARSKI:def 2;
suppose
A75: k = 1;
set x = union rng F1;
reconsider x as Element of S by MESFUNC2:31;
take x;
thus thesis by A75;
end;
suppose
A76: k = 2;
set x = F.(n+1);
F.(n+1) in rng F & rng F c= S by A30,FINSEQ_1:def 4,FUNCT_1:3;
then reconsider x as Element of S;
take x;
thus thesis by A76;
end;
end;
consider G be FinSequence of S such that
A77: dom G = Seg 2 & for k be Nat st k in Seg 2 holds PG[k,G.
k] from FINSEQ_1:sch 5(A73);
A78: 1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A79: b.1 = 0. by A72;
A80: b.1 = 0. by A72,A78;
2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A81: b.2 = a.(n+1) by A72;
A82: 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A83: G.2 = F.(n+1) by A77;
A84: 1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A85: G.1 = union rng F1 by A77;
A86: for u,v be object st u <> v holds G.u misses G.v
proof
let u,v be object;
assume
A87: u <> v;
per cases;
suppose
A88: u in dom G & v in dom G;
then
A89: u = 1 or u = 2 by A77,FINSEQ_1:2,TARSKI:def 2;
per cases by A77,A87,A88,A89,FINSEQ_1:2,TARSKI:def 2;
suppose
A90: u = 1 & v = 2;
assume G.u meets G.v;
then consider z be object such that
A91: z in G.u and
A92: z in G.v by XBOOLE_0:3;
consider A be set such that
A93: z in A and
A94: A in rng F1 by A85,A90,A91,TARSKI:def 4;
consider k9 be object such that
A95: k9 in dom F1 and
A96: A = F1.k9 by A94,FUNCT_1:def 3;
reconsider k9 as Element of NAT by A95;
A97: z in F.k9 by A93,A95,A96,FUNCT_1:47;
k9 in dom F /\ Seg n by A95,RELAT_1:61;
then k9 in Seg n by XBOOLE_0:def 4;
then k9 <= n by FINSEQ_1:1;
then k9 < n+1 by NAT_1:13;
then
A98: F.k9 misses F.(n+1) by PROB_2:def 2;
z in F.(n+1) by A77,A82,A90,A92;
hence contradiction by A98,A97,XBOOLE_0:3;
end;
suppose
A99: u = 2 & v = 1;
assume G.u meets G.v;
then consider z be object such that
A100: z in G.u and
A101: z in G.v by XBOOLE_0:3;
consider A be set such that
A102: z in A and
A103: A in rng F1 by A85,A99,A101,TARSKI:def 4;
consider k9 be object such that
A104: k9 in dom F1 and
A105: A = F1.k9 by A103,FUNCT_1:def 3;
reconsider k9 as Element of NAT by A104;
A106: z in F.k9 by A102,A104,A105,FUNCT_1:47;
k9 in dom F /\ Seg n by A104,RELAT_1:61;
then k9 in Seg n by XBOOLE_0:def 4;
then k9 <= n by FINSEQ_1:1;
then k9 < n+1 by NAT_1:13;
then
A107: F.k9 misses F.(n+1) by PROB_2:def 2;
z in F.(n+1) by A77,A82,A99,A100;
hence contradiction by A107,A106,XBOOLE_0:3;
end;
end;
suppose
not u in dom G or not v in dom G;
then G.u = {} or G.v = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
len G = 2 by A77,FINSEQ_1:def 3;
then
A108: G = <* union rng F1, F.(n+1) *> by A85,A83,FINSEQ_1:44;
deffunc Fy(Nat) = b.$1*(M*G).$1;
consider y be FinSequence of ExtREAL such that
A109: len y = 2 & for m be Nat st m in dom y holds y.m = Fy(m)
from FINSEQ_2:sch 1;
A110: dom y = Seg 2 by A109,FINSEQ_1:def 3;
1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A111: y.1 = b.1*(M*G).1 by A109,A110;
consider sumy be sequence of ExtREAL such that
A112: Sum y = sumy.len y and
A113: sumy.0 = 0. and
A114: for k be Nat st k < len y holds sumy.(k+1) =
sumy.k + y .(k+1) by EXTREAL1:def 2;
A115: sumy.1 = sumy.0 + y.(0+1) by A109,A114
.= 0. by A79,A111,A113;
A116: 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then (M*G).2 = M.(F.(n+1)) by A77,A83,FUNCT_1:13
.= (M*F).(n+1) by A30,FUNCT_1:13;
then y.2 = a.(n+1)*(M*F).(n+1) by A81,A109,A110,A116;
then
A117: y.2 = x.(n+1) by A7,A8,A30;
reconsider G as Finite_Sep_Sequence of S by A86,PROB_2:def 2;
A118: dom y = dom G by A77,A109,FINSEQ_1:def 3;
A119: for k be Nat st k in dom G for v be object st v in G.k holds f.
v = b.k
proof
let k be Nat;
assume
A120: k in dom G;
let v be object;
assume
A121: v in G.k;
per cases by A77,A120,FINSEQ_1:2,TARSKI:def 2;
suppose
k = 1;
hence thesis by A16,A29,A77,A84,A121;
end;
suppose
k = 2;
hence thesis by A6,A30,A83,A81,A121,MESFUNC3:def 1;
end;
end;
A122: for k be Nat st 2 <= k & k in dom b holds 0. < b.k & b.k < +infty
proof
let k be Nat;
assume that
A123: 2 <= k and
A124: k in dom b;
A125: k = 1 or k = 2 by A72,A124,FINSEQ_1:2,TARSKI:def 2;
then G.k <> {} by A4,A6,A11,A29,A31,A83,A123,MESFUNC3:def 1;
then consider v be object such that
A126: v in G.k by XBOOLE_0:def 1;
A127: v in dom f by A6,A16,A29,A31,A83,A123,A125,A126,MESFUNC3:def 1;
A128: f.v = b.k by A77,A72,A119,A124,A126;
hence 0. < b.k by A67,A81,A123,A125,A127,a5;
dom f c= X by RELAT_1:def 18;
then reconsider v as Element of X by A127;
|. f.v .| < +infty by A10,A127,MESFUNC2:def 1;
hence thesis by A128,EXTREAL1:21;
end;
dom f = (union rng F1) \/ F.(n+1) by A6,A31,MESFUNC3:def 1
.= union {union rng F1,F.(n+1)} by ZFMISC_1:75
.= union rng G by A108,FINSEQ_2:127;
then
A129: G,b are_Re-presentation_of f by A77,A72,A119,MESFUNC3:def 1;
Sum y = sumy.(1+1) by A109,A112
.= 0. + x.(n+1) by A109,A117,A114,A115
.= x.(n+1) by XXREAL_3:4;
hence thesis by A3,A5,A66,A109,A122,A129,A80,A118,MESFUNC3:def 2;
end;
case
A130: a.(n+1) = 0.;
defpred Pb[Nat,set] means ($1 = 1 implies $2 = 0.) & ($1 = 2
implies $2 = 1.);
defpred PG[Nat,set] means ($1 = 1 implies $2 = union rng F) & ($1
= 2 implies $2 = {});
A131: for k be Nat st k in Seg 2 ex v being Element of S st PG[k,v ]
proof
let k be Nat;
assume
A132: k in Seg 2;
per cases by A132,FINSEQ_1:2,TARSKI:def 2;
suppose
A133: k = 1;
set v = union rng F;
reconsider v as Element of S by MESFUNC2:31;
take v;
thus thesis by A133;
end;
suppose
A134: k = 2;
reconsider v = {} as Element of S by PROB_1:4;
take v;
thus thesis by A134;
end;
end;
consider G be FinSequence of S such that
A135: dom G = Seg 2 & for k be Nat st k in Seg 2 holds PG[k,G.
k] from FINSEQ_1:sch 5(A131);
A136: for u,v be object st u <> v holds G.u misses G.v
proof
let u,v be object;
assume
A137: u <> v;
per cases;
suppose
A138: u in dom G & v in dom G;
then
A139: u = 1 or u = 2 by A135,FINSEQ_1:2,TARSKI:def 2;
per cases by A135,A137,A138,A139,FINSEQ_1:2,TARSKI:def 2;
suppose
u = 1 & v = 2;
then G.v = {} by A135,A138;
hence thesis;
end;
suppose
u = 2 & v = 1;
then G.u = {} by A135,A138;
hence thesis;
end;
end;
suppose
not u in dom G or not v in dom G;
then G.u = {} or G.v = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
A140: for k be Nat st k in Seg 2 ex v be Element of ExtREAL st Pb[ k,v]
proof
let k be Nat;
assume
A141: k in Seg 2;
per cases by A141,FINSEQ_1:2,TARSKI:def 2;
suppose
A142: k = 1;
set v = 0.;
reconsider v as Element of ExtREAL;
take v;
thus thesis by A142;
end;
suppose
A143: k = 2;
set v = 1.;
reconsider v as Element of ExtREAL;
take v;
thus thesis by A143;
end;
end;
consider b be FinSequence of ExtREAL such that
A144: dom b = Seg 2 & for k be Nat st k in Seg 2 holds Pb[k,b.
k] from FINSEQ_1:sch 5(A140);
A145: 2 in dom G by A135,FINSEQ_1:2,TARSKI:def 2;
then
A146: G.2 = {} by A135;
M.(G.2) = (M*G).2 by A145,FUNCT_1:13;
then
A147: (M*G).2 = 0. by A146,VALUED_0:def 19;
1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A148: G.1 = union rng F by A135;
A149: 1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A150: b.1 = 0. by A144;
deffunc Fy(Nat) = b.$1*(M*G).$1;
consider y be FinSequence of ExtREAL such that
A151: len y = 2 & for k be Nat st k in dom y holds y.k = Fy(k)
from FINSEQ_2:sch 1;
A152: dom y = Seg 2 by A151,FINSEQ_1:def 3;
2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A153: y.2 = b.2*(M*G).2 by A151,A152;
1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then
A154: y.1 = b.1*(M*G).1 by A151,A152;
reconsider G as Finite_Sep_Sequence of S by A136,PROB_2:def 2;
A155: dom y = dom G by A135,A151,FINSEQ_1:def 3;
A156: for k be Nat st k in dom G
for v be object st v in G.k holds f. v=b.k
proof
let k be Nat;
assume
A157: k in dom G;
let v be object;
assume
A158: v in G.k;
per cases by A135,A157,FINSEQ_1:2,TARSKI:def 2;
suppose
A159: k = 1;
then f.v = 0. by A6,A16,A29,A30,A31,A130,A148,A158,
MESFUNC3:def 1;
hence thesis by A144,A149,A159;
end;
suppose
k = 2;
hence thesis by A135,A145,A158;
end;
end;
len G = 2 by A135,FINSEQ_1:def 3;
then G = <* union rng F, {} *> by A148,A146,FINSEQ_1:44;
then rng G = {union rng F, {}} by FINSEQ_2:127;
then union rng G = union rng F \/ {} by ZFMISC_1:75
.= dom f by A6,MESFUNC3:def 1;
then
A160: G,b are_Re-presentation_of f by A135,A144,A156,MESFUNC3:def 1;
consider sumy be sequence of ExtREAL such that
A161: Sum(y) = sumy.len y and
A162: sumy.0 = 0. and
A163: for k be Nat st k < len y holds sumy.(k+1) =
sumy.k + y .(k+1) by EXTREAL1:def 2;
A164: sumy.1 = sumy.0 + y.(0+1) by A151,A163
.= 0. by A150,A154,A162;
A165: 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
A166: for k be Nat st 2 <= k & k in dom b holds 0. < b.k & b.k < +infty
proof
let k be Nat;
assume that
A167: 2 <= k and
A168: k in dom b;
k = 1 or k = 2 by A144,A168,FINSEQ_1:2,TARSKI:def 2;
hence 0. < b.k by A144,A165,A167;
A169: 1 in REAL by NUMBERS:19;
Pb[k,b.k] by A144,A149,A165;
then b.k = 1 or b.k = 0.
by A144,A168,FINSEQ_1:2,TARSKI:def 2;
hence thesis by XXREAL_0:9,A169;
end;
A170: b.1 = 0. by A144,A149;
1 <= n+1 & n+1 <= len x by A46,FINSEQ_1:6,NAT_1:11;
then n+1 in dom x by FINSEQ_3:25;
then
A171: x.(n+1) = a.(n+1)*(M*F).(n+1) by A8
.= 0. by A130;
Sum y = sumy.1 + y.(1+1) by A151,A161,A163
.= 0. by A147,A153,A164;
hence thesis by A3,A5,A66,A171,A151,A166,A160,A170,A155,
MESFUNC3:def 2;
end;
end;
hence thesis;
end;
suppose
A172: dom f1 <> {};
n <= n+1 by NAT_1:11;
then
A173: Seg n c= Seg (n+1) by FINSEQ_1:5;
A174: dom F = Seg (n+1) by A9,FINSEQ_1:def 3;
then dom F1 = (Seg (n+1)) /\ Seg n by RELAT_1:61;
then
A175: dom F1 = Seg n by A173,XBOOLE_1:28;
then
A176: len F1 = n by FINSEQ_1:def 3;
consider G be Finite_Sep_Sequence of S, b,y be FinSequence of ExtREAL
such that
A177: G,b are_Re-presentation_of f1 and
A178: b.1 =0. and
A179: for n be Nat st 2 <= n & n in dom b holds 0. < b.n & b.n < +infty and
A180: dom y = dom G and
A181: for n be Nat st n in dom y holds y.n=b.n*(M*G).n and
A182: integral(M,f1)=Sum(y) by A23,MESFUNC3:def 2,a12;
A183: for i be Nat st i in dom x1 holds x1.i=a1.i*(M*F1).i
proof
let i be Nat;
assume
A184: i in dom x1;
A185: dom x1 c= dom x by RELAT_1:60;
then x.i = a.i * (M*F).i by A8,A184;
then
A186: x1.i = a.i * (M*F).i by A184,FUNCT_1:47
.= a1.i * (M*F).i by A24,A14,A184,FUNCT_1:47;
(M*F).i = M.(F.i) by A7,A184,A185,FUNCT_1:13
.= M.(F1.i) by A14,A184,FUNCT_1:47
.= (M*F1).i by A14,A184,FUNCT_1:13;
hence thesis by A186;
end;
now
per cases;
case
A187: F.(n+1) = {} or a.(n+1) = 0.;
defpred PH[Nat,set] means ($1 = 1 implies $2 = G.1 \/ F.(n+1)) & (
2 <= $1 implies $2 = G.$1);
A188: for k be Nat st k in Seg len G ex x be Element of S st PH[k, x]
proof
let k be Nat;
A189: rng G c= S by FINSEQ_1:def 4;
assume k in Seg len G;
then k in dom G by FINSEQ_1:def 3;
then
A190: G.k in rng G by FUNCT_1:3;
per cases;
suppose
A191: k = 1;
set x = G.1 \/ F.(n+1);
1 <= n+1 by NAT_1:11;
then n+1 in dom F by A9,FINSEQ_3:25;
then
A192: F.(n+1) in rng F by FUNCT_1:3;
rng F c= S by FINSEQ_1:def 4;
then reconsider x as Element of S by A190,A189,A191,A192,
FINSUB_1:def 1;
PH[k,x] by A191;
hence thesis;
end;
suppose
A193: k <> 1;
set x = G.k;
reconsider x as Element of S by A190,A189;
PH[k,x] by A193;
hence thesis;
end;
end;
consider H be FinSequence of S such that
A194: dom H = Seg len G & for k be Nat st k in Seg len G holds
PH[k,H.k] from FINSEQ_1:sch 5(A188);
A195: for u,v be object st u <> v holds H.u misses H.v
proof
let u,v be object;
assume
A196: u <> v;
per cases;
suppose
A197: u in dom H & v in dom H;
then reconsider u1=u,v1=v as Element of NAT;
per cases;
suppose
A198: u = 1;
1 <= v1 by A194,A197,FINSEQ_1:1;
then 1 < v1 by A196,A198,XXREAL_0:1;
then
A199: 1+1 <= v1 by NAT_1:13;
then
A200: H.v = G.v by A194,A197;
A201: F.(n+1) misses G.v
proof
per cases by A187;
suppose
F.(n+1) = {};
hence thesis;
end;
suppose
A202: a.(n+1) = 0.;
assume F.(n+1) meets G.v;
then consider w be object such that
A203: w in F.(n+1) and
A204: w in G.v by XBOOLE_0:3;
A205: v1 in dom G by A194,A197,FINSEQ_1:def 3;
then
A206: v1 in dom b by A177,MESFUNC3:def 1;
G.v1 in rng G by A205,FUNCT_1:3;
then w in union rng G by A204,TARSKI:def 4;
then w in dom f1 by A177,MESFUNC3:def 1;
then
A207: f.w = f1.w by FUNCT_1:47
.= b.v1 by A177,A204,A205,MESFUNC3:def 1;
1 <= n+1 by NAT_1:11;
then n+1 in Seg (n+1) by FINSEQ_1:1;
then n+1 in dom F by A9,FINSEQ_1:def 3;
then f.w = 0. by A6,A202,A203,MESFUNC3:def 1;
hence contradiction by A179,A199,A207,A206;
end;
end;
H.u = G.1 \/ F.(n+1) & G.1 misses G.v by A194,A196,A197,A198,
PROB_2:def 2;
hence thesis by A200,A201,XBOOLE_1:70;
end;
suppose
A208: u <> 1;
1 <= u1 by A194,A197,FINSEQ_1:1;
then 1 < u1 by A208,XXREAL_0:1;
then
A209: 1+1 <= u1 by NAT_1:13;
then
A210: H.u = G.u by A194,A197;
per cases;
suppose
A211: v = 1;
A212: F.(n+1) misses G.u
proof
per cases by A187;
suppose
F.(n+1) = {};
hence thesis;
end;
suppose
A213: a.(n+1) = 0.;
assume F.(n+1) meets G.u;
then consider w be object such that
A214: w in F.(n+1) and
A215: w in G.u by XBOOLE_0:3;
A216: u1 in dom G by A194,A197,FINSEQ_1:def 3;
then
A217: u1 in dom b by A177,MESFUNC3:def 1;
G.u1 in rng G by A216,FUNCT_1:3;
then w in union rng G by A215,TARSKI:def 4;
then w in dom f1 by A177,MESFUNC3:def 1;
then
A218: f.w = f1.w by FUNCT_1:47
.= b.u1 by A177,A215,A216,MESFUNC3:def 1;
1 <= n+1 by NAT_1:11;
then n+1 in Seg (n+1) by FINSEQ_1:1;
then n+1 in dom F by A9,FINSEQ_1:def 3;
then f.w = 0. by A6,A213,A214,MESFUNC3:def 1;
hence contradiction by A179,A209,A218,A217;
end;
end;
H.v = G.1 \/ F.(n+1) & G.1 misses G.u by A194,A196,A197
,A211,PROB_2:def 2;
hence thesis by A210,A212,XBOOLE_1:70;
end;
suppose
A219: v <> 1;
1 <= v1 by A194,A197,FINSEQ_1:1;
then 1 < v1 by A219,XXREAL_0:1;
then 1+1 <= v1 by NAT_1:13;
then H.v = G.v by A194,A197;
hence thesis by A196,A210,PROB_2:def 2;
end;
end;
end;
suppose
not u in dom H or not v in dom H;
then H.u = {} or H.v = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
deffunc Z(Nat) = b.$1 * (M*H).$1;
reconsider H as Finite_Sep_Sequence of S by A195,PROB_2:def 2;
consider z be FinSequence of ExtREAL such that
A220: len z = len y & for n be Nat st n in dom z holds z.n = Z
(n) from FINSEQ_2:sch 1;
G <> {} by A172,A177,MESFUNC3:def 1,RELAT_1:38,ZFMISC_1:2;
then 0+1 <= len G by NAT_1:13;
then
A221: 1 in Seg len G by FINSEQ_1:1;
A222: dom f = union rng H
proof
thus dom f c= union rng H
proof
let v be object;
assume v in dom f;
then v in union rng F by A6,MESFUNC3:def 1;
then consider A be set such that
A223: v in A and
A224: A in rng F by TARSKI:def 4;
consider u be object such that
A225: u in dom F and
A226: A = F.u by A224,FUNCT_1:def 3;
reconsider u as Element of NAT by A225;
A227: u in Seg len F by A225,FINSEQ_1:def 3;
then
A228: 1 <= u by FINSEQ_1:1;
A229: u <= n+1 by A9,A227,FINSEQ_1:1;
per cases;
suppose
u = n+1;
then H.1 = G.1 \/ A by A194,A221,A226;
then
A230: v in H.1 by A223,XBOOLE_0:def 3;
H.1 in rng H by A194,A221,FUNCT_1:3;
hence thesis by A230,TARSKI:def 4;
end;
suppose
u <> n+1;
then u < n+1 by A229,XXREAL_0:1;
then u <= n by NAT_1:13;
then u in Seg n by A228,FINSEQ_1:1;
then F1.u in rng F1 & A = F1.u by A175,A226,FUNCT_1:3,47;
then v in union rng F1 by A223,TARSKI:def 4;
then v in union rng G by A16,A177,MESFUNC3:def 1;
then consider B be set such that
A231: v in B and
A232: B in rng G by TARSKI:def 4;
consider w be object such that
A233: w in dom G and
A234: B = G.w by A232,FUNCT_1:def 3;
reconsider w as Element of NAT by A233;
A235: w in Seg len G by A233,FINSEQ_1:def 3;
per cases;
suppose
A236: w = 1;
H.1 = G.1 \/ F.(n+1) by A194,A221;
then
A237: v in H.1 by A231,A234,A236,XBOOLE_0:def 3;
H.1 in rng H by A194,A221,FUNCT_1:3;
hence thesis by A237,TARSKI:def 4;
end;
suppose
A238: w <> 1;
1 <= w by A233,FINSEQ_3:25;
then 1 < w by A238,XXREAL_0:1;
then 1+1 <= w by NAT_1:13;
then
A239: v in H.w by A194,A231,A234,A235;
H.w in rng H by A194,A235,FUNCT_1:3;
hence thesis by A239,TARSKI:def 4;
end;
end;
end;
let v be object;
assume v in union rng H;
then consider A be set such that
A240: v in A and
A241: A in rng H by TARSKI:def 4;
consider k be object such that
A242: k in dom H and
A243: A = H.k by A241,FUNCT_1:def 3;
reconsider k as Element of NAT by A242;
per cases;
suppose
k = 1;
then
A244: H.k = G.1 \/ F.(n+1) by A194,A242;
per cases by A240,A243,A244,XBOOLE_0:def 3;
suppose
A245: v in G.1;
1 in dom G by A221,FINSEQ_1:def 3;
then G.1 in rng G by FUNCT_1:3;
then v in union rng G by A245,TARSKI:def 4;
then v in dom f1 by A177,MESFUNC3:def 1;
then v in dom f /\ (union rng F1) by RELAT_1:61;
hence thesis by XBOOLE_0:def 4;
end;
suppose
A246: v in F.(n+1);
1 <= n+1 by NAT_1:11;
then n+1 in dom F by A9,FINSEQ_3:25;
then F.(n+1) in rng F by FUNCT_1:3;
then v in union rng F by A246,TARSKI:def 4;
hence thesis by A6,MESFUNC3:def 1;
end;
end;
suppose
A247: k <> 1;
1 <= k by A194,A242,FINSEQ_1:1;
then 1 < k by A247,XXREAL_0:1;
then 1+1 <= k by NAT_1:13;
then
A248: v in G.k by A194,A240,A242,A243;
k in dom G by A194,A242,FINSEQ_1:def 3;
then G.k in rng G by FUNCT_1:3;
then v in union rng G by A248,TARSKI:def 4;
then v in dom f1 by A177,MESFUNC3:def 1;
then v in dom f /\ (union rng F1) by RELAT_1:61;
hence thesis by XBOOLE_0:def 4;
end;
end;
A249: now
assume -infty in rng x1;
then consider l be object such that
A250: l in dom x1 and
A251: x1.l = -infty by FUNCT_1:def 3;
reconsider l as Element of NAT by A250;
l in dom x /\ (Seg n) by A250,RELAT_1:61;
then
A252: l in dom x by XBOOLE_0:def 4;
x.l = -infty by A250,A251,FUNCT_1:47;
then
A253: a.l*(M*F).l = -infty by A8,A252;
per cases;
suppose
A254: F.l <> {};
reconsider EMPTY = {} as Element of S by MEASURE1:7;
consider v be object such that
A255: v in F.l by A254,XBOOLE_0:def 1;
A256: F.l in rng F by A7,A252,FUNCT_1:3;
then v in union rng F by A255,TARSKI:def 4;
then
A257: v in dom f by A6,MESFUNC3:def 1;
rng F c= S by FINSEQ_1:def 4;
then reconsider Fl = F.l as Element of S by A256;
EMPTY c= F.l;
then M.{} <= M.(Fl) by MEASURE1:31;
then 0. <= M.(Fl) by VALUED_0:def 19;
then
A258: 0. <= (M*F).l by A7,A252,FUNCT_1:13;
a.l = f.v by A6,A7,A252,A255,MESFUNC3:def 1;
then 0. <= a.l by A257,a5;
hence contradiction by A253,A258;
end;
suppose
A259: F.l = {};
(M*F).l = M.(F.l) by A7,A252,FUNCT_1:13
.= 0. by A259,VALUED_0:def 19;
hence contradiction by A253;
end;
end;
1 <= n+1 by NAT_1:11;
then
A260: n+1 in dom F by A9,FINSEQ_3:25;
A261: x.(n+1) = 0.
proof
per cases by A187;
suppose
A262: F.(n+1) = {};
(M*F).(n+1) = M.(F.(n+1)) by A260,FUNCT_1:13;
then
A263: (M*F).(n+1) = 0. by A262,VALUED_0:def 19;
x.(n+1) = a.(n+1)*(M*F).(n+1) by A7,A8,A260;
hence thesis by A263;
end;
suppose
A264: a.(n+1) = 0.;
x.(n+1) = a.(n+1)*(M*F).(n+1) by A7,A8,A260;
hence thesis by A264;
end;
end;
A265: not -infty in rng <* x.(n+1) *> by A261;
A266: for m be Nat st m in dom H for x be object st x in H.m holds f.
x = b.m
proof
let m be Nat;
assume
A267: m in dom H;
let x be object;
assume
A268: x in H.m;
per cases;
suppose
A269: m = 1;
then
A270: H.m = G.1 \/ F.(n+1) by A194,A267;
per cases by A268,A270,XBOOLE_0:def 3;
suppose
A271: x in G.1;
A272: m in dom G by A194,A267,FINSEQ_1:def 3;
then G.1 in rng G by A269,FUNCT_1:3;
then x in union rng G by A271,TARSKI:def 4;
then
A273: x in dom f1 by A177,MESFUNC3:def 1;
f1.x = b.m by A177,A269,A271,A272,MESFUNC3:def 1;
hence thesis by A273,FUNCT_1:47;
end;
suppose
A274: x in F.(n+1);
1 <= n+1 by NAT_1:11;
then n+1 in dom F by A9,FINSEQ_3:25;
hence thesis by A6,A178,A187,A269,A274,MESFUNC3:def 1;
end;
end;
suppose
A275: m <> 1;
1 <= m by A267,FINSEQ_3:25;
then 1 < m by A275,XXREAL_0:1;
then 1+1 <= m by NAT_1:13;
then
A276: H.m = G.m by A194,A267;
A277: m in dom G by A194,A267,FINSEQ_1:def 3;
then G.m in rng G by FUNCT_1:3;
then x in union rng G by A268,A276,TARSKI:def 4;
then
A278: x in dom f1 by A177,MESFUNC3:def 1;
f1.x = b.m by A177,A268,A277,A276,MESFUNC3:def 1;
hence thesis by A278,FUNCT_1:47;
end;
end;
A279: dom z = dom y by A220,FINSEQ_3:29;
then
A280: dom z =dom H by A180,A194,FINSEQ_1:def 3;
A281: for k be Nat st k in dom z holds z.k = y.k
proof
let k be Nat;
assume
A282: k in dom z;
then
A283: z.k = b.k*(M*H).k by A220;
A284: y.k = b.k*(M*G).k by A181,A279,A282;
per cases;
suppose
A285: k = 1;
then z.k = 0. by A178,A283;
hence thesis by A178,A284,A285;
end;
suppose
A286: k <> 1;
A287: k in Seg len G by A180,A279,A282,FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then 1 < k by A286,XXREAL_0:1;
then
A288: 1+1 <= k by NAT_1:13;
(M*H).k = M.(H.k) by A280,A282,FUNCT_1:13
.= M.(G.k) by A194,A287,A288
.= (M*G).k by A180,A279,A282,FUNCT_1:13;
hence thesis by A181,A279,A282,A283;
end;
end;
len x = n+1 by A7,A9,FINSEQ_3:29;
then x = x|(n+1) by FINSEQ_1:58
.= x|Seg(n+1) by FINSEQ_1:def 16
.= x1^<* x.(n+1) *> by A7,A260,FINSEQ_5:10;
then
A289: Sum x = Sum(x1)+Sum<* x.(n+1) *> by A249,A265,EXTREAL1:10
.= Sum(x1)+0. by A261,EXTREAL1:8;
dom H = dom G by A194,FINSEQ_1:def 3
.= dom b by A177,MESFUNC3:def 1;
then H,b are_Re-presentation_of f by A222,A266,MESFUNC3:def 1;
then integral(M,f)=Sum(z) by A3,A5,A178,A179,A220,A280,
MESFUNC3:def 2
.=integral(M,f1) by A182,A279,A281,FINSEQ_1:13
.=Sum(x1) by A2,A23,A28,A14,A172,A183,A176,a12
.=Sum(x) by A289,XXREAL_3:4;
hence thesis;
end;
case
A290: F.(n+1) <> {} & a.(n+1) <> 0.;
defpred Pc[Nat,set] means ($1 <= len b implies $2 = b.$1) & ($1 =
len b + 1 implies $2 = a.(n+1));
A291: f is real-valued by A3,MESFUNC2:def 4;
consider v be object such that
A292: v in F.(n+1) by A290,XBOOLE_0:def 1;
A293: for k be Nat st k in Seg(len b + 1) ex v be Element of
ExtREAL st Pc[k,v]
proof
let k be Nat;
assume k in Seg(len b + 1);
per cases;
suppose
A294: k <> len b + 1;
reconsider v = b.k as Element of ExtREAL;
take v;
thus thesis by A294;
end;
suppose
A295: k = len b + 1;
reconsider v = a.(n+1) as Element of ExtREAL;
take v;
thus thesis by A295,NAT_1:13;
end;
end;
consider c be FinSequence of ExtREAL such that
A296: dom c = Seg(len b + 1) & for k be Nat st k in Seg(len b
+ 1) holds Pc[k,c.k] from FINSEQ_1:sch 5(A293);
1 <= n+1 by NAT_1:11;
then
A297: n+1 in dom F by A9,FINSEQ_3:25;
then F.(n+1) in rng F by FUNCT_1:3;
then v in union rng F by A292,TARSKI:def 4;
then
A298: v in dom f by A6,MESFUNC3:def 1;
dom f c= X by RELAT_1:def 18;
then reconsider v as Element of X by A298;
f.v = a.(n+1) by A6,A297,A292,MESFUNC3:def 1;
then |. a.(n+1) .| < +infty by A291,A298,MESFUNC2:def 1;
then
A299: a.(n+1) < +infty by EXTREAL1:21;
A300: len c = len b + 1 by A296,FINSEQ_1:def 3;
A301: 0. <= f.v by A298,a5;
then
A302: 0. < a.(n+1) by A6,A290,A297,A292,MESFUNC3:def 1;
A303: for m be Nat st 2 <= m & m in dom c holds 0. < c.m & c.m < +infty
proof
let m be Nat;
assume that
A304: 2 <= m and
A305: m in dom c;
A306: m <= len c by A305,FINSEQ_3:25;
per cases;
suppose
m = len c;
hence thesis by A302,A299,A296,A300,A305;
end;
suppose
m <> len c;
then m < len b + 1 by A300,A306,XXREAL_0:1;
then
A307: m <= len b by NAT_1:13;
1 <= m by A304,XXREAL_0:2;
then
A308: m in dom b by A307,FINSEQ_3:25;
c.m = b.m by A296,A305,A307;
hence thesis by A179,A304,A308;
end;
end;
A309: 0. <= a.(n+1) by A6,A297,A292,A301,MESFUNC3:def 1;
A310: now
assume
A311: -infty in rng y or -infty in rng <* a.(n+1)*(M*F).(n+1 ) *>;
per cases by A311;
suppose
-infty in rng y;
then consider k be object such that
A312: k in dom y and
A313: -infty = y.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A312;
A314: y.k = b.k*(M*G).k by A181,A312;
k in Seg len y by A312,FINSEQ_1:def 3;
then
A315: 1 <= k by FINSEQ_1:1;
per cases;
suppose
k = 1;
hence contradiction by A178,A313,A314;
end;
suppose
k <> 1;
then 1 < k by A315,XXREAL_0:1;
then
A316: 1+1 <= k by NAT_1:13;
k in dom b by A177,A180,A312,MESFUNC3:def 1;
then
A317: 0. < b.k by A179,A316;
G.k in rng G & rng G c= S by A180,A312,FINSEQ_1:def 4
,FUNCT_1:3;
then reconsider Gk = G.k as Element of S;
reconsider EMPTY = {} as Element of S by PROB_1:4;
M.EMPTY <= M.(Gk) by MEASURE1:31,XBOOLE_1:2;
then
A318: 0. <= M.(Gk) by VALUED_0:def 19;
(M*G).k = M.(G.k) by A180,A312,FUNCT_1:13;
hence contradiction by A313,A314,A317,A318;
end;
end;
suppose
A319: -infty in rng <* a.(n+1)*(M*F).(n+1) *>;
reconsider EMPTY = {} as Element of S by PROB_1:4;
A320: rng F c= S by FINSEQ_1:def 4;
1 <= n+1 by NAT_1:11;
then
A321: n+1 in dom F by A9,FINSEQ_3:25;
then F.(n+1) in rng F by FUNCT_1:3;
then reconsider Fn1 = F.(n+1) as Element of S by A320;
A322: (M*F).(n+1) = M.(Fn1) by A321,FUNCT_1:13;
M.EMPTY <= M.(Fn1) by MEASURE1:31,XBOOLE_1:2;
then
A323: 0. <= M.(Fn1) by VALUED_0:def 19;
-infty in { a.(n+1)*(M*F).(n+1) } by A319,FINSEQ_1:38;
hence contradiction by A309,A323,A322,TARSKI:def 1;
end;
end;
A324: not -infty in rng x1
proof
reconsider EMPTY = {} as Element of S by PROB_1:4;
assume -infty in rng x1;
then consider k be object such that
A325: k in dom x1 and
A326: -infty = x1.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A325;
k in (dom x)/\(Seg n) by A325,RELAT_1:61;
then
A327: k in dom x by XBOOLE_0:def 4;
then
A328: x.k = a.k*(M*F).k by A8;
A329: F.k in rng F by A7,A327,FUNCT_1:3;
rng F c= S by FINSEQ_1:def 4;
then reconsider Fk = F.k as Element of S by A329;
per cases;
suppose
F.k <> {};
then consider v be object such that
A330: v in F.k by XBOOLE_0:def 1;
v in union rng F by A329,A330,TARSKI:def 4;
then
A331: v in dom f by A6,MESFUNC3:def 1;
a.k = f.v by A6,A7,A327,A330,MESFUNC3:def 1;
then
A332: 0. <= a.k by A331,a5;
M.EMPTY <= M.Fk by MEASURE1:31,XBOOLE_1:2;
then
A333: 0. <= M.Fk by VALUED_0:def 19;
M.Fk = (M*F).k by A7,A327,FUNCT_1:13;
hence contradiction by A325,A326,A328,A332,A333,FUNCT_1:47;
end;
suppose
F.k = {};
then 0. = M.(F.k) by VALUED_0:def 19
.= (M*F).k by A7,A327,FUNCT_1:13;
hence contradiction by A325,A326,A328,FUNCT_1:47;
end;
end;
defpred PH[Nat,set] means ($1 <= len G implies $2 = G.$1) & ($1 =
len G + 1 implies $2 = F.(n+1));
A334: dom G = dom b by A177,MESFUNC3:def 1;
A335: Seg len G = dom G by FINSEQ_1:def 3
.= Seg len b by A334,FINSEQ_1:def 3;
then
A336: len G = len b by FINSEQ_1:6;
A337: for k be Nat st k in Seg(len G + 1) ex v be Element of S st PH[k,v]
proof
let k be Nat;
assume
A338: k in Seg(len G + 1);
per cases;
suppose
A339: k <> len G + 1;
k <= len G + 1 by A338,FINSEQ_1:1;
then k < len G + 1 by A339,XXREAL_0:1;
then
A340: k <= len G by NAT_1:13;
1 <= k by A338,FINSEQ_1:1;
then k in dom G by A340,FINSEQ_3:25;
then
A341: G.k in rng G by FUNCT_1:3;
rng G c= S by FINSEQ_1:def 4;
then reconsider v = G.k as Element of S by A341;
take v;
thus thesis by A339;
end;
suppose
A342: k = len G + 1;
F.(n+1) in rng F & rng F c= S by A297,FINSEQ_1:def 4,FUNCT_1:3;
then reconsider v = F.(n+1) as Element of S;
take v;
thus thesis by A342,NAT_1:13;
end;
end;
consider H be FinSequence of S such that
A343: dom H = Seg(len G + 1) & for k be Nat st k in Seg(len G
+ 1) holds PH[k,H.k] from FINSEQ_1:sch 5(A337);
A344: for i,j be object st i <> j holds H.i misses H.j
proof
let i,j be object;
assume
A345: i <> j;
per cases;
suppose
A346: i in dom H & j in dom H;
then reconsider i,j as Element of NAT;
A347: 1 <= i by A343,A346,FINSEQ_1:1;
A348: j <= len G + 1 by A343,A346,FINSEQ_1:1;
A349: for k be Nat st 1 <= k & k <= len G holds H.k misses F.( n+1)
proof
A350: union rng F1 misses F.(n+1)
proof
assume union rng F1 meets F.(n+1);
then consider v be object such that
A351: v in union rng F1 and
A352: v in F.(n+1) by XBOOLE_0:3;
consider A be set such that
A353: v in A and
A354: A in rng F1 by A351,TARSKI:def 4;
consider m be object such that
A355: m in dom F1 and
A356: A = F1.m by A354,FUNCT_1:def 3;
reconsider m as Element of NAT by A355;
m in Seg len F1 by A355,FINSEQ_1:def 3;
then m <= n by A176,FINSEQ_1:1;
then
A357: m <> n+1 by NAT_1:13;
F1.m = F.m by A355,FUNCT_1:47;
then A misses F.(n+1) by A356,A357,PROB_2:def 2;
then A /\ F.(n+1) = {};
hence contradiction by A352,A353,XBOOLE_0:def 4;
end;
let k be Nat;
assume that
A358: 1 <= k and
A359: k <= len G;
k in dom G by A358,A359,FINSEQ_3:25;
then G.k c= union rng G by FUNCT_1:3,ZFMISC_1:74;
then G.k c= dom f1 by A177,MESFUNC3:def 1;
then
A360: G.k c= (dom f)/\(union rng F1) by RELAT_1:61;
k <= len G + 1 by A359,NAT_1:12;
then k in Seg(len G + 1) by A358,FINSEQ_1:1;
then H.k = G.k by A343,A359;
hence thesis by A360,A350,XBOOLE_1:18,63;
end;
A361: 1 <= j by A343,A346,FINSEQ_1:1;
A362: i <= len G + 1 by A343,A346,FINSEQ_1:1;
A363: PH[i,H.i] by A343,A346;
A364: PH[j,H.j] by A343,A346;
per cases;
suppose
A365: i = len G + 1;
then j < len G + 1 by A345,A348,XXREAL_0:1;
then j <= len G by NAT_1:13;
hence thesis by A361,A363,A349,A365;
end;
suppose
i <> len G + 1;
then
A366: i < len G + 1 by A362,XXREAL_0:1;
then
A367: i <= len G by NAT_1:13;
per cases;
suppose
j = len G + 1;
hence thesis by A347,A364,A349,A367;
end;
suppose
j <> len G + 1;
then j < len G + 1 by A348,XXREAL_0:1;
hence thesis by A345,A363,A364,A366,NAT_1:13,PROB_2:def 2;
end;
end;
end;
suppose
A368: not i in dom H or not j in dom H;
per cases by A368;
suppose
not i in dom H;
then H.i = {} by FUNCT_1:def 2;
hence thesis;
end;
suppose
not j in dom H;
then H.j = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
end;
A369: len H = len G + 1 by A343,FINSEQ_1:def 3;
A370: Seg len H = Seg(len G + 1) by A343,FINSEQ_1:def 3;
defpred Pz[Nat,set] means ($1 <= len y implies $2 = b.$1*(M*H).$1)
& ($1 = len y + 1 implies $2 = a.(n+1)*(M*F).(n+1));
A371: for k be Nat st k in Seg(len y + 1) ex v be Element of
ExtREAL st Pz[k,v]
proof
let k be Nat;
assume k in Seg(len y + 1);
per cases;
suppose
A372: k <> len y + 1;
reconsider v = b.k*(M*H).k as Element of ExtREAL;
take v;
thus thesis by A372;
end;
suppose
A373: k = len y + 1;
reconsider v = a.(n+1)*(M*F).(n+1) as Element of ExtREAL;
take v;
thus thesis by A373,NAT_1:13;
end;
end;
consider z be FinSequence of ExtREAL such that
A374: dom z = Seg(len y + 1) & for k be Nat st k in Seg(len y
+ 1) holds Pz[k,z.k] from FINSEQ_1:sch 5(A371);
A375: len y = len G by A180,FINSEQ_3:29;
then
A376: len z = len G + 1 by A374,FINSEQ_1:def 3;
then
A377: len z in dom H by A343,FINSEQ_1:4;
A378: len z in Seg(len G + 1) by A376,FINSEQ_1:4;
A379: (M*F).(n+1) = M.(F.(n+1)) by A174,FINSEQ_1:4,FUNCT_1:13
.= M.(H.len z) by A343,A376,A378
.= (M*H).len z by A377,FUNCT_1:13;
A380: for m be Nat st m in dom z holds z.m = c.m*(M*H).m
proof
let m be Nat;
assume
A381: m in dom z;
then
A382: Pc[m,c.m] by A296,A336,A374,A375;
per cases;
suppose
m = len y + 1;
hence thesis by A335,A374,A375,A376,A379,A381,A382,FINSEQ_1:6;
end;
suppose
A383: m <> len y + 1;
m <= len y + 1 by A374,A381,FINSEQ_1:1;
then m < len y + 1 by A383,XXREAL_0:1;
then
A384: m <= len b by A336,A375,NAT_1:13;
then c.m = b.m by A296,A336,A374,A375,A381;
hence thesis by A336,A374,A375,A381,A384;
end;
end;
reconsider H as Finite_Sep_Sequence of S by A344,PROB_2:def 2;
A385: len G = len y by A180,FINSEQ_3:29;
A386: len z= len y + 1 by A374,FINSEQ_1:def 3;
then len z in Seg(len y + 1) by FINSEQ_1:4;
then
A387: z.len z=a.(n+1)*(M*F).(n+1) by A374,A386;
A388: for k be Nat st 1 <= k & k <= len z holds z.k = (y^<* a.(n+1
)*(M*F).(n+1) *>).k
proof
let k be Nat;
assume that
A389: 1 <= k and
A390: k <= len z;
per cases;
suppose
k = len z;
hence thesis by A386,A387,FINSEQ_1:42;
end;
suppose
k <> len z;
then k < len z by A390,XXREAL_0:1;
then
A391: k <= len y by A386,NAT_1:13;
then
A392: k in dom y by A389,FINSEQ_3:25;
then
A393: (y^<* a.(n+1)*(M*F).(n+1) *>).k = y.k by FINSEQ_1:def 7
.= b.k*(M*G).k by A181,A392
.= b.k*(M.(G.k)) by A180,A392,FUNCT_1:13;
A394: k in Seg len z by A389,A390,FINSEQ_1:1;
then
A395: M.(H.k) = (M*H).k by A343,A385,A386,FUNCT_1:13;
H.k = G.k by A343,A385,A386,A391,A394;
hence thesis by A374,A386,A391,A393,A394,A395;
end;
end;
len (y^<* a.(n+1)*(M*F).(n+1) *>) = len y + 1 by FINSEQ_2:16
.= len z by A374,FINSEQ_1:def 3;
then
A396: z = y^<* a.(n+1)*(M*F).(n+1) *> by A388,FINSEQ_1:14;
len x = n+1 by A7,A9,FINSEQ_3:29;
then
A397: x = x|(n+1) by FINSEQ_1:58
.= x|Seg(n+1) by FINSEQ_1:def 16
.= x1^<* x.(n+1) *> by A7,A297,FINSEQ_5:10
.= x1^<* a.(n+1)*(M*F).(n+1) *> by A7,A8,A297;
dom G <> {}
proof
assume dom G = {};
then {} = union rng G by RELAT_1:42,ZFMISC_1:2
.= dom f1 by A177,MESFUNC3:def 1;
hence contradiction by A172;
end;
then b <> {} by A177,MESFUNC3:def 1,RELAT_1:38;
then len b in Seg len b by FINSEQ_1:3;
then
A398: 1 <= len b by FINSEQ_1:1;
A399: for k be Nat st 1 <= k & k <= len H holds H.k = (G^<* F.(n+1
) *>).k
proof
let k be Nat;
assume that
A400: 1 <= k and
A401: k <= len H;
k in Seg(len G + 1) by A370,A400,A401,FINSEQ_1:1;
then
A402: PH[k,H.k] by A343;
per cases;
suppose
k = len G + 1;
hence thesis by A402,FINSEQ_1:42;
end;
suppose
k <> len G + 1;
then
A403: k < len G + 1 by A369,A401,XXREAL_0:1;
then k <= len G by NAT_1:13;
then k in dom G by A400,FINSEQ_3:25;
hence thesis by A402,A403,FINSEQ_1:def 7,NAT_1:13;
end;
end;
len H = len G + 1 by A343,FINSEQ_1:def 3
.= len G + len <* F.(n+1) *> by FINSEQ_1:39
.= len (G^<* F.(n+1) *>) by FINSEQ_1:22;
then H = G^<* F.(n+1) *> by A399,FINSEQ_1:14;
then
A404: rng H = rng G \/ rng <* F.(n+1) *> by FINSEQ_1:31
.= rng G \/ {F.(n+1)} by FINSEQ_1:38;
F|(Seg (n+1)) = F1^<* F.(n+1) *> by A174,FINSEQ_1:4,FINSEQ_5:10;
then F1^<* F.(n+1) *> = F|(n+1) by FINSEQ_1:def 16
.= F by A9,FINSEQ_1:58;
then rng F = rng F1 \/ rng <* F.(n+1) *> by FINSEQ_1:31
.= rng F1 \/ {F.(n+1)} by FINSEQ_1:38;
then
A405: dom f = union (rng F1 \/ {F.(n+1)}) by A6,MESFUNC3:def 1
.= dom f1 \/ union {F.(n+1)} by A16,ZFMISC_1:78
.= union rng G \/ union {F.(n+1)} by A177,MESFUNC3:def 1
.= union rng H by A404,ZFMISC_1:78;
for m be Nat st m in dom H for v be object st v in H.m holds f.
v = c. m
proof
let m be Nat;
assume
A406: m in dom H;
then
A407: PH[m,H.m] by A343;
A408: m <= len G + 1 by A343,A406,FINSEQ_1:1;
let v be object;
assume
A409: v in H.m;
A410: Pc[m,c.m] by A343,A296,A336,A406;
A411: 1 <= m by A343,A406,FINSEQ_1:1;
per cases;
suppose
A412: m = len G + 1;
n+1 in dom F by A174,FINSEQ_1:4;
hence thesis by A6,A335,A407,A410,A409,A412,FINSEQ_1:6
,MESFUNC3:def 1;
end;
suppose
m <> len G + 1;
then
A413: m < len G + 1 by A408,XXREAL_0:1;
then
A414: m <= len G by NAT_1:13;
then m in Seg len G by A411,FINSEQ_1:1;
then m in dom G by FINSEQ_1:def 3;
then
A415: G.m in rng G by FUNCT_1:3;
H.m in rng H by A406,FUNCT_1:3;
then
A416: v in dom f by A405,A409,TARSKI:def 4;
union rng G = union rng F1 by A16,A177,MESFUNC3:def 1;
then v in union rng F1 by A407,A409,A413,A415,NAT_1:13
,TARSKI:def 4;
then v in (dom f)/\(union rng F1) by A416,XBOOLE_0:def 4;
then
A417: v in dom f1 by RELAT_1:61;
m in Seg len G by A411,A414,FINSEQ_1:1;
then m in dom G by FINSEQ_1:def 3;
then f1.v = c.m by A177,A336,A407,A410,A409,A413,MESFUNC3:def 1
,NAT_1:13;
hence thesis by A417,FUNCT_1:47;
end;
end;
then
A418: H,c are_Re-presentation_of f by A343,A296,A336,A405,MESFUNC3:def 1;
1 <= len b + 1 by NAT_1:11;
then 1 in Seg(len b + 1) by FINSEQ_1:1;
then c.1 =0. by A178,A296,A398;
then integral(M,f)=Sum z by A3,A5,A343,A303,A374,A375,A380,A418
,MESFUNC3:def 2
.=Sum(y) + Sum<* a.(n+1)*(M*H).(len z) *> by A379,A310,A396,
EXTREAL1:10
.=integral(M,f1) + a.(n+1)*(M*H).(len z)
by A182,EXTREAL1:8
.=Sum(x1) + a.(n+1)*(M*F).(n+1) by A2,A23,A28,A14,A172,A183
,A176,A379,a12
.=Sum(x1) + Sum<* a.(n+1)*(M*F).(n+1) *> by EXTREAL1:8
.=Sum(x) by A310,A324,A397,EXTREAL1:10;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A419: P[0]
proof
let f be PartFunc of X,ExtREAL;
let F be Finite_Sep_Sequence of S;
let a,x be FinSequence of ExtREAL;
assume that
f is_simple_func_in S and
A420: dom f <> {} and f is nonnegative and
A421: F,a are_Re-presentation_of f and
dom x = dom F and
for i be Nat st i in dom x holds x.i = a.i*(M*F).i and
A422: len F = 0;
Seg len F = {} by A422;
then dom F = {} by FINSEQ_1:def 3;
then union rng F = {} by RELAT_1:42,ZFMISC_1:2;
hence thesis by A420,A421,MESFUNC3:def 1;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A419,A1);
hence thesis;
end;
theorem Th3:
for X be non empty set, S be SigmaField of X, f be PartFunc of X,
ExtREAL, M be sigma_Measure of S, F be Finite_Sep_Sequence of S, a,x be
FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} &
f is nonnegative &
F,a are_Re-presentation_of f & dom x = dom F &
(for n be Nat st n in dom x holds x.n=a.n*(M*F).n) holds integral(M,f)=Sum(
x)
proof
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
let M be sigma_Measure of S;
let F be Finite_Sep_Sequence of S;
let a,x be FinSequence of ExtREAL;
A1: len F = len F;
assume f is_simple_func_in S & dom f <> {} & f is nonnegative &
F,a are_Re-presentation_of f &( dom x = dom F & for n be Nat
st n in dom x holds x.n=a.n*(M*F).n);
hence thesis by A1,Th2;
end;
theorem Th4:
for X be non empty set, S be SigmaField of X, f be PartFunc of X,
ExtREAL, M be sigma_Measure of S st f is_simple_func_in S & dom f <> {} &
f is nonnegative
ex F be Finite_Sep_Sequence of S,
a,x be FinSequence of ExtREAL st F,a are_Re-presentation_of f & dom x = dom F &
(for n be Nat st n in dom x holds x.n=a.n*(M*F).n) & integral(M,f)=Sum(x)
proof
let X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL, M
be sigma_Measure of S;
assume that
A1: f is_simple_func_in S and
A2: dom f <> {} & f is nonnegative;
consider F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL such
that
A3: F,a are_Re-presentation_of f by A1,MESFUNC3:12;
ex x be FinSequence of ExtREAL st dom x = dom F & for n be Nat st n in
dom x holds x.n =a.n*(M*F).n
proof
deffunc Q(Nat) = a.$1*(M*F).$1;
consider x be FinSequence of ExtREAL such that
A4: len x = len F & for k be Nat st k in dom x holds x.k=Q(k) from
FINSEQ_2:sch 1;
take x;
dom x = Seg len F by A4,FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3;
hence thesis by A4;
end;
then consider x be FinSequence of ExtREAL such that
A5: dom x = dom F & for n be Nat st n in dom x holds x.n=a.n*(M*F).n;
integral(M,f)=Sum(x) by A1,A2,A3,A5,Th3;
hence thesis by A3,A5;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} &
f is nonnegative &
g is_simple_func_in S & dom g = dom f & g is nonnegative
holds f+g is_simple_func_in S &
dom
(f+g) <> {} &
(for x be object st x in dom (f+g) holds 0. <= (f+g).x) & integral(
M,f+g)=integral(M,f)+integral(M,g)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g
be PartFunc of X,ExtREAL such that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: f is nonnegative and
:::for x be object st x in dom f holds 0. <= f.x and
A4: g is_simple_func_in S and
A5: dom g = dom f and
A6: g is nonnegative;
A7: g is real-valued by A4,MESFUNC2:def 4;
then
A8: dom (f+g) = dom f /\ dom f by A5,MESFUNC2:2
.= dom f;
consider G be Finite_Sep_Sequence of S, b,y be FinSequence of ExtREAL such
that
A9: G,b are_Re-presentation_of g and
dom y = dom G and
for n be Nat st n in dom y holds y.n=b.n*(M*G).n and
integral(M,g)=Sum(y) by A2,A4,A5,A6,Th4;
set lb = len b;
consider F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL such
that
A10: F,a are_Re-presentation_of f and
dom x = dom F and
for n be Nat st n in dom x holds x.n=a.n*(M*F).n and
integral(M,f)=Sum(x) by A1,A2,A3,Th4;
deffunc B1(Nat) = b.(($1-' 1) mod lb +1);
deffunc A1(Nat) = a.(($1-' 1) div lb +1);
set la = len a;
A11: dom F = dom a by A10,MESFUNC3:def 1;
deffunc FG1(Nat) = F.(($1-'1) div lb + 1) /\ G.(($1-'1) mod lb + 1);
consider FG be FinSequence such that
A12: len FG = la*lb and
A13: for k be Nat st k in dom FG holds FG.k=FG1(k) from FINSEQ_1:sch 2;
A14: dom FG = Seg(la*lb) by A12,FINSEQ_1:def 3;
A15: dom G= dom b by A9,MESFUNC3:def 1;
now
reconsider la9=la,lb9=lb as Nat;
let k be Nat;
set i=(k-'1) div lb + 1;
set j=(k-'1) mod lb + 1;
assume
A16: k in dom FG;
then
A17: k in Seg (la*lb) by A12,FINSEQ_1:def 3;
then
A18: k <= la*lb by FINSEQ_1:1;
then (k -' 1) <= (la*lb -' 1) by NAT_D:42;
then
A19: (k -' 1) div lb <= (la*lb -' 1) div lb by NAT_2:24;
1 <= k by A17,FINSEQ_1:1;
then
A20: lb9 divides (la9*lb9) & 1 <= la*lb by A18,NAT_D:def 3,XXREAL_0:2;
A21: lb <> 0 by A17;
then lb >= 0+1 by NAT_1:13;
then ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A20,NAT_2:15;
then
A22: (k -' 1) div lb + 1 <= la*lb div lb by A19,XREAL_1:19;
reconsider la,lb as Nat;
i >= 0+1 & i <= la by A21,A22,NAT_D:18,XREAL_1:6;
then i in Seg la by FINSEQ_1:1;
then i in dom F by A11,FINSEQ_1:def 3;
then
A23: F.i in rng F by FUNCT_1:3;
(k -' 1) mod lb < lb by A21,NAT_D:1;
then j >= 0+1 & j <= lb by NAT_1:13;
then j in Seg lb by FINSEQ_1:1;
then j in dom G by A15,FINSEQ_1:def 3;
then
A24: G.j in rng G by FUNCT_1:3;
rng F c= S & rng G c= S by FINSEQ_1:def 4;
then F.i /\ G.j in S by A23,A24,MEASURE1:34;
hence FG.k in S by A13,A16;
end;
then reconsider FG as FinSequence of S by FINSEQ_2:12;
for k,l be Nat st k in dom FG & l in dom FG & k <> l holds FG.k misses FG.l
proof
reconsider la9=la,lb9=lb as Nat;
let k,l be Nat;
assume that
A25: k in dom FG and
A26: l in dom FG and
A27: k <> l;
A28: l in Seg (la*lb) by A12,A26,FINSEQ_1:def 3;
set m=(l-'1) mod lb + 1;
set n=(l-'1) div lb + 1;
set j=(k-'1) mod lb + 1;
set i=(k-'1) div lb + 1;
A29: FG.k = F.i /\ G.j by A13,A25;
A30: k in Seg (la*lb) by A12,A25,FINSEQ_1:def 3;
then
A31: k <= la*lb by FINSEQ_1:1;
A32: 1 <= k by A30,FINSEQ_1:1;
then
A33: lb9 divides (la9*lb9) & 1 <= la*lb by A31,NAT_D:def 3,XXREAL_0:2;
A34: lb <> 0 by A30;
then lb >= 0+1 by NAT_1:13;
then
A35: ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A33,NAT_2:15;
(k -' 1) <= (la*lb -' 1) by A31,NAT_D:42;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A35,NAT_2:24;
then
A36: (k -' 1) div lb + 1 <= la*lb div lb by XREAL_1:19;
reconsider la,lb as Nat;
i >= 0+1 & i <= la by A34,A36,NAT_D:18,XREAL_1:6;
then i in Seg la by FINSEQ_1:1;
then
A37: i in dom F by A11,FINSEQ_1:def 3;
A38: 1 <= l by A28,FINSEQ_1:1;
A39: i <> n or j <> m
proof
(l-'1)+1=(n-1)*lb+(m-1)+1 by A34,NAT_D:2;
then
A40: l - 1 + 1 = (n-1)*lb+m by A38,XREAL_1:233;
(k-'1)+1=(i-1)*lb+(j-1)+1 by A34,NAT_D:2;
then
A41: k - 1 + 1 = (i-1)*lb + j by A32,XREAL_1:233;
assume i=n & j=m;
hence contradiction by A27,A41,A40;
end;
(l -' 1) mod lb < lb by A34,NAT_D:1;
then m >= 0+1 & m <= lb by NAT_1:13;
then m in Seg lb by FINSEQ_1:1;
then
A42: m in dom G by A15,FINSEQ_1:def 3;
(k -' 1) mod lb < lb by A34,NAT_D:1;
then j >= 0+1 & j <= lb by NAT_1:13;
then j in Seg lb by FINSEQ_1:1;
then
A43: j in dom G by A15,FINSEQ_1:def 3;
l <= la*lb by A28,FINSEQ_1:1;
then (l -' 1) <= (la*lb -' 1) by NAT_D:42;
then (l -' 1) div lb <= (la*lb div lb) - 1 by A35,NAT_2:24;
then (l -' 1) div lb + 1 <= la*lb div lb by XREAL_1:19;
then n >= 0+1 & n <= la by A34,NAT_D:18,XREAL_1:6;
then n in Seg la by FINSEQ_1:1;
then
A44: n in dom F by A11,FINSEQ_1:def 3;
per cases by A39;
suppose
i <> n;
then
A45: F.i misses F.n by A37,A44,MESFUNC3:4;
FG.k /\ FG.l= (F.i /\ G.j) /\ (F.n /\ G.m) by A13,A26,A29
.= F.i /\ (G.j /\ (F.n /\ G.m)) by XBOOLE_1:16
.= F.i /\ (F.n /\ (G.j /\ G.m)) by XBOOLE_1:16
.= (F.i /\ F.n) /\ (G.j /\ G.m) by XBOOLE_1:16
.= {} /\ (G.j /\ G.m) by A45
.= {};
hence thesis;
end;
suppose
j <> m;
then
A46: G.j misses G.m by A43,A42,MESFUNC3:4;
FG.k /\ FG.l= (F.i /\ G.j) /\ (F.n /\ G.m) by A13,A26,A29
.= F.i /\ (G.j /\ (F.n /\ G.m)) by XBOOLE_1:16
.= F.i /\ (F.n /\ (G.j /\ G.m)) by XBOOLE_1:16
.= (F.i /\ F.n) /\ (G.j /\ G.m) by XBOOLE_1:16
.= (F.i /\ F.n) /\ {} by A46
.= {};
hence thesis;
end;
end;
then reconsider FG as Finite_Sep_Sequence of S by MESFUNC3:4;
consider a1 be FinSequence of ExtREAL such that
A47: len a1 = len FG and
A48: for k be Nat st k in dom a1 holds a1.k=A1(k) from FINSEQ_2:sch 1;
consider b1 be FinSequence of ExtREAL such that
A49: len b1 = len FG and
A50: for k be Nat st k in dom b1 holds b1.k=B1(k) from FINSEQ_2:sch 1;
A51: dom f = union rng F by A10,MESFUNC3:def 1;
A52: dom a1 = Seg len FG by A47,FINSEQ_1:def 3;
A53: for k be Nat st k in dom FG for x be object st x in FG.k holds f.x=a1.k
proof
reconsider la9=la,lb9=lb as Nat;
let k be Nat;
set i=(k-'1) div lb + 1;
assume
A54: k in dom FG;
then
A55: k in Seg len FG by FINSEQ_1:def 3;
A56: k in Seg len FG by A54,FINSEQ_1:def 3;
then
A57: k <= la*lb by A12,FINSEQ_1:1;
A58: lb <> 0 by A12,A56;
then
A59: lb >= 0+1 by NAT_1:13;
1 <= k by A56,FINSEQ_1:1;
then lb9 divides (la9*lb9) & 1 <= la*lb by A57,NAT_D:def 3,XXREAL_0:2;
then
A60: ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A59,NAT_2:15;
A61: la*lb div lb = la by A58,NAT_D:18;
(k -' 1) <= (la*lb -' 1) by A57,NAT_D:42;
then (k -' 1) div lb <= (la*lb -' 1) div lb by NAT_2:24;
then i >= 0+1 & i <= la*lb div lb by A60,XREAL_1:6,19;
then i in Seg la by A61,FINSEQ_1:1;
then
A62: i in dom F by A11,FINSEQ_1:def 3;
let x be object;
assume
A63: x in FG.k;
FG.k = F.((k-'1) div lb + 1) /\ G.((k-'1) mod lb + 1) by A13,A54;
then x in F.i by A63,XBOOLE_0:def 4;
hence f.x=a.i by A10,A62,MESFUNC3:def 1
.=a1.k by A48,A52,A55;
end;
A64: dom b1 = Seg len FG by A49,FINSEQ_1:def 3;
A65: for k be Nat st k in dom FG for x be object st x in FG.k holds g.x=b1.k
proof
let k be Nat;
set j=(k-'1) mod lb + 1;
assume
A66: k in dom FG;
then
A67: k in Seg len FG by FINSEQ_1:def 3;
k in Seg len FG by A66,FINSEQ_1:def 3;
then lb <> 0 by A12;
then (k -' 1) mod lb < lb by NAT_D:1;
then j >= 0+1 & j <= lb by NAT_1:13;
then j in Seg lb by FINSEQ_1:1;
then
A68: j in dom G by A15,FINSEQ_1:def 3;
let x be object;
assume
A69: x in FG.k;
FG.k = F.( (k-'1) div lb + 1 ) /\ G.( (k-'1) mod lb + 1 ) by A13,A66;
then x in G.j by A69,XBOOLE_0:def 4;
hence g.x=b.j by A9,A68,MESFUNC3:def 1
.=b1.k by A50,A64,A67;
end;
A70: dom g = union rng G by A9,MESFUNC3:def 1;
A71: dom f = union rng FG
proof
thus dom f c= union rng FG
proof
let z be object;
assume
A72: z in dom f;
then consider Y be set such that
A73: z in Y and
A74: Y in rng F by A51,TARSKI:def 4;
consider Z be set such that
A75: z in Z and
A76: Z in rng G by A5,A70,A72,TARSKI:def 4;
consider j be object such that
A77: j in dom G and
A78: Z = G.j by A76,FUNCT_1:def 3;
reconsider j as Element of NAT by A77;
A79: j in Seg len b by A15,A77,FINSEQ_1:def 3;
then
A80: 1 <= j by FINSEQ_1:1;
then consider j9 being Nat such that
A81: j = 1 + j9 by NAT_1:10;
consider i be object such that
A82: i in dom F and
A83: Y = F.i by A74,FUNCT_1:def 3;
reconsider i as Element of NAT by A82;
A84: i in Seg len a by A11,A82,FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then consider i9 being Nat such that
A85: i = 1 + i9 by NAT_1:10;
A86: j <= lb by A79,FINSEQ_1:1;
then
A87: j9 < lb by A81,NAT_1:13;
set k=(i-1)*lb+j;
reconsider k as Nat by A85;
A88: k >= 0 + j by A85,XREAL_1:6;
then
A89: k -' 1 = k - 1 by A80,XREAL_1:233,XXREAL_0:2
.= i9*lb + j9 by A85,A81;
then
A90: i = (k-'1) div lb +1 by A85,A87,NAT_D:def 1;
i <= la by A84,FINSEQ_1:1;
then i-1 <= la-1 by XREAL_1:9;
then (i-1)*lb <= (la - 1)*lb by XREAL_1:64;
then
A91: k <= (la - 1) * lb + j by XREAL_1:6;
(la - 1) * lb + j <= (la - 1) * lb + lb by A86,XREAL_1:6;
then
A92: k <= la*lb by A91,XXREAL_0:2;
k >= 1 by A80,A88,XXREAL_0:2;
then
A93: k in Seg (la*lb) by A92,FINSEQ_1:1;
then k in dom FG by A12,FINSEQ_1:def 3;
then
A94: FG.k in rng FG by FUNCT_1:def 3;
A95: j = (k-'1) mod lb +1 by A81,A89,A87,NAT_D:def 2;
z in F.i /\ G.j by A73,A83,A75,A78,XBOOLE_0:def 4;
then z in FG.k by A13,A14,A90,A95,A93;
hence thesis by A94,TARSKI:def 4;
end;
reconsider la9=la,lb9=lb as Nat;
let z be object;
assume z in union rng FG;
then consider Y be set such that
A96: z in Y and
A97: Y in rng FG by TARSKI:def 4;
consider k be object such that
A98: k in dom FG and
A99: Y = FG.k by A97,FUNCT_1:def 3;
reconsider k as Element of NAT by A98;
set j=(k-'1) mod lb +1;
set i=(k-'1) div lb +1;
FG.k=F.i /\ G.j by A13,A98;
then
A100: z in F.i by A96,A99,XBOOLE_0:def 4;
A101: k in Seg len FG by A98,FINSEQ_1:def 3;
then
A102: k <= la*lb by A12,FINSEQ_1:1;
A103: lb <> 0 by A12,A101;
then
A104: lb >= 0+1 by NAT_1:13;
1 <= k by A101,FINSEQ_1:1;
then lb9 divides (la9*lb9) & 1 <= la*lb by A102,NAT_D:def 3,XXREAL_0:2;
then
A105: ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A104,NAT_2:15;
reconsider i as Nat;
A106: la*lb div lb = la by A103,NAT_D:18;
(k -' 1) <= (la*lb -' 1) by A102,NAT_D:42;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A105,NAT_2:24;
then i >= 0+1 & i <= la*lb div lb by XREAL_1:6,19;
then i in Seg la by A106,FINSEQ_1:1;
then i in dom F by A11,FINSEQ_1:def 3;
then F.i in rng F by FUNCT_1:def 3;
hence thesis by A51,A100,TARSKI:def 4;
end;
A107: for k being Nat,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
reconsider la9=la,lb9=lb as Nat;
let k be Nat;
let x,y be Element of X;
assume that
A108: k in dom FG and
A109: x in FG.k and
A110: y in FG.k;
set j=(k-'1) mod lb + 1;
A111: FG.k = F.( (k-'1) div lb + 1 ) /\ G.( (k-'1) mod lb + 1 ) by A13,A108;
then
A112: x in G.j by A109,XBOOLE_0:def 4;
set i=(k-'1) div lb + 1;
A113: k in Seg len FG by A108,FINSEQ_1:def 3;
then
A114: k <= la*lb by A12,FINSEQ_1:1;
then
A115: (k -' 1) <= (la*lb -' 1) by NAT_D:42;
1 <= k by A113,FINSEQ_1:1;
then
A116: lb9 divides (la9*lb9) & 1 <= la*lb by A114,NAT_D:def 3,XXREAL_0:2;
A117: lb <> 0 by A12,A113;
then lb >= 0+1 by NAT_1:13;
then ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A116,NAT_2:15;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A115,NAT_2:24;
then (k -' 1) div lb + 1 <= la*lb div lb by XREAL_1:19;
then i >= 0+1 & i <= la by A117,NAT_D:18,XREAL_1:6;
then i in Seg la by FINSEQ_1:1;
then
A118: i in dom F by A11,FINSEQ_1:def 3;
x in F.i by A109,A111,XBOOLE_0:def 4;
then
A119: f.x=a.i by A10,A118,MESFUNC3:def 1;
(k -' 1) mod lb < lb by A117,NAT_D:1;
then j >= 0+1 & j <= lb by NAT_1:13;
then j in Seg lb by FINSEQ_1:1;
then
A120: j in dom G by A15,FINSEQ_1:def 3;
y in F.i by A110,A111,XBOOLE_0:def 4;
then
A121: f.y=a.i by A10,A118,MESFUNC3:def 1;
A122: y in G.j by A110,A111,XBOOLE_0:def 4;
A123: FG.k in rng FG by A108,FUNCT_1:def 3;
then
A124: y in dom (f+g) by A71,A8,A110,TARSKI:def 4;
x in dom (f+g) by A71,A8,A109,A123,TARSKI:def 4;
hence (f+g).x= f.x+g.x by MESFUNC1:def 3
.= a.i+b.j by A9,A120,A112,A119,MESFUNC3:def 1
.= f.y+g.y by A9,A120,A122,A121,MESFUNC3:def 1
.= (f+g).y by A124,MESFUNC1:def 3;
end;
ex y1 be FinSequence of ExtREAL st dom y1 = dom FG & for n be Nat st n
in dom y1 holds y1.n =b1.n*(M*FG).n
proof
deffunc Y1(Nat) = b1.$1*(M*FG).$1;
consider y1 be FinSequence of ExtREAL such that
A125: len y1 = len FG & for k be Nat st k in dom y1 holds y1.k=Y1(k)
from FINSEQ_2:sch 1;
take y1;
dom y1 = Seg len FG by A125,FINSEQ_1:def 3
.= dom FG by FINSEQ_1:def 3;
hence thesis by A125;
end;
then consider y1 be FinSequence of ExtREAL such that
A126: dom y1 = dom FG and
A127: for n be Nat st n in dom y1 holds y1.n=b1.n*(M*FG).n;
ex x1 be FinSequence of ExtREAL st dom x1 = dom FG & for n be Nat st n
in dom x1 holds x1.n =a1.n*(M*FG).n
proof
deffunc X1(Nat) = a1.$1*(M*FG).$1;
consider x1 be FinSequence of ExtREAL such that
A128: len x1 = len FG & for k be Nat st k in dom x1 holds x1.k=X1(k)
from FINSEQ_2:sch 1;
take x1;
thus thesis by A128,FINSEQ_3:29;
end;
then consider x1 be FinSequence of ExtREAL such that
A129: dom x1 = dom FG and
A130: for n be Nat st n in dom x1 holds x1.n=a1.n*(M*FG).n;
dom FG = Seg len a1 by A47,FINSEQ_1:def 3
.= dom a1 by FINSEQ_1:def 3;
then FG,a1 are_Re-presentation_of f by A71,A53,MESFUNC3:def 1;
then
A131: integral(M,f)=Sum x1 by A1,A2,A3,A129,A130,Th3;
deffunc C1(Nat) = a1.$1+b1.$1;
consider c1 be FinSequence of ExtREAL such that
A132: len c1 = len FG and
A133: for k be Nat st k in dom c1 holds c1.k=C1(k) from FINSEQ_2:sch 1;
ex z1 be FinSequence of ExtREAL st dom z1 = dom FG & for n be Nat st n
in dom z1 holds z1.n =c1.n*(M*FG).n
proof
deffunc Z1(Nat) = c1.$1*(M*FG).$1;
consider z1 be FinSequence of ExtREAL such that
A134: len z1 = len FG & for k be Nat st k in dom z1 holds z1.k=Z1(k)
from FINSEQ_2:sch 1;
take z1;
thus thesis by A134,FINSEQ_3:29;
end;
then consider z1 be FinSequence of ExtREAL such that
A135: dom z1 = dom FG and
A136: for n be Nat st n in dom z1 holds z1.n=c1.n*(M*FG).n;
A137: dom c1 = Seg len FG by A132,FINSEQ_1:def 3;
A138: for k be Nat st k in dom FG
for x be object st x in FG.k holds (f+g).x=c1 .k
proof
let k be Nat;
A139: dom (f+g) c= X by RELAT_1:def 18;
assume
A140: k in dom FG;
then
A141: k in Seg len FG by FINSEQ_1:def 3;
let x be object;
assume
A142: x in FG.k;
FG.k in rng FG by A140,FUNCT_1:def 3;
then x in dom (f+g) by A71,A8,A142,TARSKI:def 4;
hence (f+g).x= f.x+g.x by A139,MESFUNC1:def 3
.=a1.k+g.x by A53,A140,A142
.=a1.k+b1.k by A65,A140,A142
.=c1.k by A133,A137,A141;
end;
A143: for i be Nat st i in dom y1 holds 0. <= y1.i
proof
let i be Nat;
set i9 = (i -' 1) mod lb + 1;
assume
A144: i in dom y1;
then
A145: y1.i=b1.i*(M*FG).i by A127;
A146: i in Seg len FG by A126,A144,FINSEQ_1:def 3;
then lb <> 0 by A12;
then (i -' 1) mod lb < lb by NAT_D:1;
then i9 >= 0+1 & i9 <= lb by NAT_1:13;
then i9 in Seg lb by FINSEQ_1:1;
then
A147: i9 in dom G by A15,FINSEQ_1:def 3;
per cases;
suppose
G.i9 <> {};
then consider x9 be object such that
A148: x9 in G.i9 by XBOOLE_0:def 1;
FG.i in rng FG & rng FG c= S by A126,A144,FINSEQ_1:def 4,FUNCT_1:3;
then reconsider FGi = FG.i as Element of S;
reconsider EMPTY = {} as Element of S by MEASURE1:7;
EMPTY c= FGi;
then
A149: M.({}) <= M.FGi by MEASURE1:31;
g.x9 = b.i9 by A9,A147,A148,MESFUNC3:def 1
.= b1.i by A50,A64,A146;
then
A151: 0. <= b1.i by A6,SUPINF_2:51;
M.{} = 0. by VALUED_0:def 19;
then 0. <= (M*FG).i by A126,A144,A149,FUNCT_1:13;
hence thesis by A145,A151;
end;
suppose
A152: G.i9 = {};
FG.i = F.((i-'1) div lb + 1) /\ G.i9 by A13,A126,A144;
then M.(FG.i) = 0. by A152,VALUED_0:def 19;
then (M*FG).i = 0. by A126,A144,FUNCT_1:13;
hence thesis by A145;
end;
end; then
for i be object st i in dom y1 holds 0. <= y1.i; then
Y: y1 is nonnegative by SUPINF_2:52;
not -infty in rng y1
proof
assume -infty in rng y1;
then ex i be object st i in dom y1 & y1.i = -infty by FUNCT_1:def 3;
hence contradiction by A143;
end;
then
A153: x1"{+infty} /\ y1"{-infty} =x1"{+infty} /\ {} by FUNCT_1:72
.={};
A154: for i be Nat st i in dom x1 holds 0. <= x1.i
proof
reconsider la9=la,lb9=lb as Nat;
let i be Nat;
set i9 = (i -' 1) div lb + 1;
assume
A155: i in dom x1;
then
A156: x1.i=a1.i*(M*FG).i by A130;
A157: i in Seg len FG by A129,A155,FINSEQ_1:def 3;
then
A158: i <= la*lb by A12,FINSEQ_1:1;
A159: lb <> 0 by A12,A157;
then
A160: lb >= 0+1 by NAT_1:13;
1 <= i by A157,FINSEQ_1:1;
then lb9 divides (la9*lb9) & 1 <= la*lb by A158,NAT_D:def 3,XXREAL_0:2;
then
A161: ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A160,NAT_2:15;
i -' 1 <= (la*lb -' 1) by A158,NAT_D:42;
then (i -' 1) div lb <= (la*lb div lb) - 1 by A161,NAT_2:24;
then
A162: i9 >= 0+1 & i9 <= la*lb div lb by XREAL_1:6,19;
la*lb div lb = la by A159,NAT_D:18;
then i9 in Seg la by A162,FINSEQ_1:1;
then
A163: i9 in dom F by A11,FINSEQ_1:def 3;
per cases;
suppose
F.i9 <> {};
then consider x9 be object such that
A164: x9 in F.i9 by XBOOLE_0:def 1;
FG.i in rng FG & rng FG c= S by A129,A155,FINSEQ_1:def 4,FUNCT_1:3;
then reconsider FGi = FG.i as Element of S;
reconsider EMPTY = {} as Element of S by MEASURE1:7;
EMPTY c= FGi;
then
A165: M.({}) <= M.FGi by MEASURE1:31;
f.x9 = a.i9 by A10,A163,A164,MESFUNC3:def 1
.= a1.i by A48,A52,A157;
then
A167: 0. <= a1.i by A3,SUPINF_2:51;
M.{} = 0. by VALUED_0:def 19;
then 0. <= (M*FG).i by A129,A155,A165,FUNCT_1:13;
hence thesis by A156,A167;
end;
suppose
A168: F.i9 = {};
FG.i = F.i9 /\ G.((i-'1) mod lb + 1) by A13,A129,A155;
then M.(FG.i) = 0. by A168,VALUED_0:def 19;
then (M*FG).i = 0. by A129,A155,FUNCT_1:13;
hence thesis by A156;
end;
end; then
for i be object st i in dom x1 holds 0. <= x1.i; then
Z: x1 is nonnegative by SUPINF_2:52;
not -infty in rng x1
proof
assume -infty in rng x1;
then ex i be object st i in dom x1 & x1.i = -infty by FUNCT_1:def 3;
hence contradiction by A154;
end;
then x1"{-infty} /\ y1"{+infty} = {} /\ y1"{+infty} by FUNCT_1:72
.={};
then
A169: dom (x1+y1) =(dom x1 /\ dom y1) \ ({} \/ {}) by A153,MESFUNC1:def 3
.=dom z1 by A129,A126,A135;
A170: for k be Nat st k in dom z1 holds z1.k = (x1+y1).k
proof
reconsider la9=la,lb9=lb as Nat;
let k be Nat;
set p=(k-'1) div lb + 1;
set q=(k-'1) mod lb + 1;
assume
A171: k in dom z1;
then
A172: k in Seg len FG by A135,FINSEQ_1:def 3;
then
A173: k <= la*lb by A12,FINSEQ_1:1;
then
A174: (k -' 1) <= (la*lb -' 1) by NAT_D:42;
1 <= k by A172,FINSEQ_1:1;
then
A175: lb9 divides (la9*lb9) & 1 <= la*lb by A173,NAT_D:def 3,XXREAL_0:2;
A176: lb <> 0 by A12,A172;
then lb >= 0+1 by NAT_1:13;
then ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A175,NAT_2:15;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A174,NAT_2:24;
then p <= la*lb div lb by XREAL_1:19;
then p >= 0+1 & p <= la by A176,NAT_D:18,XREAL_1:6;
then p in Seg la by FINSEQ_1:1;
then
A177: p in dom F by A11,FINSEQ_1:def 3;
(k -' 1) mod lb < lb by A176,NAT_D:1;
then q >= 0+1 & q <= lb by NAT_1:13;
then q in Seg lb by FINSEQ_1:1;
then
A178: q in dom G by A15,FINSEQ_1:def 3;
A179: (a1.k+b1.k)*(M*FG).k = a1.k*(M*FG).k + b1.k*(M*FG).k
proof
per cases;
suppose
FG.k <> {};
then F.p /\ G.q <> {} by A13,A135,A171;
then consider v be object such that
A180: v in F.p /\ G.q by XBOOLE_0:def 1;
A181: v in G.q by A180,XBOOLE_0:def 4;
b.q = g.v by A9,A178,A181,MESFUNC3:def 1;
then 0. <= b.q by A6,SUPINF_2:51;
then
A183: 0. = b1.k or 0. < b1.k by A50,A64,A172;
A184: v in F.p by A180,XBOOLE_0:def 4;
a.p = f.v by A10,A177,A184,MESFUNC3:def 1;
then 0. <= a.p by A3,SUPINF_2:51;
then 0. = a1.k or 0. < a1.k by A48,A52,A172;
hence thesis by A183,XXREAL_3:96;
end;
suppose
FG.k = {};
then M.(FG.k) = 0. by VALUED_0:def 19;
then
A186: (M*FG).k = 0. by A135,A171,FUNCT_1:13;
hence (a1.k+b1.k)*(M*FG).k =0 .= a1.k*(M*FG).k + b1.k*(M*FG).k by A186;
end;
end;
thus z1.k = c1.k*(M*FG).k by A136,A171
.= a1.k*(M*FG).k+b1.k*(M*FG).k by A133,A137,A172,A179
.= x1.k + b1.k*(M*FG).k by A129,A130,A135,A171
.= x1.k + y1.k by A126,A127,A135,A171
.= (x1+y1).k by A169,A171,MESFUNC1:def 3;
end;
A187: dom (f+g) = dom g /\ dom g by A5,A7,MESFUNC2:2
.= dom g;
now
let x be Element of X;
assume
A188: x in dom (f+g);
then |. (f+g).x .| = |. f.x + g.x .| by MESFUNC1:def 3;
then
A189: |. (f+g).x .| <= |. f.x .| + |. g.x .| by EXTREAL1:24;
g is real-valued by A4,MESFUNC2:def 4;
then
A190: |. g.x .| < +infty by A187,A188,MESFUNC2:def 1;
f is real-valued by A1,MESFUNC2:def 4;
then |. f.x .| < +infty by A8,A188,MESFUNC2:def 1;
then |. f.x .| + |. g.x .| <> +infty by A190,XXREAL_3:16;
hence |. (f+g).x .| < +infty by A189,XXREAL_0:2,4;
end;
then f+g is real-valued by MESFUNC2:def 1;
hence
A191: f+g is_simple_func_in S by A71,A8,A107,MESFUNC2:def 4;
thus dom (f+g) <> {} by A2,A8;
thus for x be object st x in dom (f+g) holds 0. <= (f+g).x
proof
let x be object;
A193: dom f c= X by RELAT_1:def 18;
assume
A194: x in dom (f+g);
0. <= f.x & 0. <= g.x by A3,A6,SUPINF_2:51;
then 0. <= f.x + g.x;
hence thesis by A8,A194,A193,MESFUNC1:def 3;
end; then
X:f+g is nonnegative by SUPINF_2:52;
dom FG = dom c1 by A132,FINSEQ_3:29;
then FG,c1 are_Re-presentation_of (f+g) by A71,A8,A138,MESFUNC3:def 1;
then
A195: integral(M,f+g)=Sum z1 by X,A2,A135,A136,A8,A191,Th3;
dom (x1+y1) = Seg len z1 by A169,FINSEQ_1:def 3;
then x1+y1 is FinSequence by FINSEQ_1:def 2;
then
A196: z1=x1+y1 by A169,A170,FINSEQ_1:13;
dom FG = Seg len b1 by A49,FINSEQ_1:def 3
.= dom b1 by FINSEQ_1:def 3;
then FG,b1 are_Re-presentation_of g by A5,A71,A65,MESFUNC3:def 1;
then integral(M,g)=Sum y1 by A2,A4,A5,A6,A126,A127,Th3;
hence thesis by A129,A126,A131,A195,A196,Th1,Y,Z;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,ExtREAL, c be R_eal st f is_simple_func_in S & dom f <> {}
& f is nonnegative &
0. <= c & c < +infty & dom g =
dom f & (for x be set st x in dom g holds g.x=c*f.x) holds integral(M,g)=c*
integral(M,f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g
be PartFunc of X,ExtREAL, c be R_eal such that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: f is nonnegative and
A4: 0. <= c and
A5: c < +infty and
A6: dom g = dom f and
A7: for x be set st x in dom g holds g.x=c*f.x;
for x be object st x in dom g holds 0. <= g.x
proof
let x be object;
assume
A9: x in dom g;
0. <= f.x by A3,SUPINF_2:51;
then 0. <= c*f.x by A4;
hence thesis by A7,A9;
end; then
X: g is nonnegative by SUPINF_2:52;
A10: ex G be Finite_Sep_Sequence of S st (dom g = union rng G & for n be Nat
, x,y be Element of X st n in dom G & x in G.n & y in G.n holds g.x = g.y)
proof
consider G be Finite_Sep_Sequence of S such that
A11: dom f = union rng G and
A12: for n be Nat, x,y be Element of X st n in dom G & x in G.n & y in
G.n holds f.x = f.y by A1,MESFUNC2:def 4;
take G;
for n be Nat, x,y be Element of X st n in dom G & x in G.n & y in G.n
holds g.x = g.y
proof
let n be Nat;
let x,y be Element of X;
assume that
A13: n in dom G and
A14: x in G.n and
A15: y in G.n;
A16: G.n in rng G by A13,FUNCT_1:3;
then y in dom g by A6,A11,A15,TARSKI:def 4;
then
A17: g.y = c*f.y by A7;
x in dom g by A6,A11,A14,A16,TARSKI:def 4;
then g.x = c*f.x by A7;
hence thesis by A12,A13,A14,A15,A17;
end;
hence thesis by A6,A11;
end;
consider F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL, x be
FinSequence of ExtREAL such that
A18: F,a are_Re-presentation_of f and
A19: dom x = dom F and
A20: for n be Nat st n in dom x holds x.n=a.n*(M*F).n and
A21: integral(M,f)=Sum(x) by A1,A2,A3,Th4;
ex b be FinSequence of ExtREAL st dom b = dom a & for n be Nat st n in
dom b holds b.n=c*a.n
proof
deffunc ca(Nat) = c*a.$1;
consider b be FinSequence such that
A22: len b = len a & for n be Nat st n in dom b holds b.n = ca(n) from
FINSEQ_1:sch 2;
A23: rng b c= ExtREAL
proof
let v be object;
assume v in rng b;
then consider k be object such that
A24: k in dom b and
A25: v = b.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A24;
v = c*a.k by A22,A24,A25;
hence thesis;
end;
A26: dom b = Seg len b by FINSEQ_1:def 3;
reconsider b as FinSequence of ExtREAL by A23,FINSEQ_1:def 4;
take b;
thus thesis by A22,A26,FINSEQ_1:def 3;
end;
then consider b be FinSequence of ExtREAL such that
A27: dom b = dom a and
A28: for n be Nat st n in dom b holds b.n=c*a.n;
A29: c in REAL by A4,A5,XXREAL_0:14;
ex z be FinSequence of ExtREAL st dom z = dom x & for n be Nat st n in
dom z holds z.n=c*x.n
proof
deffunc cx(Nat) = c*x.$1;
consider z be FinSequence such that
A30: len z = len x & for n be Nat st n in dom z holds z.n = cx(n) from
FINSEQ_1:sch 2;
A31: rng z c= ExtREAL
proof
let v be object;
assume v in rng z;
then consider k be object such that
A32: k in dom z and
A33: v = z.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A32;
v = c*x.k by A30,A32,A33;
hence thesis;
end;
A34: dom z = Seg len z by FINSEQ_1:def 3;
reconsider z as FinSequence of ExtREAL by A31,FINSEQ_1:def 4;
take z;
thus thesis by A30,A34,FINSEQ_1:def 3;
end;
then consider z be FinSequence of ExtREAL such that
A35: dom z = dom x and
A36: for n be Nat st n in dom z holds z.n=c*x.n;
A37: for n be Nat st n in dom z holds z.n=b.n*(M*F).n
proof
let n be Nat;
A38: dom a = dom F by A18,MESFUNC3:def 1;
assume
A39: n in dom z;
hence z.n = c*x.n by A36
.=c*(a.n*(M*F).n) by A20,A35,A39
.= c*a.n*((M*F).n) by XXREAL_3:66
.=b.n*(M*F).n by A19,A27,A28,A35,A39,A38;
end;
A40: dom g =union rng F by A6,A18,MESFUNC3:def 1;
A41: now
let n be Nat;
assume
A42: n in dom F;
then
A43: n in dom b by A18,A27,MESFUNC3:def 1;
let x be object;
assume
A44: x in F.n;
F.n in rng F by A42,FUNCT_1:3;
then x in dom g by A40,A44,TARSKI:def 4;
hence g.x= c*f.x by A7
.= c*a.n by A18,A42,A44,MESFUNC3:def 1
.= b.n by A28,A43;
end;
dom F = dom b by A18,A27,MESFUNC3:def 1;
then
A45: F,b are_Re-presentation_of g by A40,A41,MESFUNC3:def 1;
A46: f is real-valued by A1,MESFUNC2:def 4;
for x be Element of X st x in dom g holds |. g.x .| < +infty
proof
let x be Element of X;
assume
A47: x in dom g;
c*f.x <> -infty by A29,A46;
then g.x <> -infty by A7,A47;
then -infty < g.x by XXREAL_0:6;
then
A48: -(+infty) < g.x by XXREAL_3:def 3;
c*f.x <> +infty by A29,A46;
then g.x <> +infty by A7,A47;
then g.x < +infty by XXREAL_0:4;
hence thesis by A48,EXTREAL1:22;
end;
then g is real-valued by MESFUNC2:def 1;
then g is_simple_func_in S by A10,MESFUNC2:def 4;
hence integral(M,g)=Sum z by A2,A6,A19,A35,A45,A37,Th3,X
.=c*integral(M,f) by A29,A21,A35,A36,MESFUNC3:10;
end;