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