:: Construction of Measure from Semialgebra of Sets :: by Noboru Endou :: :: Received August 14, 2015 :: Copyright (c) 2015-2016 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, SUBSET_1, CARD_3, FUNCT_1, RELAT_1, FINSEQ_1, XBOOLE_0, ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, ORDINAL4, PROB_1, FINSUB_1, SETFAM_1, PROB_2, MEASURE9, MSSUBFAM, FUNCOP_1, SUPINF_2, VALUED_0, PARTFUN1, MEASURE1, ORDINAL2, SERIES_1, MESFUNC5, SUPINF_1, MEASURE4, SEQ_2, MATRIX_1, QC_LANG1, MATRIXC1, ORDINAL1, PRE_POLY, TREES_1, FINSEQ_3, INCSP_1, FINSEQ_2, XREAL_0, MEASURE8, REAL_1, XCMPLX_0, COMPLEX1, DBLSEQ_1, DBLSEQ_2, MESFUNC9, RFINSEQ, SIMPLEX0, ASYMPT_1, SRINGS_3, DBLSEQ_3, LATTICE5; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSUB_1, CARD_3, NUMBERS, XXREAL_3, BINOP_1, XTUPLE_0, PROB_1, XCMPLX_0, XREAL_0, XXREAL_0, SIMPLEX0, NAT_1, VALUED_0, SUPINF_1, SEQ_1, MEASURE8, FINSEQ_1, FINSEQ_2, FINSEQOP, SUPINF_2, PROB_2, MEASURE1, MEASURE4, MESFUNC1, MESFUNC5, MESFUNC9, MATRIX_0, SEQ_2, SERIES_1, RVSUM_1, RFINSEQ, WSIERP_1, MATRLIN, EXTREAL1, SRINGS_3, DBLSEQ_3; constructors PROB_2, EXTREAL1, SUPINF_1, MESFUNC9, RINFSUP2, FINSEQOP, MATRPROB, MATRLIN, MEASURE6, SEQ_1, MEASURE8, SERIES_1, WSIERP_1, COMSEQ_2, RFINSEQ, SRINGS_3, DBLSEQ_3; registrations XREAL_0, MEMBERED, FUNCT_1, XBOOLE_0, FINSEQ_1, RELAT_1, SUBSET_1, XXREAL_0, ROUGHS_1, NUMBERS, VALUED_0, FUNCT_2, ORDINAL1, RELSET_1, FINSUB_1, MEASURE1, MESFUNC5, MATRLIN, NAT_1, XXREAL_3, CARD_1, PBOOLE, SIMPLEX0, SEQ_2, SEQ_1, SETFAM_1, NUMPOLY1, SRINGS_3, DBLSEQ_3; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; equalities FINSEQ_1, XXREAL_3, BINOP_1, SRINGS_3; expansions FINSEQ_1, SETFAM_1, PARTFUN1; theorems TARSKI, XBOOLE_0, XREAL_0, FINSEQ_1, NAT_1, FUNCT_1, CARD_3, XXREAL_0, ZFMISC_1, FINSEQ_3, XBOOLE_1, PROB_2, XREAL_1, PROB_1, FINSUB_1, SETFAM_1, FUNCOP_1, XXREAL_3, MEASURE1, VALUED_0, FUNCT_2, MEASURE7, RELAT_1, MESFUNC5, EXTREAL1, MESFUNC9, FINSEQ_2, PARTFUN1, ORDINAL1, RINFSUP2, MEASURE8, MESFUNC3, RFINSEQ, PRE_POLY, MATRLIN, RVSUM_1, MESFUNC1, MATRPROB, ORDERS_1, SERIES_1, SUPINF_2, VALUED_1, MATRIX_0, ROUGHS_1, FINSEQOP, SEQM_3, POLYNOM3, XTUPLE_0, SRINGS_3, SEQ_1, DBLSEQ_3; schemes FINSEQ_1, NAT_1, FUNCT_2, MATRIX_0, FINSEQ_2, BINOP_1; begin :: Join of many finite sequence theorem Th52: for K be Relation st rng K is empty-membered holds union rng K = {} proof let K be Relation; assume A2: rng K is empty-membered; now let x be object; assume x in union rng K; then ex A be set st x in A & A in rng K by TARSKI:def 4; hence x in {} by A2; end; then union rng K c= {} by TARSKI:def 3; hence union rng K = {}; end; theorem for K be Function holds rng K is empty-membered iff (for x be object holds K.x = {}) proof let K be Function; hereby assume A1: rng K is empty-membered; let x be object; per cases; suppose x in dom K; hence K.x = {} by A1,FUNCT_1:3; end; suppose not x in dom K; hence K.x = {} by FUNCT_1:def 2; end; end; assume A2: for x be object holds K.x = {}; now assume ex y be non empty set st y in rng K; then consider y be non empty set such that A3: y in rng K; ex a be object st a in dom K & y = K.a by A3,FUNCT_1:def 3; hence contradiction by A2; end; hence rng K is empty-membered; end; definition let D be set, F be FinSequenceSet of D, f be FinSequence of F, n be Nat; redefine func f.n -> FinSequence of D; correctness proof per cases; suppose n in dom f; then f.n in rng f by FUNCT_1:3; hence f.n is FinSequence of D by FINSEQ_2:def 3; end; suppose not n in dom f; then f.n = <*>D by FUNCT_1:def 2; hence f.n is FinSequence of D; end; end; end; definition let D be set, Y be FinSequenceSet of D, F be FinSequence of Y; func Length F -> FinSequence of NAT means :Def1: dom it = dom F & for n be Nat st n in dom it holds it.n = len(F.n); existence proof defpred P[Nat,object] means $2 = len(F.$1); A1:for k be Nat st k in Seg len F ex x be Element of NAT st P[k,x]; consider IT be FinSequence of NAT such that A2: dom IT = Seg len F & for k be Nat st k in Seg len F holds P[k,IT.k] from FINSEQ_1:sch 5(A1); take IT; thus dom IT = dom F by A2,FINSEQ_1:def 3; thus for n be Nat st n in dom IT holds IT.n = len(F.n) by A2; end; uniqueness proof let IT1,IT2 be FinSequence of NAT; assume that A1: dom IT1 = dom F & for n be Nat st n in dom IT1 holds IT1.n = len(F.n) and A2: dom IT2 = dom F & for n be Nat st n in dom IT2 holds IT2.n = len(F.n); A3:len IT1 = len IT2 by A1,A2,FINSEQ_3:29; now let k be Nat; assume k in dom IT1; then IT1.k = len(F.k) & IT2.k = len(F.k) by A1,A2; hence IT1.k = IT2.k; end; hence IT1 = IT2 by A3,FINSEQ_2:9; end; end; theorem for D be set, Y be FinSequenceSet of D, F be FinSequence of Y st (for n be Nat st n in dom F holds F.n = <*>D) holds Sum Length F = 0 proof let D be set, Y be FinSequenceSet of D, F be FinSequence of Y; assume A1: for n be Nat st n in dom F holds F.n = <*>D; A2:dom (Length F) = dom F by Def1 .= Seg len F by FINSEQ_1:def 3; A6:len F |-> (0 qua Real) = Seg len F --> (0 qua Real) by FINSEQ_2:def 2; then A3:dom(len F |-> (0 qua Real)) = Seg len F by FUNCT_2:def 1; now let k be Nat; assume A4: k in dom (Length F); then k in dom F by Def1; then F.k = <*>D by A1; then (Length F).k = 0 by A4,Def1; hence (Length F).k = (len F |-> (0 qua Real)).k by A2,A4,A6,FUNCOP_1:7; end; then Length F = (len F |-> (0 qua Real)) by A2,A3,FINSEQ_1:13; hence Sum Length F = 0 by RVSUM_1:81; end; theorem Th2: for D be set, Y be FinSequenceSet of D, F be FinSequence of Y, k be Nat st k < len F holds Length(F|(k+1)) = Length(F|k) ^ <*len(F.(k+1))*> proof let D be set, Y be FinSequenceSet of D, F be FinSequence of Y, k be Nat; assume A1: k < len F; then k+1 <= len F by NAT_1:13; then A3:len(F|(k+1)) = k+1 by FINSEQ_1:59; A6:len(F|k) = k by A1,FINSEQ_1:59; A5:dom (Length(F|(k+1))) = dom (F|(k+1)) & dom (Length(F|k)) = dom(F|k) by Def1; then A7:len(Length(F|(k+1))) = k+1 & len(Length(F|k)) = k by A3,A6,FINSEQ_3:29; then A8:len( Length(F|k) ^ <*len(F.(k+1))*> ) = k + len <*len(F.(k+1))*> by FINSEQ_1:22 .= k+1 by FINSEQ_1:40; now let n be Nat; assume A9: 1 <= n & n <= len(Length(F|(k+1))); then n in dom(Length(F|(k+1))) by FINSEQ_3:25; then A10: (Length(F|(k+1))).n = len((F|(k+1)).n) by Def1 .= len(F.n) by A7,A9,FINSEQ_3:112; per cases; suppose n = len(Length(F|(k+1))); hence (Length(F|(k+1))).n = (Length(F|k)^<*len(F.(k+1))*>).n by A7,A10,FINSEQ_1:42; end; suppose n <> len(Length(F|(k+1))); then n < k+1 by A7,A9,XXREAL_0:1; then A11: n <= k by NAT_1:13; then (Length(F|k) ^ <*len(F.(k+1))*>).n = (Length(F|k)).n by A9,A7,FINSEQ_1:64 .= len((F|k).n) by A11,Def1,A9,A5,A6,FINSEQ_3:25 .= len(F.n) by A11,FINSEQ_3:112; hence (Length(F|(k+1))).n = (Length(F|k) ^ <*len(F.(k+1))*>).n by A10; end; end; hence thesis by A5,A8,A3,FINSEQ_3:29; end; theorem Th3: for D be set, Y be FinSequenceSet of D, F be FinSequence of Y, n be Nat st 1 <= n & n <= Sum Length F holds ex k,m be Nat st 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)) proof let D be set, Y be FinSequenceSet of D, F be FinSequence of Y, n be Nat; assume A1: 1<= n & n <= Sum Length F; now assume A2: for k be Nat holds n <= Sum Length(F|k) or n > Sum Length(F|(k+1)); defpred P[Nat] means n > Sum Length(F|($1+1)); dom Length(F|0) = dom {} by Def1; then Length(F|0) = {}; then A3: P[0] by A2,A1,RVSUM_1:72; A4: for k be Nat st P[k] holds P[k+1] by A2; for k be Nat holds P[k] from NAT_1:sch 2(A3,A4); then n > Sum Length(F|(len F + 1)); hence contradiction by A1,FINSEQ_1:58,NAT_1:11; end; then consider k be Nat such that A6: Sum Length(F|k) < n & n <= Sum Length(F|(k+1)); consider m be Nat such that A7: n = Sum Length(F|k) + m by A6,NAT_1:10; take k,m; A8:now assume A9: len F <= k; k <= k+1 by NAT_1:11; then (F|(k+1)) = F & F|k = F by A9,XXREAL_0:2,FINSEQ_1:58; hence contradiction by A6; end; then Length(F|(k+1)) = Length(F|k) ^ <*len(F.(k+1))*> by Th2; then m + Sum Length(F|k) <= Sum Length(F|k) + len(F.(k+1)) by A6,A7,RVSUM_1:74; hence thesis by A6,A7,NAT_1:19,A8,XREAL_1:6; end; RFINSEQlm3: for n be Nat, D be set, f be FinSequence of D st len f<=n holds (f|n) = f proof let n be Nat, D be set,f be FinSequence of D; A1:dom f = Seg len f by FINSEQ_1:def 3; assume len f<=n; hence thesis by A1,FINSEQ_1:5,RELAT_1:68; end; RFINSEQ6: for D be set, f be FinSequence of D, n,m be Nat holds n in dom f & m in Seg n implies (f|n).m = f.m & m in dom f proof let D be set,f be FinSequence of D, n,m be Nat; assume that A1: n in dom f and A2: m in Seg n; A3:dom f = Seg len f & n<=len f by A1,FINSEQ_1:def 3,FINSEQ_3:25; then A4:Seg n c= dom f by FINSEQ_1:5; Seg n = dom f /\ Seg n by A3,FINSEQ_1:5,XBOOLE_1:28 .= dom(f|n) by RELAT_1:61; hence thesis by A2,A4,FUNCT_1:47; end; RFINSEQ8: for D be set, f be FinSequence of D, n be Nat holds (f|n)^(f/^n) = f proof let D be set, f be FinSequence of D,n be Nat; set fn = f/^n; per cases; suppose len fD & f|n = f by RFINSEQ:def 1,RFINSEQlm3; hence thesis by FINSEQ_1:34; end; suppose A1: n<=len f; then A3: len (f|n) = n by FINSEQ_1:59; A4: len fn = len f - n by A1,RFINSEQ:def 1; then A5: len ((f|n)^(f/^n)) = n+(len f - n) by A3,FINSEQ_1:22; A6: dom(f|n) = Seg n by A3,FINSEQ_1:def 3; now let m be Nat; assume m in dom f; then A8: 1<=m & m<=len f by FINSEQ_3:25; per cases; suppose A10: m<=n; then 1<=n by A8,XXREAL_0:2; then A11: n in dom f by A1,FINSEQ_3:25; A12: m in Seg n by A8,A10; hence ((f|n)^(f/^n)).m = (f|n).m by A6,FINSEQ_1:def 7 .= f.m by A12,A11,RFINSEQ6; end; suppose A13: n k2; per cases by A6,XXREAL_0:1; suppose k1 < k2; then k1+1 <= k2 by NAT_1:13; then Sum Length(F|(k1+1)) <= Sum Length(F|k2) by Th5; then n <= Sum Length(F|k2) by A3,XXREAL_0:2; hence contradiction by A2,A1,NAT_1:19; end; suppose k1 > k2; then k2+1 <= k1 by NAT_1:13; then Sum Length(F|(k2+1)) <= Sum Length(F|k1) by Th5; then n <= Sum Length(F|k1) by A2,A4,XXREAL_0:2; hence contradiction by A1,NAT_1:19; end; end; now assume m1 <> m2; then Sum Length(F|k1) - Sum Length(F|k2) <> 0 by A2; hence k1 <> k2; end; hence thesis by A5; end; definition let D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y; func joined_FinSeq F -> FinSequence of D means :Def2: len it = Sum Length F & for n be Nat st n in dom it ex k,m be Nat st 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)) & it.n = (F.(k+1)).m; existence proof defpred P[Nat,object] means ex k,m be Nat st 1<= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = $1 & $1 <= Sum Length(F|(k+1)) & $2 = (F.(k+1)).m; A1:for n be Nat st n in Seg (Sum Length F) ex x be Element of D st P[n,x] proof let n be Nat; assume n in Seg (Sum Length F); then 1 <= n & n <= Sum Length F by FINSEQ_1:1; then consider k,m be Nat such that A2: 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)) by Th3; m in dom (F.(k+1)) by A2,FINSEQ_3:25; then (F.(k+1)).m in rng(F.(k+1)) by FUNCT_1:3; then reconsider x = (F.(k+1)).m as Element of D; take x; thus thesis by A2; end; consider IT be FinSequence of D such that A3: dom IT = Seg (Sum Length F) & for n be Nat st n in Seg (Sum Length F) holds P[n,IT.n] from FINSEQ_1:sch 5(A1); take IT; thus len IT = Sum Length F by A3,FINSEQ_1:def 3; thus for n be Nat st n in dom IT holds ex k,m be Nat st 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)) & IT.n = (F.(k+1)).m by A3; end; uniqueness proof let IT1,IT2 be FinSequence of D; assume that A1: len IT1 = Sum Length F & (for n be Nat st n in dom IT1 ex k,m be Nat st 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)) & IT1.n = (F.(k+1)).m) and A2: len IT2 = Sum Length F & (for n be Nat st n in dom IT2 ex k,m be Nat st 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)) & IT2.n = (F.(k+1)).m); A3:dom IT1 = dom IT2 by A1,A2,FINSEQ_3:29; now let n be Nat; assume A4: n in dom IT1; then consider k1,m1 be Nat such that A5: 1 <= m1 & m1 <= len(F.(k1+1)) & k1 < len F & m1 + Sum Length(F|k1) = n & n <= Sum Length(F|(k1+1)) & IT1.n = (F.(k1+1)).m1 by A1; consider k2,m2 be Nat such that A6: 1 <= m2 & m2 <= len(F.(k2+1)) & k2 < len F & m2 + Sum Length(F|k2) = n & n <= Sum Length(F|(k2+1)) & IT2.n = (F.(k2+1)).m2 by A2,A3,A4; k1 = k2 & m1 = m2 by A5,A6,Th6; hence IT1.n = IT2.n by A5,A6; end; hence IT1=IT2 by A1,A2,FINSEQ_3:29,FINSEQ_1:13; end; end; definition let D be set, Y be FinSequenceSet of D, s be sequence of Y; func Length s -> sequence of NAT means :Def3: for n be Nat holds it.n = len(s.n); existence proof defpred P[Nat,object] means $2 = len(s.$1); A1:for k be Element of NAT ex x be Element of NAT st P[k,x]; consider IT be Function of NAT,NAT such that A2: for k be Element of NAT holds P[k,IT.k] from FUNCT_2:sch 3(A1); take IT; hereby let n be Nat; n is Element of NAT by ORDINAL1:def 12; hence IT.n = len(s.n) by A2; end; end; uniqueness proof let IT1,IT2 be sequence of NAT; assume that A1: for n be Nat holds IT1.n = len(s.n) and A2: for n be Nat holds IT2.n = len(s.n); now let n be Element of NAT; IT1.n = len(s.n) by A1; hence IT1.n = IT2.n by A2; end; hence IT1 = IT2 by FUNCT_2:63; end; end; definition let s be sequence of NAT; redefine func Partial_Sums s -> sequence of NAT; correctness proof A2:Partial_Sums s is total; now let y be object; assume y in rng(Partial_Sums s); then consider n be object such that A3: n in dom(Partial_Sums s) & y = (Partial_Sums s).n by FUNCT_1:def 3; reconsider n as Nat by A3; defpred P[Nat] means (Partial_Sums s).$1 is Nat; (Partial_Sums s).0 = s.0 by SERIES_1:def 1; then A4: P[0]; A5: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; then reconsider Pk = (Partial_Sums s).k as Nat; (Partial_Sums s).(k+1) = Pk + s.(k+1) by SERIES_1:def 1; hence P[k+1]; end; for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); then (Partial_Sums s).n is Nat; hence y in NAT by A3,ORDINAL1:def 12; end; hence Partial_Sums s is sequence of NAT by A2,TARSKI:def 3,FUNCT_2:2; end; end; registration let D be non empty set; cluster non empty with_non-empty_element for FinSequenceSet of D; existence proof consider x be object such that A1:x in D by XBOOLE_0:def 1; reconsider x as Element of D by A1; set S = {<*x*>}; for a be object st a in S holds a is FinSequence of D by TARSKI:def 1; then reconsider S as FinSequenceSet of D by FINSEQ_2:def 3; take S; thus S is non empty with_non-empty_element; end; end; theorem Th7: for D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, n be Nat holds len(s.n) >= 1 & n < (Partial_Sums(Length s)).n & (Partial_Sums(Length s)).n < (Partial_Sums(Length s)).(n+1) proof let D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, n be Nat; defpred P[Nat] means $1 < (Partial_Sums(Length s)).$1; A1:for k be Nat holds len(s.k) >= 1 proof let k be Nat; dom s = NAT by FUNCT_2:def 1; then k in dom s by ORDINAL1:def 12; hence len(s.k) >= 1 by FINSEQ_1:20; end; (Partial_Sums(Length s)).0 = (Length s).0 by SERIES_1:def 1 .= len(s.0) by Def3; then A3:P[0]; A4:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A5: P[k]; A6: (Partial_Sums(Length s)).(k+1) = (Partial_Sums(Length s)).k + (Length s).(k+1) by SERIES_1:def 1; (Length s).(k+1) = len(s.(k+1)) by Def3; hence P[k+1] by A1,A6,A5,XREAL_1:8; end; for k be Nat holds P[k] from NAT_1:sch 2(A3,A4); hence len(s.n) >= 1 & n < (Partial_Sums(Length s)).n by A1; (Partial_Sums(Length s)).(n+1) = (Partial_Sums(Length s)).n + (Length s).(n+1) by SERIES_1:def 1 .= (Partial_Sums(Length s)).n + len(s.(n+1)) by Def3; hence thesis by XREAL_1:29; end; theorem Th8: for D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, n be Nat holds ex k,m be Nat st m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n proof let D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, n be Nat; per cases; suppose A1: n < len(s.0); set k = 0; set m = n+1; take k,m; A4: m <= len(s.k) by A1,NAT_1:13; (Partial_Sums(Length s)).k = (Length s).0 by SERIES_1:def 1 .= len(s.k) by Def3; hence m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m-1= n by NAT_1:11,A4,FINSEQ_3:25; end; suppose A5: len(s.0) <= n; then (Length s).0 <= n by Def3; then A6: (Partial_Sums(Length s)).0 <= n by SERIES_1:def 1; now assume A8: for k be Nat st k < n holds n < (Partial_Sums(Length s)).k or (Partial_Sums(Length s)).(k+1) <= n; defpred P[Nat] means $1 < n implies (Partial_Sums(Length s)).($1+1) <= n; A9: P[0] by A6,A8; A12: for k be Nat st P[k] holds P[k+1] by A8,NAT_1:13; A13: for k be Nat holds P[k] from NAT_1:sch 2(A9,A12); reconsider n1 = n-1 as Nat by A5,NAT_1:20; (Partial_Sums(Length s)).(n1+1) <= n by A13,NAT_1:19; hence contradiction by Th7; end; then consider k1 be Nat such that A14: k1 < n & (Partial_Sums(Length s)).k1 <= n & n < (Partial_Sums(Length s)).(k1+1); take k = k1+1; reconsider m1 = (Partial_Sums(Length s)).k - n as Nat by A14,NAT_1:21; (Partial_Sums(Length s)).k = (Partial_Sums(Length s)).k1 + (Length s).k by SERIES_1:def 1; then A15:m1 = (Partial_Sums(Length s)).k1 + len(s.k) - n by Def3; (Partial_Sums(Length s)).k1 - n <= 0 by A14,XREAL_1:47; then A17:(Partial_Sums(Length s)).k1 - n + len(s.k) <= len(s.k) by XREAL_1:32; then m1 <= len(s.k) & len(s.k) <= len(s.k)+1 by A15,NAT_1:11; then reconsider m = len(s.k) +1 - m1 as Nat by NAT_1:21,XXREAL_0:2; take m; m1 > 0 by A14,XREAL_1:50; then len(s.k) - m1 >= 0 & 1-m1 <= 0 by A15,A17,NAT_1:14,XREAL_1:47,48; then len(s.k) - m1 + 1 >= 0+1 & len(s.k) + (1 - m1) <= len(s.k) + 0 by XREAL_1:6; hence m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m -1 = n by FINSEQ_3:25; end; end; theorem Th9: for D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y holds Partial_Sums(Length s) is increasing proof let D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y; now let n,m be Nat; assume A1: n in dom(Partial_Sums(Length s)) & m in dom(Partial_Sums(Length s)) & n < m; defpred P[Nat] means (Partial_Sums(Length s)).n < (Partial_Sums(Length s)).(n+1+$1); (Partial_Sums(Length s)).(n+1+0) = (Partial_Sums(Length s)).n + (Length s).(n+1) by SERIES_1:def 1 .= (Partial_Sums(Length s)).n + len(s.(n+1)) by Def3; then A3: P[0] by XREAL_1:29; A4: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A5: P[k]; (Partial_Sums(Length s)).(n+1+(k+1)) = (Partial_Sums(Length s)).(n+1+k) + (Length s).(n+1+k+1) by SERIES_1:def 1 .= (Partial_Sums(Length s)).(n+1+k) + len(s.(n+1+k+1)) by Def3; then (Partial_Sums(Length s)).(n+1+(k+1)) > (Partial_Sums(Length s)).(n+1+k) by XREAL_1:29; hence P[k+1] by A5,XXREAL_0:2; end; A7: for k be Nat holds P[k] from NAT_1:sch 2(A3,A4); n+1 <= m by A1,NAT_1:13; then reconsider k = m - (n+1) as Nat by NAT_1:21; m = n+1+k; hence (Partial_Sums(Length s)).n < (Partial_Sums(Length s)).m by A7; end; hence Partial_Sums(Length s) is increasing by SEQM_3:def 1; end; theorem Th10: for D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, m1,m2,k1,k2 be Nat st m1 in dom(s.k1) & m2 in dom(s.k2) & (Partial_Sums(Length s)).k1 - len(s.k1) + m1 = (Partial_Sums(Length s)).k2 - len(s.k2) + m2 holds m1=m2 & k1=k2 proof let D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, m1,m2,k1,k2 be Nat; assume that A1: m1 in dom(s.k1) & m2 in dom(s.k2) and A2: (Partial_Sums(Length s)).k1 - len(s.k1) + m1 = (Partial_Sums(Length s)).k2 - len(s.k2) + m2; set n = (Partial_Sums(Length s)).k1 - len(s.k1) + m1; A3:1 <= m1 & m1 <= len(s.k1) & 1 <= m2 & m2 <= len(s.k2) by A1,FINSEQ_3:25; then len(s.k1) - m1 >= 0 & len(s.k2) - m2 >= 0 by XREAL_1:48; then A4:(Partial_Sums(Length s)).k1 - (len(s.k1) - m1) <= (Partial_Sums(Length s)).k1 & (Partial_Sums(Length s)).k2 - (len(s.k2) - m2) <= (Partial_Sums(Length s)).k2 by XREAL_1:43; A5:dom(Partial_Sums(Length s)) = NAT by FUNCT_2:def 1; then A6:k1 in dom(Partial_Sums(Length s)) & k2 in dom(Partial_Sums(Length s)) by ORDINAL1:def 12; A7:Partial_Sums(Length s) is increasing by Th9; A14:now assume A8: k1 <> k2; per cases by A8,XXREAL_0:1; suppose k1 < k2; then A10: k1+1 <= k2 by NAT_1:13; 1 <= k1+1 by NAT_1:11; then reconsider j = k2-1 as Element of NAT by NAT_1:21,A10,XXREAL_0:2; A11: k1 <= j by A10,XREAL_1:19; A12: (Partial_Sums(Length s)).k1 <= (Partial_Sums(Length s)).j proof k1 = j or k1 < j by A11,XXREAL_0:1; hence thesis by A5,A6,A7,SEQM_3:def 1; end; (Partial_Sums(Length s)).(j+1) = (Partial_Sums(Length s)).j + (Length s).(j+1) by SERIES_1:def 1 .= (Partial_Sums(Length s)).j + len(s.k2) by Def3; then n > (Partial_Sums(Length s)).j by A3,A2,XREAL_1:29; hence contradiction by A4,A12,XXREAL_0:2; end; suppose k2 < k1; then A10: k2+1 <= k1 by NAT_1:13; 1 <= k2+1 by NAT_1:11; then reconsider j = k1-1 as Element of NAT by NAT_1:21,A10,XXREAL_0:2; A11: k2 <= j by A10,XREAL_1:19; A12: (Partial_Sums(Length s)).k2 <= (Partial_Sums(Length s)).j proof k2 = j or k2 < j by A11,XXREAL_0:1; hence thesis by A5,A6,A7,SEQM_3:def 1; end; (Partial_Sums(Length s)).(j+1) = (Partial_Sums(Length s)).j + (Length s).(j+1) by SERIES_1:def 1 .= (Partial_Sums(Length s)).j + len(s.k1) by Def3; then n > (Partial_Sums(Length s)).j by A3,XREAL_1:29; hence contradiction by A2,A4,A12,XXREAL_0:2; end; end; then (Partial_Sums(Length s)).k1 - len(s.k1) = (Partial_Sums(Length s)).k2 - len(s.k2); hence m1=m2 & k1=k2 by A2,A14; end; theorem Th11: for D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y ex N be increasing sequence of NAT st for k be Nat holds N.k = (Partial_Sums(Length s)).k - 1 proof let D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y; defpred P[Nat,Nat] means $2 = (Partial_Sums(Length s)).$1 - 1; A1:for k be Element of NAT ex n be Element of NAT st P[k,n] proof let k be Element of NAT; reconsider n = (Partial_Sums(Length s)).k - 1 as Element of NAT by Th7,NAT_1:20; take n; thus thesis; end; consider N be Function of NAT,NAT such that A2: for k be Element of NAT holds P[k,N.k] from FUNCT_2:sch 3(A1); A3:for k be Nat holds N.k = (Partial_Sums(Length s)).k - 1 proof let k be Nat; k is Element of NAT by ORDINAL1:def 12; hence thesis by A2; end; for n be Nat holds N.n < N.(n+1) proof let n be Nat; (Partial_Sums(Length s)).n - 1 < (Partial_Sums(Length s)).(n+1) - 1 by Th7,XREAL_1:9; then N.n < (Partial_Sums(Length s)).(n+1) - 1 by A3; hence N.n < N.(n+1) by A3; end; then reconsider N as increasing sequence of NAT by VALUED_1:def 13; take N; thus thesis by A3; end; definition let D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y; func joined_seq s -> sequence of D means :Def4: for n be Nat ex k,m be Nat st m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n & it.n = (s.k).m; existence proof defpred P[Nat,object] means ex k,m be Nat st m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m -1 = $1 & $2 = (s.k).m; A1:for n be Element of NAT ex y be Element of D st P[n,y] proof let n be Element of NAT; consider k,m be Nat such that A2: m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n by Th8; (s.k).m in rng(s.k) by A2,FUNCT_1:3; then reconsider y = (s.k).m as Element of D; take y; thus thesis by A2; end; consider IT be Function of NAT,D such that A4: for n be Element of NAT holds P[n,IT.n] from FUNCT_2:sch 3(A1); reconsider IT as sequence of D; take IT; hereby let n be Nat; n is Element of NAT by ORDINAL1:def 12; hence ex k,m be Nat st m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m-1 = n & IT.n = (s.k).m by A4; end; end; uniqueness proof let f1,f2 be sequence of D such that A1: (for n be Nat ex k,m be Nat st m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n & f1.n = (s.k).m) and A2: (for n be Nat ex k,m be Nat st m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n & f2.n = (s.k).m); for n be Element of NAT holds f1.n = f2.n proof let n be Element of NAT; consider k1,m1 be Nat such that A3: m1 in dom(s.k1) & (Partial_Sums(Length s)).k1 - len(s.k1) + m1 - 1 = n & f1.n = (s.k1).m1 by A1; consider k2,m2 be Nat such that A4: m2 in dom(s.k2) & (Partial_Sums(Length s)).k2 - len(s.k2) + m2 - 1 = n & f2.n = (s.k2).m2 by A2; m1 = m2 & k1 = k2 by A3,A4,Th10; hence f1.n = f2.n by A3,A4; end; hence f1 = f2 by FUNCT_2:def 8; end; end; theorem for D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, s1 be sequence of D st ( for n be Nat holds s1.n = (joined_seq s).(Partial_Sums(Length s).n - 1) ) holds s1 is subsequence of joined_seq s proof let D be non empty set, Y be with_non-empty_element FinSequenceSet of D; let s be non-empty sequence of Y, s1 be sequence of D; assume A1:for n be Nat holds s1.n = (joined_seq s).(Partial_Sums(Length s).n - 1); consider N be increasing sequence of NAT such that A2: for n be Nat holds N.n = (Partial_Sums(Length s)).n - 1 by Th11; for n be Element of NAT holds s1.n = ((joined_seq s)*N).n proof let n be Element of NAT; s1.n = (joined_seq s).(Partial_Sums(Length s).n - 1) by A1; then s1.n = (joined_seq s).(N.n) by A2; hence s1.n = ((joined_seq s)*N).n by FUNCT_2:15; end; hence s1 is subsequence of joined_seq s by FUNCT_2:def 8; end; theorem Th13: for D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, k,m be Nat st m in dom(s.k) ex n be Nat st n = (Partial_Sums(Length s)).k - len(s.k) + m - 1 & (joined_seq s).n = (s.k).m proof let D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, k,m be Nat; assume A0: m in dom(s.k); then A1:1 <= m & m <= len(s.k) by FINSEQ_3:25; now per cases; suppose A2: k = 0; then (Partial_Sums(Length s)).k = (Length s).0 by SERIES_1:def 1 .= len(s.0) by Def3; hence (Partial_Sums(Length s)).k - len(s.k) + m - 1 is Nat by A1,A2,NAT_1:21; end; suppose k <> 0; then reconsider k1 = k-1 as Element of NAT by NAT_1:14,21; k = k1+1; then (Partial_Sums(Length s)).k = (Partial_Sums(Length s)).k1 + (Length s).k by SERIES_1:def 1 .= (Partial_Sums(Length s)).k1 + len(s.k) by Def3; then reconsider n1= (Partial_Sums(Length s)).k - len(s.k) as Nat; n1+m >= m by NAT_1:11; hence (Partial_Sums(Length s)).k - len(s.k) + m - 1 is Nat by A1,XXREAL_0:2,NAT_1:21; end; end; then reconsider n = (Partial_Sums(Length s)).k - len(s.k) + m - 1 as Nat; take n; thus n = (Partial_Sums(Length s)).k - len(s.k) + m - 1; consider k2,m2 be Nat such that A4: m2 in dom(s.k2) & (Partial_Sums(Length s)).k2 - len(s.k2) + m2 - 1 = n & (joined_seq s).n = (s.k2).m2 by Def4; m = m2 & k = k2 by A0,A4,Th10; hence (joined_seq s).n = (s.k).m by A4; end; theorem Th14: for D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y st ( for n,m be Nat st n <> m holds union rng(F.n) misses union rng(F.m) ) & ( for n be Nat holds F.n is disjoint_valued) holds (joined_FinSeq F) is disjoint_valued proof let D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y; assume that A1: for n,m be Nat st n <> m holds union rng(F.n) misses union rng(F.m) and A2: for n be Nat holds F.n is disjoint_valued; now let x,y be object; assume A3: x <> y; per cases; suppose A4: x in dom(joined_FinSeq F) & y in dom(joined_FinSeq F); then reconsider n1=x, n2=y as Nat; consider k1,m1 be Nat such that A5: 1<=m1 & m1<=len(F.(k1+1)) & k1 {} by XBOOLE_0:def 7; then consider z be object such that A10: z in (joined_FinSeq F).x /\ (joined_FinSeq F).y by XBOOLE_0:def 1; z in (joined_FinSeq F).x & z in (joined_FinSeq F).y by A10,XBOOLE_0:def 4; then z in union rng(F.(k1+1)) & z in union rng(F.(k2+1)) by A8,TARSKI:def 4; then A11: k1+1 = k2+1 by A1,XBOOLE_0:3; (F.(k1+1)) is disjoint_valued by A2; hence contradiction by A5,A6,A3,A9,A11,PROB_2:def 2; end; hence (joined_FinSeq F).x misses (joined_FinSeq F).y; end; suppose not x in dom(joined_FinSeq F) or not y in dom(joined_FinSeq F); then (joined_FinSeq F).x = {} or (joined_FinSeq F).y = {} by FUNCT_1:def 2; hence (joined_FinSeq F).x misses (joined_FinSeq F).y by XBOOLE_1:65; end; end; hence joined_FinSeq F is disjoint_valued by PROB_2:def 2; end; theorem Th15: for D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y holds rng(joined_FinSeq F) = union {rng(F.n) where n is Nat : n in dom F} proof let D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y; now let x be object; assume x in rng(joined_FinSeq F); then consider n be object such that A1: n in dom(joined_FinSeq F) & x = (joined_FinSeq F).n by FUNCT_1:def 3; reconsider n as Nat by A1; consider k,m be Nat such that A2: 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)) & (joined_FinSeq F).n = (F.(k+1)).m by A1,Def2; 1 <= k+1 & k+1 <= len F by A2,NAT_1:11,13; then A3: k+1 in dom F by FINSEQ_3:25; m in dom(F.(k+1)) by A2,FINSEQ_3:25; then A4: x in rng(F.(k+1)) by A1,A2,FUNCT_1:3; rng(F.(k+1)) in {rng(F.n) where n is Nat: n in dom F} by A3; hence x in union{rng(F.n) where n is Nat: n in dom F} by A4,TARSKI:def 4; end; then A5:rng(joined_FinSeq F) c= union {rng(F.n) where n is Nat : n in dom F} by TARSKI:def 3; now let x be object; assume x in union{rng(F.n) where n is Nat: n in dom F}; then consider A be set such that A6: x in A & A in {rng(F.n) where n is Nat: n in dom F} by TARSKI:def 4; consider k be Nat such that A7: A = rng(F.k) & k in dom F by A6; consider m be object such that A8: m in dom(F.k) & x = (F.k).m by A6,A7,FUNCT_1:def 3; reconsider m as Nat by A8; A9: 1 <= k & k <= len F by A7,FINSEQ_3:25; reconsider k1 = k-1 as Nat by A7,FINSEQ_3:25,NAT_1:21; set n = m + Sum Length(F|k1); Length(F|(k1+1)) = Length(F|k1) ^ <*len(F.(k1+1))*> by Th2,A9,NAT_1:13; then A11:Sum Length(F|(k1+1)) = Sum Length(F|k1) + len(F.(k1+1)) by RVSUM_1:74; A14:1 <= m & m <= len(F.(k1+1)) by A8,FINSEQ_3:25; then A12:n <= Sum Length(F|(k1+1)) by A11,XREAL_1:6; Sum Length(F|(k1+1)) <= Sum Length(F|(len F)) by A9,Th5; then n <= Sum Length(F|(len F)) by A12,XXREAL_0:2; then n <= Sum Length F by FINSEQ_1:58; then A13:n <= len (joined_FinSeq F) by Def2; m <= n by NAT_1:11; then 1 <= n by A14,XXREAL_0:2; then A17:n in dom (joined_FinSeq F) by A13,FINSEQ_3:25; then consider k2,m2 be Nat such that A15: 1 <= m2 & m2 <= len(F.(k2+1)) & k2 < len F & m2 + Sum Length(F|k2) = n & n <= Sum Length(F|(k2+1)) & (joined_FinSeq F).n = (F.(k2+1)).m2 by Def2; m = m2 & k1 = k2 by A14,A15,A12,Th6; hence x in rng(joined_FinSeq F) by A8,A15,A17,FUNCT_1:3; end; then union {rng(F.n) where n is Nat:n in dom F} c= rng(joined_FinSeq F) by TARSKI:def 3; hence thesis by A5,XBOOLE_0:def 10; end; begin :: Extended real valued matrix definition let x be ext-real number; redefine func <*x*> -> FinSequence of ExtREAL; coherence proof now let y be object; assume y in rng <*x*>; then y in {x} by FINSEQ_1:39; hence y in ExtREAL by XXREAL_0:def 1; end; hence thesis by TARSKI:def 3,FINSEQ_1:def 4; end; end; definition let e be FinSequence of ExtREAL*; func Sum e -> FinSequence of ExtREAL means :Def5: len it = len e & for k be Nat st k in dom it holds it.k = Sum(e.k); existence proof deffunc f(Nat) = Sum(e.$1); consider e1 be FinSequence of ExtREAL such that A1: len e1 = len e & for k be Nat st k in dom e1 holds e1.k = f(k) from FINSEQ_2:sch 1; take e1; thus thesis by A1; end; uniqueness proof let e1,e2 be FinSequence of ExtREAL such that A2: len e1 = len e and A3: for k be Nat st k in dom e1 holds e1.k = Sum(e.k) and A4: len e2 = len e and A5: for k be Nat st k in dom e2 holds e2.k = Sum(e.k); dom e1 = dom e2 & for k be Nat st k in dom e1 holds e1.k = e2.k proof thus A6: dom e1 = Seg len e by A2,FINSEQ_1:def 3 .= dom e2 by A4,FINSEQ_1:def 3; let k be Nat such that A7: k in dom e1; thus e1.k = Sum(e.k) by A3,A7 .= e2.k by A5,A6,A7; end; hence thesis by FINSEQ_1:13; end; end; definition let M be Matrix of ExtREAL; func SumAll M -> Element of ExtREAL equals Sum Sum M; coherence; end; theorem Th16: for M be Matrix of ExtREAL holds len Sum M = len M & for i be Nat st i in Seg len M holds (Sum M).i=Sum Line(M,i) proof let M be Matrix of ExtREAL; thus len Sum M = len M by Def5; thus for k be Nat st k in Seg len M holds (Sum M).k=Sum Line(M,k) proof let k be Nat such that A1: k in Seg len M; A2: k in dom M by A1,FINSEQ_1:def 3; k in Seg len Sum M by A1,Def5; then k in dom Sum M by FINSEQ_1:def 3; hence (Sum M).k = Sum(M.k) by Def5 .= Sum(Line(M,k)) by A2,MATRIX_0:60; end; end; theorem Th17: for F be FinSequence of ExtREAL st for i be Nat st i in dom F holds F.i <> -infty holds Sum F <> -infty proof let F be FinSequence of ExtREAL; assume A1: for i be Nat st i in dom F holds F.i <> -infty; consider f be Function of NAT,ExtREAL such that A2: Sum F = f.(len F) & f.0 = 0 & for i be Nat st i < len F holds f.(i+1) = f.i + F.(i+1) by EXTREAL1:def 2; defpred P[Nat] means $1 <= len F implies f.$1 <> -infty; A4:P[0] by A2; A5:for j be Nat st P[j] holds P[j+1] proof let j be Nat; assume A6: P[j]; now assume B2: j+1 <= len F; then A8: f.(j+1) = f.j + F.(j+1) by A2,NAT_1:13; 1 <= j+1 by NAT_1:11; then F.(j+1) <> -infty by A1,B2,FINSEQ_3:25; hence f.(j+1) <> -infty by A8,A6,B2,NAT_1:13,XXREAL_3:17; end; hence P[j+1]; end; for i be Nat holds P[i] from NAT_1:sch 2(A4,A5); hence Sum F <> -infty by A2; end; theorem Th18: for F,G,H be FinSequence of ExtREAL st not -infty in rng F & not -infty in rng G & 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: not -infty in rng F & not -infty in rng G and A3: dom F = dom G and A4: H = F + G; B1:for y be object st y in rng F holds not y in {-infty} by A1,TARSKI:def 1; then A7:F"{-infty} = {} by XBOOLE_0:3,RELAT_1:138; B2:for y be object st y in rng G holds not y in {-infty} by A1,TARSKI:def 1; then A10: G"{-infty} = {} by XBOOLE_0:3,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 Function of NAT,ExtREAL such that A13: Sum H = h.(len H) & h.0 = 0. & for i be Nat st i < len H holds h.(i+1) = h.i + H.(i+1) by EXTREAL1:def 2; consider f be Function of NAT,ExtREAL such that A16: Sum F = f.(len F) & f.0 = 0. & for i be Nat st i < len F holds f.(i+1) = f.i + F.(i+1) by EXTREAL1:def 2; consider g be Function of NAT,ExtREAL such that A19: Sum G = g.(len G) & g.0 = 0. & 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 be Nat st P[k] holds P[k + 1] proof let k be Nat; assume A24: P[k]; assume A25: k+1 <= len H; A26:k < len H by A25,NAT_1:13; A27:f.(k+1) = f.k + F.(k+1) & g.(k+1) = g.k + G.(k+1) by A16,A19,A12,A22,A25,NAT_1:13; A28:k+1 in dom H by A25,NAT_1:11,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; then m+1 in dom H by NAT_1:11,FINSEQ_3:25; then not F.(m+1) in {-infty} by B1,A11,FUNCT_1:3; then A33: F.(m+1) <> -infty by TARSKI:def 1; f.(m+1) = f.m + F.(m+1) by A12,A16,A32,NAT_1:13; hence thesis by A33,A32,NAT_1:13,A31,XXREAL_3:17; end; A34: Pf[0] by A16; 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; then m+1 in dom H by NAT_1:11,FINSEQ_3:25; then not G.(m+1) in {-infty} by B2,A11,A3,FUNCT_1:3; then A38: G.(m+1) <> -infty by TARSKI:def 1; g.(m+1) = g.m + G.(m+1) by A19,A22,A37,NAT_1:13; hence thesis by A38,A37,NAT_1:13,A36,XXREAL_3:17; end; A39: Pg[0] by A19; 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,A11,A28,FUNCT_1:3; thus thesis by A1,A3,A11,A28,FUNCT_1:3; 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 A13,A24,A25,NAT_1:13 .= (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 A16,A19,A13; for i be Nat holds P[i] from NAT_1:sch 2(A42,A23); hence thesis by A16,A19,A13,A12,A22; end; theorem Th19: for r be R_eal, F be FinSequence of ExtREAL holds Sum(F^<*r*>) = Sum F + r proof let r be R_eal, F be FinSequence of ExtREAL; consider f be Function of NAT,ExtREAL such that A1: Sum(F^<*r*>) = f.(len (F^<*r*>)) & f.0 = 0 & for i be Nat st i < len (F^<*r*>) holds f.(i+1) = f.i + (F^<*r*>).(i+1) by EXTREAL1:def 2; consider g be Function of NAT,ExtREAL such that A2: Sum F = g.(len F) & g.0 = 0 & for i be Nat st i < len F holds g.(i+1) = g.i + F.(i+1) by EXTREAL1:def 2; len (F^<*r*>) = len F + len <*r*> by FINSEQ_1:22; then B1:len (F^<*r*>) = len F + 1 by FINSEQ_1:39; then B2:len F < len (F^<*r*>) by NAT_1:13; defpred P[Nat] means $1 <= len F implies f.$1 = g.$1; A3:P[0] by A1,A2; A4:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A5: P[k]; assume A6: k+1 <= len F; then A7: k < len F by NAT_1:13; A9: (F^<*r*>).(k+1) = F.(k+1) by A6,FINSEQ_1:64,NAT_1:11; k < len (F^<*r*>) by A7,B1,NAT_1:13; then f.(k+1) = f.k + (F^<*r*>).(k+1) by A1; hence f.(k+1) = g.(k+1) by A2,A6,A5,A9,NAT_1:13; end; for i be Nat holds P[i] from NAT_1:sch 2(A3,A4); then f.(len F) = g.(len F); then f.(len F + 1) = g.(len F) + (F^<*r*>).(len F+1) by A1,B2; hence Sum(F^<*r*>) = Sum F + r by A1,A2,B1,FINSEQ_1:42; end; theorem Th20: for r be R_eal, i be Nat st r is real holds Sum(i |-> r) = i*r proof let r be R_eal, i be Nat; assume A0: r is real; defpred P[Nat] means Sum($1 |->r) = $1*r; A1:for i be Nat st P[i] holds P[i+1] proof let i be Nat such that A2: Sum(i |-> r) = i*r; reconsider i1 = i, One = 1 as ext-real number; thus Sum((i+1) |-> r) = Sum((i |-> r)^<*r*>) by FINSEQ_2:60 .= i*r + r by A2,Th19 .= i*r + 1*r by XXREAL_3:81 .= (i1+One)*r by A0,XXREAL_3:95 .= (i+1)*r by XXREAL_3:def 2; end; A3:P[0] by EXTREAL1:7,FINSEQ_2:58; for i be Nat holds P[i] from NAT_1:sch 2(A3,A1); hence thesis; end; theorem Th21: for M be Matrix of ExtREAL st len M = 0 holds SumAll M = 0 proof let M be Matrix of ExtREAL; assume len M = 0; then len Sum M = 0 by Def5; then Sum M is empty; hence thesis by EXTREAL1:7; end; theorem Th22: for m be Nat, M be Matrix of m,0,ExtREAL holds SumAll M = 0 proof let m be Nat, M be Matrix of m,0,ExtREAL; per cases; suppose m = 0; then len M = 0 by MATRIX_0:def 2; hence thesis by Th21; end; suppose m > 0; then len M > 0 by MATRIX_0:def 2; then reconsider k = len Sum M as non zero Nat by Def5; reconsider Z = 0. as R_eal; for k be Nat st k in dom Sum M holds (Sum M).k = 0 proof len M = len Sum M by Def5; then A2: dom M = dom Sum M by FINSEQ_3:29; hereby let k be Nat; assume A3: k in dom Sum M; then M.k in rng M by A2,FUNCT_1:def 3; then M.k = <*>ExtREAL by MATRIX_0:def 2; hence (Sum M).k = 0 by A3,Def5,EXTREAL1:7; end; end; then Sum M = k |-> 0. by MATRPROB:1; then SumAll M = (len Sum M) * Z by Th20; hence SumAll M = 0; end; end; theorem Th23: for n,m,k be Nat, M1 be Matrix of n,k,ExtREAL, M2 be Matrix of m,k,ExtREAL holds Sum (M1^M2) = (Sum M1)^(Sum M2) proof let n,m,k be Nat; let M1 be Matrix of n,k,ExtREAL; let M2 be Matrix of m,k,ExtREAL; A1:dom Sum(M1^M2) = Seg len Sum(M1^M2) by FINSEQ_1:def 3; A2:now let i be Nat; assume A3: i in dom Sum(M1^M2); then i in Seg len (M1^M2) by A1,Def5; then A4: i in dom (M1^M2) by FINSEQ_1:def 3; A8: len M1 = len Sum M1 & len M2 = len Sum M2 by Def5; then A6: dom M1 = dom Sum M1 & dom M2 = dom Sum M2 by FINSEQ_3:29; per cases by A4,FINSEQ_1:25; suppose A5: i in dom M1; thus Sum(M1^M2).i = Sum ((M1^M2).i) by A3,Def5 .= Sum (M1.i) by A5,FINSEQ_1:def 7 .= (Sum M1).i by A5,A6,Def5 .= ((Sum M1)^(Sum M2)).i by A5,A6,FINSEQ_1:def 7; end; suppose ex n be Nat st n in dom M2 & i = len M1 + n; then consider n be Nat such that A10: n in dom M2 & i = len M1 + n; thus Sum(M1^M2).i = Sum ((M1^M2).i) by A3,Def5 .= Sum (M2.n) by A10,FINSEQ_1:def 7 .= (Sum M2).n by A10,A6,Def5 .= ((Sum M1)^(Sum M2)).i by A10,A8,A6,FINSEQ_1:def 7; end; end; len Sum(M1^M2) = len (M1^M2) by Def5 .= len M1 + len M2 by FINSEQ_1:22 .= len Sum M1 + len M2 by Def5 .= len Sum M1 + len Sum M2 by Def5 .= len ((Sum M1)^(Sum M2)) by FINSEQ_1:22; hence thesis by A2,FINSEQ_2:9; end; theorem Th24: for M1,M2 be Matrix of ExtREAL st (for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) & (for i be Nat st i in dom M2 holds not -infty in rng (M2.i) ) holds Sum M1 + Sum M2 = Sum (M1 ^^ M2) proof let M1,M2 be Matrix of ExtREAL; reconsider M = min(len M1,len M2) as Element of NAT; assume B0: (for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) & (for i be Nat st i in dom M2 holds not -infty in rng (M2.i) ); now assume -infty in rng (Sum M1); then consider i be Nat such that C1: i in dom Sum M1 & (Sum M1).i = -infty by FINSEQ_2:10; i in Seg len Sum M1 by C1,FINSEQ_1:def 3; then i in Seg len M1 by Def5; then i in dom M1 by FINSEQ_1:def 3; then C2: not -infty in rng (M1.i) by B0; (Sum M1).i = Sum(M1.i) by C1,Def5; then ex j be Nat st j in dom (M1.i) & (M1.i).j = -infty by C1,Th17; hence contradiction by C2,FUNCT_1:3; end; then D1:(Sum M1)"{-infty} = {} by FUNCT_1:72; now assume -infty in rng (Sum M2); then consider i be Nat such that C1: i in dom Sum M2 & (Sum M2).i = -infty by FINSEQ_2:10; i in Seg len Sum M2 by C1,FINSEQ_1:def 3; then i in Seg len M2 by Def5; then i in dom M2 by FINSEQ_1:def 3; then C2: not -infty in rng (M2.i) by B0; (Sum M2).i = Sum(M2.i) by C1,Def5; then ex j be Nat st j in dom (M2.i) & (M2.i).j = -infty by C1,Th17; hence contradiction by C2,FUNCT_1:3; end; then (Sum M2)"{-infty} = {} by FUNCT_1:72; then D2:dom Sum M1 /\ dom Sum M2 =(dom Sum M1 /\ dom Sum M2) \ (((Sum M1)"{-infty} /\ (Sum M2)"{+infty}) \/ ((Sum M2)"{-infty} /\ (Sum M1)"{+infty})) by D1; A1:Seg M = Seg len M1 /\ Seg len M2 by FINSEQ_2:2 .= Seg len M1 /\ dom M2 by FINSEQ_1:def 3 .= dom M1 /\ dom M2 by FINSEQ_1:def 3 .= dom (M1 ^^ M2) by PRE_POLY:def 4 .= Seg len (M1 ^^ M2) by FINSEQ_1:def 3; A0:dom Sum M1 = Seg(len Sum M1) & dom Sum M2 = Seg(len Sum M2) by FINSEQ_1:def 3; dom(Sum M1 + Sum M2) = dom Sum M1 /\ dom Sum M2 by D2,MESFUNC1:def 3; then K1:dom(Sum M1 + Sum M2) = Seg min(len Sum M1,len Sum M2) by A0,FINSEQ_2:2; then reconsider SM12 = Sum M1 + Sum M2 as FinSequence by FINSEQ_1:def 2; len SM12 = min(len Sum M1,len Sum M2) by K1,FINSEQ_1:def 3; then A2:len SM12 = min(len M1,len Sum M2) by Def5 .= min(len M1,len M2) by Def5 .= len (M1 ^^ M2) by A1,FINSEQ_1:6 .= len Sum(M1 ^^ M2) by Def5; A3:dom (Sum M1 + Sum M2) = Seg len SM12 by FINSEQ_1:def 3; now let i be Nat; assume A4: i in dom (Sum M1 + Sum M2); then i in Seg len SM12 by FINSEQ_1:def 3; then i in Seg len(M1 ^^ M2) by A2,Def5; then A6: i in dom (M1 ^^ M2) by FINSEQ_1:def 3; then i in dom M1 /\ dom M2 by PRE_POLY:def 4; then B1: i in dom M1 & i in dom M2 by XBOOLE_0:def 4; then i in Seg len M1 & i in Seg len M2 by FINSEQ_1:def 3; then i in Seg len Sum M1 & i in Seg len Sum M2 by Def5; then A8: i in dom Sum M1 & i in dom Sum M2 by FINSEQ_1:def 3; A10:i in dom Sum(M1 ^^ M2) by A2,A3,A4,FINSEQ_1:def 3; A11:((M1.i) ^ (M2.i)) = (M1 ^^ M2).i by A6,PRE_POLY:def 4; B3: not -infty in rng (M1.i) & not -infty in rng (M2.i) by B0,B1; thus (Sum M1 + Sum M2).i = (Sum M1).i + (Sum M2).i by A4,MESFUNC1:def 3 .= Sum (M1.i) + (Sum M2.i) by A8,Def5 .= Sum (M1.i) + Sum (M2.i) by A8,Def5 .= Sum ((M1 ^^ M2).i) by A11,B3,EXTREAL1:10 .= (Sum(M1 ^^ M2)).i by A10,Def5; end; hence thesis by A2,FINSEQ_2:9; end; theorem Th25: for M1,M2 be Matrix of ExtREAL st len M1 = len M2 & (for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) & (for i be Nat st i in dom M2 holds not -infty in rng (M2.i) ) holds SumAll M1 + SumAll M2 = SumAll(M1 ^^ M2) proof let M1,M2 be Matrix of ExtREAL such that A1: len M1 = len M2 & (for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) & (for i be Nat st i in dom M2 holds not -infty in rng (M2.i) ); A2:len Sum M1 = len M1 by Def5 .= len Sum M2 by A1,Def5; then reconsider p1=Sum M1, p2 = Sum M2 as Element of (len Sum M1)-tuples_on ExtREAL by FINSEQ_2:92; C0:now assume -infty in rng (Sum M1); then consider i be Nat such that C1: i in dom Sum M1 & (Sum M1).i = -infty by FINSEQ_2:10; i in Seg len Sum M1 by C1,FINSEQ_1:def 3; then i in Seg len M1 by Def5; then i in dom M1 by FINSEQ_1:def 3; then C2: not -infty in rng (M1.i) by A1; (Sum M1).i = Sum(M1.i) by C1,Def5; then ex j be Nat st j in dom (M1.i) & (M1.i).j = -infty by C1,Th17; hence contradiction by C2,FUNCT_1:3; end; A3:now assume -infty in rng (Sum M2); then consider i be Nat such that C1: i in dom Sum M2 & (Sum M2).i = -infty by FINSEQ_2:10; i in Seg len Sum M2 by C1,FINSEQ_1:def 3; then i in Seg len M2 by Def5; then i in dom M2 by FINSEQ_1:def 3; then C2: not -infty in rng (M2.i) by A1; (Sum M2).i = Sum(M2.i) by C1,Def5; then ex j be Nat st j in dom (M2.i) & (M2.i).j = -infty by C1,Th17; hence contradiction by C2,FUNCT_1:3; end; A4:dom Sum M1 = dom Sum M2 by A2,FINSEQ_3:29; Sum (M1 ^^ M2) = Sum M1 + Sum M2 by A1,Th24; hence SumAll M1 + SumAll M2 = SumAll(M1 ^^ M2) by A3,C0,A4,Th18; end; theorem Th26: for p be FinSequence of ExtREAL st not -infty in rng p holds SumAll <*p*> = SumAll(<*p*>@) proof defpred x[FinSequence of ExtREAL] means not -infty in rng $1 implies SumAll <*$1*> = SumAll(<*$1*>@); let p be FinSequence of ExtREAL; assume B0: not -infty in rng p; A2:for p be FinSequence of ExtREAL, x be Element of ExtREAL st x[p] holds x[p^<*x*>] proof let p be FinSequence of ExtREAL, x be Element of ExtREAL such that A3: not -infty in rng p implies SumAll <*p*> = SumAll (<*p*>@); assume not -infty in rng (p^<*x*>); then not -infty in rng p \/ rng <*x*> by FINSEQ_1:31; then B3: not -infty in rng p & not -infty in rng <*x*> by XBOOLE_0:def 3; Seg len (<*p*> ^^ <*<*x*>*>) = dom (<*p*> ^^ <*<*x*>*>) by FINSEQ_1:def 3 .= dom <*p*> /\ dom <*<*x*>*> by PRE_POLY:def 4 .= Seg 1 /\ dom <*<*x*>*> by FINSEQ_1:38 .= Seg 1 /\ Seg 1 by FINSEQ_1:38 .= Seg 1; then A4: len (<*p*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6 .= len <*p^<*x*>*> by FINSEQ_1:39; A5: dom <*p^<*x*>*> = Seg len <*p^<*x*>*> by FINSEQ_1:def 3; A6: now let i be Nat; reconsider M1 = <*p*>.i,M2 = <*<*x*>*>.i as FinSequence; assume A7: i in dom <*p^<*x*>*>; then A8: i = 1 by FINSEQ_1:90; i in dom (<*p*> ^^ <*<*x*>*>) by A4,A5,A7,FINSEQ_1:def 3; hence (<*p*> ^^ <*<*x*>*>).i = M1 ^ M2 by PRE_POLY:def 4 .= p ^ M2 by A8,FINSEQ_1:40 .= p ^ <*x*> by A8,FINSEQ_1:40 .= <*p^<*x*>*>.i by A8,FINSEQ_1:40; end; per cases; suppose len p = 0; then A9: p = {}; hence SumAll <*p^<*x*>*> = SumAll <*<*x*>*> by FINSEQ_1:34 .= SumAll (<*<*x*>*>@) by MATRLIN:15 .= SumAll (<*p^<*x*>*>@) by A9,FINSEQ_1:34; end; suppose A10: len p <> 0; A11: len <*<*x*>*> = 1 & len <*p*> = 1 & len <*x*> = 1 by FINSEQ_1:40; then A12: width <*<*x*>*> = 1 & width <*p*> = len p by MATRIX_0:20; then A16: len (<*p*>@) = len p by MATRIX_0:def 6; P5: width (<*p*>@) = 1 by A10,A11,A12,MATRIX_0:29; then reconsider d1 = <*p*>@ as Matrix of len p,1,ExtREAL by A10,A16,MATRIX_0:20; A13: len (<*<*x*>*>@) = 1 by A12,MATRIX_0:54; PP5: width (<*<*x*>*>@) = 1 by A11,A12,MATRIX_0:29; then reconsider d2 = <*<*x*>*>@ as Matrix of 1,1,ExtREAL by A13,MATRIX_0:20; len <*p^<*x*>*> = 1 by FINSEQ_1:40; then A18: width <*p^<*x*>*> = len (p^<*x*>) by MATRIX_0:20 .= len p + 1 by A11,FINSEQ_1:22; A19: (<*<*x*>*>@)@ = <*<*x*>*> by A11,A12,MATRIX_0:57; width (<*p*>@) = width(<*<*x*>*>@) by P5,A11,A12,MATRIX_0:29; then A21: (d1 ^ d2)@ = ((<*p*>@)@) ^^ ((<*<*x*>*>@)@) by MATRLIN:28 .= <*p*> ^^ <*<*x*>*> by A10,A11,A12,A19,MATRIX_0:57 .= <*p^<*x*>*> by A4,A6,FINSEQ_2:9 .= (<*p^<*x*>*>@)@ by A18,MATRIX_0:57; A22: len ((<*p*>@) ^ (<*<*x*>*>@)) = len (<*p*>@) + len (<*<*x*>*>@) by FINSEQ_1:22 .= width <*p*> + len (<*<*x*>*>@) by MATRIX_0:def 6 .= width <*p*> + width <*<*x*>*> by MATRIX_0:def 6 .= len (<*p^<*x*>*>@) by A12,A18,MATRIX_0:def 6; B4: now let i be Nat; assume i in dom <*p*>; then i = 1 by FINSEQ_1:90; hence not -infty in rng (<*p*>.i) by B3,FINSEQ_1:def 8; end; B5: now let i be Nat; assume i in dom <*<*x*>*>; then i = 1 by FINSEQ_1:90; hence not -infty in rng (<*<*x*>*>.i) by B3,FINSEQ_1:def 8; end; dom <*p*> = Seg 1 by FINSEQ_1:38; then 1 in dom <*p*>; then B6: not -infty in rng (<*p*>.1) by B4; then T6: not -infty in rng p by FINSEQ_1:def 8; for x be object st x in dom (Sum d1) holds (Sum d1).x <> -infty proof let x be object; assume P1: x in dom(Sum d1); then reconsider i = x as Nat; P2: (Sum d1).x = Sum(d1.i) by P1,Def5; 1 <= i & i <= len (Sum d1) by P1,FINSEQ_3:25; then P3: 1 <= i & i <= len d1 by Def5; then i in dom p by A16,FINSEQ_3:25; then R10: p.i <> -infty by T6,FUNCT_1:3; i in dom d1 by P3,FINSEQ_3:25; then P4: d1.i = Line(d1,i) by MATRIX_0:60; dom d1 = Seg len p by A16,FINSEQ_1:def 3; then R2: Indices d1 = [: Seg len p, {1} :] by P5,FINSEQ_1:2,MATRIX_0:def 4; R3: i in Seg len p by P3,A16; for j be Nat st j in dom Line(d1,i) holds Line(d1,i).j <> -infty proof let j be Nat; assume j in dom Line(d1,i); then 1 <= j & j <= len Line(d1,i) by FINSEQ_3:25; then 1 <= j & j <= width d1 by MATRIX_0:def 7; then P6: j in Seg width d1; then R4: [i,j] in [: Seg len p, {1}:] by P5,R3,FINSEQ_1:2,ZFMISC_1:def 2; then [j,i] in Indices (d1@) by R2,MATRIX_0:def 6; then consider F be FinSequence of ExtREAL such that R7: F = (d1@).j & (d1@)*(j,i) = F.i by MATRIX_0:def 5; F = <*p*>.j by A10,A12,R7,A11,MATRIX_0:57; then F = <*p*>.1 by P5,P6,FINSEQ_1:2,TARSKI:def 1; then R9: F = p by FINSEQ_1:def 8; Line(d1,i).j = (<*p*>@)*(i,j) by P6,MATRIX_0:def 7; hence Line(d1,i).j <> -infty by R7,R9,R10,R2,R4,MATRIX_0:def 6; end; hence (Sum d1).x <> -infty by P2,P4,Th17; end; then B7: not -infty in rng Sum d1 by FUNCT_1:def 3; for z be object st z in dom (Sum d2) holds (Sum d2).z <> -infty proof let z be object; assume P1: z in dom(Sum d2); then reconsider i = z as Nat; P2: (Sum d2).z = Sum(d2.i) by P1,Def5; 1 <= i & i <= len (Sum d2) by P1,FINSEQ_3:25; then P3: 1 <= i & i <= len d2 by Def5; then R1: 1 <= i & i <= len <*x*> by A13,FINSEQ_1:40; then i in dom <*x*> by FINSEQ_3:25; then R10: <*x*>.i <> -infty by B3,FUNCT_1:3; i in dom d2 by P3,FINSEQ_3:25; then P4: d2.i = Line(d2,i) by MATRIX_0:60; dom d2 = Seg len <*x*> by A13,FINSEQ_1:def 3,40; then R2: Indices d2 = [: Seg len <*x*>, {1} :] by PP5,FINSEQ_1:2,MATRIX_0:def 4; R3: i in Seg len <*x*> by R1; for j be Nat st j in dom Line(d2,i) holds Line(d2,i).j <> -infty proof let j be Nat; assume j in dom Line(d2,i); then 1 <= j & j <= len Line(d2,i) by FINSEQ_3:25; then 1 <= j & j <= width d2 by MATRIX_0:def 7; then P6: j in Seg width d2; then R4: [i,j] in [: Seg len <*x*>, {1} :] by PP5,R3,FINSEQ_1:2,ZFMISC_1:def 2; then [j,i] in Indices(d2@) by R2,MATRIX_0:def 6; then consider F be FinSequence of ExtREAL such that R7: F = (d2@).j & (d2@)*(j,i) = F.i by MATRIX_0:def 5; F = <*<*x*>*>.j by A12,R7,A11,MATRIX_0:57; then F = <*<*x*>*>.1 by PP5,P6,FINSEQ_1:2,TARSKI:def 1; then R9: F = <*x*> by FINSEQ_1:def 8; Line(d2,i).j = ( <*<*x*>*>@ )*(i,j) by P6,MATRIX_0:def 7; hence Line(d2,i).j <> -infty by R7,R9,R10,R2,R4,MATRIX_0:def 6; end; hence (Sum d2).z <> -infty by P2,P4,Th17; end; then B8: not -infty in rng Sum d2 by FUNCT_1:def 3; thus SumAll <*p^<*x*>*> = SumAll (<*p*> ^^ <*<*x*>*>) by A4,A6,FINSEQ_2:9 .= SumAll (<*p*>) + SumAll <*<*x*>*> by A11,B4,B5,Th25 .= SumAll (<*p*>@) + SumAll (<*<*x*>*>@) by A3,B6,FINSEQ_1:def 8,MATRLIN:15 .= Sum (Sum d1 ^ Sum d2) by B7,B8,EXTREAL1:10 .= SumAll (d1 ^ d2) by Th23 .= SumAll (<*p^<*x*>*>@) by A22,A21,MATRIX_0:53; end; end; A23:x[<*>(ExtREAL)] proof reconsider M1 = <* <*>(ExtREAL) *> as Matrix of 1,0,ExtREAL by MATRIX_0:14; len M1 = 1 by MATRIX_0:def 2; then width M1 = 0 by MATRIX_0:20; then A24:len (M1@) = 0 by MATRIX_0:def 6; SumAll M1 = 0 by Th22; hence thesis by A24,Th21; end; for p be FinSequence of ExtREAL holds x[p] from FINSEQ_2:sch 2(A23,A2); hence thesis by B0; end; theorem Th27: for p be ext-real number, M be Matrix of ExtREAL st (for i be Nat st i in dom M holds not p in rng (M.i)) holds (for j be Nat st j in dom (M@) holds not p in rng((M@).j)) proof let p be ext-real number; let M be Matrix of ExtREAL; assume A1: for i be Nat st i in dom M holds not p in rng (M.i); hereby let j be Nat; assume A2: j in dom(M@); then A3: M@.j = Line(M@,j) by MATRIX_0:60; j in Seg len (M@) by A2,FINSEQ_1:def 3; then j in Seg width M by MATRIX_0:def 6; then A5: Line(M@,j) = Col(M,j) by MATRIX_0:59; for v be object st v in dom Line(M@,j) holds Line(M@,j).v <> p proof let v be object; assume A6: v in dom Line(M@,j); then reconsider i = v as Element of NAT; 1 <= i & i <= len Line(M@,j) by A6,FINSEQ_3:25; then 1 <= i & i <= width (M@) by MATRIX_0:def 7; then i in Seg width (M@); then [j,i] in [:dom(M@),Seg width(M@):] by A2,ZFMISC_1:def 2; then [j,i] in Indices (M@) by MATRIX_0:def 4; then A7: [i,j] in Indices M by MATRIX_0:def 6; then A8: i in dom M & j in dom (M.i) by MATRPROB:13; then Line(M@,j).v = M*(i,j) by A5,MATRIX_0:def 8; then Line(M@,j).v = (M.i).j by A7,MATRPROB:14; then Line(M@,j).v in rng (M.i) by A8,FUNCT_1:3; hence Line(M@,j).v <> p by A1,A7,MATRPROB:13; end; hence not p in rng (M@.j) by A3,FUNCT_1:def 3; end; end; theorem Th28: for M be Matrix of ExtREAL st (for i be Nat st i in dom M holds not -infty in rng (M.i)) holds SumAll M = SumAll(M@) proof let M be Matrix of ExtREAL; assume A0: for i be Nat st i in dom M holds not -infty in rng (M.i); defpred x[Nat] means for M be Matrix of ExtREAL st len M = $1 & (for i be Nat st i in dom M holds not -infty in rng (M.i)) holds SumAll M = SumAll (M@); A1:for n be Nat st x[n] holds x[n+1] proof let n be Nat; assume A2: for M be Matrix of ExtREAL st len M = n & (for i be Nat st i in dom M holds not -infty in rng (M.i)) holds SumAll M = SumAll (M@); thus for M be Matrix of ExtREAL st len M = n+1 & (for i be Nat st i in dom M holds not -infty in rng (M.i)) holds SumAll M = SumAll (M@) proof let M be Matrix of ExtREAL; assume A3: len M = n+1 & (for i be Nat st i in dom M holds not -infty in rng (M.i)); per cases; suppose A4: n = 0; 1 <= len M by A3,NAT_1:11; then A5: not -infty in rng (M.1) by A3,FINSEQ_3:25; M = <*M.1*> by A3,A4,FINSEQ_1:40; hence thesis by A5,Th26; end; suppose A30: n > 0; reconsider M9 = M as Matrix of n+1,width M,ExtREAL by A3,MATRIX_0:20; reconsider M1 = M.(n+1) as FinSequence of ExtREAL; reconsider w = Del(M9,n+1) as Matrix of n,width M,ExtREAL by MATRLIN:3; V1: 1 <= n+1 by NAT_1:11; then M.(n+1) = Line(M,n+1) by A3,FINSEQ_3:25,MATRIX_0:60; then Y11: len M1 = width M by MATRIX_0:def 7; then reconsider r = <*M1*> as Matrix of 1,width M,ExtREAL; A31: width w = width M9 by A30,MATRLIN:2 .= width r by MATRLIN:2; A32: len (w@) = width w by MATRIX_0:def 6 .= len (r@) by A31,MATRIX_0:def 6; A33: len (Del(M,n+1)) = n by A3,PRE_POLY:12; T5: not -infty in rng M1 by V1,A3,FINSEQ_3:25; for v be object st v in dom (Sum w) holds (Sum w).v <> -infty proof let v be object; assume P1: v in dom (Sum w); then reconsider i = v as Nat; P2: (Sum w).v = Sum(w.i) by P1,Def5; 1 <= i & i <= len (Sum w) by P1,FINSEQ_3:25; then P3: 1 <= i & i <= len w by Def5; then S0: 1 <= i & i <= n+1 by A33,NAT_1:12; R1: i in dom w by P3,FINSEQ_3:25; then P4: w.i = Line(w,i) by MATRIX_0:60; for j be Nat st j in dom Line(w,i) holds Line(w,i).j <> -infty proof let j be Nat; assume j in dom Line(w,i); then 1 <= j & j <= len Line(w,i) by FINSEQ_3:25; then 1 <= j & j <= width w by MATRIX_0:def 7; then P6: j in Seg width w; then [i,j] in [:dom w,Seg width w:] by R1,ZFMISC_1:def 2; then [i,j] in Indices w by MATRIX_0:def 4; then consider F be FinSequence of ExtREAL such that R7: F = w.i & w*(i,j) = F.j by MATRIX_0:def 5; M <> {} by A3; then M = Del(M,len M) ^ <*M.(len M)*> by MATRLIN:4; then M.i = w.i by A3,R1,FINSEQ_1:def 7; then S2: not -infty in rng F by R7,A3,S0,FINSEQ_3:25; len F = width w by P4,R7,MATRIX_0:def 7; then j in dom F by P6,FINSEQ_1:def 3; then F.j in rng F by FUNCT_1:3; hence Line(w,i).j <> -infty by R7,S2,P6,MATRIX_0:def 7; end; hence (Sum w).v <> -infty by P2,P4,Th17; end; then L1: not -infty in rng Sum w by FUNCT_1:def 3; for v be object st v in dom (Sum r) holds (Sum r).v <> -infty proof let v be object; assume P1: v in dom (Sum r); then reconsider i = v as Nat; P2: (Sum r).v = Sum(r.i) by P1,Def5; 1 <= i & i <= len (Sum r) by P1,FINSEQ_3:25; then P3: 1 <= i & i <= len r by Def5; then 1 <= i & i <= 1 by FINSEQ_1:40; then i = 1 by XXREAL_0:1; then n+i in Seg (n+1) by FINSEQ_1:4; then S0: n+i in dom M by A3,FINSEQ_1:def 3; R1: i in dom r by P3,FINSEQ_3:25; then P4: r.i = Line(r,i) by MATRIX_0:60; for j be Nat st j in dom Line(r,i) holds Line(r,i).j <> -infty proof let j be Nat; assume j in dom Line(r,i); then 1 <= j & j <= len Line(r,i) by FINSEQ_3:25; then 1 <= j & j <= width r by MATRIX_0:def 7; then P6: j in Seg width r; then [i,j] in [:dom r, Seg width r:] by R1,ZFMISC_1:def 2; then [i,j] in Indices r by MATRIX_0:def 4; then consider F be FinSequence of ExtREAL such that R7: F = r.i & r*(i,j) = F.j by MATRIX_0:def 5; M <> {} by A3; then M = w ^ <*M.(n+1)*> by A3,MATRLIN:4; then M.(n + i) = r.i by A33,R1,FINSEQ_1:def 7; then S2: not -infty in rng F by R7,A3,S0; len F = width r by P4,R7,MATRIX_0:def 7; then j in dom F by P6,FINSEQ_1:def 3; then F.j in rng F by FUNCT_1:3; hence Line(r,i).j <> -infty by R7,S2,P6,MATRIX_0:def 7; end; hence (Sum r).v <> -infty by P2,P4,Th17; end; then T3: not -infty in rng Sum r by FUNCT_1:def 3; T4: for i be Nat st i in dom (Del(M,n+1)) holds not -infty in rng((Del(M,n+1)).i) proof let i be Nat; assume R1: i in dom(Del(M,n+1)); then P4: w.i = Line(w,i) by MATRIX_0:60; 1 <= i & i <= len w by R1,FINSEQ_3:25; then S0: 1 <= i & i <= n+1 by A33,NAT_1:12; for v be object st v in dom Line(w,i) holds Line(w,i).v <> -infty proof let v be object; assume TT0:v in dom Line(w,i); then reconsider j=v as Nat; 1 <= j & j <= len Line(w,i) by TT0,FINSEQ_3:25; then 1 <= j & j <= width w by MATRIX_0:def 7; then P6: j in Seg width w; then [i,j] in [:dom w, Seg width w:] by R1,ZFMISC_1:def 2; then [i,j] in Indices w by MATRIX_0:def 4; then consider F be FinSequence of ExtREAL such that R7: F = w.i & w*(i,j) = F.j by MATRIX_0:def 5; M <> {} by A3; then M = Del(M,len M) ^ <*M.(len M)*> by MATRLIN:4; then M.i = w.i by A3,R1,FINSEQ_1:def 7; then S2: not -infty in rng F by R7,A3,S0,FINSEQ_3:25; len F = width w by P4,R7,MATRIX_0:def 7; then j in dom F by P6,FINSEQ_1:def 3; then F.j in rng F by FUNCT_1:3; hence Line(w,i).v <> -infty by R7,S2,P6,MATRIX_0:def 7; end; hence not -infty in rng((Del(M,n+1)).i) by P4,FUNCT_1:def 3; end; M <> {} by A3; then M = Del(M,len M) ^ <*M.(len M)*> by MATRLIN:4; then H1: M@ = (w@) ^^ (<*M.(n+1)*>)@ by A3,A31,MATRLIN:28; then Q4: dom (M@) = dom (w@) /\ dom((<*M.(n+1)*>)@) by PRE_POLY:def 4; dom (w@) = Seg len (w@) by FINSEQ_1:def 3; then dom (w@) = Seg width w by MATRIX_0:def 6; then dom (w@) = Seg len (<*M.(n+1)*>@) by A31,MATRIX_0:def 6; then Z0: dom (w@) = dom (<*M.(n+1)*>@) by FINSEQ_1:def 3; Y2: len <*M.(n+1)*> = 1 by FINSEQ_1:40; then Z2: width <*M.(n+1)*> = width M by Y11,MATRIX_0:20; T6: for i be Nat st i in dom (w@) holds not -infty in rng (w@.i) proof let i be Nat; assume R1: i in dom (w@); then P4: w@.i = Line(w@,i) by MATRIX_0:60; 1 <= i & i <= len (w@) by R1,FINSEQ_3:25; then 1 <= i & i <= width w by MATRIX_0:def 6; then 1 <= width w by XXREAL_0:2; then V5: 1 <= width M by A30,MATRLIN:2; for v be object st v in dom Line(w@,i) holds Line(w@,i).v <> -infty proof let v be object; assume TT0:v in dom Line(w@,i); then reconsider j = v as Nat; 1 <= j & j <= len Line(w@,i) by TT0,FINSEQ_3:25; then 1 <= j & j <= width (w@) by MATRIX_0:def 7; then P6: j in Seg width (w@); then [i,j] in [:dom (w@), Seg width(w@):] by R1,ZFMISC_1:def 2; then [i,j] in Indices (w@) by MATRIX_0:def 4; then consider F be FinSequence of ExtREAL such that R7: F = (w@).i & (w@)*(i,j) = F.j by MATRIX_0:def 5; width (<*M.(n+1)*>@) = len <*M.(n+1)*> by V5,Z2,MATRIX_0:29; then 1 in Seg width (<*M.(n+1)*>@) by Y2; then [i,1] in [:dom(<*M.(n+1)*>@), Seg width(<*M.(n+1)*>@):] by Z0,R1,ZFMISC_1:87; then [i,1] in Indices (<*M.(n+1)*>@) by MATRIX_0:def 4; then consider G be FinSequence of ExtREAL such that Q7: G = (<*M.(n+1)*>@).i & (<*M.(n+1)*>@)*(i,1) = G.1 by MATRIX_0:def 5; (M@).i = F^G by R7,H1,Z0,Q4,R1,Q7,PRE_POLY:def 4; then not -infty in rng (F^G) by Z0,Q4,R1,A3,Th27; then not -infty in (rng F \/ rng G) by FINSEQ_1:31; then S2: not -infty in rng F & not -infty in rng G by XBOOLE_0:def 3; len F = width (w@) by P4,R7,MATRIX_0:def 7; then j in dom F by P6,FINSEQ_1:def 3; then F.j in rng F by FUNCT_1:3; hence Line(w@,i).v <> -infty by R7,S2,P6,MATRIX_0:def 7; end; hence not -infty in rng (w@.i) by P4,FUNCT_1:def 3; end; T7: for i be Nat st i in dom (r@) holds not -infty in rng (r@.i) proof let i be Nat; assume R1: i in dom (r@); then P4: r@.i = Line(r@,i) by MATRIX_0:60; 1 <= i & i <= len (r@) by R1,FINSEQ_3:25; then 1 <= i & i <= width r by MATRIX_0:def 6; then 1 <= width r by XXREAL_0:2; then M1: 1 <= width M9 by MATRLIN:2; for v be object st v in dom Line(r@,i) holds Line(r@,i).v <> -infty proof let v be object; assume TT0: v in dom Line(r@,i); then reconsider j = v as Nat; 1 <= j & j <= len Line(r@,i) by TT0,FINSEQ_3:25; then 1 <= j & j <= width (r@) by MATRIX_0:def 7; then P6: j in Seg width (r@); then [i,j] in [:dom(r@),Seg width(r@):] by R1,ZFMISC_1:def 2; then [i,j] in Indices (r@) by MATRIX_0:def 4; then consider G be FinSequence of ExtREAL such that R7: G = (r@).i & (r@)*(i,j) = G.j by MATRIX_0:def 5; 1 <= width w by A30,M1,MATRLIN:2; then width (w@) = len w by MATRIX_0:29; then n in Seg width (w@) by A30,A33,FINSEQ_1:3; then [i,n] in [:dom(w@),Seg width(w@):] by Z0,R1,ZFMISC_1:87; then [i,n] in Indices (w@) by MATRIX_0:def 4; then consider F be FinSequence of ExtREAL such that Q7: F = (w@).i & (w@)*(i,n) = F.n by MATRIX_0:def 5; (M@).i = F^G by R7,H1,Z0,Q4,R1,Q7,PRE_POLY:def 4; then not -infty in rng (F^G) by Z0,Q4,R1,A3,Th27; then not -infty in (rng F \/ rng G) by FINSEQ_1:31; then S2: not -infty in rng F & not -infty in rng G by XBOOLE_0:def 3; len G = width (r@) by P4,R7,MATRIX_0:def 7; then j in dom G by P6,FINSEQ_1:def 3; then G.j in rng G by FUNCT_1:3; hence Line(r@,i).v <> -infty by S2,R7,P6,MATRIX_0:def 7; end; hence not -infty in rng (r@.i) by P4,FUNCT_1:def 3; end; thus SumAll M = SumAll (w ^ r) by A3,PRE_POLY:13 .= Sum (Sum w ^ Sum r) by Th23 .= SumAll (Del(M,n+1)) + SumAll r by T3,L1,EXTREAL1:10 .= SumAll (Del(M,n+1)@) + SumAll r by A2,A33,T4 .= SumAll (Del(M,n+1)@) + SumAll (r@) by T5,Th26 .= SumAll ((w@) ^^ (r@)) by A32,Th25,T6,T7 .= SumAll ((w ^ r)@) by A31,MATRLIN:28 .= SumAll (M@) by A3,PRE_POLY:13; end; end; end; A34: x[0] proof let M be Matrix of ExtREAL; assume A35: len M = 0 & (for i be Nat st i in dom M holds not -infty in rng (M.i)); then width M = 0 by MATRIX_0:def 3; then A36:len (M@) = 0 by MATRIX_0:def 6; thus SumAll M = 0 by A35,Th21 .= SumAll (M@) by A36,Th21; end; for n be Nat holds x[n] from NAT_1:sch 2(A34,A1); then x[len M]; hence thesis by A0; end; begin :: Definition of pre-measure registration let x be object; cluster <*x*> -> disjoint_valued; correctness proof now let i,j be object; assume A3: i<>j; per cases; suppose i in dom <*x*>; then i in {1} by FINSEQ_1:2,38; then i = 1 by TARSKI:def 1; then not j in {1} by A3,TARSKI:def 1; then not j in dom <*x*> by FINSEQ_1:2,38; then <*x*>.j = {} by FUNCT_1:def 2; hence <*x*>.i misses <*x*>.j by XBOOLE_1:65; end; suppose not i in dom <*x*>; then <*x*>.i = {} by FUNCT_1:def 2; hence <*x*>.i misses <*x*>.j by XBOOLE_1:65; end; end; hence <*x*> is disjoint_valued by PROB_2:def 2; end; end; theorem for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, F be FinSequence of S, G be Element of S ex H be disjoint_valued FinSequence of S st G \ Union F = Union H proof let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, F be FinSequence of S, G be Element of S; defpred P[Nat] means for f be FinSequence of S st len f = $1 holds ex H be disjoint_valued FinSequence of S st G \ Union f = Union H; for f be FinSequence of S st len f = 0 holds ex H be disjoint_valued FinSequence of S st G \ Union f = Union H proof let f be FinSequence of S; assume len f = 0; then f = {}; then rng f = {}; then A4: Union f = {} by CARD_3:def 4,ZFMISC_1:2; A5: rng <*G*> = {G} by FINSEQ_1:38; reconsider H = <*G*> as disjoint_valued FinSequence of S; take H; union rng H = G by A5,ZFMISC_1:25; hence G \ Union f = Union H by A4,CARD_3:def 4; end; then A6:P[0]; A7:for i be Nat st P[i] holds P[i+1] proof let i be Nat; assume A8: P[i]; now let f be FinSequence of S; assume A9: len f = i+1; then len (f|i) = i by NAT_1:11,FINSEQ_1:59; then consider h be disjoint_valued FinSequence of S such that A12: G \ Union(f|i) = Union h by A8; A10: f = (f|i)^<*f.(i+1)*> by A9,FINSEQ_3:55; then reconsider f1 = <*f.(i+1)*> as FinSequence of S by FINSEQ_1:36; A11: Union f1 = union rng f1 by CARD_3:def 4 .= union {f.(i+1)} by FINSEQ_1:38 .= f.(i+1) by ZFMISC_1:25; Union f = (Union(f|i)) \/ Union f1 by A10,ROUGHS_1:5; then A13: G \ Union f = (G \ Union(f|i)) \ f.(i+1) by A11,XBOOLE_1:41 .= Union h \ f.(i+1) by A12; deffunc F(Nat) = h.$1 \ f.(i+1); consider V be FinSequence such that A14: len V = len h & for k be Nat st k in dom V holds V.k = F(k) from FINSEQ_1:sch 2; A19: for k be Nat st k in dom V ex D be disjoint_valued FinSequence of S st V.k = Union D proof let k be Nat; assume A15: k in dom V; k in dom h by A14,A15,FINSEQ_3:29; then A16: h.k in rng h by FUNCT_1:3; i+1 in Seg len f by A9,FINSEQ_1:4; then i+1 in dom f by FINSEQ_1:def 3; then f.(i+1) in rng f by FUNCT_1:3; then consider D be disjoint_valued FinSequence of S such that A18: h.k \ f.(i+1) = Union D by A16,SRINGS_3:def 1; take D; thus V.k = Union D by A15,A14,A18; end; defpred P[Nat,object] means ex D be disjoint_valued FinSequence of S st $2 = D & V.$1 = Union D; P1: for k be Nat st k in Seg len V ex x be object st P[k,x] proof let k be Nat; assume k in Seg len V; then k in dom V by FINSEQ_1:def 3; then consider D be disjoint_valued FinSequence of S such that P2: V.k = Union D by A19; take D; thus thesis by P2; end; consider FinS be FinSequence such that P3: dom FinS = Seg len V & for k be Nat st k in Seg len V holds P[k,FinS.k] from FINSEQ_1:sch 1(P1); now let a be object; assume a in rng FinS; then consider x be object such that P4: x in dom FinS & a = FinS.x by FUNCT_1:def 3; consider D be disjoint_valued FinSequence of S such that P5: FinS.x = D & V.x = Union D by P3,P4; thus a is FinSequence of S by P4,P5; end; then reconsider Y = rng FinS as FinSequenceSet of S by FINSEQ_2:def 3; reconsider FinS as FinSequence of Y by FINSEQ_1:def 4; H1: for n,m be Nat st n<>m holds union rng(FinS.n) misses union rng(FinS.m) proof let n,m be Nat; assume H2: n<>m; per cases; suppose H3: n in dom FinS & m in dom FinS; then consider D1 be disjoint_valued FinSequence of S such that H4: FinS.n = D1 & V.n = Union D1 by P3; consider D2 be disjoint_valued FinSequence of S such that H5: FinS.m = D2 & V.m = Union D2 by H3,P3; H6: V.n = union rng(FinS.n) & V.m = union rng(FinS.m) by H4,H5,CARD_3:def 4; n in dom V & m in dom V by H3,P3,FINSEQ_1:def 3; then P15: V.n = h.n \ f.(i+1) & V.m = h.m \ f.(i+1) by A14; then V.n misses h.m by XBOOLE_1:80,H2,PROB_2:def 2; hence union rng(FinS.n) misses union rng(FinS.m) by H6,P15,XBOOLE_1:80; end; suppose not n in dom FinS or not m in dom FinS; then FinS.n = {} or FinS.m = {} by FUNCT_1:def 2; then rng(FinS.n) = {} or rng(FinS.m) = {}; hence union rng(FinS.n) misses union rng(FinS.m) by ZFMISC_1:2,XBOOLE_1:65; end; end; for n be Nat holds FinS.n is disjoint_valued proof let n be Nat; per cases; suppose not n in dom FinS; hence FinS.n is disjoint_valued by FUNCT_1:def 2; end; suppose n in dom FinS; then ex D be disjoint_valued FinSequence of S st FinS.n = D & V.n = Union D by P3; hence FinS.n is disjoint_valued; end; end; then reconsider H= joined_FinSeq FinS as disjoint_valued FinSequence of S by H1,Th14; take H; Union H = union rng H by CARD_3:def 4; then X1: Union H = union union{rng(FinS.n) where n is Nat : n in dom FinS} by Th15; X2: G \ Union f = union rng h \ f.(i+1) by CARD_3:def 4,A13; now let x be object; assume B0: x in union rng h \ f.(i+1); then consider A be set such that B2: x in A & A in rng h by TARSKI:def 4; consider k be object such that B3: k in dom h & A = h.k by B2,FUNCT_1:def 3; reconsider k as Nat by B3; B4: k in dom V by A14,B3,FINSEQ_3:29; B5: k in dom FinS by P3,FINSEQ_1:def 3,A14,B3; then consider D be disjoint_valued FinSequence of S such that B6: FinS.k = D & V.k = Union D by P3; B7: V.k = union rng(FinS.k) by B6,CARD_3:def 4; x in union rng h & not x in f.(i+1) by B0,XBOOLE_0:def 5; then x in h.k \ f.(i+1) by B2,B3,XBOOLE_0:def 5; then x in V.k by A14,B4; then consider V be set such that B8: x in V & V in rng(FinS.k) by B7,TARSKI:def 4; rng(FinS.k) in {rng(FinS.n) where n is Nat : n in dom FinS} by B5; then V in union {rng(FinS.n) where n is Nat : n in dom FinS} by B8,TARSKI:def 4; hence x in union union {rng(FinS.n) where n is Nat : n in dom FinS} by B8,TARSKI:def 4; end; then B9: G \ Union f c= Union H by X1,X2,TARSKI:def 3; now let x be object; assume x in union union{rng(FinS.n) where n is Nat:n in dom FinS}; then consider A be set such that C1: x in A & A in union{rng(FinS.n) where n is Nat: n in dom FinS} by TARSKI:def 4; consider D1 be set such that C2: A in D1 & D1 in {rng(FinS.n) where n is Nat: n in dom FinS} by C1,TARSKI:def 4; consider k be Nat such that C3: D1 = rng(FinS.k) & k in dom FinS by C2; consider D2 be disjoint_valued FinSequence of S such that C4: FinS.k = D2 & V.k = Union D2 by C3,P3; C5: k in dom V by C3,P3,FINSEQ_1:def 3; then V.k = h.k \ f.(i+1) by A14; then h.k \ f.(i+1) = union D1 by C3,C4,CARD_3:def 4; then C6: x in (h.k \ f.(i+1)) by C1,C2,TARSKI:def 4; then C7: x in h.k & not x in f.(i+1) by XBOOLE_0:def 5; dom V = dom h by A14,FINSEQ_3:29; then h.k in rng h by C5,FUNCT_1:3; then x in union rng h by C6,TARSKI:def 4; hence x in (union rng h) \ f.(i+1) by C7,XBOOLE_0:def 5; end; then Union H c= G \ Union f by X1,X2,TARSKI:def 3; hence G \ Union f = Union H by B9,XBOOLE_0:def 10; end; hence P[i+1]; end; for i be Nat holds P[i] from NAT_1:sch 2(A6,A7); then for f be FinSequence of S st len f = len F holds ex H be disjoint_valued FinSequence of S st G \ Union f = Union H; hence thesis; end; registration let X be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X; cluster disjoint_valued for sequence of P; existence proof consider F be sequence of {{}} such that A1: for n be Element of NAT holds F.n = {} by MEASURE1:16; {{}} c= P by ZFMISC_1:31,SETFAM_1:def 8; then reconsider F as sequence of P by FUNCT_2:7; take F; for x,y be object st x <> y holds F.x misses F.y proof let x,y be object; assume x <> y; per cases; suppose x in dom F; then F.x = {} by A1; hence F.x misses F.y by XBOOLE_1:65; end; suppose not x in dom F; then F.x = {} by FUNCT_1:def 2; hence F.x misses F.y by XBOOLE_1:65; end; end; hence F is disjoint_valued by PROB_2:def 2; end; end; LM: for X be set, P be non empty Subset-Family of X holds P --> 0. is nonnegative & P --> 0. is additive & P --> 0. is zeroed proof let X be set, P be non empty Subset-Family of X; set M = P --> 0.; for A be Element of P holds 0. <= M.A; hence P --> 0. is nonnegative by MEASURE1:def 2; now let A,B be Element of P; assume A misses B & A \/ B in P; then reconsider D = A \/ B as Element of P; M.A = 0. & M.B = 0. & M.D = 0. by FUNCOP_1:7; hence M.(A \/ B) = M.A + M.B; end; hence P --> 0. is additive by MEASURE1:def 3; per cases; suppose {} in P; then (P --> 0.).{} = 0. by FUNCOP_1:7; hence P --> 0. is zeroed by VALUED_0:def 19; end; suppose not {} in P; then not {} in dom (P--> 0.); then (P--> 0.).{} = 0 by FUNCT_1:def 2; hence P --> 0. is zeroed by VALUED_0:def 19; end; end; registration let X be set, P be non empty Subset-Family of X; cluster nonnegative additive zeroed for Function of P,ExtREAL; existence proof reconsider M = P --> 0. as Function of P,ExtREAL; take M; thus thesis by LM; end; end; registration let X be set, P be with_empty_element Subset-Family of X; cluster disjoint_valued for Function of NAT,P; existence proof {} in P by SETFAM_1:def 8; then reconsider F = NAT --> {} as Function of NAT,P by FUNCOP_1:46; take F; now let i,j be object; assume i <> j; per cases; suppose i in dom F; then F.i = {} by FUNCOP_1:7; hence F.i misses F.j by XBOOLE_1:65; end; suppose not i in dom F; then F.i = {} by FUNCT_1:def 2; hence F.i misses F.j by XBOOLE_1:65; end; end; hence F is disjoint_valued by PROB_2:def 2; end; end; definition let X be set, P be with_empty_element Subset-Family of X; mode pre-Measure of P -> nonnegative zeroed Function of P,ExtREAL means :Def8: ( for F be disjoint_valued FinSequence of P st Union F in P holds it.(Union F) = Sum(it*F) ) & ( for K be disjoint_valued Function of NAT,P st Union K in P holds it.(Union K) <= SUM(it*K) ); existence proof reconsider M = P --> 0. as Function of P,ExtREAL; ( for x be Element of P holds 0.<= M.x) & M.{} = 0 by FUNCOP_1:7,SETFAM_1:def 8; then reconsider M as nonnegative zeroed Function of P,ExtREAL by MEASURE1:def 2,VALUED_0:def 19; take M; 0 is Element of REAL by XREAL_0:def 1; then reconsider m = P --> 0 as Function of P,REAL by FUNCOP_1:46; A2:for F be disjoint_valued FinSequence of P st Union F in P holds M.(Union F) = Sum(M*F) proof let F be disjoint_valued FinSequence of P; assume Union F in P; then A3: M.(Union F) = 0. by FUNCOP_1:7; rng F c= P & dom M = P & dom m = P by FUNCT_2:def 1; then A4: dom(M*F) = dom F & dom(m*F) = dom F by RELAT_1:27; A7: Sum(M*F) = Sum(m*F) by MESFUNC3:2; A8: m*F = F"P --> 0 by FUNCOP_1:19; then dom F = F"P by A4,FUNCOP_1:13; then Seg len F = F"P by FINSEQ_1:def 3; then m*F = (len F) |-> 0 by A8,FINSEQ_2:def 2; hence M.(Union F) = Sum(M*F) by A3,A7,RVSUM_1:81; end; for K be disjoint_valued Function of NAT,P st Union K in P holds M.(Union K) <= SUM(M*K) proof let K be disjoint_valued Function of NAT,P; assume Union K in P; then A10:M.(Union K) = 0. by FUNCOP_1:7; now let n be Element of NAT; (M*K).n = M.(K.n) by FUNCT_2:15; hence (M*K).n = 0. by FUNCOP_1:7; end; hence M.(Union K) <= SUM(M*K) by A10,MEASURE7:1; end; hence thesis by A2; end; end; theorem for X be with_empty_element set, F be FinSequence of X holds ex G be Function of NAT,X st (for i be Nat holds F.i = G.i) & Union F = Union G proof let X be with_empty_element set; let F be FinSequence of X; defpred P[Element of NAT,set] means ($1 in dom F implies F.$1 = $2) & (not $1 in dom F implies $2 = {}); A1:for i be Element of NAT ex y be Element of X st P[i,y] proof let i be Element of NAT; per cases; suppose A2: i in dom F; then F.i in rng F & rng F c= X by FUNCT_1:3; then reconsider y = F.i as Element of X; take y; thus P[i,y] by A2; end; suppose A3: not i in dom F; reconsider y = {} as Element of X by SETFAM_1:def 8; take y; thus P[i,y] by A3; end; end; consider G be Function of NAT,X such that A4: for i be Element of NAT holds P[i,G.i] from FUNCT_2:sch 3(A1); take G; A5:now let i be Nat; per cases; suppose i in dom F; hence F.i = G.i by A4; end; suppose not i in dom F; reconsider j = i as Element of NAT by ORDINAL1:def 12; P[j,G.j] by A4; hence F.i = G.i by FUNCT_1:def 2; end; end; B1:Union F = union rng F & Union G = union rng G by CARD_3:def 4; now let x be object; assume x in Union F; then consider A be set such that A7: x in A & A in rng F by B1,TARSKI:def 4; consider k be object such that A8: k in dom F & A = F.k by A7,FUNCT_1:def 3; reconsider k as Nat by A8; dom G = NAT by FUNCT_2:def 1; then A = G.k & G.k in rng G by A5,A8,FUNCT_1:3; hence x in Union G by A7,B1,TARSKI:def 4; end; then A9:Union F c= Union G by TARSKI:def 3; now let x be object; assume x in Union G; then consider A be set such that A10: x in A & A in rng G by B1,TARSKI:def 4; consider k be object such that A11: k in dom G & A = G.k by A10,FUNCT_1:def 3; reconsider k as Nat by A11; A12:now assume not k in dom F; then F.k = {} by FUNCT_1:def 2; hence contradiction by A5,A10,A11; end; A13:F.k = G.k by A5; F.k in rng F by A12,FUNCT_1:3; hence x in Union F by B1,A10,A11,A13,TARSKI:def 4; end; then Union G c= Union F by TARSKI:def 3; hence thesis by A5,A9,XBOOLE_0:def 10; end; theorem for X be non empty set, F be FinSequence of X, G be Function of NAT,X st (for i be Nat holds F.i = G.i) holds F is disjoint_valued iff G is disjoint_valued proof let X be non empty set, F be FinSequence of X, G be Function of NAT,X; assume A1: for i be Nat holds F.i = G.i; hereby assume A2: F is disjoint_valued; now let x,y be object; assume A3: x <> y; per cases; suppose x in dom F & y in dom F; then G.x = F.x & G.y = F.y by A1; hence G.x misses G.y by A2,A3,PROB_2:def 2; end; suppose not x in dom F & x in dom G; then F.x = {} & G.x = F.x by A1,FUNCT_1:def 2; hence G.x misses G.y by XBOOLE_1:65; end; suppose not x in dom F & not x in dom G; then G.x = {} by FUNCT_1:def 2; hence G.x misses G.y by XBOOLE_1:65; end; suppose not y in dom F & y in dom G; then F.y = {} & G.y = F.y by A1,FUNCT_1:def 2; hence G.x misses G.y by XBOOLE_1:65; end; suppose not y in dom F & not y in dom G; then G.y = {} by FUNCT_1:def 2; hence G.x misses G.y by XBOOLE_1:65; end; end; hence G is disjoint_valued by PROB_2:def 2; end; assume A8: G is disjoint_valued; now let x,y be object; assume A9: x <> y; per cases; suppose x in dom G & y in dom G; then F.x = G.x & F.y = G.y by A1; hence F.x misses F.y by A8,A9,PROB_2:def 2; end; suppose A10: not x in dom G or not y in dom G; dom F c= NAT; then dom F c= dom G by FUNCT_2:def 1; then not x in dom F or not y in dom F by A10; then F.x = {} or F.y = {} by FUNCT_1:def 2; hence F.x misses F.y by XBOOLE_1:65; end; end; hence F is disjoint_valued by PROB_2:def 2; end; theorem for F be FinSequence of ExtREAL, G be ExtREAL_sequence st (for i be Nat holds F.i = G.i) holds F is nonnegative iff G is nonnegative proof let F be FinSequence of ExtREAL, G be ExtREAL_sequence; assume A1: for i be Nat holds F.i = G.i; hereby assume A3: F is nonnegative; now let i be object; assume A4: i in dom G; per cases; suppose i in dom F; then G.i = F.i by A1; hence G.i >= 0 by A3,SUPINF_2:51; end; suppose not i in dom F; then F.i = 0 by FUNCT_1:def 2; hence G.i >= 0 by A1,A4; end; end; hence G is nonnegative by SUPINF_2:52; end; assume A5: G is nonnegative; now let i be object; per cases; suppose i in dom F; then F.i = G.i by A1; hence F.i >= 0 by A5,SUPINF_2:51; end; suppose not i in dom F; hence F.i >= 0 by FUNCT_1:def 2; end; end; hence F is nonnegative by SUPINF_2:51; end; LL1: <*+infty*> is nonnegative & <*+infty*> is without-infty proof set F = <*+infty*>; now let i be object; per cases; suppose i in dom F; then i in Seg 1 by FINSEQ_1:38; then i = 1 by TARSKI:def 1,FINSEQ_1:2; hence F.i >= 0 by FINSEQ_1:40; end; suppose not i in dom F; hence F.i >= 0 by FUNCT_1:def 2; end; end; hence F is nonnegative by SUPINF_2:51; hence F is without-infty; end; LL2: <*-infty*> is nonpositive & <*-infty*> is without+infty proof set F = <*-infty*>; now let i be object; per cases; suppose i in dom F; then i in Seg 1 by FINSEQ_1:38; then i = 1 by TARSKI:def 1,FINSEQ_1:2; hence F.i <= 0 by FINSEQ_1:40; end; suppose not i in dom F; hence F.i <= 0 by FUNCT_1:def 2; end; end; hence F is nonpositive by MESFUNC5:8; hence F is without+infty; end; registration cluster nonnegative for FinSequence of ExtREAL; existence by LL1; cluster without-infty for FinSequence of ExtREAL; existence by LL1; cluster nonpositive for FinSequence of ExtREAL; existence by LL2; cluster without+infty for FinSequence of ExtREAL; existence by LL2; cluster nonnegative -> without-infty for FinSequence of ExtREAL; correctness; cluster nonpositive -> without+infty for FinSequence of ExtREAL; correctness; end; registration let X,Y be non empty set, F be without-infty Function of Y,ExtREAL, G be Function of X,Y; cluster F*G -> without-infty for Function of X,ExtREAL; correctness proof for x be object holds -infty < (F*G).x proof let x be object; per cases; suppose x in dom (F*G); then (F*G).x = F.(G.x) by FUNCT_1:12; hence -infty < (F*G).x by MESFUNC5:def 5; end; suppose not x in dom (F*G); hence -infty < (F*G).x by FUNCT_1:def 2; end; end; hence thesis by MESFUNC5:def 5; end; end; registration let X,Y be non empty set, F be nonnegative Function of Y,ExtREAL, G be Function of X,Y; cluster F*G -> nonnegative for Function of X,ExtREAL; correctness by MEASURE1:25; end; theorem Th33: for a be R_eal holds Sum <*a*> = a proof let a be R_eal; consider f be sequence of ExtREAL such that A1: Sum <*a*> = f.(len <*a*>) & f.0 = 0. & for i be Nat st i < len <*a*> holds f.(i+1) = f.i+ <*a*>.(i+1) by EXTREAL1:def 2; A2:len <*a*> = 1 by FINSEQ_1:39; f.(0+1) = f.0 + <*a*>.(0+1) by A1 .= 0 + a by A1,FINSEQ_1:40; hence Sum <*a*> = a by A1,A2,XXREAL_3:4; end; theorem Th34: for F be FinSequence of ExtREAL, k be Nat holds (F is without-infty implies F|k is without-infty) & (F is without+infty implies F|k is without+infty) proof let F be FinSequence of ExtREAL, k be Nat; hereby assume A1: F is without-infty; now assume -infty in rng(F|k); then consider i be Element of NAT such that A2: i in dom(F|k) & -infty = (F|k).i by PARTFUN1:3; dom(F|k) c= dom F by RELAT_1:60; then i in dom F & (F|k).i = F.i by A2,FUNCT_1:47; then -infty in rng F by A2,FUNCT_1:3; hence contradiction by A1,MESFUNC5:def 3; end; hence F|k is without-infty by MESFUNC5:def 3; end; assume A3: F is without+infty; now assume +infty in rng(F|k); then consider i be Element of NAT such that A4: i in dom(F|k) & +infty = (F|k).i by PARTFUN1:3; dom(F|k) c= dom F by RELAT_1:60; then i in dom F & (F|k).i = F.i by A4,FUNCT_1:47; then +infty in rng F by A4,FUNCT_1:3; hence contradiction by A3,MESFUNC5:def 4; end; hence F|k is without+infty by MESFUNC5:def 4; end; theorem Th35: for F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence st (for i be Nat holds F.i = G.i) holds for i be Nat holds Sum(F|i) = (Partial_Sums G).i proof let F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence; assume A1: for i be Nat holds F.i = G.i; hereby let i be Nat; defpred P[Nat] means Sum(F|$1) = (Partial_Sums G).$1; A3: ex f0 be sequence of ExtREAL st Sum(F|0) = f0.(len (F|0)) & f0.0 = 0. & for i be Nat st i < len (F|0) holds f0.(i+1)= f0.i+(F|0).(i+1) by EXTREAL1:def 2; not 0 in Seg len F by FINSEQ_1:1; then not 0 in dom F by FINSEQ_1:def 3; then F.0 = 0 by FUNCT_1:def 2; then G.0 = 0 by A1; then A4: P[0] by A3,MESFUNC9:def 1; A5: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A6: P[k]; F|k is without-infty by Th34; then A7: not -infty in rng(F|k) by MESFUNC5:def 3; A8: now assume -infty in rng <*F.(k+1)*>; then -infty in { F.(k+1) } by FINSEQ_1:39; then A9: F.(k+1) = -infty by TARSKI:def 1; per cases; suppose k+1 in dom F; then F.(k+1) in rng F by FUNCT_1:3; hence contradiction by A9,MESFUNC5:def 3; end; suppose not k+1 in dom F; hence contradiction by A9,FUNCT_1:def 2; end; end; per cases; suppose k+1 <= len F; then F|(k+1) = F|k ^ <*F.(k+1)*> by NAT_1:13,POLYNOM3:19; then Sum(F|(k+1)) = Sum(F|k) + Sum(<*F.(k+1)*>) by A7,A8,EXTREAL1:10 .= (Partial_Sums G).k + F.(k+1) by A6,Th33 .= (Partial_Sums G).k + G.(k+1) by A1; hence P[k+1] by MESFUNC9:def 1; end; suppose A10: k+1 > len F; then A11: F|k = F & F|(k+1) = F by NAT_1:13,FINSEQ_1:58; not k+1 in dom F by A10,FINSEQ_3:25; then F.(k+1) = 0 by FUNCT_1:def 2; then G.(k+1) = 0 by A1; then (Partial_Sums G).(k+1) = (Partial_Sums G).k + 0 by MESFUNC9:def 1; hence P[k+1] by A6,A11,XXREAL_3:4; end; end; for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); hence Sum(F|i) = (Partial_Sums G).i; end; end; theorem for F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence st (for i be Nat holds F.i = G.i) holds G is summable & Sum F = Sum G proof let F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence; assume A1: for i be Nat holds F.i = G.i; then A2:Sum(F|len F) = (Partial_Sums G).(len F) by Th35; defpred P[Nat] means Sum F = (Partial_Sums G).(len F + $1); B1:P[0] by A2,FINSEQ_1:58; B2:for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; len F < len F + (k+1) by NAT_1:11,19; then not len F + k+1 in dom F by FINSEQ_3:25; then F.(len F + k+1) = 0 by FUNCT_1:def 2; then A4: G.(len F + k+1) = 0 by A1; (Partial_Sums G).(len F + (k+1)) = (Partial_Sums G).(len F + k) + G.(len F + k + 1) by MESFUNC9:def 1 .= (Partial_Sums G).(len F + k) by A4,XXREAL_3:4; hence P[k+1] by A3; end; A5:for k be Nat holds P[k] from NAT_1:sch 2(B1,B2); hereby per cases by XXREAL_0:14; suppose Sum F in REAL; then reconsider r = Sum F as Real; B1: for p be Real st 0

= len F; then F|i = F & F|(i+1) = F by NAT_1:12,FINSEQ_1:58; hence P[i+1] by A5; end; suppose i < len F; then A8: i+1 <= len F by NAT_1:13; set F1 = F|(i+1); A9: F1|i = F|i by NAT_1:12,FINSEQ_1:82; F1 = F1|i ^ <*F1.(i+1)*> by A8,FINSEQ_1:17,FINSEQ_3:55; then rng F1 = rng(F1|i) \/ rng <*F1.(i+1)*> by FINSEQ_1:31; then rng F1 = rng(F|i) \/ {F1.(i+1)} by A9,FINSEQ_1:38; then rng F1 = rng(F|i) \/ {F.(i+1)} by FINSEQ_3:112; then union rng F1 = union rng(F|i) \/ union {F.(i+1)} by ZFMISC_1:78; then Union F1 = union rng(F|i) \/ union {F.(i+1)} by CARD_3:def 4; then Union F1 = Union (F|i) \/ union {F.(i+1)} by CARD_3:def 4; then A11: Union F1 = Union (F|i) \/ F.(i+1) by ZFMISC_1:25; i+1 in dom F by A8,NAT_1:12,FINSEQ_3:25; then F.(i+1) in rng F by FUNCT_1:3; then F.(i+1) in S; hence P[i+1] by A1,A5,A11,FINSUB_1:def 1; end; end; for i be Nat holds P[i] from NAT_1:sch 2(A3,A4); hence thesis; end; theorem for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S, F1,F2 be disjoint_valued FinSequence of S st Union F1 in S & Union F1 = Union F2 holds P.(Union F1) = P.(Union F2); theorem FStoMAT1: for S be non empty cap-closed set, F1,F2 be FinSequence of S holds ex Mx be Matrix of len F1,len F2,S st for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = F1.i /\ F2.j proof let S be non empty cap-closed set; let F1,F2 be FinSequence of S; defpred P[Nat,Nat,set] means $3 = F1.$1 /\ F2.$2; A2:for i,j be Nat st [i,j] in [:Seg len F1, Seg len F2:] ex K be Element of S st P[i,j,K] proof let i,j be Nat; assume [i,j] in [:Seg len F1,Seg len F2:]; then i in Seg len F1 & j in Seg len F2 by ZFMISC_1:87; then i in dom F1 & j in dom F2 by FINSEQ_1:def 3; then F1.i in rng F1 & F2.j in rng F2 by FUNCT_1:3; then F1.i /\ F2.j in S by FINSUB_1:def 2; hence thesis; end; consider Mx be Matrix of len F1,len F2,S such that A3: for i,j be Nat st [i,j] in Indices Mx holds P[i,j,Mx*(i,j)] from MATRIX_0:sch 2(A2); take Mx; thus thesis by A3; end; theorem Th40: for X be set, S be with_empty_element cap-closed Subset-Family of X, F1,F2 be non empty disjoint_valued FinSequence of S, P be nonnegative zeroed Function of S,ExtREAL, Mx be Matrix of len F1,len F2,ExtREAL st Union F1 = Union F2 & ( for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) ) & ( for F be disjoint_valued FinSequence of S st Union F in S holds P.(Union F) = Sum(P*F) ) holds ( for i be Nat st i <= len(P*F1) holds (P*F1).i = (Sum Mx).i ) & Sum(P*F1) = SumAll(Mx) proof let X be set, S be with_empty_element cap-closed Subset-Family of X, F1,F2 be non empty disjoint_valued FinSequence of S, P be nonnegative zeroed Function of S,ExtREAL, Mx be Matrix of len F1,len F2,ExtREAL; assume that A1: Union F1 = Union F2 and A2: for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) and A3: for F be disjoint_valued FinSequence of S st Union F in S holds P.(Union F) = Sum(P*F); consider Kx be Matrix of len F1,len F2,S such that KX1:for i,j be Nat st [i,j] in Indices Kx holds Kx*(i,j) = F1.i /\ F2.j by FStoMAT1; C0:len Kx = len F1 & len Mx = len F1 by MATRIX_0:def 2; then C1:len (P*F1) = len Mx & len (P*F1) = len Kx by FINSEQ_2:33; C4:width Kx = len F2 & width Mx = len F2 by C0,MATRIX_0:20; C2:len (P*F1) = len (Sum Mx) by C1,Def5; thus C6:for i be Nat st i <= len(P*F1) holds (P*F1).i = (Sum Mx).i proof let i be Nat; assume E0: i <= len (P*F1); per cases; suppose i = 0; then not i in dom(P*F1) & not i in dom(Sum Mx) by FINSEQ_3:24; then (P*F1).i = 0 & (Sum Mx).i = 0 by FUNCT_1:def 2; hence (P*F1).i = (Sum Mx).i; end; suppose i <> 0; then E1: 1 <= i by NAT_1:14; then i in dom (P*F1) by E0,FINSEQ_3:25; then E2: i in dom F1 by FUNCT_1:11; then F1.i c= union rng F1 by FUNCT_1:3,ZFMISC_1:74; then F1.i c= Union F2 by A1,CARD_3:def 4; then E3: F1.i /\ Union F2 = F1.i by XBOOLE_1:28; E4: F1.i in rng F1 by E2,FUNCT_1:3; E5: i in dom Kx & i in dom Mx by C1,E0,E1,FINSEQ_3:25; for p,q be object st p <> q holds (Kx.i).p misses (Kx.i).q proof let p,q be object; assume SA0: p <> q; per cases; suppose SA1: p in dom (Kx.i) & q in dom (Kx.i); then reconsider p1 = p, q1 = q as Nat; E6: [i,p1] in Indices Kx & [i,q1] in Indices Kx by SA1,E5,MATRIX_0:37; Kx*(i,p1) = (Kx.i).p & Kx*(i,q1) = (Kx.i).q by E6,MATRPROB:14; then (Kx.i).p = F1.i /\ F2.p1 & (Kx.i).q = F1.i /\ F2.q1 by E6,KX1; hence (Kx.i).p misses (Kx.i).q by SA0,PROB_2:def 2,XBOOLE_1:76; end; suppose not p in dom(Kx.i); then (Kx.i).p = {} by FUNCT_1:def 2; hence (Kx.i).p misses (Kx.i).q by XBOOLE_1:65; end; suppose not q in dom(Kx.i); then (Kx.i).q = {} by FUNCT_1:def 2; hence (Kx.i).p misses (Kx.i).q by XBOOLE_1:65; end; end; then E8: Kx.i is disjoint_valued FinSequence of S by PROB_2:def 2; now let x be object; assume x in Union(Kx.i); then x in union rng (Kx.i) by CARD_3:def 4; then consider A be set such that E9: x in A & A in rng(Kx.i) by TARSKI:def 4; consider m be object such that E10: m in dom(Kx.i) & A = (Kx.i).m by E9,FUNCT_1:def 3; reconsider m as Nat by E10; E11: [i,m] in Indices Kx by E10,E5,MATRIX_0:37; then (Kx.i).m = Kx*(i,m) by MATRPROB:14; then (Kx.i).m = F1.i /\ F2.m by E11,KX1; then E12: x in F1.i & x in F2.m by E9,E10,XBOOLE_0:def 4; 1 <= m & m <= len F2 by E11,MATRIX_0:33; then m in dom F2 by FINSEQ_3:25; then F2.m in rng F2 by FUNCT_1:3; then x in union rng F2 by E12,TARSKI:def 4; then x in Union F2 by CARD_3:def 4; hence x in (F1.i /\ Union F2) by E12,XBOOLE_0:def 4; end; then E13: Union(Kx.i) c= (F1.i /\ Union F2) by TARSKI:def 3; now let x be object; assume x in F1.i /\ Union F2; then E14: x in F1.i & x in Union F2 by XBOOLE_0:def 4; then x in union rng F2 by CARD_3:def 4; then consider A be set such that E15: x in A & A in rng F2 by TARSKI:def 4; consider m be object such that E16: m in dom F2 & A = F2.m by E15,FUNCT_1:def 3; reconsider m as Nat by E16; 1 <= i & i <= len F1 & 1 <= m & m <= len F2 by E2,E16,FINSEQ_3:25; then E17: [i,m] in Indices Kx by MATRIX_0:31; then (Kx.i).m = Kx*(i,m) by MATRPROB:14; then (Kx.i).m = F1.i /\ F2.m by E17,KX1; then E18: x in (Kx.i).m by E14,E15,E16,XBOOLE_0:def 4; m in dom(Kx.i) by E17,MATRIX_0:38; then (Kx.i).m in rng(Kx.i) by FUNCT_1:3; then x in union rng(Kx.i) by E18,TARSKI:def 4; hence x in Union(Kx.i) by CARD_3:def 4; end; then F1.i /\ Union F2 c= Union(Kx.i) by TARSKI:def 3; then F1.i /\ Union F2 = Union(Kx.i) by E13,XBOOLE_0:def 10; then E19: P.(F1.i /\ Union F2) = Sum(P*(Kx.i)) by E3,E4,E8,A3; E20: i in Seg len Mx by C1,E0,E1; E21: Mx.i = Line(Mx,i) & Kx.i = Line(Kx,i) by E5,MATRIX_0:60; rng(Kx.i) c= S; then rng(Kx.i) c= dom P by FUNCT_2:def 1; then E22: dom(P*(Kx.i)) = dom (Kx.i) by RELAT_1:27; then len(P*(Kx.i)) = len (Kx.i) by FINSEQ_3:29; then E23a:len(P*(Kx.i)) = width Kx by E21,MATRIX_0:def 7; then E23: len(P*(Kx.i)) = len (Mx.i) by C4,E21,MATRIX_0:def 7; for k be Nat st 1 <= k & k <= len (P*(Kx.i)) holds (P*(Kx.i)).k = (Mx.i).k proof let k be Nat; assume E24: 1 <= k & k <= len (P*(Kx.i)); then k in dom (Kx.i) & k in dom(Mx.i) by E23,E22,FINSEQ_3:25; then E25: [i,k] in Indices Kx & [i,k] in Indices Mx by E5,MATRPROB:13; k in dom(P*(Kx.i)) by E24,FINSEQ_3:25; then (P*(Kx.i)).k = P.((Kx.i).k) by FUNCT_1:12; then (P*(Kx.i)).k = P.(Kx*(i,k)) by E25,MATRPROB:14; then (P*(Kx.i)).k = P.(F1.i /\ F2.k) by E25,KX1; then (P*(Kx.i)).k = Mx*(i,k) by E25,A2; hence (P*(Kx.i)).k = (Mx.i).k by E25,MATRPROB:14; end; then E27: P*(Kx.i) = Mx.i by E23a,C4,E21,MATRIX_0:def 7; F1.i c= union rng F1 by E2,FUNCT_1:3,ZFMISC_1:74; then F1.i c= Union F1 by CARD_3:def 4; then F1.i /\ Union F2 = F1.i by A1,XBOOLE_1:28; then (P*F1).i = Sum(P*(Kx.i)) by E2,E19,FUNCT_1:13; hence (P*F1).i = (Sum Mx).i by E20,E27,E21,Th16; end; end; consider SMF1 be Function of NAT,ExtREAL such that A2: Sum(P*F1) = SMF1.(len(P*F1)) & SMF1.0 = 0 & for i be Nat st i < len (P*F1) holds SMF1.(i+1) = SMF1.i + (P*F1).(i+1) by EXTREAL1:def 2; consider LL be Function of NAT,ExtREAL such that C7: SumAll(Mx) = LL.(len (Sum Mx)) & LL.0 = 0. & for i be Nat st i < len (Sum Mx) holds LL.(i+1) = LL.i + (Sum Mx).(i+1) by EXTREAL1:def 2; defpred PK1[Nat] means $1 <= len(P*F1) implies SMF1.$1 = LL.$1; C8: PK1[0] by A2,C7; C9: for i be Nat st PK1[i] holds PK1[i+1] proof let i be Nat; assume V1: PK1[i]; assume V3: i+1 <= len (P*F1); then SMF1.(i+1) = SMF1.i + (P*F1).(i+1) by A2,NAT_1:13; then SMF1.(i+1) = LL.i + (Sum Mx).(i+1) by C6,V1,V3,NAT_1:13; hence SMF1.(i+1) = LL.(i+1) by C7,V3,C2,NAT_1:13; end; for i be Nat holds PK1[i] from NAT_1:sch 2(C8,C9); hence Sum(P*F1) = SumAll(Mx) by A2,C2,C7; end; theorem Th41: for X be set, S be with_empty_element cap-closed Subset-Family of X, F1,F2 be non empty disjoint_valued FinSequence of S, P be nonnegative zeroed Function of S,ExtREAL, Mx be Matrix of len F1,len F2,ExtREAL st Union F1 = Union F2 & ( for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) ) & ( for F be disjoint_valued FinSequence of S st Union F in S holds P.(Union F) = Sum(P*F) ) holds ( for i be Nat st i <= len (P*F2) holds (P*F2).i = (Sum(Mx@)).i ) & Sum(P*F2) = SumAll(Mx@) proof let X be set, S be with_empty_element cap-closed Subset-Family of X, F1,F2 be non empty disjoint_valued FinSequence of S, P be nonnegative zeroed Function of S,ExtREAL, Mx be Matrix of len F1,len F2,ExtREAL; assume that A1: Union F1 = Union F2 and A2: for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) and A3: for F be disjoint_valued FinSequence of S st Union F in S holds P.(Union F) = Sum(P*F); consider Kx be Matrix of len F1,len F2,S such that KX1:for i,j be Nat st [i,j] in Indices Kx holds Kx*(i,j) = F1.i /\ F2.j by FStoMAT1; A5:len (P*F2) = len F2 by FINSEQ_2:33; C3:len Kx = len F1 & len Mx = len F1 by MATRIX_0:def 2; then width Kx = len F2 & width Mx = len F2 by MATRIX_0:20; then C5:len (Kx@) = len F2 & len (Mx@) = len F2 & width (Kx@) = len F1 & width(Mx@) = len F1 by C3,MATRIX_0:29; then D2: len (P*F2) = len (Sum(Mx@)) by A5,Def5; thus D6:for i be Nat st i <= len (P*F2) holds (P*F2).i = (Sum(Mx@)).i proof let i be Nat; assume E0: i <= len (P*F2); per cases; suppose i = 0; then not i in dom(P*F2) & not i in dom(Sum(Mx@)) by FINSEQ_3:24; then (P*F2).i = 0 & (Sum(Mx@)).i = 0 by FUNCT_1:def 2; hence (P*F2).i = (Sum(Mx@)).i; end; suppose i <> 0; then E1: 1 <= i by NAT_1:14; then i in dom (P*F2) by E0,FINSEQ_3:25; then E2: i in dom F2 by FUNCT_1:11; then F2.i c= union rng F2 by FUNCT_1:3,ZFMISC_1:74; then F2.i c= Union F1 by A1,CARD_3:def 4; then E3: F2.i /\ Union F1 = F2.i by XBOOLE_1:28; E4: F2.i in rng F2 by E2,FUNCT_1:3; E5: i in dom(Kx@) & i in dom(Mx@) by C5,A5,E0,E1,FINSEQ_3:25; for p,q be object st p <> q holds ((Kx@).i).p misses ((Kx@).i).q proof let p,q be object; assume SA0: p <> q; per cases; suppose SA1: p in dom((Kx@).i) & q in dom((Kx@).i); then reconsider p1 = p, q1 = q as Nat; E6: [i,p1] in Indices(Kx@) & [i,q1] in Indices(Kx@) by SA1,E5,MATRIX_0:37; then EE6: [p1,i] in Indices(Kx) & [q1,i] in Indices(Kx) by MATRIX_0:def 6; (Kx@)*(i,p1) = ((Kx@).i).p & (Kx@)*(i,q1) = ((Kx@).i).q by E6,MATRPROB:14; then ((Kx@).i).p = Kx*(p1,i) & ((Kx@).i).q = Kx*(q1,i) by EE6,MATRIX_0:def 6; then ((Kx@).i).p = F2.i /\ F1.p1 & ((Kx@).i).q = F2.i /\ F1.q1 by EE6,KX1; hence ((Kx@).i).p misses ((Kx@).i).q by SA0,PROB_2:def 2,XBOOLE_1:76; end; suppose not p in dom((Kx@).i); then ((Kx@).i).p = {} by FUNCT_1:def 2; hence ((Kx@).i).p misses ((Kx@).i).q by XBOOLE_1:65; end; suppose not q in dom((Kx@).i); then ((Kx@).i).q = {} by FUNCT_1:def 2; hence ((Kx@).i).p misses ((Kx@).i).q by XBOOLE_1:65; end; end; then E8: (Kx@).i is disjoint_valued FinSequence of S by PROB_2:def 2; now let x be object; assume x in Union((Kx@).i); then x in union rng ((Kx@).i) by CARD_3:def 4; then consider A be set such that E9: x in A & A in rng((Kx@).i) by TARSKI:def 4; consider m be object such that E10: m in dom((Kx@).i) & A = ((Kx@).i).m by E9,FUNCT_1:def 3; reconsider m as Nat by E10; E11: [i,m] in Indices (Kx@) by E10,E5,MATRIX_0:37; then EE11: [m,i] in Indices(Kx) by MATRIX_0:def 6; ((Kx@).i).m = (Kx@)*(i,m) by E11,MATRPROB:14; then ((Kx@).i).m = (Kx)*(m,i) by EE11,MATRIX_0:def 6; then ((Kx@).i).m = F2.i /\ F1.m by EE11,KX1; then E12: x in F2.i & x in F1.m by E9,E10,XBOOLE_0:def 4; 1 <= m & m <= len F1 by EE11,MATRIX_0:33; then m in dom F1 by FINSEQ_3:25; then F1.m in rng F1 by FUNCT_1:3; then x in union rng F1 by E12,TARSKI:def 4; then x in Union F1 by CARD_3:def 4; hence x in (F2.i /\ Union F1) by E12,XBOOLE_0:def 4; end; then E13: Union((Kx@).i) c= (F2.i /\ Union F1) by TARSKI:def 3; now let x be object; assume x in F2.i /\ Union F1; then E14: x in F2.i & x in Union F1 by XBOOLE_0:def 4; then x in union rng F1 by CARD_3:def 4; then consider A be set such that E15: x in A & A in rng F1 by TARSKI:def 4; consider m be object such that E16: m in dom F1 & A = F1.m by E15,FUNCT_1:def 3; reconsider m as Nat by E16; 1 <= i & i <= len F2 & 1 <= m & m <= len F1 by E2,E16,FINSEQ_3:25; then EE17: [m,i] in Indices Kx by MATRIX_0:31; then E17: [i,m] in Indices (Kx@) by MATRIX_0:def 6; ((Kx@).i).m = (Kx@)*(i,m) by E17,MATRPROB:14; then ((Kx@).i).m = Kx*(m,i) by EE17,MATRIX_0:def 6; then ((Kx@).i).m = F2.i /\ F1.m by EE17,KX1; then E18: x in ((Kx@).i).m by E14,E15,E16,XBOOLE_0:def 4; m in dom((Kx@).i) by E17,MATRIX_0:38; then ((Kx@).i).m in rng((Kx@).i) by FUNCT_1:3; then x in union rng((Kx@).i) by E18,TARSKI:def 4; hence x in Union((Kx@).i) by CARD_3:def 4; end; then F2.i /\ Union F1 c= Union((Kx@).i) by TARSKI:def 3; then F2.i /\ Union F1 = Union((Kx@).i) by E13,XBOOLE_0:def 10; then E19: P.(F2.i /\ Union F1) = Sum(P*((Kx@).i)) by E3,E4,E8,A3; E20: i in Seg len (Mx@) by C5,A5,E0,E1; E21: (Mx@).i = Line((Mx@),i) & (Kx@).i = Line((Kx@),i) by E5,MATRIX_0:60; rng((Kx@).i) c= S; then rng((Kx@).i) c= dom P by FUNCT_2:def 1; then E22: dom(P*((Kx@).i)) = dom ((Kx@).i) by RELAT_1:27; then len(P*((Kx@).i)) = len ((Kx@).i) by FINSEQ_3:29; then F23: len(P*((Kx@).i)) = width (Kx@) by E21,MATRIX_0:def 7; then E23: len(P*((Kx@).i)) = len ((Mx@).i) by C5,E21,MATRIX_0:def 7; for k be Nat st 1 <= k & k <= len (P*((Kx@).i)) holds (P*((Kx@).i)).k = ((Mx@).i).k proof let k be Nat; assume E24: 1 <= k & k <= len (P*((Kx@).i)); then k in dom((Kx@).i) & k in dom((Mx@).i) by E23,E22,FINSEQ_3:25; then E25: [i,k] in Indices(Kx@) & [i,k] in Indices(Mx@) by E5,MATRPROB:13; then EE25: [k,i] in Indices Kx & [k,i] in Indices Mx by MATRIX_0:def 6; k in dom(P*((Kx@).i)) by E24,FINSEQ_3:25; then (P*((Kx@).i)).k = P.(((Kx@).i).k) by FUNCT_1:12; then (P*((Kx@).i)).k = P.((Kx@)*(i,k)) by E25,MATRPROB:14; then (P*((Kx@).i)).k = P.(Kx*(k,i)) by EE25,MATRIX_0:def 6; then (P*((Kx@).i)).k = P.(F2.i /\ F1.k) by EE25,KX1; then (P*((Kx@).i)).k = Mx*(k,i) by EE25,A2; then (P*((Kx@).i)).k = (Mx@)*(i,k) by EE25,MATRIX_0:def 6; hence (P*((Kx@).i)).k = ((Mx@).i).k by E25,MATRPROB:14; end; then E27: P*((Kx@).i) = (Mx@).i by F23,C5,E21,MATRIX_0:def 7; F2.i c= union rng F2 by E2,FUNCT_1:3,ZFMISC_1:74; then F2.i c= Union F2 by CARD_3:def 4; then F2.i /\ Union F1 = F2.i by A1,XBOOLE_1:28; then (P*F2).i = Sum(P*((Kx@).i)) by E2,E19,FUNCT_1:13; hence (P*F2).i = (Sum(Mx@)).i by E20,E27,E21,Th16; end; end; consider SMF2 be Function of NAT,ExtREAL such that A3: Sum(P*F2) = SMF2.(len(P*F2)) & SMF2.0 = 0 & for i be Nat st i < len (P*F2) holds SMF2.(i+1) = SMF2.i + (P*F2).(i+1) by EXTREAL1:def 2; consider LL be Function of NAT,ExtREAL such that D7: SumAll(Mx@) = LL.(len (Sum(Mx@))) & LL.0 = 0. & for i be Nat st i < len (Sum(Mx@)) holds LL.(i+1) = LL.i + (Sum(Mx@)).(i+1) by EXTREAL1:def 2; defpred PK2[Nat] means $1 <= len(P*F2) implies SMF2.$1 = LL.$1; D8: PK2[0] by A3,D7; D9: for i be Nat st PK2[i] holds PK2[i+1] proof let i be Nat; assume V1: PK2[i]; assume V3: i+1 <= len (P*F2); then SMF2.(i+1) = SMF2.i + (P*F2).(i+1) by A3,NAT_1:13; then SMF2.(i+1) = LL.i + (Sum(Mx@)).(i+1) by D6,V1,V3,NAT_1:13; hence SMF2.(i+1) = LL.(i+1) by D7,V3,D2,NAT_1:13; end; for i be Nat holds PK2[i] from NAT_1:sch 2(D8,D9); hence Sum(P*F2) = SumAll(Mx@) by A3,D2,D7; end; theorem Th42: for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S, A be set st A in Ring_generated_by S holds for F1,F2 be disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds Sum(P*F1) = Sum(P*F2) proof let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S, A be set; assume A in Ring_generated_by S; hereby let F1,F2 be disjoint_valued FinSequence of S; assume A1: A = Union F1 & A = Union F2; consider SMF1 be Function of NAT,ExtREAL such that A2: Sum(P*F1) = SMF1.(len(P*F1)) & SMF1.0 = 0 & for i be Nat st i < len (P*F1) holds SMF1.(i+1) = SMF1.i + (P*F1).(i+1) by EXTREAL1:def 2; consider SMF2 be Function of NAT,ExtREAL such that A3: Sum(P*F2) = SMF2.(len(P*F2)) & SMF2.0 = 0 & for i be Nat st i < len (P*F2) holds SMF2.(i+1) = SMF2.i + (P*F2).(i+1) by EXTREAL1:def 2; dom P = S by FUNCT_2:def 1; then rng F1 c= dom P & rng F2 c= dom P; then A4: dom (P*F1) = dom F1 & dom (P*F2) = dom F2 by RELAT_1:27; then A5: dom (P*F1) = Seg len F1 & dom(P*F2) = Seg len F2 & len (P*F1) = len F1 & len (P*F2) = len F2 by FINSEQ_1:def 3,FINSEQ_3:29; per cases; suppose A6: len (P*F1) = 0; then P*F1 = {}; then F1 = {} by A4; then rng F1 = {}; then Union F2 = {} by A1,CARD_3:def 4,ZFMISC_1:2; then G7: union rng F2 = {} by CARD_3:def 4; defpred S[Nat] means $1 <= len(P*F2) implies SMF2.$1 = 0; A8: S[0] by A3; A9: for i be Nat st S[i] holds S[i+1] proof let i be Nat; assume A10: S[i]; assume A11: i+1 <= len (P*F2); then A13: SMF2.(i+1) = SMF2.i + (P*F2).(i+1) & SMF2.i = 0 by A3,A10,NAT_1:13; A14: i+1 in dom(P*F2) by A11,NAT_1:11,FINSEQ_3:25; then F2.(i+1) = {} by A4,G7,ORDERS_1:6,FUNCT_1:3; then P.(F2.(i+1)) = 0 by VALUED_0:def 19; then (P*F2).(i+1) = 0 by A14,FUNCT_1:12; hence SMF2.(i+1) = 0 by A13; end; for i be Nat holds S[i] from NAT_1:sch 2(A8,A9); hence Sum(P*F1) = Sum(P*F2) by A2,A3,A6; end; suppose B6: len (P*F2) = 0; then P*F2 = {}; then F2 = {} by A4; then rng F2 = {}; then Union F1 = {} by A1,CARD_3:def 4,ZFMISC_1:2; then E7: union rng F1 = {} by CARD_3:def 4; defpred S[Nat] means $1 <= len(P*F1) implies SMF1.$1 = 0; B8: S[0] by A2; B9: for i be Nat st S[i] holds S[i+1] proof let i be Nat; assume B10: S[i]; assume B11: i+1 <= len (P*F1); then B13: SMF1.(i+1) = SMF1.i + (P*F1).(i+1) & SMF1.i = 0 by A2,B10,NAT_1:13; B14: i+1 in dom(P*F1) by B11,NAT_1:11,FINSEQ_3:25; then F1.(i+1) = {} by A4,E7,ORDERS_1:6,FUNCT_1:3; then P.(F1.(i+1)) = 0 by VALUED_0:def 19; then (P*F1).(i+1) = 0 by B14,FUNCT_1:12; hence SMF1.(i+1) = 0 by B13; end; for i be Nat holds S[i] from NAT_1:sch 2(B8,B9); hence Sum(P*F1) = Sum(P*F2) by A2,A3,B6; end; suppose A15: len (P*F1) <> 0 & len (P*F2) <> 0; defpred Mx[Nat,Nat,set] means $3 = P.(F1.$1 /\ F2.$2); MX0: for i,j be Nat st [i,j] in [:Seg len F1, Seg len F2:] ex A be Element of ExtREAL st Mx[i,j,A]; consider Mx be Matrix of len F1,len F2,ExtREAL such that MX1: for i,j be Nat st [i,j] in Indices Mx holds Mx[i,j,Mx*(i,j)] from MATRIX_0:sch 2(MX0); C3: len Mx = len F1 by MATRIX_0:def 2; then C4: width Mx = len F2 by A15,A5,MATRIX_0:20; CC0: for F be disjoint_valued FinSequence of S st Union F in S holds P.(Union F) = Sum(P*F) by Def8; C0: F1 is non empty & F2 is non empty by A15; then C10: Sum(P*F1) = SumAll(Mx) by A1,MX1,CC0,Th40; D10:Sum(P*F2) = SumAll(Mx@) by C0,A1,MX1,CC0,Th41; for i be Nat st i in dom Mx holds not -infty in rng(Mx.i) proof let i be Nat; assume F1: i in dom Mx; assume -infty in rng(Mx.i); then consider j be object such that F2: j in dom(Mx.i) & (Mx.i).j = -infty by FUNCT_1:def 3; reconsider j as Nat by F2; F3: [i,j] in Indices Mx by F1,F2,MATRPROB:13; then (Mx.i).j = Mx*(i,j) by MATRPROB:14; then F5: (Mx.i).j = P.(F1.i /\ F2.j) by F3,MX1; i in Seg len Mx & j in Seg width Mx by F3,MATRPROB:12; then i in dom F1 & j in dom F2 by C3,C4,FINSEQ_1:def 3; then F1.i in rng F1 & F2.j in rng F2 by FUNCT_1:3; then F1.i /\ F2.j in S by FINSUB_1:def 2; hence contradiction by F2,F5,MEASURE1:def 2; end; hence Sum(P*F1) = Sum(P*F2) by C10,D10,Th28; end; end; end; theorem Th43: for f1,f2 be FinSequence st f1 is disjoint_valued & f2 is disjoint_valued & union rng f1 misses union rng f2 holds f1^f2 is disjoint_valued proof let f1,f2 be FinSequence; assume that A1: f1 is disjoint_valued & f2 is disjoint_valued and A2: union rng f1 misses union rng f2; now let x,y be object; assume A3: x <> y; per cases; suppose A4: x in dom (f1^f2) & y in dom (f1^f2); then reconsider x1=x, y1=y as Nat; per cases by A4,FINSEQ_1:25; suppose x1 in dom f1 & y1 in dom f1; then (f1^f2).x = f1.x & (f1^f2).y = f1.y by FINSEQ_1:def 7; hence (f1^f2).x misses (f1^f2).y by A1,A3,PROB_2:def 2; end; suppose A6: x1 in dom f1 & ex n be Nat st n in dom f2 & y1=len f1 + n; then consider n be Nat such that A7: n in dom f2 & y1 = len f1 + n; (f1^f2).x = f1.x by A6,FINSEQ_1:def 7; then A8: (f1^f2).x in rng f1 by A6,FUNCT_1:3; (f1^f2).y = f2.n by A7,FINSEQ_1:def 7; then A9: (f1^f2).y in rng f2 by A7,FUNCT_1:3; now assume (f1^f2).x meets (f1^f2).y; then consider z be object such that A10: z in (f1^f2).x & z in (f1^f2).y by XBOOLE_0:3; z in union rng f1 & z in union rng f2 by A8,A9,A10,TARSKI:def 4; hence contradiction by A2,XBOOLE_0:3; end; hence (f1^f2).x misses (f1^f2).y; end; suppose A11: y1 in dom f1 & ex n be Nat st n in dom f2 & x1=len f1 + n; then consider n be Nat such that A12: n in dom f2 & x1 = len f1 + n; (f1^f2).x = f2.n by A12,FINSEQ_1:def 7; then A13: (f1^f2).x in rng f2 by A12,FUNCT_1:3; (f1^f2).y = f1.y by A11,FINSEQ_1:def 7; then A14: (f1^f2).y in rng f1 by A11,FUNCT_1:3; now assume (f1^f2).x meets (f1^f2).y; then consider z be object such that A15: z in (f1^f2).x & z in (f1^f2).y by XBOOLE_0:3; z in union rng f1 & z in union rng f2 by A13,A14,A15,TARSKI:def 4; hence contradiction by A2,XBOOLE_0:3; end; hence (f1^f2).x misses (f1^f2).y; end; suppose A16: (ex n be Nat st n in dom f2 & x1 = len f1 + n) & (ex m be Nat st m in dom f2 & y1 = len f1 + m); then consider n be Nat such that A17: n in dom f2 & x1 = len f1 + n; A18: (f1^f2).x = f2.n by A17,FINSEQ_1:def 7; consider m be Nat such that A19: m in dom f2 & y1 = len f1 + m by A16; (f1^f2).y = f2.m by A19,FINSEQ_1:def 7; hence (f1^f2).x misses (f1^f2).y by A1,A18,A17,A19,A3,PROB_2:def 2; end; end; suppose not x in dom (f1^f2) or not y in dom(f1^f2); then (f1^f2).x = {} or (f1^f2).y = {} by FUNCT_1:def 2; hence (f1^f2).x misses (f1^f2).y by XBOOLE_1:65; end; end; hence f1^f2 is disjoint_valued by PROB_2:def 2; end; theorem for X be set, P be with_empty_element semi-diff-closed Subset-Family of X, M be pre-Measure of P, A,B be set st A in P & B in P & A \ B in P & B c= A holds M.A >= M.B proof let X be set, P be with_empty_element semi-diff-closed Subset-Family of X, M be pre-Measure of P, A,B be set; assume that A1: A in P & B in P & A \ B in P and A2: B c= A; consider F be disjoint_valued FinSequence of P such that A3: A \ B = Union F by A1,SRINGS_3:def 1; A7:rng <*B*> = {B} by FINSEQ_1:38; then reconsider G = <*B*> as disjoint_valued FinSequence of P by FINSEQ_1:def 4,A1,ZFMISC_1:31; now assume union rng G meets union rng F; then consider x be object such that A4: x in union rng G & x in union rng F by XBOOLE_0:3; consider P be set such that A5: x in P & P in rng G by A4,TARSKI:def 4; P in {B} by A5,FINSEQ_1:38; then A6: x in B by A5,TARSKI:def 1; x in A \ B by A3,A4,CARD_3:def 4; hence contradiction by A6,XBOOLE_0:def 5; end; then reconsider H = G^F as disjoint_valued FinSequence of P by Th43; A8:union rng G = B by A7,ZFMISC_1:25; rng H = rng G \/ rng F by FINSEQ_1:31; then union rng H = union rng G \/ union rng F by ZFMISC_1:78; then Union H = B \/ union rng F by A8,CARD_3:def 4 .= B \/ (A \ B) by A3,CARD_3:def 4; then Union H = A \/ B by XBOOLE_1:39; then Union H = A by A2,XBOOLE_1:12; then A9:M.A = Sum(M*H) by A1,Def8; Union G = B by A8,CARD_3:def 4; then A10:M.B = Sum(M*G) by A1,Def8; B0:now assume -infty in rng(M*G); then consider n be Element of NAT such that B1: n in dom(M*G) & -infty = (M*G).n by PARTFUN1:3; M.(G.n) = -infty by B1,FUNCT_1:12; hence contradiction by SUPINF_2:51; end; A11:now assume -infty in rng(M*F); then consider n be Element of NAT such that B2: n in dom(M*F) & -infty = (M*F).n by PARTFUN1:3; M.(F.n) = -infty by B2,FUNCT_1:12; hence contradiction by SUPINF_2:51; end; A12:now let n be Nat; assume n in dom(M*F); then (M*F).n = M.(F.n) & F.n in dom M by FUNCT_1:11,12; hence (M*F).n >= 0 by SUPINF_2:51; end; M*H = (M*G)^(M*F) by FINSEQOP:9; then Sum(M*H) = Sum(M*G) + Sum(M*F) by A11,B0,EXTREAL1:10; hence M.B <= M.A by A9,A10,A12,MESFUNC5:53,XXREAL_3:39; end; theorem Th45: for Y,S be non empty set, F be PartFunc of Y,S, M be Function of S,ExtREAL st M is nonnegative holds M*F is nonnegative proof let Y,S be non empty set; let F be PartFunc of Y,S; let M be Function of S,ExtREAL; assume A1: M is nonnegative; now let n be object; per cases; suppose n in dom(M*F); then (M*F).n = M.(F.n) by FUNCT_1:12; hence (M*F).n >= 0 by A1,SUPINF_2:51; end; suppose not n in dom(M*F); hence (M*F).n >= 0 by FUNCT_1:def 2; end; end; hence thesis by SUPINF_2:51; end; theorem Th46: for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S ex M be nonnegative additive zeroed Function of (Ring_generated_by S),ExtREAL st for A be set st A in Ring_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds M.A = Sum(P*F) proof let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S; defpred P[object,object] means for F be disjoint_valued FinSequence of S st $1 = Union F holds $2 = Sum(P*F); A1:for A be object st A in Ring_generated_by S ex p be object st p in ExtREAL & P[A,p] proof let A be object; assume A2: A in Ring_generated_by S; then A in DisUnion S by SRINGS_3:18; then consider V be Subset of X such that A3: A = V & ex F be disjoint_valued FinSequence of S st V = Union F; consider F be disjoint_valued FinSequence of S such that A4: V = Union F by A3; set p = Sum(P*F); take p; thus p in ExtREAL & P[A,p] by A2,A3,A4,Th42; end; consider M be Function of (Ring_generated_by S),ExtREAL such that A5: for A be object st A in Ring_generated_by S holds P[A,M.A] from FUNCT_2:sch 1(A1); A18:for A be Element of Ring_generated_by S holds 0 <= M.A proof let A be Element of Ring_generated_by S; A in Ring_generated_by S; then A in DisUnion S by SRINGS_3:18; then consider V be Subset of X such that A7: A = V & ex F be disjoint_valued FinSequence of S st V = Union F; consider F be disjoint_valued FinSequence of S such that A8: V = Union F by A7; consider PF be sequence of ExtREAL such that A10: Sum(P*F) = PF.(len(P*F)) & PF.0 = 0. & for i be Nat st i < len(P*F) holds PF.(i+1) = PF.i + (P*F).(i+1) by EXTREAL1:def 2; defpred P2[Nat] means $1 <= len(P*F) implies PF.$1 >= 0; A11:P2[0] by A10; A12:for i be Nat st P2[i] holds P2[i+1] proof let i be Nat; assume A13: P2[i]; assume A14: i+1 <= len(P*F); then i+1 in dom(P*F) by NAT_1:11,FINSEQ_3:25; then (P*F).(i+1) = P.(F.(i+1)) by FUNCT_1:12; then A17: (P*F).(i+1) >= 0 by SUPINF_2:51; PF.(i+1) = PF.i + (P*F).(i+1) by A14,A10,NAT_1:13; hence PF.(i+1) >= 0 by A13,A14,A17,NAT_1:13; end; for i be Nat holds P2[i] from NAT_1:sch 2(A11,A12); then Sum(P*F) >= 0 by A10; hence 0 <= M.A by A7,A8,A5; end; for A,B be Element of Ring_generated_by S st A misses B & A \/ B in Ring_generated_by S holds M.(A \/ B) = M.A + M.B proof let A,B be Element of Ring_generated_by S; assume A19: A misses B & A \/ B in Ring_generated_by S; A in Ring_generated_by S; then A in DisUnion S by SRINGS_3:18; then consider V be Subset of X such that A20: A = V & ex F be disjoint_valued FinSequence of S st V = Union F; consider F be disjoint_valued FinSequence of S such that A21: V = Union F by A20; B in Ring_generated_by S; then B in DisUnion S by SRINGS_3:18; then consider W be Subset of X such that A22: B = W & ex G be disjoint_valued FinSequence of S st W = Union G; consider G be disjoint_valued FinSequence of S such that A23: W = Union G by A22; set H = F^G; A24:A = union rng F & B = union rng G by A20,A21,A22,A23,CARD_3:def 4; then reconsider H as disjoint_valued FinSequence of S by A19,Th43; rng H = rng F \/ rng G by FINSEQ_1:31; then union rng H = union rng F \/ union rng G by ZFMISC_1:78; then A \/ B = Union H by A24,CARD_3:def 4; then A25:M.(A \/ B) = Sum(P*H) by A5; A26:M.A = Sum(P*F) & M.B = Sum(P*G) by A20,A21,A22,A23,A5; P*F is nonnegative by Th45; then A27:not -infty in rng(P*F) by SUPINF_2:def 9,def 12; P*G is nonnegative by Th45; then A28:not -infty in rng(P*G) by SUPINF_2:def 9,def 12; P*H = (P*F)^(P*G) by FINSEQOP:9; hence M.(A \/ B) = M.A + M.B by A25,A26,A27,A28,EXTREAL1:10; end; then A29:M is additive by MEASURE1:def 3; reconsider E = {} as Element of S by SETFAM_1:def 8; reconsider F = <*E*> as disjoint_valued FinSequence of S; rng F = {{}} by FINSEQ_1:38; then union rng F = {} by ZFMISC_1:25; then Union F = {} by CARD_3:def 4; then M.{} = Sum(P*F) by A5,FINSUB_1:7; then M.{} = Sum(<*P.{}*>) by FINSEQ_2:35; then M.{} = P.{} by EXTREAL1:8; then M.{} = 0 by VALUED_0:def 19; then reconsider M as nonnegative additive zeroed Function of (Ring_generated_by S),ExtREAL by A18,A29,VALUED_0:def 19,MEASURE1:def 2; take M; thus thesis by A5; end; theorem for X,Y be set, F,G be Function of NAT,bool X st (for i be Nat holds G.i = F.i /\ Y) & Union F = Y holds Union G = Union F proof let X,Y be set, F,G be Function of NAT,bool X; assume that A1: for i be Nat holds G.i = F.i /\ Y and A2: Union F = Y; now let x be object; assume x in Union G; then x in union rng G by CARD_3:def 4; then consider A be set such that A3: x in A & A in rng G by TARSKI:def 4; consider i be Element of NAT such that A4: A = G.i by A3,FUNCT_2:113; dom F = NAT by FUNCT_2:def 1; then A = F.i /\ Y & i in dom F by A1,A4; then x in F.i & F.i in rng F by A3,XBOOLE_0:def 4,FUNCT_1:3; then x in union rng F by TARSKI:def 4; hence x in Union F by CARD_3:def 4; end; then A5:Union G c= Union F by TARSKI:def 3; now let x be object; assume A6: x in Union F; then x in union rng F by CARD_3:def 4; then consider A be set such that A7: x in A & A in rng F by TARSKI:def 4; consider i be Element of NAT such that A8: A = F.i by A7,FUNCT_2:113; dom G = NAT by FUNCT_2:def 1; then x in F.i /\ Y & i in dom G by A2,A6,A7,A8,XBOOLE_0:def 4; then x in G.i & G.i in rng G by A1,FUNCT_1:3; then x in union rng G by TARSKI:def 4; hence x in Union G by CARD_3:def 4; end; then Union F c= Union G by TARSKI:def 3; hence thesis by A5,XBOOLE_0:def 10; end; theorem for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S ex M be Function of Ring_generated_by S,ExtREAL st M.{} = 0 & for K be disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds M.(Union K) = Sum(P*K) proof let X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S; consider M be nonnegative additive zeroed Function of (Ring_generated_by S),ExtREAL such that A1: for A be set st A in Ring_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds M.A = Sum(P*F) by Th46; take M; thus M.{} = 0 by VALUED_0:def 19; thus for K be disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds M.(Union K) = Sum(P*K) by A1; end; theorem for X,Z be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X, K be disjoint_valued Function of NAT,Ring_generated_by P st Z = {[n,F] where n is Nat, F is disjoint_valued FinSequence of P : Union F = K.n & (K.n = {} implies F = <*{}*>) } holds proj2 Z is FinSequenceSet of P & (for x be object holds x in rng K iff ex F be FinSequence of P st F in proj2 Z & Union F = x) & proj2 Z is with_non-empty_elements proof let X,Z be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X, K be disjoint_valued Function of NAT,Ring_generated_by P; assume A1: Z={[n,F] where n is Nat, F is disjoint_valued FinSequence of P : Union F = K.n & (K.n = {} implies F = <*{}*>)}; now let a be object; assume a in proj2 Z; then consider k be object such that A2: [k,a] in Z by XTUPLE_0:def 13; consider n be Nat, F be disjoint_valued FinSequence of P such that A3: [k,a] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A2; thus a is FinSequence of P by A3,XTUPLE_0:1; end; hence proj2 Z is FinSequenceSet of P by FINSEQ_2:def 3; hereby let x be object; hereby assume x in rng K; then consider n be Element of NAT such that A6: x = K.n by FUNCT_2:113; K.n in Ring_generated_by P; then K.n in DisUnion P by SRINGS_3:18; then consider A be Subset of X such that A7: x = A & ex F be disjoint_valued FinSequence of P st A=Union F by A6; consider F be disjoint_valued FinSequence of P such that A8: A = Union F by A7; per cases; suppose A9: K.n = {}; A10: rng <*{}*> = { {} } by FINSEQ_1:38; {} in P by SETFAM_1:def 8; then reconsider F1 = <*{}*> as disjoint_valued FinSequence of P by A10,ZFMISC_1:31,FINSEQ_1:def 4; rng F1 = { {} } by FINSEQ_1:38; then union rng F1 = {} by ZFMISC_1:25; then B1: Union F1 = {} by CARD_3:def 4; then [n,F1] in Z by A9,A1; then F1 in proj2 Z by XTUPLE_0:def 13; hence ex F be FinSequence of P st F in proj2 Z & Union F = x by A9,B1,A6; end; suppose K.n <> {}; then [n,F] in Z by A1,A6,A7,A8; then F in proj2 Z by XTUPLE_0:def 13; hence ex F be FinSequence of P st F in proj2 Z & Union F = x by A8,A7; end; end; assume ex F be FinSequence of P st F in proj2 Z & Union F = x; then consider z be FinSequence of P such that A12: z in proj2 Z & Union z = x; consider y be object such that A13: [y,z] in Z by A12,XTUPLE_0:def 13; consider n be Nat, F be disjoint_valued FinSequence of P such that A14: [y,z] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A13; y=n & z=F by A14,XTUPLE_0:1; hence x in rng K by A12,A14,FUNCT_2:4,ORDINAL1:def 12; end; now assume {} in proj2 Z; then consider y be object such that A16: [ y,{} ] in Z by XTUPLE_0:def 13; consider n be Nat, F be disjoint_valued FinSequence of P such that A17: [ y,{} ] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A16; y=n & {}=F by A17,XTUPLE_0:1; then union rng F = {} by ZFMISC_1:2; hence contradiction by A17,XTUPLE_0:1,CARD_3:def 4; end; hence proj2 Z is with_non-empty_elements; end; theorem for X be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X, K be disjoint_valued Function of NAT,Ring_generated_by P st rng K is with_non-empty_element holds ex Y be non empty FinSequenceSet of P st Y = {F where F is disjoint_valued FinSequence of P : Union F in rng K & F <> {} } & Y is with_non-empty_elements proof let X be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X, K be disjoint_valued Function of NAT,Ring_generated_by P; assume A0: rng K is with_non-empty_element; set Y = {F where F is disjoint_valued FinSequence of P : Union F in rng K & F <> {} }; now let a be object; assume a in Y; then ex A be disjoint_valued FinSequence of P st a = A & Union A in rng K & A <> {}; hence a is FinSequence of P; end; then reconsider Y as FinSequenceSet of P by FINSEQ_2:def 3; consider k be non empty set such that A2: k in rng K by A0; consider i be Element of NAT such that A3: k = K.i by A2,FUNCT_2:113; K.i in Ring_generated_by P; then K.i in DisUnion P by SRINGS_3:18; then consider A be Subset of X such that A4: K.i = A & ex F be disjoint_valued FinSequence of P st A = Union F; consider F be disjoint_valued FinSequence of P such that A5: A = Union F by A4; now assume F = {}; then union rng F = {} by ZFMISC_1:2; hence contradiction by A5,A4,A3,CARD_3:def 4; end; then F in Y by A2,A3,A4,A5; then reconsider Y as non empty FinSequenceSet of P; take Y; thus Y = {A where A is disjoint_valued FinSequence of P : Union A in rng K & A <> {} }; now assume {} in Y; then ex A be disjoint_valued FinSequence of P st {} = A & Union A in rng K & A <> {}; hence contradiction; end; hence Y is with_non-empty_elements; end; begin :: Pre-measure on semialgera and construction of measure theorem Th51: for X,Z be set, P be semialgebra_of_sets of X, K be disjoint_valued Function of NAT,Field_generated_by P st Z = {[n,F] where n is Nat, F is disjoint_valued FinSequence of P : Union F = K.n & (K.n = {} implies F = <*{}*>) } holds proj2 Z is FinSequenceSet of P & (for x be object holds x in rng K iff ex F be FinSequence of P st F in proj2 Z & Union F = x) & proj2 Z is with_non-empty_elements proof let X,Z be set, P be semialgebra_of_sets of X, K be disjoint_valued Function of NAT,Field_generated_by P; assume A1: Z={[n,F] where n is Nat, F is disjoint_valued FinSequence of P : Union F = K.n & (K.n = {} implies F = <*{}*>)}; now let a be object; assume a in proj2 Z; then consider k be object such that A2: [k,a] in Z by XTUPLE_0:def 13; ex n be Nat, F be disjoint_valued FinSequence of P st [k,a] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A2; hence a is FinSequence of P by XTUPLE_0:1; end; hence proj2 Z is FinSequenceSet of P by FINSEQ_2:def 3; hereby let x be object; hereby assume x in rng K; then consider n be Element of NAT such that A6: x = K.n by FUNCT_2:113; K.n in Field_generated_by P; then K.n in DisUnion P by SRINGS_3:22; then consider A be Subset of X such that A7: x = A & ex F be disjoint_valued FinSequence of P st A=Union F by A6; consider F be disjoint_valued FinSequence of P such that A8: A = Union F by A7; per cases; suppose A9: K.n = {}; A10: rng <*{}*> = { {} } by FINSEQ_1:38; {} in P by SETFAM_1:def 8; then reconsider F1 = <*{}*> as disjoint_valued FinSequence of P by A10,ZFMISC_1:31,FINSEQ_1:def 4; rng F1 = { {} } by FINSEQ_1:38; then union rng F1 = {} by ZFMISC_1:25; then B1: Union F1 = {} by CARD_3:def 4; then [n,F1] in Z by A9,A1; then F1 in proj2 Z by XTUPLE_0:def 13; hence ex F be FinSequence of P st F in proj2 Z & Union F = x by A9,B1,A6; end; suppose K.n <> {}; then [n,F] in Z by A1,A6,A7,A8; then F in proj2 Z by XTUPLE_0:def 13; hence ex F be FinSequence of P st F in proj2 Z & Union F = x by A8,A7; end; end; assume ex F be FinSequence of P st F in proj2 Z & Union F = x; then consider z be FinSequence of P such that A12: z in proj2 Z & Union z = x; consider y be object such that A13: [y,z] in Z by A12,XTUPLE_0:def 13; consider n be Nat, F be disjoint_valued FinSequence of P such that A14: [y,z] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A13; y=n & z=F by A14,XTUPLE_0:1; hence x in rng K by A12,A14,ORDINAL1:def 12,FUNCT_2:4; end; now assume {} in proj2 Z; then consider y be object such that A16: [ y,{} ] in Z by XTUPLE_0:def 13; consider n be Nat, F be disjoint_valued FinSequence of P such that A17: [ y,{} ] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A16; y=n & {}=F by A17,XTUPLE_0:1; then union rng F = {} by ZFMISC_1:2; hence contradiction by A17,XTUPLE_0:1,CARD_3:def 4; end; hence proj2 Z is with_non-empty_elements; end; theorem Th54: for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S, A be set holds for F1,F2 be disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds Sum(P*F1) = Sum(P*F2) proof let X be set, S be semialgebra_of_sets of X, P be pre-Measure of S, A be set; hereby let F1,F2 be disjoint_valued FinSequence of S; assume A1: A = Union F1 & A = Union F2; consider SMF1 be Function of NAT,ExtREAL such that A2: Sum(P*F1) = SMF1.(len(P*F1)) & SMF1.0 = 0 & for i be Nat st i < len (P*F1) holds SMF1.(i+1) = SMF1.i + (P*F1).(i+1) by EXTREAL1:def 2; consider SMF2 be Function of NAT,ExtREAL such that A3: Sum(P*F2) = SMF2.(len(P*F2)) & SMF2.0 = 0 & for i be Nat st i < len (P*F2) holds SMF2.(i+1) = SMF2.i + (P*F2).(i+1) by EXTREAL1:def 2; dom P = S by FUNCT_2:def 1; then rng F1 c= dom P & rng F2 c= dom P; then A4: dom (P*F1) = dom F1 & dom (P*F2) = dom F2 by RELAT_1:27; then A5: dom (P*F1) = Seg len F1 & dom(P*F2) = Seg len F2 & len (P*F1) = len F1 & len (P*F2) = len F2 by FINSEQ_1:def 3,FINSEQ_3:29; per cases; suppose A6: len (P*F1) = 0; then P*F1 = {}; then F1 = {} by A4; then rng F1 = {}; then Union F2 = {} by A1,CARD_3:def 4,ZFMISC_1:2; then A7: union rng F2 = {} by CARD_3:def 4; defpred S[Nat] means $1 <= len(P*F2) implies SMF2.$1 = 0; A8: S[0] by A3; A9: for i be Nat st S[i] holds S[i+1] proof let i be Nat; assume A10: S[i]; assume A11: i+1 <= len (P*F2); then A13: SMF2.(i+1) = SMF2.i + (P*F2).(i+1) & SMF2.i = 0 by A3,A10,NAT_1:13; A14: i+1 in dom(P*F2) by A11,NAT_1:11,FINSEQ_3:25; then F2.(i+1) = {} by A4,A7,ORDERS_1:6,FUNCT_1:3; then P.(F2.(i+1)) = 0 by VALUED_0:def 19; then (P*F2).(i+1) = 0 by A14,FUNCT_1:12; hence SMF2.(i+1) = 0 by A13; end; for i be Nat holds S[i] from NAT_1:sch 2(A8,A9); hence Sum(P*F1) = Sum(P*F2) by A2,A3,A6; end; suppose B6: len (P*F2) = 0; then P*F2 = {}; then F2 = {} by A4; then rng F2 = {}; then Union F1 = {} by A1,CARD_3:def 4,ZFMISC_1:2; then B7: union rng F1 = {} by CARD_3:def 4; defpred S[Nat] means $1 <= len(P*F1) implies SMF1.$1 = 0; B8: S[0] by A2; B9: for i be Nat st S[i] holds S[i+1] proof let i be Nat; assume B10: S[i]; assume B11: i+1 <= len (P*F1); then B13: SMF1.(i+1) = SMF1.i + (P*F1).(i+1) & SMF1.i = 0 by A2,B10,NAT_1:13; B14: i+1 in dom(P*F1) by B11,NAT_1:11,FINSEQ_3:25; then F1.(i+1) = {} by A4,B7,ORDERS_1:6,FUNCT_1:3; then P.(F1.(i+1)) = 0 by VALUED_0:def 19; then (P*F1).(i+1) = 0 by B14,FUNCT_1:12; hence SMF1.(i+1) = 0 by B13; end; for i be Nat holds S[i] from NAT_1:sch 2(B8,B9); hence Sum(P*F1) = Sum(P*F2) by A2,A3,B6; end; suppose A15: len (P*F1) <> 0 & len (P*F2) <> 0; defpred Mx[Nat,Nat,set] means $3 = P.(F1.$1 /\ F2.$2); MX0: for i,j be Nat st [i,j] in [:Seg len F1, Seg len F2:] ex A be Element of ExtREAL st Mx[i,j,A]; consider Mx be Matrix of len F1,len F2,ExtREAL such that MX1: for i,j be Nat st [i,j] in Indices Mx holds Mx[i,j,Mx*(i,j)] from MATRIX_0:sch 2(MX0); C3: len Mx = len F1 by MATRIX_0:def 2; then C4: width Mx = len F2 by A15,A5,MATRIX_0:20; CC0: for F be disjoint_valued FinSequence of S st Union F in S holds P.(Union F) = Sum(P*F) by Def8; F1 is non empty & F2 is non empty by A15; then C10: Sum(P*F1) = SumAll(Mx) & Sum(P*F2) = SumAll(Mx@) by A1,MX1,CC0,Th40,Th41; for i be Nat st i in dom Mx holds not -infty in rng(Mx.i) proof let i be Nat; assume F1: i in dom Mx; assume -infty in rng(Mx.i); then consider j be object such that F2: j in dom(Mx.i) & (Mx.i).j = -infty by FUNCT_1:def 3; reconsider j as Nat by F2; F3: [i,j] in Indices Mx by F1,F2,MATRPROB:13; then (Mx.i).j = Mx*(i,j) by MATRPROB:14; then F5: (Mx.i).j = P.(F1.i /\ F2.j) by F3,MX1; i in Seg len Mx & j in Seg width Mx by F3,MATRPROB:12; then i in dom F1 & j in dom F2 by C3,C4,FINSEQ_1:def 3; then F1.i in rng F1 & F2.j in rng F2 by FUNCT_1:3; then F1.i /\ F2.j in S by FINSUB_1:def 2; hence contradiction by F2,F5,MEASURE1:def 2; end; hence Sum(P*F1) = Sum(P*F2) by C10,Th28; end; end; end; theorem Th55: for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S ex M be Measure of Field_generated_by S st for A be set st A in Field_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds M.A = Sum(P*F) proof let X be set, S be semialgebra_of_sets of X, P be pre-Measure of S; defpred P[object,object] means for F be disjoint_valued FinSequence of S st $1 = Union F holds $2 = Sum(P*F); A1:for A be object st A in Field_generated_by S ex p be object st p in ExtREAL & P[A,p] proof let A be object; assume A in Field_generated_by S; then A in DisUnion S by SRINGS_3:22; then consider V be Subset of X such that A3: A = V & ex F be disjoint_valued FinSequence of S st V = Union F; consider F be disjoint_valued FinSequence of S such that A4: V = Union F by A3; set p = Sum(P*F); take p; thus p in ExtREAL & P[A,p] by A3,A4,Th54; end; consider M be Function of (Field_generated_by S),ExtREAL such that A5: for A be object st A in Field_generated_by S holds P[A,M.A] from FUNCT_2:sch 1(A1); A18:for A be Element of Field_generated_by S holds 0 <= M.A proof let A be Element of Field_generated_by S; A in Field_generated_by S; then A in DisUnion S by SRINGS_3:22; then consider V be Subset of X such that A7: A = V & ex F be disjoint_valued FinSequence of S st V = Union F; consider F be disjoint_valued FinSequence of S such that A8: V = Union F by A7; consider PF be sequence of ExtREAL such that A10: Sum(P*F) = PF.(len(P*F)) & PF.0 = 0. & for i be Nat st i < len(P*F) holds PF.(i+1) = PF.i + (P*F).(i+1) by EXTREAL1:def 2; defpred P2[Nat] means $1 <= len(P*F) implies PF.$1 >= 0; A11:P2[0] by A10; A12:for i be Nat st P2[i] holds P2[i+1] proof let i be Nat; assume A13: P2[i]; assume A14: i+1 <= len(P*F); then i+1 in dom(P*F) by NAT_1:11,FINSEQ_3:25; then (P*F).(i+1) = P.(F.(i+1)) by FUNCT_1:12; then A17: (P*F).(i+1) >= 0 by SUPINF_2:51; PF.(i+1) = PF.i + (P*F).(i+1) by A14,A10,NAT_1:13; hence PF.(i+1) >= 0 by A13,A14,NAT_1:13,A17; end; for i be Nat holds P2[i] from NAT_1:sch 2(A11,A12); then Sum(P*F) >= 0 by A10; hence 0 <= M.A by A7,A8,A5; end; A29:for A,B be Element of Field_generated_by S st A misses B holds M.(A \/ B) = M.A + M.B proof let A,B be Element of Field_generated_by S; assume A19: A misses B; A in Field_generated_by S; then A in DisUnion S by SRINGS_3:22; then consider V be Subset of X such that A20: A = V & ex F be disjoint_valued FinSequence of S st V = Union F; consider F be disjoint_valued FinSequence of S such that A21: V = Union F by A20; B in Field_generated_by S; then B in DisUnion S by SRINGS_3:22; then consider W be Subset of X such that A22: B = W & ex G be disjoint_valued FinSequence of S st W = Union G; consider G be disjoint_valued FinSequence of S such that A23: W = Union G by A22; set H = F^G; A24:A = union rng F & B = union rng G by A20,A21,A22,A23,CARD_3:def 4; then reconsider H as disjoint_valued FinSequence of S by A19,Th43; rng H = rng F \/ rng G by FINSEQ_1:31; then union rng H = union rng F \/ union rng G by ZFMISC_1:78; then A \/ B = Union H by A24,CARD_3:def 4; then A25:M.(A \/ B) = Sum(P*H) by A5; A26:M.A = Sum(P*F) & M.B = Sum(P*G) by A20,A21,A22,A23,A5; P*F is nonnegative by Th45; then A27:not -infty in rng(P*F) by SUPINF_2:def 12,def 9; P*G is nonnegative by Th45; then A28:not -infty in rng(P*G) by SUPINF_2:def 12,def 9; P*H = (P*F)^(P*G) by FINSEQOP:9; hence M.(A \/ B) = M.A + M.B by A25,A26,A27,A28,EXTREAL1:10; end; reconsider E = {} as Element of S by SETFAM_1:def 8; reconsider F = <*E*> as disjoint_valued FinSequence of S; rng F = {{}} by FINSEQ_1:38; then union rng F = {} by ZFMISC_1:25; then Union F = {} by CARD_3:def 4; then M.{} = Sum(P*F) by A5,FINSUB_1:7; then M.{} = Sum(<*P.{}*>) by FINSEQ_2:35; then M.{} = P.{} by EXTREAL1:8; then M.{} = 0 by VALUED_0:def 19; then reconsider M as nonnegative additive zeroed Function of (Field_generated_by S),ExtREAL by A18,A29,VALUED_0:def 19,MEASURE1:def 2,def 8; take M; thus thesis by A5; end; theorem for F be ExtREAL_sequence, n be Nat, a be R_eal st (for k be Nat holds F.k = a) holds (Partial_Sums F).n = a*(n+1) proof let F be ExtREAL_sequence, n be Nat, a be R_eal; assume A1: for k be Nat holds F.k = a; defpred P[Nat] means (Partial_Sums F).$1 = a*($1 + 1); (Partial_Sums F).0 = F.0 by MESFUNC9:def 1; then (Partial_Sums F).0 = a by A1; then A2:P[0] by XXREAL_3:81; A3:for i be Nat st P[i] holds P[i+1] proof let i be Nat; assume A4: P[i]; i+1 in REAL & 1 in REAL by XREAL_0:def 1; then reconsider i1= i+1, One=1 as R_eal by XBOOLE_0:def 3,XXREAL_0:def 4; (Partial_Sums F).(i+1) = (Partial_Sums F).i + F.(i+1) by MESFUNC9:def 1; then (Partial_Sums F).(i+1) = a*(i+1) + a by A1,A4; then (Partial_Sums F).(i+1) = a*(i+1) + a*1 by XXREAL_3:81; then (Partial_Sums F).(i+1) = a*((i1)+One) by XXREAL_3:96; hence P[i+1] by XXREAL_3:def 2; end; for i be Nat holds P[i] from NAT_1:sch 2(A2,A3); hence thesis; end; theorem Th57: for X be non empty set, F be sequence of X, n be Nat holds rng(F|Segm(n+1)) = rng(F|Segm n) \/ {F.n} proof let X be non empty set, F be sequence of X, n be Nat; now let y be object; assume y in rng(F|Segm(n+1)); then consider x be object such that A1: x in dom(F|Segm(n+1)) & y = (F|Segm(n+1)).x by FUNCT_1:def 3; reconsider x as Nat by A1; A4: y = F.x by A1,FUNCT_1:47; x in dom F /\ Segm(n+1) by A1,RELAT_1:61; then A2: x in dom F & x in Segm(n+1) by XBOOLE_0:def 4; x < n+1 by A2,NAT_1:44; then A3: x <= n by NAT_1:13; per cases; suppose x = n; then y in {F.n} by A4,TARSKI:def 1; hence y in rng(F|Segm n) \/ {F.n} by XBOOLE_0:def 3; end; suppose x <> n; then x < n by A3,XXREAL_0:1; then x in Segm n by NAT_1:44; then x in dom F /\ Segm n by A2,XBOOLE_0:def 4; then x in dom(F|Segm n) by RELAT_1:61; then (F|Segm n).x in rng(F|Segm n) & (F|Segm n).x = F.x by FUNCT_1:3,47; hence y in rng(F|Segm n) \/ {F.n} by A4,XBOOLE_0:def 3; end; end; then A5:rng(F|Segm(n+1)) c= rng(F|Segm n) \/ {F.n} by TARSKI:def 3; now let y be object; assume A6: y in rng(F|Segm n) \/ {F.n}; per cases by A6,XBOOLE_0:def 3; suppose A7: y in rng(F|Segm n); n <= n+1 by NAT_1:11; then F|Segm n c= F|Segm(n+1) by NAT_1:39,RELAT_1:75; then rng(F|Segm n) c= rng(F|Segm(n+1)) by RELAT_1:11; hence y in rng(F|Segm(n+1)) by A7; end; suppose y in {F.n}; then A8: y = F.n by TARSKI:def 1; n in NAT by ORDINAL1:def 12; then n in dom F & n in Segm(n+1) by FUNCT_2:def 1,NAT_1:45; then n in dom F /\ Segm(n+1) by XBOOLE_0:def 4; then A9: n in dom(F|Segm(n+1)) by RELAT_1:61; then F.n = (F|Segm(n+1)).n by FUNCT_1:47; hence y in rng(F|Segm(n+1)) by A8,A9,FUNCT_1:3; end; end; then rng(F|Segm n) \/ {F.n} c= rng(F|Segm(n+1)) by TARSKI:def 3; hence thesis by A5,XBOOLE_0:def 10; end; theorem Th58: for X be set, S be Field_Subset of X, M be Measure of S, F be Sep_Sequence of S, n be Nat holds union rng(F|Segm(n+1)) in S & Partial_Sums(M*F).n = M.(union rng(F|Segm(n+1))) proof let X be set, S be Field_Subset of X, M be Measure of S, F be Sep_Sequence of S, n be Nat; A2: rng(F|Segm(0+1)) = rng(F|Segm 0) \/ {F.0} by Th57 .= {F.0}; then A2a:union rng(F|Segm(0+1)) = F.0 by ZFMISC_1:25; defpred P2[Nat] means union rng(F|Segm($1+1)) in S; A14:P2[0] by A2a; A15:for k be Nat st P2[k] holds P2[k+1] proof let k be Nat; assume A16: P2[k]; union rng(F|Segm(k+1+1)) = union(rng(F|Segm(k+1)) \/ {F.(k+1)}) by Th57 .= union rng(F|Segm(k+1)) \/ union {F.(k+1)} by ZFMISC_1:78 .= union rng(F|Segm(k+1)) \/ F.(k+1) by ZFMISC_1:25; hence union rng(F|Segm(k+1+1)) in S by A16,PROB_1:3; end; P1: for k be Nat holds P2[k] from NAT_1:sch 2(A14,A15); hence union rng(F|Segm(n+1)) in S; defpred P[Nat] means Partial_Sums(M*F).$1 = M.(union rng (F|Segm ($1+1))); A1: Partial_Sums(M*F).0 = (M*F).0 by MESFUNC9:def 1 .= M.(F.0) by FUNCT_2:15; A3: P[0] by A1,A2,ZFMISC_1:25; A4: for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume A5: P[n]; A6: Partial_Sums(M*F).(n+1) = Partial_Sums(M*F).n + (M*F).(n+1) by MESFUNC9:def 1 .= M.(union rng(F|Segm(n+1))) + M.(F.(n+1)) by A5,FUNCT_2:15; A13: now assume ex x be object st x in union rng(F|Segm(n+1)) /\ F.(n+1); then consider x be object such that A7: x in union rng(F|Segm(n+1)) /\ F.(n+1); A8: x in union rng(F|Segm(n+1)) & x in F.(n+1) by A7,XBOOLE_0:def 4; then consider A be set such that A9: x in A & A in rng(F|Segm(n+1)) by TARSKI:def 4; consider k be object such that A10: k in dom(F|Segm(n+1)) & A = (F|Segm(n+1)).k by A9,FUNCT_1:def 3; reconsider k as Nat by A10; A11: k < n+1 by A10,RELAT_1:57,NAT_1:44; A = F.k by A10,FUNCT_1:47; then x in F.k /\ F.(n+1) by A8,A9,XBOOLE_0:def 4; hence contradiction by A11,PROB_2:def 2,XBOOLE_0:4; end; union rng(F|Segm(n+1)) in S by P1; then M.(union rng(F|Segm(n+1))) + M.(F.(n+1)) = M.(union rng(F|Segm(n+1)) \/ F.(n+1)) by A13,XBOOLE_0:4,MEASURE1:def 8 .= M.( union rng(F|Segm(n+1)) \/ union {F.(n+1)} ) by ZFMISC_1:25 .= M.( union (rng(F|Segm(n+1)) \/ {F.(n+1)}) ) by ZFMISC_1:78 .= M.( union rng(F|Segm(n+1+1)) ) by Th57; hence thesis by A6; end; for n be Nat holds P[n] from NAT_1:sch 2(A3,A4); hence Partial_Sums(M*F).n = M.(union rng (F|Segm (n+1))); end; theorem Th59: for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be Measure of Field_generated_by S st ( for A be set st A in Field_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds M.A = Sum(P*F) ) holds M is completely-additive proof let X be set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be Measure of Field_generated_by S; assume A1: for A be set st A in Field_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds M.A = Sum(P*F); now let FSets be Sep_Sequence of Field_generated_by S; assume B0: union rng FSets in Field_generated_by S; then union rng FSets in DisUnion S by SRINGS_3:22; then consider A be Subset of X such that B1: A = union rng FSets & ex F be disjoint_valued FinSequence of S st A = Union F; consider D be disjoint_valued FinSequence of S such that B2: A = Union D by B1; set Z = {[n,E] where n is Nat, E is disjoint_valued FinSequence of S : Union E = FSets.n & (FSets.n={} implies E = <*{}*>) }; reconsider Y = proj2 Z as FinSequenceSet of S by Th51; E4: Y is with_non-empty_elements by Th51; per cases; suppose rng FSets is with_non-empty_element; then consider a be non empty set such that E6: a in rng FSets; ex E be FinSequence of S st E in Y & Union E = a by E6,Th51; then reconsider Y as non empty with_non-empty_element FinSequenceSet of S by E4; defpred P[Element of NAT,object] means [$1,$2] in Z; F2: for n be Element of NAT ex y be Element of Y st P[n,y] proof let n be Element of NAT; FSets.n in Field_generated_by S; then FSets.n in DisUnion S by SRINGS_3:22; then consider A be Subset of X such that F3: FSets.n = A & ex F be disjoint_valued FinSequence of S st A = Union F; consider F be disjoint_valued FinSequence of S such that F4: A = Union F by F3; per cases; suppose F5: FSets.n = {}; F6: rng <*{}*> = { {} } by FINSEQ_1:38; {} in S by SETFAM_1:def 8; then reconsider E = <*{}*> as disjoint_valued FinSequence of S by F6,ZFMISC_1:31,FINSEQ_1:def 4; union rng E = {} by F6,ZFMISC_1:25; then Union E = {} by CARD_3:def 4; then F7: [n,E] in Z by F5; then E in Y by XTUPLE_0:def 13; hence ex y be Element of Y st P[n,y] by F7; end; suppose FSets.n <> {}; then F8: [n,F] in Z by F4,F3; then F in Y by XTUPLE_0:def 13; hence ex y be Element of Y st P[n,y] by F8; end; end; consider s be Function of NAT,Y such that F9: for n be Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(F2); now let n be object; assume n in dom s; then reconsider n1=n as Element of NAT; [n1,s.n1] in Z by F9; then F11: ex m be Nat, E be disjoint_valued FinSequence of S st [n1,s.n1] = [m,E] & Union E = FSets.m & (FSets.m={} implies E=<*{}*>); now assume F15: s.n = {}; then union rng(s.n1) = {} by ZFMISC_1:2; then Union s.n1 = {} by CARD_3:def 4; hence contradiction by F11,F15,XTUPLE_0:1; end; hence s.n is non empty; end; then reconsider s as non-empty sequence of Y by FUNCT_1:def 9; reconsider G = joined_seq s as sequence of S; now let x,y be object; assume F16: x <> y; per cases; suppose not x in NAT or not y in NAT; then not x in dom G or not y in dom G; then G.x = {} or G.y = {} by FUNCT_1:def 2; hence G.x misses G.y by XBOOLE_1:65; end; suppose x in NAT & y in NAT; then reconsider n1=x, n2=y as Element of NAT; consider k1,m1 be Nat such that F17: m1 in dom(s.k1) & (Partial_Sums(Length s)).k1 - len(s.k1) + m1-1 = n1 & G.n1 = (s.k1).m1 by Def4; consider k2,m2 be Nat such that F18: m2 in dom(s.k2) & (Partial_Sums(Length s)).k2 - len(s.k2) + m2-1 = n2 & G.n2 = (s.k2).m2 by Def4; k1 is Element of NAT & k2 is Element of NAT by ORDINAL1:def 12; then F21: [k1,s.k1] in Z & [k2,s.k2] in Z by F9; then consider i1 be Nat, E1 be disjoint_valued FinSequence of S such that F22: [k1,s.k1] = [i1,E1] & Union E1 = FSets.i1 & (FSets.i1={} implies E1 = <*{}*>); consider i2 be Nat, E2 be disjoint_valued FinSequence of S such that F23: [k2,s.k2] = [i2,E2] & Union E2 = FSets.i2 & (FSets.i2={} implies E2 = <*{}*>) by F21; F24: k1=i1 & s.k1=E1 & k2=i2 & s.k2=E2 by F22,F23,XTUPLE_0:1; now assume k1<>k2; then FSets.i1 misses FSets.i2 by F24,PROB_2:def 2; then union rng(s.k1) misses Union(s.k2) by F22,F23,F24,CARD_3:def 4; then F25: union rng(s.k1) misses union rng(s.k2) by CARD_3:def 4; G.n1 c= union rng(s.k1) & G.n2 c= union rng(s.k2) by F17,F18,FUNCT_1:3,ZFMISC_1:74; hence G.n1 misses G.n2 by F25,XBOOLE_1:64; end; hence G.x misses G.y by F16,F17,F18,F24,PROB_2:def 2; end; end; then reconsider G as disjoint_valued sequence of S by PROB_2:def 2; now let x be object; assume x in Union FSets; then x in union rng FSets by CARD_3:def 4; then consider A be set such that G1: x in A & A in rng FSets by TARSKI:def 4; consider n be Element of NAT such that G2: A = FSets.n by G1,FUNCT_2:113; [n,s.n] in Z by F9; then consider n2 be Nat, E2 be disjoint_valued FinSequence of S such that G6: [n,s.n] = [n2,E2] & Union E2 = FSets.n2 & (FSets.n2={} implies E2=<*{}*>); n=n2 & s.n = E2 by G6,XTUPLE_0:1; then x in union rng(s.n) by G1,G2,G6,CARD_3:def 4; then consider A2 be set such that G8: x in A2 & A2 in rng (s.n) by TARSKI:def 4; consider m be object such that G9: m in dom (s.n) & A2 = (s.n).m by G8,FUNCT_1:def 3; reconsider m as Nat by G9; consider N be Nat such that G10: N = (Partial_Sums(Length s)).n - len(s.n) + m - 1 & G.N = (s.n).m by G9,Th13; A2 in rng G by FUNCT_2:4,G9,G10,ORDINAL1:def 12; then x in union rng G by G8,TARSKI:def 4; hence x in Union G by CARD_3:def 4; end; then T0: Union FSets c= Union G by TARSKI:def 3; now let x be object; assume x in Union G; then x in union rng G by CARD_3:def 4; then consider A be set such that G11: x in A & A in rng G by TARSKI:def 4; consider n be Element of NAT such that G12: A = G.n by G11,FUNCT_2:113; consider k,m be Nat such that G13: m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n & G.n = (s.k).m by Def4; k is Element of NAT by ORDINAL1:def 12; then [k,s.k] in Z by F9; then consider k2 be Nat, E be disjoint_valued FinSequence of S such that G14: [k,s.k] = [k2,E] & Union E = FSets.k2 & (FSets.k2={} implies E=<*{}*>); G15: k = k2 & s.k = E by G14,XTUPLE_0:1; x in (s.k).m & (s.k).m in rng(s.k) by G11,G12,G13,FUNCT_1:3; then x in union rng(s.k) by TARSKI:def 4; then G16: x in FSets.k2 by G14,G15,CARD_3:def 4; FSets.k2 in rng FSets by FUNCT_2:4,ORDINAL1:def 12; then x in union rng FSets by G16,TARSKI:def 4; hence x in Union FSets by CARD_3:def 4; end; then Union G c= Union FSets by TARSKI:def 3; then T1: Union FSets = Union G by T0,XBOOLE_0:def 10; defpred Q[Nat,Nat,object] means ($1 + 1 <= len D implies $3 = D.($1 +1) /\ G.$2) & ($1 + 1 > len D implies $3 = {}); D0: for i be Element of NAT for j be Element of NAT ex z be Element of S st Q[i,j,z] proof let i,j be Element of NAT; per cases; suppose D1: i+1 <= len D; then i+1 in dom D by NAT_1:11,FINSEQ_3:25; then D.(i+1) in rng D by FUNCT_1:3; then D.(i+1) /\ G.j in S by FINSUB_1:def 2; hence ex z be Element of S st Q[i,j,z] by D1; end; suppose D4: i+1 > len D; {} in S by SETFAM_1:def 8; hence ex z be Element of S st Q[i,j,z] by D4; end; end; consider LG be Function of [:NAT,NAT:],S such that D5: for i be Element of NAT for j be Element of NAT holds Q[i,j,LG.(i,j)] from BINOP_1:sch 3(D0); D5a: for i,j be Nat holds (i+1 <= len D implies LG.(i,j) = D.(i+1) /\ G.j) & (i+1 > len D implies LG.(i,j) = {}) proof let i,j be Nat; reconsider i1=i, j1=j as Element of NAT by ORDINAL1:def 12; DD5: now assume i+1 <= len D; then LG.(i1,j1) = D.(i+1) /\ G.j by D5; hence LG.(i,j) = D.(i+1) /\ G.j; end; now assume i+1 > len D; then LG.(i1,j1) = {} by D5; hence LG.(i,j) = {}; end; hence thesis by DD5; end; Union FSets = union rng FSets by CARD_3:def 4; then X2: M.(Union FSets) = Sum(P*D) by A1,B0,B1,B2; consider SumPD be sequence of ExtREAL such that X3: Sum(P*D) = SumPD.(len(P*D)) & SumPD.0 = 0. & for i be Nat st i < len(P*D) holds SumPD.(i+1) = SumPD.i + (P*D).(i+1) by EXTREAL1:def 2; X4: for i be Element of NAT st i < len D holds D.(i+1) = Union ProjMap1(LG,i) proof let i be Element of NAT; assume X40: i < len D; then 1 <= i+1 & i+1 <= len D by NAT_1:11,13; then i+1 in dom D by FINSEQ_3:25; then X41: D.(i+1) in rng D by FUNCT_1:3; now let x be object; assume X44: x in D.(i+1); then x in union rng D by X41,TARSKI:def 4; then x in Union D by CARD_3:def 4; then x in Union G by B1,B2,T1,CARD_3:def 4; then x in union rng G by CARD_3:def 4; then consider Gx be set such that X42: x in Gx & Gx in rng G by TARSKI:def 4; consider j be Element of NAT such that X43: Gx = G.j by X42,FUNCT_2:113; X46: dom ProjMap1(LG,i) = NAT by FUNCT_2:def 1; X45: x in D.(i+1) /\ G.j by X44,X42,X43,XBOOLE_0:def 4; i+1 <= len D implies LG.(i,j) = D.(i+1) /\ G.j by D5; then X47: x in ProjMap1(LG,i).j by X40,NAT_1:13,X45,MESFUNC9:def 6; ProjMap1(LG,i).j in rng ProjMap1(LG,i) by X46,FUNCT_1:3; then x in union rng ProjMap1(LG,i) by X47,TARSKI:def 4; hence x in Union ProjMap1(LG,i) by CARD_3:def 4; end; then X48: D.(i+1) c= Union ProjMap1(LG,i) by TARSKI:def 3; now let x be object; assume x in Union ProjMap1(LG,i); then x in union rng ProjMap1(LG,i) by CARD_3:def 4; then consider Px be set such that X50: x in Px & Px in rng ProjMap1(LG,i) by TARSKI:def 4; consider j be Element of NAT such that X51: Px = ProjMap1(LG,i).j by X50,FUNCT_2:113; ProjMap1(LG,i).j = LG.(i,j) by MESFUNC9:def 6; then x in D.(i+1) /\ G.j by X50,X51,D5; hence x in D.(i+1) by XBOOLE_0:def 4; end; then Union ProjMap1(LG,i) c= D.(i+1) by TARSKI:def 3; hence thesis by X48,XBOOLE_0:def 10; end; X5: for i be Element of NAT st i < len D holds (P*D).(i+1) <= (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).i proof let i be Element of NAT; assume X50: i < len D; then X50a: 1 <= i+1 & i+1 <= len D by NAT_1:11,13; then X51: i+1 in dom D by FINSEQ_3:25; then X52: D.(i+1) in rng D by FUNCT_1:3; now let x,y be object; assume V1: x<>y; per cases; suppose not x in dom(ProjMap1(LG,i)) or not y in dom(ProjMap1(LG,i)); then ProjMap1(LG,i).x = {} or ProjMap1(LG,i).y = {} by FUNCT_1:def 2; hence ProjMap1(LG,i).x misses ProjMap1(LG,i).y by XBOOLE_1:65; end; suppose x in dom(ProjMap1(LG,i)) & y in dom(ProjMap1(LG,i)); then reconsider x1=x,y1=y as Element of NAT; ProjMap1(LG,i).x = LG.(i,x1) & ProjMap1(LG,i).y = LG.(i,y1) by MESFUNC9:def 6; then ProjMap1(LG,i).x = D.(i+1) /\ G.x1 & ProjMap1(LG,i).y = D.(i+1) /\ G.y1 by X50a,D5; hence ProjMap1(LG,i).x misses ProjMap1(LG,i).y by V1,PROB_2:def 2,XBOOLE_1:76; end; end; then X53: ProjMap1(LG,i) is disjoint_valued Function of NAT,S by PROB_2:def 2; X54: D.(i+1) = Union ProjMap1(LG,i) by X4,X50; X55: (P*D).(i+1) = P.(D.(i+1)) by X51,FUNCT_1:13 .= P.(Union ProjMap1(LG,i)) by X4,X50; X56: now let k be Element of NAT; P.(LG.(i,k)) = (P*LG).(i,k) by ZFMISC_1:87,FUNCT_2:15; then ProjMap1(P*LG,i).k = P.(LG.(i,k)) by MESFUNC9:def 6 .= P.(ProjMap1(LG,i).k) by MESFUNC9:def 6; hence (P*ProjMap1(LG,i)).k = (ProjMap1(P*LG,i)).k by FUNCT_2:15; end; SUM(P*(ProjMap1(LG,i))) = Sum(P*(ProjMap1(LG,i))) by MEASURE8:2 .= lim Partial_Sums(P*ProjMap1(LG,i)) by MESFUNC9:def 3 .= lim Partial_Sums(ProjMap1(P*LG,i)) by X56,FUNCT_2:def 8 .= lim ProjMap1(Partial_Sums_in_cod2(P*LG),i) by DBLSEQ_3:53 .= (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).i by DBLSEQ_3:def 13; hence thesis by X55,X52,X53,X54,Def8; end; defpred SPD[Nat] means $1 < len(P*D) implies SumPD.($1+1) <= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).$1; rng D c= S; then rng D c= dom P by FUNCT_2:def 1; then dom(P*D) = dom D by RELAT_1:27; then X71: len(P*D) = len D by FINSEQ_3:29; now assume X60: 0 < len(P*D); then X61: (P*D).(0+1) <= (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).0 by X5,X71; SumPD.(0+1) = SumPD.0 + (P*D).(0+1) by X60,X3; then SumPD.(0+1) = (P*D).1 by X3,XXREAL_3:4; hence SumPD.(0+1) <= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).0 by X61,MESFUNC9:def 1; end; then X62: SPD[0]; X63: for k be Nat st SPD[k] holds SPD[k+1] proof let k be Nat; assume X64: SPD[k]; assume X65: k+1 < len(P*D); then X67: (P*D).(k+1+1) <= (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(k+1) by X5,X71; SumPD.(k+1+1) = SumPD.(k+1) + (P*D).(k+1+1) by X3,X65; then SumPD.(k+1+1) <= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).k + (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(k+1) by NAT_1:13,X67,X64,X65,XXREAL_3:36; hence SumPD.(k+1+1) <= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(k+1) by MESFUNC9:def 1; end; X68: for k be Nat holds SPD[k] from NAT_1:sch 2(X62,X63); XX70:now assume D = {}; then union rng D = {} by ZFMISC_1:2; then X69: union rng FSets = {} by B1,B2,CARD_3:def 4; union {a} c= union rng FSets by E6,ZFMISC_1:31,77; hence contradiction by X69; end; then consider i1 be Nat such that X70: len D = i1 + 1 by NAT_1:6; reconsider i1 as Element of NAT by ORDINAL1:def 12; i1 < len D by X70,NAT_1:13; then X72: Sum(P*D) <= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).i1 by X70,X71,X68,X3; X73: len(P*D) >= i1 by X70,X71,NAT_1:11; W3: Partial_Sums_in_cod2(P*LG) is convergent_in_cod2 by DBLSEQ_3:66; then X80: lim_in_cod2(Partial_Sums_in_cod2(P*LG)) is nonnegative by DBLSEQ_3:65; then X74: (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).i1 <= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D)) by X73,RINFSUP2:7,MESFUNC9:16; (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D)) = (lim_in_cod2(Partial_Sums(P*LG))).(len(P*D)) proof per cases; suppose X75: (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D)) = +infty; then ex k be Element of NAT st k <= len(P*D) & ProjMap1(Partial_Sums_in_cod2(P*LG),k) is convergent_to_+infty by DBLSEQ_3:74; then lim ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1(P*LG)),len(P*D)) = +infty by DBLSEQ_3:77; then lim ProjMap1(Partial_Sums(P*LG),len(P*D)) = +infty by DBLSEQ_3:def 16; hence (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D)) = (lim_in_cod2(Partial_Sums(P*LG))).(len(P*D)) by X75,DBLSEQ_3:def 13; end; suppose (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D)) <> +infty; then X81: (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D)) < +infty by XXREAL_0:4; for m be Element of NAT holds ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_finite_number proof let m be Element of NAT; W5: ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_+infty or ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_finite_number or ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_-infty by W3,DBLSEQ_3:def 11,MESFUNC5:def 11; per cases; suppose m <= len(P*D); then W1: Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m <= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)) by X80,MESFUNC9:16,RINFSUP2:7; (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m <= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m by X80,DBLSEQ_3:4; then W2: (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m <= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)) by W1,XXREAL_0:2; (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m >= 0 by X80,SUPINF_2:51; then (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m in REAL by W2,X81,XXREAL_0:14; then lim ProjMap1(Partial_Sums_in_cod2(P*LG),m) in REAL by DBLSEQ_3:def 13; hence ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_finite_number by W5,MESFUNC5:def 12; end; suppose m > len(P*D); then consider j be Nat such that W7: m = len(P*D) + j by NAT_1:10; defpred H[Nat] means Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)+$1) = Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)); W8: H[0]; W9: for i be Nat st H[i] holds H[i+1] proof let i be Nat; assume W12: H[i]; W13: Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)+i+1) = Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).len(P*D) + (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)+i+1) by W12,MESFUNC9:def 1; for s be Nat holds ProjMap1(Partial_Sums_in_cod2(P*LG),len(P*D)+i+1).s = 0 proof let s be Nat; reconsider s1 = s as Element of NAT by ORDINAL1:def 12; W15: ProjMap1(Partial_Sums_in_cod2(P*LG),len(P*D)+i+1).s1 = (Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,s) by MESFUNC9:def 6; P0: for k,j be Nat holds (P*LG).(len(P*D)+k+1,j) = 0 proof let k,j be Nat; reconsider k1=k, j1=j as Element of NAT by ORDINAL1:def 12; len D + k +1 >= len D by NAT_1:11,12; then P1: len D + k1 + 1 + 1> len D by NAT_1:13; [len(P*D)+k1+1,j1] in [:NAT,NAT:] by ZFMISC_1:87; then [len(P*D)+k1+1,j1] in dom LG by FUNCT_2:def 1; then (P*LG).(len(P*D)+k+1,j) = P.(LG.(len D + k1+1,j1)) by X71,FUNCT_1:13; then (P*LG).(len(P*D)+k+1,j) = P.{} by D5,P1; hence thesis by VALUED_0:def 19; end; defpred G[Nat] means (Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,$1) = 0; (Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,0) = (P*LG).(len(P*D)+i+1,0) by DBLSEQ_3:def 14; then W16: G[0] by P0; W17: for j be Nat st G[j] holds G[j+1] proof let j be Nat; assume P2: G[j]; (Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,j+1) = (Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,j) + (P*LG).(len(P*D)+i+1,j+1) by DBLSEQ_3:def 14 .= (P*LG).(len(P*D)+i+1,j+1) by P2,XXREAL_3:4; hence G[j+1] by P0; end; for j be Nat holds G[j] from NAT_1:sch 2(W16,W17); hence ProjMap1(Partial_Sums_in_cod2(P*LG),len(P*D)+i+1).s = 0 by W15; end; then lim (ProjMap1(Partial_Sums_in_cod2(P*LG),len(P*D)+i+1)) = 0 by MESFUNC5:52; then (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)+i+1) = 0 by DBLSEQ_3:def 13; hence H[i+1] by W13,XXREAL_3:4; end; for i be Nat holds H[i] from NAT_1:sch 2(W8,W9); then H[j]; then W10: (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m <= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)) by W7,X80,DBLSEQ_3:4; (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m > -infty by X80,SUPINF_2:51; then (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m in REAL by W10,X81,XXREAL_0:14; then lim ProjMap1(Partial_Sums_in_cod2(P*LG),m) in REAL by DBLSEQ_3:def 13; hence ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_finite_number by W5,MESFUNC5:def 12; end; end; then Partial_Sums (P*LG) is convergent_in_cod2_to_finite by DBLSEQ_3:def 10,81; then (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D)) = lim(ProjMap1(Partial_Sums_in_cod2 (Partial_Sums_in_cod1 (P*LG)),len(P*D))) by DBLSEQ_3:82 .= lim(ProjMap1(Partial_Sums (P*LG),len(P*D))) by DBLSEQ_3:def 16; hence (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D)) = (lim_in_cod2(Partial_Sums(P*LG))).(len(P*D)) by DBLSEQ_3:def 13; end; end; then X100:Sum(P*D) <= (lim_in_cod2(Partial_Sums(P*LG))).(len(P*D)) by X74,X72,XXREAL_0:2; for j be Nat holds (Partial_Sums_in_cod1(P*LG)).(len(P*D),j) = (P*G).j proof let j be Nat; reconsider j1=j as Element of NAT by ORDINAL1:def 12; consider k,m be Nat such that M0: m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = j & G.j = (s.k).m by Def4; reconsider k1=k as Element of NAT by ORDINAL1:def 12; [k1,s.k1] in Z by F9; then consider k2 be Nat, Sk be disjoint_valued FinSequence of S such that M1: [k1,s.k1] = [k2,Sk] & Union Sk = FSets.k2 & (FSets.k2={} implies Sk=<*{}*>); M2: s.k = Sk & Union Sk = FSets.k & (FSets.k = {} implies Sk=<*{}*>) by M1,XTUPLE_0:1; defpred Cj[Nat,object] means $2 = D.$1 /\ G.j; M3: for k be Nat st k in Seg len D ex x be Element of S st Cj[k,x] proof let k be Nat; assume M5: k in Seg len D; then 1 <= k & k <= len D by FINSEQ_1:1; then consider k1 be Nat such that M4: k = k1+1 by NAT_1:6; reconsider kk1=k1 as Element of NAT by ORDINAL1:def 12; LG.(kk1,j1) = D.k /\ G.j by M4,M5,D5,FINSEQ_1:1; hence thesis; end; consider Cj be FinSequence of S such that M7: dom Cj = Seg len D & for k be Nat st k in Seg len D holds Cj[k,Cj.k] from FINSEQ_1:sch 5(M3); M7a: len Cj = len D by M7,FINSEQ_1:def 3; now let x,y be object; assume M61: x <> y; per cases; suppose M62: x in dom Cj & y in dom Cj; then reconsider x1=x, y1=y as Nat; Cj.x = D.x1 /\ G.j & Cj.y = D.y1 /\ G.j by M7,M62; hence Cj.x misses Cj.y by M61,PROB_2:def 2,XBOOLE_1:76; end; suppose not x in dom Cj or not y in dom Cj; then Cj.x = {} or Cj.y = {} by FUNCT_1:def 2; hence Cj.x misses Cj.y by XBOOLE_1:65; end; end; then reconsider Cj as disjoint_valued FinSequence of S by PROB_2:def 2; now let x be object; assume x in Union Cj; then x in union rng Cj by CARD_3:def 4; then consider V be set such that M64: x in V & V in rng Cj by TARSKI:def 4; consider y be object such that M65: y in dom Cj & V = Cj.y by M64,FUNCT_1:def 3; reconsider y as Nat by M65; Cj.y = D.y /\ G.j by M65,M7; hence x in G.j by M64,M65,XBOOLE_0:def 4; end; then M66: Union Cj c= G.j by TARSKI:def 3; now let x be object; assume M67a: x in G.j; then x in Sk.m & Sk.m in rng Sk by M0,M2,FUNCT_1:3; then x in union rng Sk by TARSKI:def 4; then M67: x in FSets.k2 by M1,CARD_3:def 4; dom FSets = NAT by FUNCT_2:def 1; then FSets.k2 in rng FSets by FUNCT_1:3,ORDINAL1:def 12; then x in union rng FSets by M67,TARSKI:def 4; then x in union rng D by B1,B2,CARD_3:def 4; then consider V be set such that M68: x in V & V in rng D by TARSKI:def 4; consider y be object such that M69: y in dom D & V = D.y by M68,FUNCT_1:def 3; reconsider y as Nat by M69; M70: x in D.y /\ G.j by M67a,M68,M69,XBOOLE_0:def 4; y in Seg len D by M69,FINSEQ_1:def 3; then M71: x in Cj.y by M7,M70; y in dom Cj by M69,FINSEQ_1:def 3,M7; then Cj.y in rng Cj by FUNCT_1:3; then x in union rng Cj by M71,TARSKI:def 4; hence x in Union Cj by CARD_3:def 4; end; then G.j c= Union Cj by TARSKI:def 3; then M6: Union Cj = G.j by M66,XBOOLE_0:def 10; M6b: P.(G.j) = Sum(P*Cj) by M6,Def8; j in NAT by ORDINAL1:def 12; then j in dom G by FUNCT_2:def 1; then M6a: (P*G).j = Sum(P*Cj) by M6b,FUNCT_1:13; consider SumPCj be sequence of ExtREAL such that M8: Sum(P*Cj) = SumPCj.(len (P*Cj)) & SumPCj.0 = 0. & for i be Nat st i < len (P*Cj) holds SumPCj.(i+1) = SumPCj.i+(P*Cj).(i+1) by EXTREAL1:def 2; rng Cj c= S; then rng Cj c= dom P by FUNCT_2:def 1; then N9: dom(P*Cj) = dom Cj by RELAT_1:27; then M9: len(P*Cj) = len Cj by FINSEQ_3:29; M13: for i be Nat st i < len D holds (P*Cj).(i+1) = (P*LG).(i,j) proof let i be Nat; assume i < len D; then M11: 1<= i+1 & i+1 <= len D by NAT_1:11,13; then M12: i+1 in Seg len D; (P*Cj).(i+1) = P.(Cj.(i+1)) by M11,N9,M7a,FINSEQ_3:25,FUNCT_1:12; then (P*Cj).(i+1) = P.(D.(i+1) /\ G.j) by M7,M12; then M10: (P*Cj).(i+1) = P.(LG.(i,j)) by M11,D5a; i in NAT & j in NAT by ORDINAL1:def 12; then [i,j] in [:NAT,NAT:] by ZFMISC_1:87; then [i,j] in dom LG by FUNCT_2:def 1; hence (P*Cj).(i+1) = (P*LG).(i,j) by M10,FUNCT_1:13; end; MM15: len(P*D) +1 > len D by X71,NAT_1:13; len(P*D) in NAT & j in NAT by ORDINAL1:def 12; then [len(P*D),j] in [:NAT,NAT:] by ZFMISC_1:87; then [len(P*D),j] in dom LG by FUNCT_2:def 1; then (P*LG).(len(P*D),j) = P.(LG.(len(P*D),j)) by FUNCT_1:13; then (P*LG).(len(P*D),j) = P.{} by MM15,D5a; then M15: (P*LG).(len(P*D),j) = 0 by VALUED_0:def 19; consider LENDM1 be Nat such that M23: len D = LENDM1 + 1 by XX70,NAT_1:6; M24: LENDM1 < len(P*D) by M23,X71,NAT_1:13; defpred EQ[Nat] means $1 < len(P*D) implies (Partial_Sums_in_cod1(P*LG)).($1,j) = SumPCj.($1 + 1); (Partial_Sums_in_cod1(P*LG)).(0,j) = (P*LG).(0,j) by DBLSEQ_3:def 15; then M17: (Partial_Sums_in_cod1(P*LG)).(0,j) = (P*Cj).(0+1) by XX70,M13; SumPCj.(0+1) = 0 + (P*Cj).(0+1) by XX70,M7a,M9,M8; then M18: EQ[0] by M17,XXREAL_3:4; M22: for k be Nat st EQ[k] holds EQ[k+1] proof let k be Nat; assume M19: EQ[k]; assume M20: k+1 < len(P*D); then (Partial_Sums_in_cod1(P*LG)).(k+1,j) = SumPCj.(k+1) + (P*LG).(k+1,j) by M19,NAT_1:13,DBLSEQ_3:def 15 .= SumPCj.(k+1) + (P*Cj).(k+1+1) by M20,M13,X71; hence (Partial_Sums_in_cod1(P*LG)).(k+1,j) = SumPCj.(k+1+1) by M20,M9,M7a,M8,X71; end; for k be Nat holds EQ[k] from NAT_1:sch 2(M18,M22); then (Partial_Sums_in_cod1(P*LG)).(LENDM1,j) = (P*G).j by M6a,M8,M24,M23,M7a,M9; then (Partial_Sums_in_cod1(P*LG)).(len(P*D),j) = (P*G).j + 0 by M15,X71,M23,DBLSEQ_3:def 15; hence thesis by XXREAL_3:4; end; then X120:M.(Union FSets) <= Sum(P*G) by X2,X100,DBLSEQ_3:41; Partial_Sums (P*G) is non-decreasing by MESFUNC9:16; then X123:Partial_Sums (P*G) is convergent by RINFSUP2:37; X124:Partial_Sums(M*FSets) is subsequence of Partial_Sums(P*G) proof consider N be increasing sequence of NAT such that Z0: for k be Nat holds N.k = (Partial_Sums(Length s)).k - 1 by Th11; defpred P[Nat] means ((Partial_Sums(P*G))*N).$1 = (Partial_Sums(M*FSets)).$1; [0,s.0] in Z by F9; then consider n0 be Nat, E0 be disjoint_valued FinSequence of S such that Z1: [0,s.0] = [n0,E0] & Union E0 = FSets.n0 & (FSets.n0={} implies E0=<*{}*>); Z2: n0 = 0 & E0 = s.0 by Z1,XTUPLE_0:1; Z4: M.(Union E0) = Sum(P*E0) by A1,Z1; consider SPE0 be sequence of ExtREAL such that Z5: Sum(P*E0) = SPE0.(len(P*E0)) & SPE0.0 = 0. & for i be Nat st i < len(P*E0) holds SPE0.(i+1)=SPE0.i + (P*E0).(i+1) by EXTREAL1:def 2; rng E0 c= S; then rng E0 c= dom P by FUNCT_2:def 1; then ZZ10: dom(P*E0) = dom E0 by RELAT_1:27; then Z10: len(P*E0) = len E0 by FINSEQ_3:29; len(s.0) >= 1 by FINSEQ_1:20; then Z11: len(s.0) in dom(s.0) & 1 in dom(s.0) by FINSEQ_3:25; then consider N0 be Nat such that Z6: N0 = (Partial_Sums(Length s)).0 - len(s.0) + len(s.0) - 1 & G.N0 = (s.0).(len(s.0)) by Th13; Z6d: N0 = N.0 by Z0,Z6; N0 = (Length s).0 - 1 by Z6,SERIES_1:def 1; then Z6c: N0+1 = len(s.0) by Def3; then Z6b: N0 < len(s.0) by NAT_1:13; defpred P0[Nat] means $1 < len(P*E0) implies (Partial_Sums(P*G)).$1 = SPE0.($1+1); consider z0 be Nat such that Z7: z0 = (Partial_Sums(Length s)).0 - len(s.0) + 1 - 1 & G.z0 = (s.0).1 by Z11,Th13; z0 = (Length s).0 - len(s.0) by Z7,SERIES_1:def 1; then Z8: z0 = len(s.0) - len(s.0) by Def3; Z12: (Partial_Sums(P*G)).0 = (P*G).0 by MESFUNC9:def 1 .= P.((s.0).1) by Z7,Z8,FUNCT_2:15 .= (P*E0).1 by Z11,Z2,FUNCT_1:13; SPE0.(0+1) = 0+(P*E0).1 by Z5,Z10,Z2; then ZZ1: P0[0] by Z12,XXREAL_3:4; ZZ2: for i be Nat st P0[i] holds P0[i+1] proof let i be Nat; assume Z13: P0[i]; assume Z14: i+1 < len(P*E0); Z16: (Partial_Sums(P*G)).(i+1) = (Partial_Sums(P*G)).i + (P*G).(i+1) by MESFUNC9:def 1 .= SPE0.(i+1) + P.(G.(i+1)) by Z14,NAT_1:13,Z13,FUNCT_2:15; Z18: 1 <= i+1+1 & i+1+1 <= len(P*E0) by Z14,NAT_1:11,13; then consider zi1 be Nat such that Z17: zi1 = (Partial_Sums(Length s)).0 - len(s.0) + (i+1+1) - 1 & G.zi1 = (s.0).(i+1+1) by Th13,ZZ10,Z2,FINSEQ_3:25; zi1 = (Length s).0 - len(s.0) + (i+1+1) - 1 by Z17,SERIES_1:def 1 .= len(s.0) - len(s.0) + (i+1+1) - 1 by Def3; then P.(G.(i+1)) = (P*E0).(i+1+1) by Z17,Z18,ZZ10,Z2,FINSEQ_3:25,FUNCT_1:13; hence (Partial_Sums(P*G)).(i+1) = SPE0.(i+1+1) by Z14,Z5,Z16; end; for i be Nat holds P0[i] from NAT_1:sch 2(ZZ1,ZZ2); then (Partial_Sums(P*G)).N0 = M.(FSets.0) by Z6b,Z6c,Z2,Z10,Z5,Z4,Z1; then (Partial_Sums(P*G)).N0 = (M*FSets).0 by FUNCT_2:15; then (Partial_Sums(P*G)).N0 = (Partial_Sums(M*FSets)).0 by MESFUNC9:def 1; then Z100: P[0] by Z6d,FUNCT_2:15; Z101: for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume Z20: P[n]; [n+1,s.(n+1)] in Z by F9; then consider N1 be Nat, E be disjoint_valued FinSequence of S such that Z21: [n+1,s.(n+1)] = [N1,E] & Union E = FSets.N1 & (FSets.N1={} implies E=<*{}*>); Z22: n+1 = N1 & s.(n+1) = E by Z21,XTUPLE_0:1; Z24: M.(Union E) = Sum(P*E) by A1,Z21; consider SPE be sequence of ExtREAL such that Z25: Sum(P*E) = SPE.(len(P*E)) & SPE.0 = 0. & for i be Nat st i < len(P*E) holds SPE.(i+1) = SPE.i + (P*E).(i+1) by EXTREAL1:def 2; rng E c= S; then rng E c= dom P by FUNCT_2:def 1; then ZZ30: dom(P*E) = dom E by RELAT_1:27; then Z30: len(P*E) = len E by FINSEQ_3:29; len(s.(n+1)) >= 1 by FINSEQ_1:20; then Z31: len(s.(n+1)) in dom(s.(n+1)) & 1 in dom(s.(n+1)) by FINSEQ_3:25; then consider NEnd be Nat such that Z26: NEnd = (Partial_Sums(Length s)).(n+1) - len(s.(n+1)) + len(s.(n+1))-1 & G.NEnd = (s.(n+1)).(len(s.(n+1))) by Th13; Z26d: NEnd = N.(n+1) by Z0,Z26; consider NSt be Nat such that Z27: NSt = (Partial_Sums(Length s)).(n+1) - len(s.(n+1)) + 1 - 1 & G.NSt = (s.(n+1)).1 by Z31,Th13; NSt = (Partial_Sums(Length s)).n + (Length s).(n+1) - len(s.(n+1)) by Z27,SERIES_1:def 1; then Z28: NSt = (Partial_Sums(Length s)).n + len(s.(n+1)) - len(s.(n+1)) by Def3; Z50: N.n = (Partial_Sums(Length s)).n - 1 by Z0; defpred PE[Nat] means $1 < len(P*E) implies (Partial_Sums(P*G)).(N.n + $1 + 1) = (Partial_Sums(P*G)).(N.n) + SPE.($1 + 1); Z40: (Partial_Sums(P*G)).(N.n + 1) = (Partial_Sums(P*G)).(N.n) + (P*G).(N.n + 1) by MESFUNC9:def 1 .= (Partial_Sums(P*G)).(N.n) + P.(G.(N.n + 1)) by FUNCT_2:15 .= (Partial_Sums(P*G)).(N.n) + (P*E).1 by Z31,Z22,Z50,Z28,Z27,FUNCT_1:13; SPE.(0+1) = SPE.0 + (P*E).(0+1) by Z25,Z30,Z22; then Z60: PE[0] by Z40,Z25,XXREAL_3:4; Z61: for j be Nat st PE[j] holds PE[j+1] proof let j be Nat; assume Z52: PE[j]; assume Z53: j+1 < len(P*E); then Z58a: 1 <= j+1+1 & j+1+1 <= len(P*E) by NAT_1:11,13; then consider Nj be Nat such that Z58: Nj = (Partial_Sums(Length s)).(n+1) - len(s.(n+1)) + (j+1+1) - 1 & G.Nj = (s.(n+1)).(j+1+1) by Th13,ZZ30,Z22,FINSEQ_3:25; Z55: (Partial_Sums(P*G)).(N.n) > -infty by SUPINF_2:51; Z56: P.(G.(N.n + j+1+1)) > -infty by SUPINF_2:51; defpred SP[Nat] means $1 <= len(P*E) implies SPE.$1 >=0; ZZ1: SP[0] by Z25; ZZ2: for t be Nat st SP[t] holds SP[t+1] proof let t be Nat; assume ZZ3: SP[t]; assume ZZ6: t+1 <= len(P*E); then ZZ5: SPE.(t+1) = SPE.t + (P*E).(t+1) by Z25,NAT_1:13; t+1 in dom(P*E) by NAT_1:11,ZZ6,FINSEQ_3:25; then (P*E).(t+1) = P.(E.(t+1)) by FUNCT_1:12; then (P*E).(t+1) >= 0 by SUPINF_2:51; hence thesis by ZZ3,ZZ6,NAT_1:13,ZZ5; end; for t be Nat holds SP[t] from NAT_1:sch 2(ZZ1,ZZ2); then Z57: SPE.(j+1) >=0 by Z53; (Partial_Sums(P*G)).(N.n + (j+1) + 1) = (Partial_Sums(P*G)).(N.n + (j+1)) + (P*G).(N.n + (j+1) + 1) by MESFUNC9:def 1 .= ( (Partial_Sums(P*G)).(N.n) + SPE.(j+1) ) + P.(G.(N.n + j+1+1)) by Z53,Z52,NAT_1:13,FUNCT_2:15 .= (Partial_Sums(P*G)).(N.n) + ( SPE.(j+1) + P.(G.(N.n + j+1+1)) ) by Z55,Z56,Z57,XXREAL_3:29 .= (Partial_Sums(P*G)).(N.n) + ( SPE.(j+1) + (P*E).(j+1+1) ) by Z58a,Z58,Z50,Z28,Z27,Z22,ZZ30,FINSEQ_3:25,FUNCT_1:13; hence thesis by Z53,Z25; end; Z62: for j be Nat holds PE[j] from NAT_1:sch 2(Z60,Z61); Z59a: N.n + len(P*E) = (Partial_Sums(Length s)).n - 1 + len(s.(n+1)) by Z0,Z30,Z22 .= (Partial_Sums(Length s)).n - 1 + (Length s).(n+1) by Def3 .= (Partial_Sums(Length s)).n + (Length s).(n+1) - 1 .= N.(n+1) by Z26,Z26d,SERIES_1:def 1; consider sn1 be Nat such that Z63: len(P*E) = sn1 + 1 by Z22,Z30,NAT_1:6; sn1 < len(P*E) by Z63,NAT_1:13; then TA: (Partial_Sums(P*G)).(N.n + sn1+1) = (Partial_Sums(P*G)).(N.n) + Sum(P*E) by Z25,Z62,Z63 .= (Partial_Sums(P*G)).(N.n) + (M*FSets).(n+1) by Z24,Z21,Z22,FUNCT_2:15; (Partial_Sums(M*FSets)).(n+1) = ((Partial_Sums(P*G))*N).n + (M*FSets).(n+1) by Z20,MESFUNC9:def 1 .= (Partial_Sums(P*G)).(N.(n+1)) by TA,Z59a,Z63,ORDINAL1:def 12,FUNCT_2:15 .= ((Partial_Sums(P*G))*N).(n+1) by FUNCT_2:15; hence thesis; end; for n be Nat holds P[n] from NAT_1:sch 2(Z100,Z101); then for n be Element of NAT holds (Partial_Sums(M*FSets)).n = (Partial_Sums(P*G) * N).n; hence Partial_Sums(M*FSets) is subsequence of Partial_Sums(P*G) by FUNCT_2:def 8; end; X125:Sum(M*FSets) = Sum(P*G) proof per cases by X123,MESFUNC5:def 11,MESFUNC9:8; suppose L1: Partial_Sums(P*G) is convergent_to_+infty; then lim Partial_Sums(M*FSets) = +infty by X124,DBLSEQ_3:27; then lim Partial_Sums(M*FSets) = lim Partial_Sums(P*G) by L1,MESFUNC9:7; then Sum(M*FSets) = lim Partial_Sums(P*G) by MESFUNC9:def 3; hence Sum(M*FSets) = Sum(P*G) by MESFUNC9:def 3; end; suppose Partial_Sums(P*G) is convergent_to_finite_number; then lim Partial_Sums(M*FSets) = lim Partial_Sums(P*G) by X124,DBLSEQ_3:26; then Sum(M*FSets) = lim Partial_Sums(P*G) by MESFUNC9:def 3; hence Sum(M*FSets) = Sum(P*G) by MESFUNC9:def 3; end; end; H0: Partial_Sums(M*FSets) is non-decreasing by MESFUNC9:16; for n be Nat holds Partial_Sums(M*FSets).n <= M.(union rng FSets) proof let n be Nat; H1: union rng(FSets|Segm(n+1)) in Field_generated_by S by Th58; rng (FSets|Segm(n+1)) c= rng FSets by RELAT_1:70; then M.(union rng(FSets|Segm(n+1))) <= M.(union rng FSets) by B0,H1,MEASURE1:8,ZFMISC_1:77; hence Partial_Sums(M*FSets).n <= M.(union rng FSets) by Th58; end; then lim Partial_Sums(M*FSets) <= M.(union rng FSets) by H0,RINFSUP2:37,MESFUNC9:9; then Sum(M*FSets) <= M.(union rng FSets) by MESFUNC9:def 3; then Sum(M*FSets) <= M.(Union FSets) by CARD_3:def 4; then X126:M.(Union FSets) = Sum(M*FSets) by X125,X120,XXREAL_0:1; Sum(M*FSets) = SUM(M*FSets) by MEASURE8:2; hence SUM(M*FSets) = M.(union rng FSets) by X126,CARD_3:def 4; end; suppose LL1: rng FSets is empty-membered; then union rng FSets = {} by Th52; then L2: M.(union rng FSets) = 0 by VALUED_0:def 19; LL3: for n be Nat holds (M*FSets).n = 0 proof let n be Nat; LL4: dom FSets = NAT by FUNCT_2:def 1; then FSets.n in rng FSets by FUNCT_1:3,ORDINAL1:def 12; then FSets.n = {} by LL1; then (M*FSets).n = M.{} by LL4,ORDINAL1:def 12,FUNCT_1:13; hence (M*FSets).n = 0 by VALUED_0:def 19; end; LL5: dom (Partial_Sums(M*FSets)) = NAT & dom (seq_const 0) = NAT by FUNCT_2:def 1; for n be object st n in dom(Partial_Sums(M*FSets)) holds (Partial_Sums(M*FSets)).n = (seq_const 0).n proof let n be object; assume n in dom(Partial_Sums(M*FSets)); then reconsider n1 = n as Nat; defpred P[Nat] means (Partial_Sums(M*FSets)).$1 = 0; (Partial_Sums(M*FSets)).0 = (M*FSets).0 by MESFUNC9:def 1; then LL8: P[0] by LL3; LL9: for i be Nat st P[i] holds P[i+1] proof let i be Nat; assume P[i]; then (Partial_Sums(M*FSets)).i + (M*FSets).(i+1) = (M*FSets).(i+1) by XXREAL_3:4; then (Partial_Sums(M*FSets)).(i+1) = (M*FSets).(i+1) by MESFUNC9:def 1; hence P[i+1] by LL3; end; for i be Nat holds P[i] from NAT_1:sch 2(LL8,LL9); then (Partial_Sums(M*FSets)).n1 = 0; hence thesis by SEQ_1:57; end; then Partial_Sums(M*FSets) = seq_const 0 by LL5,FUNCT_1:def 11; then L4: Partial_Sums(M*FSets) is convergent_to_finite_number & Partial_Sums(M*FSets) is convergent & lim Partial_Sums(M*FSets) = lim (seq_const 0) by RINFSUP2:14; SUM(M*FSets) = Sum(M*FSets) by MEASURE8:2; hence SUM(M*FSets) = M.(union rng FSets) by L2,L4,MESFUNC9:def 3; end; end; hence M is completely-additive by MEASURE8:def 11; end; definition let X be set, S be semialgebra_of_sets of X, P be pre-Measure of S; mode induced_Measure of S,P -> Measure of Field_generated_by S means :Def9: for A be set st A in Field_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds it.A = Sum(P*F); existence by Th55; end; theorem Th60: for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be induced_Measure of S,P holds M is completely-additive proof let X be set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be induced_Measure of S,P; for A be set st A in Field_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds M.A = Sum(P*F) by Def9; hence thesis by Th59; end; theorem Th61: for X be non empty set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be induced_Measure of S,P holds (sigma_Meas(C_Meas M))|(sigma (Field_generated_by S)) is sigma_Measure of sigma Field_generated_by S proof let X be non empty set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be induced_Measure of S,P; M is completely-additive by Th60; then consider N be sigma_Measure of sigma Field_generated_by S such that A1: N is_extension_of M & N = (sigma_Meas(C_Meas M))|(sigma (Field_generated_by S)) by MEASURE8:33; thus thesis by A1; end; definition let X be non empty set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be induced_Measure of S,P; mode induced_sigma_Measure of S,M -> sigma_Measure of sigma Field_generated_by S means :Def10: it = (sigma_Meas(C_Meas M))|(sigma (Field_generated_by S)); existence proof (sigma_Meas(C_Meas M))|(sigma (Field_generated_by S)) is sigma_Measure of sigma Field_generated_by S by Th61; hence thesis; end; end; theorem for X be non empty set, S be semialgebra_of_sets of X, P be pre-Measure of S, m be induced_Measure of S,P, M be induced_sigma_Measure of S,m holds M is_extension_of m proof let X be non empty set, S be semialgebra_of_sets of X, P be pre-Measure of S, m be induced_Measure of S,P, M be induced_sigma_Measure of S,m; m is completely-additive by Th60; then consider N be sigma_Measure of sigma Field_generated_by S such that A2: N is_extension_of m & N = (sigma_Meas(C_Meas m))|(sigma (Field_generated_by S)) by MEASURE8:33; thus M is_extension_of m by A2,Def10; end;