:: Linearity of {L}ebesgue Integral of Simple Valued Function :: by Noboru Endou and Yasunari Shidama :: :: Received September 14, 2005 :: Copyright (c) 2005-2019 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: now assume -infty in rng <* x.(n+1) *>; then -infty in {x.(n+1)} by FINSEQ_1:39; hence contradiction by A261; end; 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 15 .= 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 15 .= 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 15 .= 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;