:: MEASURE7 semantic presentation begin theorem Th1: :: MEASURE7:1 for F being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n = 0. ) holds SUM F = 0. proof let F be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds F . n = 0. ) implies SUM F = 0. ) defpred S1[ Element of NAT ] means (Ser F) . \$1 = 0. ; assume A1: for n being Element of NAT holds F . n = 0. ; ::_thesis: SUM F = 0. A2: for t being Element of NAT st S1[t] holds S1[t + 1] proof let t be Element of NAT ; ::_thesis: ( S1[t] implies S1[t + 1] ) assume (Ser F) . t = 0. ; ::_thesis: S1[t + 1] hence (Ser F) . (t + 1) = 0. + (F . (t + 1)) by SUPINF_2:44 .= F . (t + 1) by XXREAL_3:4 .= 0. by A1 ; ::_thesis: verum end; A3: (Ser F) . 0 = F . 0 by SUPINF_2:44 .= 0. by A1 ; then A4: S1[ 0 ] ; A5: for s being Element of NAT holds S1[s] from NAT_1:sch_1(A4, A2); A6: rng (Ser F) = {0.} proof thus rng (Ser F) c= {0.} :: according to XBOOLE_0:def_10 ::_thesis: {0.} c= rng (Ser F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Ser F) or x in {0.} ) assume x in rng (Ser F) ; ::_thesis: x in {0.} then consider s being set such that A7: s in dom (Ser F) and A8: x = (Ser F) . s by FUNCT_1:def_3; reconsider s = s as Element of NAT by A7; (Ser F) . s = 0. by A5; hence x in {0.} by A8, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {0.} or x in rng (Ser F) ) assume x in {0.} ; ::_thesis: x in rng (Ser F) then ( dom (Ser F) = NAT & x = 0. ) by FUNCT_2:def_1, TARSKI:def_1; hence x in rng (Ser F) by A3, FUNCT_1:def_3; ::_thesis: verum end; sup {0.} = 0. by XXREAL_2:11; hence SUM F = 0. by A6, SUPINF_2:def_17; ::_thesis: verum end; theorem Th2: :: MEASURE7:2 for F being Function of NAT,ExtREAL st F is V93() holds for n being Element of NAT holds F . n <= (Ser F) . n proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies for n being Element of NAT holds F . n <= (Ser F) . n ) assume A1: F is V93() ; ::_thesis: for n being Element of NAT holds F . n <= (Ser F) . n let n be Element of NAT ; ::_thesis: F . n <= (Ser F) . n percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: F . n <= (Ser F) . n hence F . n <= (Ser F) . n by SUPINF_2:44; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: F . n <= (Ser F) . n then consider k being Nat such that A2: n = k + 1 by NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; A3: 0. <= (Ser F) . k by A1, SUPINF_2:40; (Ser F) . n = ((Ser F) . k) + (F . n) by A2, SUPINF_2:44; then 0. + (F . n) <= (Ser F) . n by A3, XXREAL_3:36; hence F . n <= (Ser F) . n by XXREAL_3:4; ::_thesis: verum end; end; end; theorem Th3: :: MEASURE7:3 for F, G, H being Function of NAT,ExtREAL st G is V93() & H is V93() & ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) holds for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) proof let F, G, H be Function of NAT,ExtREAL; ::_thesis: ( G is V93() & H is V93() & ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) implies for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) ) assume that A1: G is V93() and A2: H is V93() ; ::_thesis: ( ex n being Element of NAT st not F . n = (G . n) + (H . n) or for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) ) defpred S1[ Element of NAT ] means (Ser F) . \$1 = ((Ser G) . \$1) + ((Ser H) . \$1); assume A3: for n being Element of NAT holds F . n = (G . n) + (H . n) ; ::_thesis: for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: (Ser F) . k = ((Ser G) . k) + ((Ser H) . k) ; ::_thesis: S1[k + 1] set n = k + 1; A6: ( (Ser G) . (k + 1) = ((Ser G) . k) + (G . (k + 1)) & (Ser H) . (k + 1) = ((Ser H) . k) + (H . (k + 1)) ) by SUPINF_2:44; A7: 0. <= H . (k + 1) by A2, SUPINF_2:39; A8: ( F . (k + 1) = (G . (k + 1)) + (H . (k + 1)) & 0. <= G . (k + 1) ) by A1, A3, SUPINF_2:39; A9: 0. <= (Ser G) . k by A1, SUPINF_2:40; A10: 0. <= (Ser G) . (k + 1) by A1, SUPINF_2:40; A11: 0. <= (Ser H) . k by A2, SUPINF_2:40; ( 0. <= G . (k + 1) & 0. <= H . (k + 1) ) by A1, A2, SUPINF_2:39; then 0. + 0. <= (G . (k + 1)) + (H . (k + 1)) by XXREAL_3:36; then 0. <= F . (k + 1) by A3; then (((Ser G) . k) + ((Ser H) . k)) + (F . (k + 1)) = (((Ser G) . k) + (F . (k + 1))) + ((Ser H) . k) by A9, A11, XXREAL_3:44 .= ((((Ser G) . k) + (G . (k + 1))) + (H . (k + 1))) + ((Ser H) . k) by A9, A7, A8, XXREAL_3:44 .= ((Ser G) . (k + 1)) + ((Ser H) . (k + 1)) by A6, A11, A10, A7, XXREAL_3:44 ; hence S1[k + 1] by A5, SUPINF_2:44; ::_thesis: verum end; A12: (Ser H) . 0 = H . 0 by SUPINF_2:44; ( (Ser F) . 0 = F . 0 & (Ser G) . 0 = G . 0 ) by SUPINF_2:44; then A13: S1[ 0 ] by A3, A12; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A4); ::_thesis: verum end; theorem Th4: :: MEASURE7:4 for F, G, H being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) & G is V93() & H is V93() holds SUM F <= (SUM G) + (SUM H) proof let F, G, H be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) & G is V93() & H is V93() implies SUM F <= (SUM G) + (SUM H) ) assume A1: for n being Element of NAT holds F . n = (G . n) + (H . n) ; ::_thesis: ( not G is V93() or not H is V93() or SUM F <= (SUM G) + (SUM H) ) defpred S1[ Element of NAT ] means (Ser F) . \$1 = ((Ser G) . \$1) + ((Ser H) . \$1); assume that A2: G is V93() and A3: H is V93() ; ::_thesis: SUM F <= (SUM G) + (SUM H) A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A5: ( (Ser G) . (k + 1) = ((Ser G) . k) + (G . (k + 1)) & (Ser H) . (k + 1) = ((Ser H) . k) + (H . (k + 1)) ) by SUPINF_2:44; A6: 0. <= (Ser G) . k by A2, SUPINF_2:40; A7: 0. <= (Ser H) . (k + 1) by A3, SUPINF_2:40; A8: 0. <= H . (k + 1) by A3, SUPINF_2:39; A9: 0. <= (Ser H) . k by A3, SUPINF_2:40; ( 0. <= G . (k + 1) & 0. <= H . (k + 1) ) by A2, A3, SUPINF_2:39; then 0. + 0. <= (G . (k + 1)) + (H . (k + 1)) by XXREAL_3:36; then A10: ( (Ser F) . (k + 1) = ((Ser F) . k) + (F . (k + 1)) & 0. <= F . (k + 1) ) by A1, SUPINF_2:44; A11: 0. <= G . (k + 1) by A2, SUPINF_2:39; assume (Ser F) . k = ((Ser G) . k) + ((Ser H) . k) ; ::_thesis: S1[k + 1] hence (Ser F) . (k + 1) = ((Ser G) . k) + (((Ser H) . k) + (F . (k + 1))) by A10, A6, A9, XXREAL_3:44 .= ((Ser G) . k) + (((Ser H) . k) + ((G . (k + 1)) + (H . (k + 1)))) by A1 .= ((Ser G) . k) + ((((Ser H) . k) + (H . (k + 1))) + (G . (k + 1))) by A11, A9, A8, XXREAL_3:44 .= ((Ser G) . (k + 1)) + ((Ser H) . (k + 1)) by A5, A6, A11, A7, XXREAL_3:44 ; ::_thesis: verum end; A12: (Ser H) . 0 = H . 0 by SUPINF_2:44; ( (Ser F) . 0 = F . 0 & (Ser G) . 0 = G . 0 ) by SUPINF_2:44; then A13: S1[ 0 ] by A1, A12; A14: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A4); (SUM G) + (SUM H) is UpperBound of rng (Ser F) proof let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not x in rng (Ser F) or x <= (SUM G) + (SUM H) ) A15: dom (Ser F) = NAT by FUNCT_2:def_1; assume x in rng (Ser F) ; ::_thesis: x <= (SUM G) + (SUM H) then consider n being set such that A16: n in NAT and A17: x = (Ser F) . n by A15, FUNCT_1:def_3; reconsider n = n as Element of NAT by A16; (Ser H) . n <= sup (rng (Ser H)) by FUNCT_2:4, XXREAL_2:4; then A18: (Ser H) . n <= SUM H by SUPINF_2:def_17; (Ser G) . n <= sup (rng (Ser G)) by FUNCT_2:4, XXREAL_2:4; then (Ser G) . n <= SUM G by SUPINF_2:def_17; then ((Ser G) . n) + ((Ser H) . n) <= (SUM G) + (SUM H) by A18, XXREAL_3:36; hence x <= (SUM G) + (SUM H) by A14, A17; ::_thesis: verum end; then sup (rng (Ser F)) <= (SUM G) + (SUM H) by XXREAL_2:def_3; hence SUM F <= (SUM G) + (SUM H) by SUPINF_2:def_17; ::_thesis: verum end; theorem Th5: :: MEASURE7:5 for F, G being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n <= G . n ) holds for n being Element of NAT holds (Ser F) . n <= SUM G proof let F, G be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds F . n <= G . n ) implies for n being Element of NAT holds (Ser F) . n <= SUM G ) assume A1: for n being Element of NAT holds F . n <= G . n ; ::_thesis: for n being Element of NAT holds (Ser F) . n <= SUM G let n be Element of NAT ; ::_thesis: (Ser F) . n <= SUM G set y = (Ser G) . n; dom (Ser G) = NAT by FUNCT_2:def_1; then ( SUM G = sup (rng (Ser G)) & (Ser G) . n in rng (Ser G) ) by FUNCT_1:def_3, SUPINF_2:def_17; hence (Ser F) . n <= SUM G by A1, SUPINF_2:42, XXREAL_2:61; ::_thesis: verum end; theorem Th6: :: MEASURE7:6 for F being Function of NAT,ExtREAL st F is V93() holds for n being Element of NAT holds (Ser F) . n <= SUM F proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies for n being Element of NAT holds (Ser F) . n <= SUM F ) for n being Element of NAT holds F . n <= F . n ; hence ( F is V93() implies for n being Element of NAT holds (Ser F) . n <= SUM F ) by Th5; ::_thesis: verum end; definition let S be non empty set ; let H be Function of S,ExtREAL; func On H -> Function of NAT,ExtREAL means :Def1: :: MEASURE7:def 1 for n being Element of NAT holds ( ( n in S implies it . n = H . n ) & ( not n in S implies it . n = 0. ) ); existence ex b1 being Function of NAT,ExtREAL st for n being Element of NAT holds ( ( n in S implies b1 . n = H . n ) & ( not n in S implies b1 . n = 0. ) ) proof defpred S1[ Element of NAT , Element of ExtREAL ] means ( ( \$1 in S implies \$2 = H . \$1 ) & ( not \$1 in S implies \$2 = 0. ) ); A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S1[n,y] percases ( n in S or not n in S ) ; suppose n in S ; ::_thesis: ex y being Element of ExtREAL st S1[n,y] then reconsider n = n as Element of S ; take H . n ; ::_thesis: S1[n,H . n] thus S1[n,H . n] ; ::_thesis: verum end; supposeA2: not n in S ; ::_thesis: ex y being Element of ExtREAL st S1[n,y] take 0. ; ::_thesis: S1[n, 0. ] thus S1[n, 0. ] by A2; ::_thesis: verum end; end; end; consider GG being Function of NAT,ExtREAL such that A3: for n being Element of NAT holds S1[n,GG . n] from FUNCT_2:sch_3(A1); take GG ; ::_thesis: for n being Element of NAT holds ( ( n in S implies GG . n = H . n ) & ( not n in S implies GG . n = 0. ) ) thus for n being Element of NAT holds ( ( n in S implies GG . n = H . n ) & ( not n in S implies GG . n = 0. ) ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds ( ( n in S implies b1 . n = H . n ) & ( not n in S implies b1 . n = 0. ) ) ) & ( for n being Element of NAT holds ( ( n in S implies b2 . n = H . n ) & ( not n in S implies b2 . n = 0. ) ) ) holds b1 = b2 proof let G1, G2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds ( ( n in S implies G1 . n = H . n ) & ( not n in S implies G1 . n = 0. ) ) ) & ( for n being Element of NAT holds ( ( n in S implies G2 . n = H . n ) & ( not n in S implies G2 . n = 0. ) ) ) implies G1 = G2 ) assume that A4: for n being Element of NAT holds ( ( n in S implies G1 . n = H . n ) & ( not n in S implies G1 . n = 0. ) ) and A5: for n being Element of NAT holds ( ( n in S implies G2 . n = H . n ) & ( not n in S implies G2 . n = 0. ) ) ; ::_thesis: G1 = G2 for n being set st n in NAT holds G1 . n = G2 . n proof let n be set ; ::_thesis: ( n in NAT implies G1 . n = G2 . n ) assume n in NAT ; ::_thesis: G1 . n = G2 . n then reconsider n = n as Element of NAT ; percases ( n in S or not n in S ) ; supposeA6: n in S ; ::_thesis: G1 . n = G2 . n then G1 . n = H . n by A4; hence G1 . n = G2 . n by A5, A6; ::_thesis: verum end; supposeA7: not n in S ; ::_thesis: G1 . n = G2 . n then G1 . n = 0. by A4; hence G1 . n = G2 . n by A5, A7; ::_thesis: verum end; end; end; hence G1 = G2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def1 defines On MEASURE7:def_1_:_ for S being non empty set for H being Function of S,ExtREAL for b3 being Function of NAT,ExtREAL holds ( b3 = On H iff for n being Element of NAT holds ( ( n in S implies b3 . n = H . n ) & ( not n in S implies b3 . n = 0. ) ) ); theorem Th7: :: MEASURE7:7 for X being non empty set for G being Function of X,ExtREAL st G is V93() holds On G is V93() proof let X be non empty set ; ::_thesis: for G being Function of X,ExtREAL st G is V93() holds On G is V93() let G be Function of X,ExtREAL; ::_thesis: ( G is V93() implies On G is V93() ) assume A1: G is V93() ; ::_thesis: On G is V93() for n being Element of NAT holds 0. <= (On G) . n proof let n be Element of NAT ; ::_thesis: 0. <= (On G) . n percases ( n in X or not n in X ) ; supposeA2: n in X ; ::_thesis: 0. <= (On G) . n then (On G) . n = G . n by Def1; hence 0. <= (On G) . n by A1, A2, SUPINF_2:39; ::_thesis: verum end; suppose not n in X ; ::_thesis: 0. <= (On G) . n hence 0. <= (On G) . n by Def1; ::_thesis: verum end; end; end; hence On G is V93() by SUPINF_2:39; ::_thesis: verum end; theorem Th8: :: MEASURE7:8 for F being Function of NAT,ExtREAL st F is V93() holds for n, k being Element of NAT st n <= k holds (Ser F) . n <= (Ser F) . k proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies for n, k being Element of NAT st n <= k holds (Ser F) . n <= (Ser F) . k ) assume A1: F is V93() ; ::_thesis: for n, k being Element of NAT st n <= k holds (Ser F) . n <= (Ser F) . k let n, k be Element of NAT ; ::_thesis: ( n <= k implies (Ser F) . n <= (Ser F) . k ) defpred S1[ Element of NAT ] means (Ser F) . n <= (Ser F) . (n + \$1); A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: (Ser F) . n <= (Ser F) . (n + k) ; ::_thesis: S1[k + 1] (Ser F) . (n + k) <= (Ser F) . ((n + k) + 1) by A1, SUPINF_2:40; hence S1[k + 1] by A3, XXREAL_0:2; ::_thesis: verum end; assume n <= k ; ::_thesis: (Ser F) . n <= (Ser F) . k then consider s being Nat such that A4: k = n + s by NAT_1:10; reconsider s = s as Element of NAT by ORDINAL1:def_12; A5: k = n + s by A4; A6: S1[ 0 ] ; for s being Element of NAT holds S1[s] from NAT_1:sch_1(A6, A2); hence (Ser F) . n <= (Ser F) . k by A5; ::_thesis: verum end; theorem Th9: :: MEASURE7:9 for k being Element of NAT for F being Function of NAT,ExtREAL st ( for n being Element of NAT st n <> k holds F . n = 0. ) holds ( ( for n being Element of NAT st n < k holds (Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds (Ser F) . n = F . k ) ) proof let k be Element of NAT ; ::_thesis: for F being Function of NAT,ExtREAL st ( for n being Element of NAT st n <> k holds F . n = 0. ) holds ( ( for n being Element of NAT st n < k holds (Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds (Ser F) . n = F . k ) ) let F be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT st n <> k holds F . n = 0. ) implies ( ( for n being Element of NAT st n < k holds (Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds (Ser F) . n = F . k ) ) ) defpred S1[ Element of NAT ] means ( \$1 < k implies (Ser F) . \$1 = 0. ); assume A1: for n being Element of NAT st n <> k holds F . n = 0. ; ::_thesis: ( ( for n being Element of NAT st n < k holds (Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds (Ser F) . n = F . k ) ) A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: ( n < k implies (Ser F) . n = 0. ) ; ::_thesis: S1[n + 1] assume A4: n + 1 < k ; ::_thesis: (Ser F) . (n + 1) = 0. then A5: ( n <= n + 1 & F . (n + 1) = 0. ) by A1, NAT_1:11; (Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:44 .= 0. by A3, A4, A5, XXREAL_0:2, XXREAL_3:4 ; hence (Ser F) . (n + 1) = 0. ; ::_thesis: verum end; A6: S1[ 0 ] proof assume 0 < k ; ::_thesis: (Ser F) . 0 = 0. then F . 0 = 0. by A1; hence (Ser F) . 0 = 0. by SUPINF_2:44; ::_thesis: verum end; A7: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A2); defpred S2[ Element of NAT ] means ( k <= \$1 implies (Ser F) . \$1 = F . k ); A8: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A9: ( k <= n implies (Ser F) . n = F . k ) ; ::_thesis: S2[n + 1] assume A10: k <= n + 1 ; ::_thesis: (Ser F) . (n + 1) = F . k percases ( k <= n or k = n + 1 ) by A10, NAT_1:8; supposeA11: k <= n ; ::_thesis: (Ser F) . (n + 1) = F . k then k <> n + 1 by NAT_1:13; then A12: F . (n + 1) = 0. by A1; (Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:44 .= F . k by A9, A11, A12, XXREAL_3:4 ; hence (Ser F) . (n + 1) = F . k ; ::_thesis: verum end; supposeA13: k = n + 1 ; ::_thesis: (Ser F) . (n + 1) = F . k then n < k by NAT_1:13; then A14: (Ser F) . n = 0. by A7; (Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:44 .= F . k by A13, A14, XXREAL_3:4 ; hence (Ser F) . (n + 1) = F . k ; ::_thesis: verum end; end; end; A15: S2[ 0 ] proof A16: 0 <= k by NAT_1:2; assume k <= 0 ; ::_thesis: (Ser F) . 0 = F . k then F . 0 = F . k by A16, XXREAL_0:1; hence (Ser F) . 0 = F . k by SUPINF_2:44; ::_thesis: verum end; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A15, A8); hence ( ( for n being Element of NAT st n < k holds (Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds (Ser F) . n = F . k ) ) by A7; ::_thesis: verum end; theorem Th10: :: MEASURE7:10 for G being Function of NAT,ExtREAL st G is V93() holds for S being non empty Subset of NAT for H being Function of S,NAT st H is one-to-one holds SUM (On (G * H)) <= SUM G proof let G be Function of NAT,ExtREAL; ::_thesis: ( G is V93() implies for S being non empty Subset of NAT for H being Function of S,NAT st H is one-to-one holds SUM (On (G * H)) <= SUM G ) assume A1: G is V93() ; ::_thesis: for S being non empty Subset of NAT for H being Function of S,NAT st H is one-to-one holds SUM (On (G * H)) <= SUM G let S be non empty Subset of NAT; ::_thesis: for H being Function of S,NAT st H is one-to-one holds SUM (On (G * H)) <= SUM G let H be Function of S,NAT; ::_thesis: ( H is one-to-one implies SUM (On (G * H)) <= SUM G ) defpred S1[ Element of NAT ] means ex m being Element of NAT st for F being Function of NAT,ExtREAL st F is V93() holds (Ser (On (F * H))) . \$1 <= (Ser F) . m; assume A2: H is one-to-one ; ::_thesis: SUM (On (G * H)) <= SUM G A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) given m0 being Element of NAT such that A4: for F being Function of NAT,ExtREAL st F is V93() holds (Ser (On (F * H))) . k <= (Ser F) . m0 ; ::_thesis: S1[k + 1] percases ( k + 1 in S or not k + 1 in S ) ; supposeA5: k + 1 in S ; ::_thesis: S1[k + 1] reconsider m1 = H . (k + 1) as Element of NAT ; set m = m0 + m1; take m0 + m1 ; ::_thesis: for F being Function of NAT,ExtREAL st F is V93() holds (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) ) defpred S2[ Element of NAT , Element of ExtREAL ] means ( ( \$1 = H . (k + 1) implies \$2 = F . \$1 ) & ( \$1 <> H . (k + 1) implies \$2 = 0. ) ); A6: for n being Element of NAT ex y being Element of ExtREAL st S2[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S2[n,y] percases ( n = H . (k + 1) or n <> H . (k + 1) ) ; supposeA7: n = H . (k + 1) ; ::_thesis: ex y being Element of ExtREAL st S2[n,y] take F . n ; ::_thesis: S2[n,F . n] thus S2[n,F . n] by A7; ::_thesis: verum end; supposeA8: n <> H . (k + 1) ; ::_thesis: ex y being Element of ExtREAL st S2[n,y] take 0. ; ::_thesis: S2[n, 0. ] thus S2[n, 0. ] by A8; ::_thesis: verum end; end; end; consider G0 being Function of NAT,ExtREAL such that A9: for n being Element of NAT holds S2[n,G0 . n] from FUNCT_2:sch_3(A6); reconsider GG0 = On (G0 * H) as Function of NAT,ExtREAL ; A10: for n being Element of NAT st n <> k + 1 holds GG0 . n = 0. proof let n be Element of NAT ; ::_thesis: ( n <> k + 1 implies GG0 . n = 0. ) assume A11: n <> k + 1 ; ::_thesis: GG0 . n = 0. percases ( n in S or not n in S ) ; supposeA12: n in S ; ::_thesis: GG0 . n = 0. then A13: GG0 . n = (G0 * H) . n by Def1 .= G0 . (H . n) by A12, FUNCT_2:15 ; reconsider n = n as Element of S by A12; not H . n = H . (k + 1) by A2, A5, A11, FUNCT_2:19; hence GG0 . n = 0. by A9, A13; ::_thesis: verum end; suppose not n in S ; ::_thesis: GG0 . n = 0. hence GG0 . n = 0. by Def1; ::_thesis: verum end; end; end; assume A14: F is V93() ; ::_thesis: (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) for n being Element of NAT holds 0. <= G0 . n proof let n be Element of NAT ; ::_thesis: 0. <= G0 . n percases ( n = H . (k + 1) or not n = H . (k + 1) ) ; suppose n = H . (k + 1) ; ::_thesis: 0. <= G0 . n then G0 . n = F . n by A9; hence 0. <= G0 . n by A14, SUPINF_2:39; ::_thesis: verum end; suppose not n = H . (k + 1) ; ::_thesis: 0. <= G0 . n hence 0. <= G0 . n by A9; ::_thesis: verum end; end; end; then A15: G0 is V93() by SUPINF_2:39; reconsider n = k + 1 as Element of S by A5; defpred S3[ Element of NAT , Element of ExtREAL ] means ( ( \$1 <> H . (k + 1) implies \$2 = F . \$1 ) & ( \$1 = H . (k + 1) implies \$2 = 0. ) ); A16: for n being Element of NAT ex y being Element of ExtREAL st S3[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S3[n,y] percases ( n <> H . (k + 1) or n = H . (k + 1) ) ; supposeA17: n <> H . (k + 1) ; ::_thesis: ex y being Element of ExtREAL st S3[n,y] take F . n ; ::_thesis: S3[n,F . n] thus S3[n,F . n] by A17; ::_thesis: verum end; supposeA18: n = H . (k + 1) ; ::_thesis: ex y being Element of ExtREAL st S3[n,y] take 0. ; ::_thesis: S3[n, 0. ] thus S3[n, 0. ] by A18; ::_thesis: verum end; end; end; consider G1 being Function of NAT,ExtREAL such that A19: for n being Element of NAT holds S3[n,G1 . n] from FUNCT_2:sch_3(A16); set GG1 = On (G1 * H); A20: (On (G1 * H)) . (k + 1) = (G1 * H) . n by Def1 .= G1 . (H . n) by FUNCT_2:15 .= 0. by A19 ; A21: GG0 . n = (G0 * H) . n by Def1 .= G0 . (H . n) by FUNCT_2:15 .= F . (H . n) by A9 ; then A22: (Ser GG0) . (k + 1) = F . (H . (k + 1)) by A10, Th9; A23: for n being Element of NAT st n <> k + 1 & n in S holds (On (G1 * H)) . n = F . (H . n) proof let n be Element of NAT ; ::_thesis: ( n <> k + 1 & n in S implies (On (G1 * H)) . n = F . (H . n) ) assume that A24: n <> k + 1 and A25: n in S ; ::_thesis: (On (G1 * H)) . n = F . (H . n) A26: (On (G1 * H)) . n = (G1 * H) . n by A25, Def1 .= G1 . (H . n) by A25, FUNCT_2:15 ; reconsider n = n as Element of S by A25; not H . n = H . (k + 1) by A2, A5, A24, FUNCT_2:19; hence (On (G1 * H)) . n = F . (H . n) by A19, A26; ::_thesis: verum end; A27: for n being Element of NAT holds (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) proof let n be Element of NAT ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) percases ( n = k + 1 or n <> k + 1 ) ; supposeA28: n = k + 1 ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) then (On (F * H)) . n = (F * H) . n by A5, Def1 .= F . (H . n) by A5, A28, FUNCT_2:15 .= (GG0 . n) + ((On (G1 * H)) . n) by A21, A20, A28, XXREAL_3:4 ; hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; ::_thesis: verum end; supposeA29: n <> k + 1 ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) now__::_thesis:_(On_(F_*_H))_._n_=_(GG0_._n)_+_((On_(G1_*_H))_._n) percases ( n in S or not n in S ) ; supposeA30: n in S ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) then A31: (On (G1 * H)) . n = F . (H . n) by A23, A29; A32: GG0 . n = 0. by A10, A29; (On (F * H)) . n = (F * H) . n by A30, Def1 .= F . (H . n) by A30, FUNCT_2:15 .= (GG0 . n) + ((On (G1 * H)) . n) by A32, A31, XXREAL_3:4 ; hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; ::_thesis: verum end; supposeA33: not n in S ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) then A34: (On (G1 * H)) . n = 0. by Def1; A35: GG0 . n = 0. by A10, A29; (On (F * H)) . n = 0. by A33, Def1 .= (GG0 . n) + ((On (G1 * H)) . n) by A35, A34, XXREAL_3:4 ; hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; ::_thesis: verum end; end; end; hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; ::_thesis: verum end; end; end; m1 <= m0 + m1 by NAT_1:11; then A36: (Ser G0) . (m0 + m1) = G0 . (H . (k + 1)) by A9, Th9; set v = H . n; A37: (Ser (On (G1 * H))) . (k + 1) = ((Ser (On (G1 * H))) . k) + ((On (G1 * H)) . (k + 1)) by SUPINF_2:44 .= (Ser (On (G1 * H))) . k by A20, XXREAL_3:4 ; A38: G0 . (H . n) = F . (H . n) by A9; for n being Element of NAT holds 0. <= G1 . n proof let n be Element of NAT ; ::_thesis: 0. <= G1 . n percases ( n <> H . (k + 1) or n = H . (k + 1) ) ; suppose n <> H . (k + 1) ; ::_thesis: 0. <= G1 . n then G1 . n = F . n by A19; hence 0. <= G1 . n by A14, SUPINF_2:39; ::_thesis: verum end; suppose n = H . (k + 1) ; ::_thesis: 0. <= G1 . n hence 0. <= G1 . n by A19; ::_thesis: verum end; end; end; then A39: G1 is V93() by SUPINF_2:39; then G1 * H is V93() by MEASURE1:25; then A40: On (G1 * H) is V93() by Th7; G0 * H is V93() by A15, MEASURE1:25; then GG0 is V93() by Th7; then A41: (Ser (On (F * H))) . (k + 1) = ((Ser GG0) . (k + 1)) + ((Ser (On (G1 * H))) . (k + 1)) by A40, A27, Th3; ( (Ser (On (G1 * H))) . k <= (Ser G1) . m0 & (Ser G1) . m0 <= (Ser G1) . (m0 + m1) ) by A4, A39, Th8, NAT_1:11; then A42: (Ser (On (G1 * H))) . (k + 1) <= (Ser G1) . (m0 + m1) by A37, XXREAL_0:2; for m being Element of NAT holds F . m = (G0 . m) + (G1 . m) proof let m be Element of NAT ; ::_thesis: F . m = (G0 . m) + (G1 . m) percases ( m = H . (k + 1) or m <> H . (k + 1) ) ; suppose m = H . (k + 1) ; ::_thesis: F . m = (G0 . m) + (G1 . m) then ( G0 . m = F . m & G1 . m = 0. ) by A9, A19; hence F . m = (G0 . m) + (G1 . m) by XXREAL_3:4; ::_thesis: verum end; suppose m <> H . (k + 1) ; ::_thesis: F . m = (G0 . m) + (G1 . m) then ( G0 . m = 0. & G1 . m = F . m ) by A9, A19; hence F . m = (G0 . m) + (G1 . m) by XXREAL_3:4; ::_thesis: verum end; end; end; then (Ser F) . (m0 + m1) = ((Ser G0) . (m0 + m1)) + ((Ser G1) . (m0 + m1)) by A15, A39, Th3; hence (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) by A22, A36, A38, A42, A41, XXREAL_3:36; ::_thesis: verum end; supposeA43: not k + 1 in S ; ::_thesis: S1[k + 1] take m0 ; ::_thesis: for F being Function of NAT,ExtREAL st F is V93() holds (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 ) A44: (On (F * H)) . (k + 1) = 0. by A43, Def1; assume A45: F is V93() ; ::_thesis: (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 (Ser (On (F * H))) . (k + 1) = ((Ser (On (F * H))) . k) + ((On (F * H)) . (k + 1)) by SUPINF_2:44 .= (Ser (On (F * H))) . k by A44, XXREAL_3:4 ; hence (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 by A4, A45; ::_thesis: verum end; end; end; A46: S1[ 0 ] proof percases ( 0 in S or not 0 in S ) ; supposeA47: 0 in S ; ::_thesis: S1[ 0 ] reconsider m = H . 0 as Element of NAT ; take m ; ::_thesis: for F being Function of NAT,ExtREAL st F is V93() holds (Ser (On (F * H))) . 0 <= (Ser F) . m let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies (Ser (On (F * H))) . 0 <= (Ser F) . m ) (Ser (On (F * H))) . 0 = (On (F * H)) . 0 by SUPINF_2:44; then A48: (Ser (On (F * H))) . 0 = (F * H) . 0 by A47, Def1 .= F . (H . 0) by A47, FUNCT_2:15 ; assume F is V93() ; ::_thesis: (Ser (On (F * H))) . 0 <= (Ser F) . m hence (Ser (On (F * H))) . 0 <= (Ser F) . m by A48, Th2; ::_thesis: verum end; supposeA49: not 0 in S ; ::_thesis: S1[ 0 ] take m = 0 ; ::_thesis: for F being Function of NAT,ExtREAL st F is V93() holds (Ser (On (F * H))) . 0 <= (Ser F) . m let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies (Ser (On (F * H))) . 0 <= (Ser F) . m ) assume F is V93() ; ::_thesis: (Ser (On (F * H))) . 0 <= (Ser F) . m then A50: ( 0. <= F . 0 & F . 0 <= (Ser F) . m ) by Th2, SUPINF_2:39; (Ser (On (F * H))) . 0 = (On (F * H)) . 0 by SUPINF_2:44; then (Ser (On (F * H))) . 0 = 0. by A49, Def1; hence (Ser (On (F * H))) . 0 <= (Ser F) . m by A50, XXREAL_0:2; ::_thesis: verum end; end; end; A51: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A46, A3); for x being ext-real number st x in rng (Ser (On (G * H))) holds ex y being ext-real number st ( y in rng (Ser G) & x <= y ) proof let x be ext-real number ; ::_thesis: ( x in rng (Ser (On (G * H))) implies ex y being ext-real number st ( y in rng (Ser G) & x <= y ) ) assume A52: x in rng (Ser (On (G * H))) ; ::_thesis: ex y being ext-real number st ( y in rng (Ser G) & x <= y ) ex y being ext-real number st ( y in rng (Ser G) & x <= y ) proof consider n being set such that A53: n in dom (Ser (On (G * H))) and A54: x = (Ser (On (G * H))) . n by A52, FUNCT_1:def_3; reconsider n = n as Element of NAT by A53; consider m being Element of NAT such that A55: for F being Function of NAT,ExtREAL st F is V93() holds (Ser (On (F * H))) . n <= (Ser F) . m by A51; take (Ser G) . m ; ::_thesis: ( (Ser G) . m in rng (Ser G) & x <= (Ser G) . m ) dom (Ser G) = NAT by FUNCT_2:def_1; hence ( (Ser G) . m in rng (Ser G) & x <= (Ser G) . m ) by A1, A54, A55, FUNCT_1:def_3; ::_thesis: verum end; hence ex y being ext-real number st ( y in rng (Ser G) & x <= y ) ; ::_thesis: verum end; then A56: sup (rng (Ser (On (G * H)))) <= sup (rng (Ser G)) by XXREAL_2:63; SUM G = sup (rng (Ser G)) by SUPINF_2:def_17; hence SUM (On (G * H)) <= SUM G by A56, SUPINF_2:def_17; ::_thesis: verum end; theorem Th11: :: MEASURE7:11 for F, G being Function of NAT,ExtREAL st G is V93() holds for S being non empty Subset of NAT for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds ( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds SUM F <= SUM G proof let F, G be Function of NAT,ExtREAL; ::_thesis: ( G is V93() implies for S being non empty Subset of NAT for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds ( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds SUM F <= SUM G ) assume A1: G is V93() ; ::_thesis: for S being non empty Subset of NAT for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds ( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds SUM F <= SUM G let S be non empty Subset of NAT; ::_thesis: for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds ( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds SUM F <= SUM G let H be Function of S,NAT; ::_thesis: ( H is one-to-one & ( for k being Element of NAT holds ( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) implies SUM F <= SUM G ) assume A2: H is one-to-one ; ::_thesis: ( ex k being Element of NAT st ( ( k in S implies F . k = (G * H) . k ) implies ( not k in S & not F . k = 0. ) ) or SUM F <= SUM G ) assume for k being Element of NAT holds ( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ; ::_thesis: SUM F <= SUM G then F = On (G * H) by Def1; hence SUM F <= SUM G by A1, A2, Th10; ::_thesis: verum end; REAL in bool REAL by ZFMISC_1:def_1; then reconsider G0 = NAT --> REAL as Function of NAT,(bool REAL) by FUNCOP_1:45; Lm1: rng G0 = {REAL} by FUNCOP_1:8; then Lm2: REAL c= union (rng G0) by ZFMISC_1:25; Lm3: for n being Element of NAT holds G0 . n is Interval proof let n be Element of NAT ; ::_thesis: G0 . n is Interval G0 . n in {REAL} by Lm1, FUNCT_2:4; hence G0 . n is Interval by TARSKI:def_1; ::_thesis: verum end; definition let A be Subset of REAL; mode Interval_Covering of A -> Function of NAT,(bool REAL) means :Def2: :: MEASURE7:def 2 ( A c= union (rng it) & ( for n being Element of NAT holds it . n is Interval ) ); existence ex b1 being Function of NAT,(bool REAL) st ( A c= union (rng b1) & ( for n being Element of NAT holds b1 . n is Interval ) ) by Lm2, Lm3, XBOOLE_1:1; end; :: deftheorem Def2 defines Interval_Covering MEASURE7:def_2_:_ for A being Subset of REAL for b2 being Function of NAT,(bool REAL) holds ( b2 is Interval_Covering of A iff ( A c= union (rng b2) & ( for n being Element of NAT holds b2 . n is Interval ) ) ); definition let A be Subset of REAL; let F be Interval_Covering of A; let n be Element of NAT ; :: original: . redefine funcF . n -> Interval; correctness coherence F . n is Interval; by Def2; end; definition let F be Function of NAT,(bool REAL); mode Interval_Covering of F -> Function of NAT,(Funcs (NAT,(bool REAL))) means :Def3: :: MEASURE7:def 3 for n being Element of NAT holds it . n is Interval_Covering of F . n; existence ex b1 being Function of NAT,(Funcs (NAT,(bool REAL))) st for n being Element of NAT holds b1 . n is Interval_Covering of F . n proof reconsider G = G0 as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8; reconsider H = NAT --> G as Function of NAT,(Funcs (NAT,(bool REAL))) ; take H ; ::_thesis: for n being Element of NAT holds H . n is Interval_Covering of F . n A1: for n being Element of NAT holds G0 is Interval_Covering of F . n proof let n be Element of NAT ; ::_thesis: G0 is Interval_Covering of F . n F . n c= union (rng G0) by Lm2, XBOOLE_1:1; hence G0 is Interval_Covering of F . n by Def2, Lm3; ::_thesis: verum end; for n being Element of NAT holds H . n is Interval_Covering of F . n proof let n be Element of NAT ; ::_thesis: H . n is Interval_Covering of F . n H . n = G by FUNCOP_1:7; hence H . n is Interval_Covering of F . n by A1; ::_thesis: verum end; hence for n being Element of NAT holds H . n is Interval_Covering of F . n ; ::_thesis: verum end; end; :: deftheorem Def3 defines Interval_Covering MEASURE7:def_3_:_ for F being Function of NAT,(bool REAL) for b2 being Function of NAT,(Funcs (NAT,(bool REAL))) holds ( b2 is Interval_Covering of F iff for n being Element of NAT holds b2 . n is Interval_Covering of F . n ); definition let A be Subset of REAL; let F be Interval_Covering of A; deffunc H1( Element of NAT ) -> Element of ExtREAL = diameter (F . \$1); funcF vol -> Function of NAT,ExtREAL means :Def4: :: MEASURE7:def 4 for n being Element of NAT holds it . n = diameter (F . n); existence ex b1 being Function of NAT,ExtREAL st for n being Element of NAT holds b1 . n = diameter (F . n) proof thus ex G being Function of NAT,ExtREAL st for n being Element of NAT holds G . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds b1 . n = diameter (F . n) ) & ( for n being Element of NAT holds b2 . n = diameter (F . n) ) holds b1 = b2 proof thus for G1, G2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds G1 . n = H1(n) ) & ( for n being Element of NAT holds G2 . n = H1(n) ) holds G1 = G2 from BINOP_2:sch_1(); ::_thesis: verum end; end; :: deftheorem Def4 defines vol MEASURE7:def_4_:_ for A being Subset of REAL for F being Interval_Covering of A for b3 being Function of NAT,ExtREAL holds ( b3 = F vol iff for n being Element of NAT holds b3 . n = diameter (F . n) ); theorem Th12: :: MEASURE7:12 for A being Subset of REAL for F being Interval_Covering of A holds F vol is V93() proof let A be Subset of REAL; ::_thesis: for F being Interval_Covering of A holds F vol is V93() let F be Interval_Covering of A; ::_thesis: F vol is V93() for n being Element of NAT holds 0. <= (F vol) . n proof let n be Element of NAT ; ::_thesis: 0. <= (F vol) . n (F vol) . n = diameter (F . n) by Def4; hence 0. <= (F vol) . n by MEASURE5:13; ::_thesis: verum end; hence F vol is V93() by SUPINF_2:39; ::_thesis: verum end; definition let F be Function of NAT,(bool REAL); let H be Interval_Covering of F; let n be Element of NAT ; :: original: . redefine funcH . n -> Interval_Covering of F . n; correctness coherence H . n is Interval_Covering of F . n; by Def3; end; definition let F be Function of NAT,(bool REAL); let G be Interval_Covering of F; funcG vol -> Function of NAT,(Funcs (NAT,ExtREAL)) means :: MEASURE7:def 5 for n being Element of NAT holds it . n = (G . n) vol ; existence ex b1 being Function of NAT,(Funcs (NAT,ExtREAL)) st for n being Element of NAT holds b1 . n = (G . n) vol proof defpred S1[ Element of NAT , set ] means \$2 = (G . \$1) vol ; A1: for n being Element of NAT ex y being Element of Funcs (NAT,ExtREAL) st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,ExtREAL) st S1[n,y] (G . n) vol is Element of Funcs (NAT,ExtREAL) by FUNCT_2:8; hence ex y being Element of Funcs (NAT,ExtREAL) st S1[n,y] ; ::_thesis: verum end; ex G0 being Function of NAT,(Funcs (NAT,ExtREAL)) st for n being Element of NAT holds S1[n,G0 . n] from FUNCT_2:sch_3(A1); hence ex b1 being Function of NAT,(Funcs (NAT,ExtREAL)) st for n being Element of NAT holds b1 . n = (G . n) vol ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,(Funcs (NAT,ExtREAL)) st ( for n being Element of NAT holds b1 . n = (G . n) vol ) & ( for n being Element of NAT holds b2 . n = (G . n) vol ) holds b1 = b2 proof deffunc H1( Element of NAT ) -> Function of NAT,ExtREAL = (G . \$1) vol ; thus for F1, F2 being Function of NAT,(Funcs (NAT,ExtREAL)) st ( for n being Element of NAT holds F1 . n = H1(n) ) & ( for n being Element of NAT holds F2 . n = H1(n) ) holds F1 = F2 from BINOP_2:sch_1(); ::_thesis: verum end; end; :: deftheorem defines vol MEASURE7:def_5_:_ for F being Function of NAT,(bool REAL) for G being Interval_Covering of F for b3 being Function of NAT,(Funcs (NAT,ExtREAL)) holds ( b3 = G vol iff for n being Element of NAT holds b3 . n = (G . n) vol ); definition let A be Subset of REAL; let F be Interval_Covering of A; func vol F -> R_eal equals :: MEASURE7:def 6 SUM (F vol); correctness coherence SUM (F vol) is R_eal; ; end; :: deftheorem defines vol MEASURE7:def_6_:_ for A being Subset of REAL for F being Interval_Covering of A holds vol F = SUM (F vol); definition let F be Function of NAT,(bool REAL); let G be Interval_Covering of F; func vol G -> Function of NAT,ExtREAL means :Def7: :: MEASURE7:def 7 for n being Element of NAT holds it . n = vol (G . n); existence ex b1 being Function of NAT,ExtREAL st for n being Element of NAT holds b1 . n = vol (G . n) proof defpred S1[ Element of NAT , Element of ExtREAL ] means \$2 = vol (G . \$1); A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y] ; consider G0 being Function of NAT,ExtREAL such that A2: for n being Element of NAT holds S1[n,G0 . n] from FUNCT_2:sch_3(A1); take G0 ; ::_thesis: for n being Element of NAT holds G0 . n = vol (G . n) thus for n being Element of NAT holds G0 . n = vol (G . n) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds b1 . n = vol (G . n) ) & ( for n being Element of NAT holds b2 . n = vol (G . n) ) holds b1 = b2 proof deffunc H1( Element of NAT ) -> R_eal = vol (G . \$1); thus for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds F1 . n = H1(n) ) & ( for n being Element of NAT holds F2 . n = H1(n) ) holds F1 = F2 from BINOP_2:sch_1(); ::_thesis: verum end; end; :: deftheorem Def7 defines vol MEASURE7:def_7_:_ for F being Function of NAT,(bool REAL) for G being Interval_Covering of F for b3 being Function of NAT,ExtREAL holds ( b3 = vol G iff for n being Element of NAT holds b3 . n = vol (G . n) ); theorem Th13: :: MEASURE7:13 for F being Function of NAT,(bool REAL) for G being Interval_Covering of F for n being Element of NAT holds 0. <= (vol G) . n proof let F be Function of NAT,(bool REAL); ::_thesis: for G being Interval_Covering of F for n being Element of NAT holds 0. <= (vol G) . n let G be Interval_Covering of F; ::_thesis: for n being Element of NAT holds 0. <= (vol G) . n let n be Element of NAT ; ::_thesis: 0. <= (vol G) . n for k being Element of NAT holds 0. <= ((G . n) vol) . k proof let k be Element of NAT ; ::_thesis: 0. <= ((G . n) vol) . k 0. <= diameter ((G . n) . k) by MEASURE5:13; hence 0. <= ((G . n) vol) . k by Def4; ::_thesis: verum end; then A1: (G . n) vol is V93() by SUPINF_2:39; (vol G) . n = vol (G . n) by Def7; hence 0. <= (vol G) . n by A1, MEASURE6:2; ::_thesis: verum end; definition let A be Subset of REAL; defpred S1[ set ] means ex F being Interval_Covering of A st \$1 = vol F; func Svc A -> Subset of ExtREAL means :Def8: :: MEASURE7:def 8 for x being R_eal holds ( x in it iff ex F being Interval_Covering of A st x = vol F ); existence ex b1 being Subset of ExtREAL st for x being R_eal holds ( x in b1 iff ex F being Interval_Covering of A st x = vol F ) proof consider D being set such that A1: for x being set holds ( x in D iff ( x in ExtREAL & S1[x] ) ) from XBOOLE_0:sch_1(); for z being set st z in D holds z in ExtREAL by A1; then reconsider D = D as Subset of ExtREAL by TARSKI:def_3; take D ; ::_thesis: for x being R_eal holds ( x in D iff ex F being Interval_Covering of A st x = vol F ) thus for x being R_eal holds ( x in D iff ex F being Interval_Covering of A st x = vol F ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of ExtREAL st ( for x being R_eal holds ( x in b1 iff ex F being Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds ( x in b2 iff ex F being Interval_Covering of A st x = vol F ) ) holds b1 = b2 proof let D1, D2 be Subset of ExtREAL; ::_thesis: ( ( for x being R_eal holds ( x in D1 iff ex F being Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds ( x in D2 iff ex F being Interval_Covering of A st x = vol F ) ) implies D1 = D2 ) assume that A2: for x being R_eal holds ( x in D1 iff S1[x] ) and A3: for x being R_eal holds ( x in D2 iff S1[x] ) ; ::_thesis: D1 = D2 thus D1 = D2 from SUBSET_1:sch_2(A2, A3); ::_thesis: verum end; end; :: deftheorem Def8 defines Svc MEASURE7:def_8_:_ for A being Subset of REAL for b2 being Subset of ExtREAL holds ( b2 = Svc A iff for x being R_eal holds ( x in b2 iff ex F being Interval_Covering of A st x = vol F ) ); registration let A be Subset of REAL; cluster Svc A -> non empty ; coherence not Svc A is empty proof REAL c= REAL ; then consider F0 being Function of NAT,(bool REAL) such that A1: rng F0 = {REAL,({} REAL)} and A2: ( F0 . 0 = REAL & ( for n being Element of NAT st 0 < n holds F0 . n = {} REAL ) ) by MEASURE1:19; ( union {REAL,{}} = REAL \/ {} & ( for n being Element of NAT holds F0 . n is Interval ) ) by A2, NAT_1:3, ZFMISC_1:75; then reconsider F0 = F0 as Interval_Covering of A by A1, Def2; defpred S1[ set ] means ex F being Interval_Covering of A st A = vol F; consider D being set such that A3: for x being set holds ( x in D iff ( x in ExtREAL & S1[x] ) ) from XBOOLE_0:sch_1(); vol F0 in D by A3; hence not Svc A is empty by Def8; ::_thesis: verum end; end; definition let A be Subset of REAL; func COMPLEX A -> Element of ExtREAL equals :: MEASURE7:def 9 inf (Svc A); correctness coherence inf (Svc A) is Element of ExtREAL ; ; end; :: deftheorem defines COMPLEX MEASURE7:def_9_:_ for A being Subset of REAL holds COMPLEX A = inf (Svc A); definition func OS_Meas -> Function of (bool REAL),ExtREAL means :Def10: :: MEASURE7:def 10 for A being Subset of REAL holds it . A = inf (Svc A); existence ex b1 being Function of (bool REAL),ExtREAL st for A being Subset of REAL holds b1 . A = inf (Svc A) proof consider G being Function of (bool REAL),ExtREAL such that A1: for A being Subset of REAL holds G . A = COMPLEX A from FUNCT_2:sch_4(); take G ; ::_thesis: for A being Subset of REAL holds G . A = inf (Svc A) for A being Subset of REAL holds G . A = inf (Svc A) proof let A be Subset of REAL; ::_thesis: G . A = inf (Svc A) G . A = COMPLEX A by A1; hence G . A = inf (Svc A) ; ::_thesis: verum end; hence for A being Subset of REAL holds G . A = inf (Svc A) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (bool REAL),ExtREAL st ( for A being Subset of REAL holds b1 . A = inf (Svc A) ) & ( for A being Subset of REAL holds b2 . A = inf (Svc A) ) holds b1 = b2 proof deffunc H1( Subset of REAL) -> Element of ExtREAL = inf (Svc \$1); thus for F1, F2 being Function of (bool REAL),ExtREAL st ( for A being Subset of REAL holds F1 . A = H1(A) ) & ( for A being Subset of REAL holds F2 . A = H1(A) ) holds F1 = F2 from BINOP_2:sch_1(); ::_thesis: verum end; end; :: deftheorem Def10 defines OS_Meas MEASURE7:def_10_:_ for b1 being Function of (bool REAL),ExtREAL holds ( b1 = OS_Meas iff for A being Subset of REAL holds b1 . A = inf (Svc A) ); definition let F be Function of NAT,(bool REAL); let G be Interval_Covering of F; let H be Function of NAT,[:NAT,NAT:]; assume B1: rng H = [:NAT,NAT:] ; func On (G,H) -> Interval_Covering of union (rng F) means :Def11: :: MEASURE7:def 11 for n being Element of NAT holds it . n = (G . ((pr1 H) . n)) . ((pr2 H) . n); existence ex b1 being Interval_Covering of union (rng F) st for n being Element of NAT holds b1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) proof defpred S1[ Element of NAT , Subset of REAL] means \$2 = (G . ((pr1 H) . \$1)) . ((pr2 H) . \$1); A1: for n being Element of NAT ex y being Subset of REAL st S1[n,y] ; consider GG being Function of NAT,(bool REAL) such that A2: for n being Element of NAT holds S1[n,GG . n] from FUNCT_2:sch_3(A1); A3: union (rng F) c= union (rng GG) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng F) or x in union (rng GG) ) assume x in union (rng F) ; ::_thesis: x in union (rng GG) then consider A being set such that A4: x in A and A5: A in rng F by TARSKI:def_4; consider n1 being set such that A6: n1 in dom F and A7: A = F . n1 by A5, FUNCT_1:def_3; reconsider n1 = n1 as Element of NAT by A6; F . n1 c= union (rng (G . n1)) by Def2; then consider AA being set such that A8: x in AA and A9: AA in rng (G . n1) by A4, A7, TARSKI:def_4; consider n2 being set such that A10: n2 in dom (G . n1) and A11: AA = (G . n1) . n2 by A9, FUNCT_1:def_3; reconsider n2 = n2 as Element of NAT by A10; consider n being set such that A12: n in dom H and A13: [n1,n2] = H . n by B1, FUNCT_1:def_3; reconsider n = n as Element of NAT by A12; [((pr1 H) . n),((pr2 H) . n)] = [n1,n2] by A13, FUNCT_2:119; then ( (pr1 H) . n = n1 & (pr2 H) . n = n2 ) by XTUPLE_0:1; then A14: x in GG . n by A2, A8, A11; GG . n in rng GG by FUNCT_2:4; hence x in union (rng GG) by A14, TARSKI:def_4; ::_thesis: verum end; for n being Element of NAT holds GG . n is Interval proof let n be Element of NAT ; ::_thesis: GG . n is Interval GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A2; hence GG . n is Interval ; ::_thesis: verum end; then reconsider GG = GG as Interval_Covering of union (rng F) by A3, Def2; take GG ; ::_thesis: for n being Element of NAT holds GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) thus for n being Element of NAT holds GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Interval_Covering of union (rng F) st ( for n being Element of NAT holds b1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) & ( for n being Element of NAT holds b2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) holds b1 = b2 proof let G1, G2 be Interval_Covering of union (rng F); ::_thesis: ( ( for n being Element of NAT holds G1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) & ( for n being Element of NAT holds G2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) implies G1 = G2 ) assume that A15: for n being Element of NAT holds G1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) and A16: for n being Element of NAT holds G2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ; ::_thesis: G1 = G2 for n being set st n in NAT holds G1 . n = G2 . n proof let n be set ; ::_thesis: ( n in NAT implies G1 . n = G2 . n ) assume n in NAT ; ::_thesis: G1 . n = G2 . n then reconsider n = n as Element of NAT ; G1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A15; hence G1 . n = G2 . n by A16; ::_thesis: verum end; hence G1 = G2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def11 defines On MEASURE7:def_11_:_ for F being Function of NAT,(bool REAL) for G being Interval_Covering of F for H being Function of NAT,[:NAT,NAT:] st rng H = [:NAT,NAT:] holds for b4 being Interval_Covering of union (rng F) holds ( b4 = On (G,H) iff for n being Element of NAT holds b4 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ); reconsider D = NAT --> ({} REAL) as Function of NAT,(bool REAL) ; theorem Th14: :: MEASURE7:14 for H being Function of NAT,[:NAT,NAT:] st H is one-to-one & rng H = [:NAT,NAT:] holds for k being Element of NAT ex m being Element of NAT st for F being Function of NAT,(bool REAL) for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m proof reconsider y = D as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8; let H be Function of NAT,[:NAT,NAT:]; ::_thesis: ( H is one-to-one & rng H = [:NAT,NAT:] implies for k being Element of NAT ex m being Element of NAT st for F being Function of NAT,(bool REAL) for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m ) assume that A1: H is one-to-one and A2: rng H = [:NAT,NAT:] ; ::_thesis: for k being Element of NAT ex m being Element of NAT st for F being Function of NAT,(bool REAL) for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m defpred S1[ Element of NAT ] means ex m being Element of NAT st for F being Function of NAT,(bool REAL) for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . \$1 <= (Ser (vol G)) . m; A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) set N0 = { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ; A4: { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } c= NAT proof let s1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not s1 in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } or s1 in NAT ) assume s1 in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ; ::_thesis: s1 in NAT then ex s being Element of NAT st ( s = s1 & (pr1 H) . (k + 1) = (pr1 H) . s ) ; hence s1 in NAT ; ::_thesis: verum end; k + 1 in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ; then reconsider N0 = { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } as non empty Subset of NAT by A4; given m0 being Element of NAT such that A5: for F being Function of NAT,(bool REAL) for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m0 ; ::_thesis: S1[k + 1] take m = m0 + ((pr1 H) . (k + 1)); ::_thesis: for F being Function of NAT,(bool REAL) for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m let F be Function of NAT,(bool REAL); ::_thesis: for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m let G be Interval_Covering of F; ::_thesis: (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m defpred S2[ Element of NAT , Function] means ( ( \$1 <> (pr1 H) . (k + 1) implies for m being Element of NAT holds \$2 . m = (G . \$1) . m ) & ( \$1 = (pr1 H) . (k + 1) implies for m being Element of NAT holds \$2 . m = {} ) ); A6: for n being Element of NAT ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y] percases ( n <> (pr1 H) . (k + 1) or n = (pr1 H) . (k + 1) ) ; supposeA7: n <> (pr1 H) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y] reconsider y = G . n as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8; take y ; ::_thesis: S2[n,y] thus S2[n,y] by A7; ::_thesis: verum end; supposeA8: n = (pr1 H) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y] take y ; ::_thesis: S2[n,y] thus S2[n,y] by A8, FUNCOP_1:7; ::_thesis: verum end; end; end; consider G1 being Function of NAT,(Funcs (NAT,(bool REAL))) such that A9: for n being Element of NAT holds S2[n,G1 . n] from FUNCT_2:sch_3(A6); A10: for n being Element of NAT holds G1 . n is Interval_Covering of D . n proof let n be Element of NAT ; ::_thesis: G1 . n is Interval_Covering of D . n consider f0 being Function such that A11: G1 . n = f0 and A12: ( dom f0 = NAT & rng f0 c= bool REAL ) by FUNCT_2:def_2; reconsider f0 = f0 as Function of NAT,(bool REAL) by A12, FUNCT_2:2; A13: for s being Element of NAT holds f0 . s is Interval proof let s be Element of NAT ; ::_thesis: f0 . s is Interval percases ( n <> (pr1 H) . (k + 1) or n = (pr1 H) . (k + 1) ) ; suppose n <> (pr1 H) . (k + 1) ; ::_thesis: f0 . s is Interval then f0 . s = (G . n) . s by A9, A11; hence f0 . s is Interval ; ::_thesis: verum end; suppose n = (pr1 H) . (k + 1) ; ::_thesis: f0 . s is Interval hence f0 . s is Interval by A9, A11; ::_thesis: verum end; end; end; D . n = {} by FUNCOP_1:7; then D . n c= union (rng f0) by XBOOLE_1:2; then reconsider f0 = f0 as Interval_Covering of D . n by A13, Def2; G1 . n = f0 by A11; hence G1 . n is Interval_Covering of D . n ; ::_thesis: verum end; defpred S3[ Element of N0, Element of NAT ] means \$2 = (pr2 H) . \$1; defpred S4[ Element of NAT , Function] means ( ( \$1 = (pr1 H) . (k + 1) implies for m being Element of NAT holds \$2 . m = (G . \$1) . m ) & ( \$1 <> (pr1 H) . (k + 1) implies for m being Element of NAT holds \$2 . m = {} ) ); A14: for n being Element of NAT ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y] percases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ; supposeA15: n = (pr1 H) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y] reconsider y = G . n as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8; take y ; ::_thesis: S4[n,y] thus S4[n,y] by A15; ::_thesis: verum end; supposeA16: n <> (pr1 H) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y] take y ; ::_thesis: S4[n,y] thus S4[n,y] by A16, FUNCOP_1:7; ::_thesis: verum end; end; end; consider G0 being Function of NAT,(Funcs (NAT,(bool REAL))) such that A17: for n being Element of NAT holds S4[n,G0 . n] from FUNCT_2:sch_3(A14); for n being Element of NAT holds G0 . n is Interval_Covering of D . n proof let n be Element of NAT ; ::_thesis: G0 . n is Interval_Covering of D . n consider f0 being Function such that A18: G0 . n = f0 and A19: ( dom f0 = NAT & rng f0 c= bool REAL ) by FUNCT_2:def_2; reconsider f0 = f0 as Function of NAT,(bool REAL) by A19, FUNCT_2:2; A20: for s being Element of NAT holds f0 . s is Interval proof let s be Element of NAT ; ::_thesis: f0 . s is Interval percases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ; suppose n = (pr1 H) . (k + 1) ; ::_thesis: f0 . s is Interval then f0 . s = (G . n) . s by A17, A18; hence f0 . s is Interval ; ::_thesis: verum end; suppose n <> (pr1 H) . (k + 1) ; ::_thesis: f0 . s is Interval hence f0 . s is Interval by A17, A18; ::_thesis: verum end; end; end; D . n = {} by FUNCOP_1:7; then D . n c= union (rng f0) by XBOOLE_1:2; then reconsider f0 = f0 as Interval_Covering of D . n by A20, Def2; G0 . n = f0 by A18; hence G0 . n is Interval_Covering of D . n ; ::_thesis: verum end; then reconsider G0 = G0 as Interval_Covering of D by Def3; set GG0 = On (G0,H); reconsider G1 = G1 as Interval_Covering of D by A10, Def3; set GG1 = On (G1,H); A21: (Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((On (G0,H)) vol) by Th6, Th12; (On (G1,H)) . (k + 1) = (G1 . ((pr1 H) . (k + 1))) . ((pr2 H) . (k + 1)) by A2, Def11 .= {} by A9 ; then A22: ((On (G1,H)) vol) . (k + 1) = 0. by Def4, MEASURE5:10; (Ser ((On (G1,H)) vol)) . (k + 1) = ((Ser ((On (G1,H)) vol)) . k) + (((On (G1,H)) vol) . (k + 1)) by SUPINF_2:44; then A23: (Ser ((On (G1,H)) vol)) . (k + 1) = (Ser ((On (G1,H)) vol)) . k by A22, XXREAL_3:4; for s being Element of NAT holds 0. <= (vol G1) . s by Th13; then vol G1 is V93() by SUPINF_2:39; then A24: (Ser (vol G1)) . m0 <= (Ser (vol G1)) . m by SUPINF_2:41; A25: for n being Element of NAT holds ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) proof let n be Element of NAT ; ::_thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) A26: ( ((On (G0,H)) vol) . n = diameter ((On (G0,H)) . n) & ((On (G1,H)) vol) . n = diameter ((On (G1,H)) . n) ) by Def4; ((On (G,H)) vol) . n = diameter ((On (G,H)) . n) by Def4; then A27: ((On (G,H)) vol) . n = diameter ((G . ((pr1 H) . n)) . ((pr2 H) . n)) by A2, Def11; percases ( (pr1 H) . n = (pr1 H) . (k + 1) or (pr1 H) . n <> (pr1 H) . (k + 1) ) ; supposeA28: (pr1 H) . n = (pr1 H) . (k + 1) ; ::_thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) A29: (On (G1,H)) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11 .= {} by A9, A28 ; (On (G0,H)) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11 .= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A17, A28 ; hence ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) by A26, A27, A29, MEASURE5:10, XXREAL_3:4; ::_thesis: verum end; supposeA30: (pr1 H) . n <> (pr1 H) . (k + 1) ; ::_thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) A31: (On (G0,H)) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11 .= {} by A17, A30 ; (On (G1,H)) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11 .= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A9, A30 ; hence ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) by A26, A27, A31, MEASURE5:10, XXREAL_3:4; ::_thesis: verum end; end; end; ( (On (G0,H)) vol is V93() & (On (G1,H)) vol is V93() ) by Th12; then A32: (Ser ((On (G,H)) vol)) . (k + 1) = ((Ser ((On (G0,H)) vol)) . (k + 1)) + ((Ser ((On (G1,H)) vol)) . (k + 1)) by A25, Th3; for s being Element of NAT holds 0. <= (vol G1) . s by Th13; then A33: vol G1 is V93() by SUPINF_2:39; (Ser ((On (G1,H)) vol)) . k <= (Ser (vol G1)) . m0 by A5; then A34: (Ser ((On (G1,H)) vol)) . (k + 1) <= (Ser (vol G1)) . m by A23, A24, XXREAL_0:2; A35: for s being Element of N0 ex y being Element of NAT st S3[s,y] ; consider SOS being Function of N0,NAT such that A36: for s being Element of N0 holds S3[s,SOS . s] from FUNCT_2:sch_3(A35); A37: for n being Element of NAT holds (vol G) . n = ((vol G0) . n) + ((vol G1) . n) proof let n be Element of NAT ; ::_thesis: (vol G) . n = ((vol G0) . n) + ((vol G1) . n) A38: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) proof percases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ; supposeA39: n = (pr1 H) . (k + 1) ; ::_thesis: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) for s being Element of NAT holds ((G . n) vol) . s <= ((G0 . n) vol) . s proof let s be Element of NAT ; ::_thesis: ((G . n) vol) . s <= ((G0 . n) vol) . s ((G0 . n) vol) . s = diameter ((G0 . n) . s) by Def4 .= diameter ((G . n) . s) by A17, A39 .= ((G . n) vol) . s by Def4 ; hence ((G . n) vol) . s <= ((G0 . n) vol) . s ; ::_thesis: verum end; then A40: SUM ((G . n) vol) <= SUM ((G0 . n) vol) by SUPINF_2:43; for s being Element of NAT holds ((G1 . n) vol) . s = 0. proof let s be Element of NAT ; ::_thesis: ((G1 . n) vol) . s = 0. diameter ((G1 . n) . s) = 0. by A9, A39, MEASURE5:10; hence ((G1 . n) vol) . s = 0. by Def4; ::_thesis: verum end; then A41: SUM ((G1 . n) vol) = 0. by Th1; for s being Element of NAT holds ((G0 . n) vol) . s <= ((G . n) vol) . s proof let s be Element of NAT ; ::_thesis: ((G0 . n) vol) . s <= ((G . n) vol) . s ((G0 . n) vol) . s = diameter ((G0 . n) . s) by Def4 .= diameter ((G . n) . s) by A17, A39 .= ((G . n) vol) . s by Def4 ; hence ((G0 . n) vol) . s <= ((G . n) vol) . s ; ::_thesis: verum end; then SUM ((G0 . n) vol) <= SUM ((G . n) vol) by SUPINF_2:43; then SUM ((G . n) vol) = SUM ((G0 . n) vol) by A40, XXREAL_0:1; hence vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) by A41, XXREAL_3:4; ::_thesis: verum end; supposeA42: n <> (pr1 H) . (k + 1) ; ::_thesis: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) A43: for s being Element of NAT holds ((G1 . n) vol) . s = ((G . n) vol) . s proof let s be Element of NAT ; ::_thesis: ((G1 . n) vol) . s = ((G . n) vol) . s ( ((G1 . n) vol) . s = diameter ((G1 . n) . s) & ((G . n) vol) . s = diameter ((G . n) . s) ) by Def4; hence ((G1 . n) vol) . s = ((G . n) vol) . s by A9, A42; ::_thesis: verum end; then for s being Element of NAT holds ((G . n) vol) . s <= ((G1 . n) vol) . s ; then A44: SUM ((G . n) vol) <= SUM ((G1 . n) vol) by SUPINF_2:43; for s being Element of NAT holds ((G0 . n) vol) . s = 0. proof let s be Element of NAT ; ::_thesis: ((G0 . n) vol) . s = 0. diameter ((G0 . n) . s) = 0. by A17, A42, MEASURE5:10; hence ((G0 . n) vol) . s = 0. by Def4; ::_thesis: verum end; then A45: SUM ((G0 . n) vol) = 0. by Th1; for s being Element of NAT holds ((G1 . n) vol) . s <= ((G . n) vol) . s by A43; then SUM ((G1 . n) vol) <= SUM ((G . n) vol) by SUPINF_2:43; then SUM ((G . n) vol) = SUM ((G1 . n) vol) by A44, XXREAL_0:1; hence vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) by A45, XXREAL_3:4; ::_thesis: verum end; end; end; ( (vol G) . n = vol (G . n) & (vol G0) . n = vol (G0 . n) ) by Def7; hence (vol G) . n = ((vol G0) . n) + ((vol G1) . n) by A38, Def7; ::_thesis: verum end; for s being Element of NAT holds 0. <= (vol G0) . s by Th13; then vol G0 is V93() by SUPINF_2:39; then A46: ( (vol G0) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . ((pr1 H) . (k + 1)) & (Ser (vol G0)) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . m ) by Th2, SUPINF_2:41; A47: for s being Element of NAT holds ( ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) & ( not s in N0 implies ((On (G0,H)) vol) . s = 0. ) ) proof let s be Element of NAT ; ::_thesis: ( ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) & ( not s in N0 implies ((On (G0,H)) vol) . s = 0. ) ) thus ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) ::_thesis: ( not s in N0 implies ((On (G0,H)) vol) . s = 0. ) proof assume A48: s in N0 ; ::_thesis: ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s then A49: ex s1 being Element of NAT st ( s1 = s & (pr1 H) . (k + 1) = (pr1 H) . s1 ) ; A50: (pr2 H) . s = SOS . s by A36, A48; ((On (G0,H)) vol) . s = diameter ((On (G0,H)) . s) by Def4 .= diameter ((G0 . ((pr1 H) . (k + 1))) . ((pr2 H) . s)) by A2, A49, Def11 .= ((G0 . ((pr1 H) . (k + 1))) vol) . (SOS . s) by A50, Def4 .= (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s by A48, FUNCT_2:15 ; hence ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ; ::_thesis: verum end; assume not s in N0 ; ::_thesis: ((On (G0,H)) vol) . s = 0. then A51: not (pr1 H) . (k + 1) = (pr1 H) . s ; ((On (G0,H)) vol) . s = diameter ((On (G0,H)) . s) by Def4 .= diameter ((G0 . ((pr1 H) . s)) . ((pr2 H) . s)) by A2, Def11 .= 0. by A17, A51, MEASURE5:10 ; hence ((On (G0,H)) vol) . s = 0. ; ::_thesis: verum end; for s1, s2 being set st s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 holds s1 = s2 proof let s1, s2 be set ; ::_thesis: ( s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 implies s1 = s2 ) assume that A52: ( s1 in N0 & s2 in N0 ) and A53: SOS . s1 = SOS . s2 ; ::_thesis: s1 = s2 reconsider s1 = s1, s2 = s2 as Element of NAT by A52; A54: ( ex s11 being Element of NAT st ( s11 = s1 & (pr1 H) . (k + 1) = (pr1 H) . s11 ) & ex s22 being Element of NAT st ( s22 = s2 & (pr1 H) . (k + 1) = (pr1 H) . s22 ) ) by A52; A55: ( H . s1 = [((pr1 H) . s1),((pr2 H) . s1)] & H . s2 = [((pr1 H) . s2),((pr2 H) . s2)] ) by FUNCT_2:119; ( SOS . s1 = (pr2 H) . s1 & SOS . s2 = (pr2 H) . s2 ) by A36, A52; hence s1 = s2 by A1, A53, A54, A55, FUNCT_2:19; ::_thesis: verum end; then A56: SOS is one-to-one by FUNCT_2:19; (G0 . ((pr1 H) . (k + 1))) vol is V93() by Th12; then SUM ((On (G0,H)) vol) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol) by A56, A47, Th11; then A57: (Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol) by A21, XXREAL_0:2; SUM ((G0 . ((pr1 H) . (k + 1))) vol) = vol (G0 . ((pr1 H) . (k + 1))) .= (vol G0) . ((pr1 H) . (k + 1)) by Def7 ; then SUM ((G0 . ((pr1 H) . (k + 1))) vol) <= (Ser (vol G0)) . m by A46, XXREAL_0:2; then A58: (Ser ((On (G0,H)) vol)) . (k + 1) <= (Ser (vol G0)) . m by A57, XXREAL_0:2; for s being Element of NAT holds 0. <= (vol G0) . s by Th13; then vol G0 is V93() by SUPINF_2:39; then (Ser (vol G)) . m = ((Ser (vol G0)) . m) + ((Ser (vol G1)) . m) by A37, A33, Th3; hence (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m by A58, A34, A32, XXREAL_3:36; ::_thesis: verum end; A59: S1[ 0 ] proof take m = (pr1 H) . 0; ::_thesis: for F being Function of NAT,(bool REAL) for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m let F be Function of NAT,(bool REAL); ::_thesis: for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m let G be Interval_Covering of F; ::_thesis: (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m reconsider GG = On (G,H) as Interval_Covering of union (rng F) ; ( (GG vol) . 0 = diameter (GG . 0) & ((G . ((pr1 H) . 0)) vol) . ((pr2 H) . 0) = diameter ((G . ((pr1 H) . 0)) . ((pr2 H) . 0)) ) by Def4; then (GG vol) . 0 <= ((G . ((pr1 H) . 0)) vol) . ((pr2 H) . 0) by A2, Def11; then (GG vol) . 0 <= vol (G . ((pr1 H) . 0)) by Th12, MEASURE6:3; then A60: ( (Ser (GG vol)) . 0 = (GG vol) . 0 & (GG vol) . 0 <= (vol G) . ((pr1 H) . 0) ) by Def7, SUPINF_2:44; for n being Element of NAT holds 0. <= (vol G) . n by Th13; then vol G is V93() by SUPINF_2:39; then (vol G) . m <= (Ser (vol G)) . m by Th2; hence (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m by A60, XXREAL_0:2; ::_thesis: verum end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A59, A3); ::_thesis: verum end; theorem Th15: :: MEASURE7:15 for F being Function of NAT,(bool REAL) for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G) proof let F be Function of NAT,(bool REAL); ::_thesis: for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G) let G be Interval_Covering of F; ::_thesis: inf (Svc (union (rng F))) <= SUM (vol G) consider H being Function of NAT,[:NAT,NAT:] such that A1: H is one-to-one and dom H = NAT and A2: rng H = [:NAT,NAT:] by MEASURE6:1; set GG = On (G,H); A3: for x being ext-real number st x in rng (Ser ((On (G,H)) vol)) holds ex y being ext-real number st ( y in rng (Ser (vol G)) & x <= y ) proof let x be ext-real number ; ::_thesis: ( x in rng (Ser ((On (G,H)) vol)) implies ex y being ext-real number st ( y in rng (Ser (vol G)) & x <= y ) ) assume x in rng (Ser ((On (G,H)) vol)) ; ::_thesis: ex y being ext-real number st ( y in rng (Ser (vol G)) & x <= y ) then consider n being set such that A4: n in dom (Ser ((On (G,H)) vol)) and A5: x = (Ser ((On (G,H)) vol)) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A4; consider m being Element of NAT such that A6: for F being Function of NAT,(bool REAL) for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . n <= (Ser (vol G)) . m by A1, A2, Th14; take (Ser (vol G)) . m ; ::_thesis: ( (Ser (vol G)) . m in rng (Ser (vol G)) & x <= (Ser (vol G)) . m ) dom (Ser (vol G)) = NAT by FUNCT_2:def_1; hence ( (Ser (vol G)) . m in rng (Ser (vol G)) & x <= (Ser (vol G)) . m ) by A5, A6, FUNCT_1:def_3; ::_thesis: verum end; set Q = vol (On (G,H)); vol (On (G,H)) in Svc (union (rng F)) by Def8; then A7: inf (Svc (union (rng F))) <= vol (On (G,H)) by XXREAL_2:3; ( SUM ((On (G,H)) vol) = sup (rng (Ser ((On (G,H)) vol))) & SUM (vol G) = sup (rng (Ser (vol G))) ) by SUPINF_2:def_17; then vol (On (G,H)) <= SUM (vol G) by A3, XXREAL_2:63; hence inf (Svc (union (rng F))) <= SUM (vol G) by A7, XXREAL_0:2; ::_thesis: verum end; theorem Th16: :: MEASURE7:16 OS_Meas is C_Measure of REAL proof set G = D; ( {} c= union (rng D) & ( for n being Element of NAT holds D . n is Interval ) ) by FUNCOP_1:7, XBOOLE_1:2; then reconsider G = D as Interval_Covering of {} REAL by Def2; A1: for A being Subset of REAL for F being Interval_Covering of A holds F vol is V93() proof let A be Subset of REAL; ::_thesis: for F being Interval_Covering of A holds F vol is V93() let F be Interval_Covering of A; ::_thesis: F vol is V93() for n being Element of NAT holds 0. <= (F vol) . n proof let n be Element of NAT ; ::_thesis: 0. <= (F vol) . n (F vol) . n = diameter (F . n) by Def4; hence 0. <= (F vol) . n by MEASURE5:13; ::_thesis: verum end; hence F vol is V93() by SUPINF_2:39; ::_thesis: verum end; A2: for A being Subset of REAL holds 0. <= OS_Meas . A proof let A be Subset of REAL; ::_thesis: 0. <= OS_Meas . A A3: 0. is LowerBound of Svc A proof let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not x in Svc A or 0. <= x ) assume x in Svc A ; ::_thesis: 0. <= x then consider F being Interval_Covering of A such that A4: x = vol F by Def8; set y = (Ser (F vol)) . 0; F vol is V93() by A1; then A5: 0. <= (Ser (F vol)) . 0 by SUPINF_2:40; ( SUM (F vol) = sup (rng (Ser (F vol))) & (Ser (F vol)) . 0 <= sup (rng (Ser (F vol))) ) by FUNCT_2:4, SUPINF_2:def_17, XXREAL_2:4; hence 0. <= x by A4, A5, XXREAL_0:2; ::_thesis: verum end; OS_Meas . A = inf (Svc A) by Def10; hence 0. <= OS_Meas . A by A3, XXREAL_2:def_4; ::_thesis: verum end; hence OS_Meas is V93() by MEASURE1:def_2; :: according to MEASURE4:def_1 ::_thesis: ( OS_Meas is V76() & ( for b1, b2 being Element of bool REAL holds ( not b1 c= b2 or ( OS_Meas . b1 <= OS_Meas . b2 & ( for b3 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b3)) <= SUM (OS_Meas * b3) ) ) ) ) ) A6: for r being Element of NAT st 0 <= r holds (G vol) . r = 0. proof let n be Element of NAT ; ::_thesis: ( 0 <= n implies (G vol) . n = 0. ) diameter (G . n) = diameter {} by FUNCOP_1:7; hence ( 0 <= n implies (G vol) . n = 0. ) by Def4, MEASURE5:10; ::_thesis: verum end; then vol G = (Ser (G vol)) . 0 by A1, SUPINF_2:48 .= (G vol) . 0 by SUPINF_2:44 .= 0. by A6 ; then A7: 0. in Svc ({} REAL) by Def8; 0. is LowerBound of Svc ({} REAL) proof let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not x in Svc ({} REAL) or 0. <= x ) assume x in Svc ({} REAL) ; ::_thesis: 0. <= x then A8: inf (Svc ({} REAL)) <= x by XXREAL_2:3; 0. <= OS_Meas . ({} REAL) by A2; then 0. <= inf (Svc ({} REAL)) by Def10; hence 0. <= x by A8, XXREAL_0:2; ::_thesis: verum end; then inf (Svc ({} REAL)) = 0. by A7, XXREAL_2:56; hence OS_Meas . {} = 0 by Def10; :: according to VALUED_0:def_19 ::_thesis: for b1, b2 being Element of bool REAL holds ( not b1 c= b2 or ( OS_Meas . b1 <= OS_Meas . b2 & ( for b3 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b3)) <= SUM (OS_Meas * b3) ) ) ) let A, B be Subset of REAL; ::_thesis: ( not A c= B or ( OS_Meas . A <= OS_Meas . B & ( for b1 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b1)) <= SUM (OS_Meas * b1) ) ) ) assume A9: A c= B ; ::_thesis: ( OS_Meas . A <= OS_Meas . B & ( for b1 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b1)) <= SUM (OS_Meas * b1) ) ) A10: Svc B c= Svc A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Svc B or x in Svc A ) assume A11: x in Svc B ; ::_thesis: x in Svc A then reconsider x = x as R_eal ; consider F being Interval_Covering of B such that A12: x = vol F by A11, Def8; B c= union (rng F) by Def2; then ( ( for n being Element of NAT holds F . n is Interval ) & A c= union (rng F) ) by A9, XBOOLE_1:1; then reconsider G = F as Interval_Covering of A by Def2; for n being Element of NAT holds (F vol) . n <= (G vol) . n proof let n be Element of NAT ; ::_thesis: (F vol) . n <= (G vol) . n (G vol) . n = diameter (G . n) by Def4 .= (F vol) . n by Def4 ; hence (F vol) . n <= (G vol) . n ; ::_thesis: verum end; then A13: SUM (F vol) <= SUM (G vol) by SUPINF_2:43; for n being Element of NAT holds (G vol) . n <= (F vol) . n proof let n be Element of NAT ; ::_thesis: (G vol) . n <= (F vol) . n (G vol) . n = diameter (G . n) by Def4 .= (F vol) . n by Def4 ; hence (G vol) . n <= (F vol) . n ; ::_thesis: verum end; then SUM (G vol) <= SUM (F vol) by SUPINF_2:43; then x = vol G by A12, A13, XXREAL_0:1; hence x in Svc A by Def8; ::_thesis: verum end; ( OS_Meas . A = inf (Svc A) & OS_Meas . B = inf (Svc B) ) by Def10; hence OS_Meas . A <= OS_Meas . B by A10, XXREAL_2:60; ::_thesis: for b1 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b1)) <= SUM (OS_Meas * b1) let F be Function of NAT,(bool REAL); ::_thesis: OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) percases ( for n being Element of NAT holds Svc (F . n) <> {+infty} or ex n being Element of NAT st Svc (F . n) = {+infty} ) ; supposeA14: for n being Element of NAT holds Svc (F . n) <> {+infty} ; ::_thesis: OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) A15: SUM (OS_Meas * F) = sup (rng (Ser (OS_Meas * F))) by SUPINF_2:def_17; A16: for n being Element of NAT holds 0. <= (OS_Meas * F) . n proof let n be Element of NAT ; ::_thesis: 0. <= (OS_Meas * F) . n (OS_Meas * F) . n = OS_Meas . (F . n) by FUNCT_2:15; hence 0. <= (OS_Meas * F) . n by A2; ::_thesis: verum end; then A17: OS_Meas * F is V93() by SUPINF_2:39; inf (Svc (union (rng F))) <= sup (rng (Ser (OS_Meas * F))) proof set y = inf (Svc (union (rng F))); set x = sup (rng (Ser (OS_Meas * F))); assume A18: not inf (Svc (union (rng F))) <= sup (rng (Ser (OS_Meas * F))) ; ::_thesis: contradiction 0. <= (OS_Meas * F) . 0 by A16; then A19: 0. <= (Ser (OS_Meas * F)) . 0 by SUPINF_2:44; (Ser (OS_Meas * F)) . 0 <= sup (rng (Ser (OS_Meas * F))) by FUNCT_2:4, XXREAL_2:4; then 0. <= sup (rng (Ser (OS_Meas * F))) by A19, XXREAL_0:2; then consider eps being real number such that A20: 0. < eps and A21: (sup (rng (Ser (OS_Meas * F)))) + eps < inf (Svc (union (rng F))) by A18, XXREAL_3:49; reconsider eps = eps as Element of ExtREAL by XXREAL_0:def_1; consider E being Function of NAT,ExtREAL such that A22: for n being Element of NAT holds 0. < E . n and A23: SUM E < eps by A20, MEASURE6:4; A24: (SUM (OS_Meas * F)) + (SUM E) <= (SUM (OS_Meas * F)) + eps by A23, XXREAL_3:36; defpred S1[ Element of NAT , set ] means ex F0 being Interval_Covering of F . \$1 st ( \$2 = F0 & vol F0 < (inf (Svc (F . \$1))) + (E . \$1) ); A25: for n being Element of NAT ex F0 being Element of Funcs (NAT,(bool REAL)) st S1[n,F0] proof let n be Element of NAT ; ::_thesis: ex F0 being Element of Funcs (NAT,(bool REAL)) st S1[n,F0] A26: ( OS_Meas . (F . n) = inf (Svc (F . n)) & 0 is Real ) by Def10; Svc (F . n) <> {+infty} by A14; then not Svc (F . n) c= {+infty} by ZFMISC_1:33; then (Svc (F . n)) \ {+infty} <> {} by XBOOLE_1:37; then consider x being set such that A27: x in (Svc (F . n)) \ {+infty} by XBOOLE_0:def_1; reconsider x = x as R_eal by A27; not x in {+infty} by A27, XBOOLE_0:def_5; then A28: x <> +infty by TARSKI:def_1; x in Svc (F . n) by A27, XBOOLE_0:def_5; then inf (Svc (F . n)) <= x by XXREAL_2:3; then inf (Svc (F . n)) < +infty by A28, XXREAL_0:2, XXREAL_0:4; then inf (Svc (F . n)) is Real by A2, A26, XXREAL_0:46; then consider S being ext-real number such that A29: S in Svc (F . n) and A30: S < (inf (Svc (F . n))) + (E . n) by A22, MEASURE6:5; consider FS being Interval_Covering of F . n such that A31: S = vol FS by A29, Def8; reconsider FS = FS as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8; take FS ; ::_thesis: S1[n,FS] thus S1[n,FS] by A30, A31; ::_thesis: verum end; consider FF being Function of NAT,(Funcs (NAT,(bool REAL))) such that A32: for n being Element of NAT holds S1[n,FF . n] from FUNCT_2:sch_3(A25); for n being Element of NAT holds FF . n is Interval_Covering of F . n proof let n be Element of NAT ; ::_thesis: FF . n is Interval_Covering of F . n ex F0 being Interval_Covering of F . n st ( F0 = FF . n & vol F0 < (inf (Svc (F . n))) + (E . n) ) by A32; hence FF . n is Interval_Covering of F . n ; ::_thesis: verum end; then reconsider FF = FF as Interval_Covering of F by Def3; A33: inf (Svc (union (rng F))) <= SUM (vol FF) by Th15; defpred S2[ Element of NAT , Element of ExtREAL ] means \$2 = ((OS_Meas * F) . \$1) + (E . \$1); A34: for n being Element of NAT ex y being Element of ExtREAL st S2[n,y] ; consider G0 being Function of NAT,ExtREAL such that A35: for n being Element of NAT holds S2[n,G0 . n] from FUNCT_2:sch_3(A34); for n being Element of NAT holds (vol FF) . n <= G0 . n proof let n be Element of NAT ; ::_thesis: (vol FF) . n <= G0 . n ( ex F0 being Interval_Covering of F . n st ( F0 = FF . n & vol F0 < (inf (Svc (F . n))) + (E . n) ) & (OS_Meas * F) . n = OS_Meas . (F . n) ) by A32, FUNCT_2:15; then vol (FF . n) < ((OS_Meas * F) . n) + (E . n) by Def10; then (vol FF) . n < ((OS_Meas * F) . n) + (E . n) by Def7; hence (vol FF) . n <= G0 . n by A35; ::_thesis: verum end; then A36: SUM (vol FF) <= SUM G0 by SUPINF_2:43; for n being Element of NAT holds 0. <= E . n by A22; then E is V93() by SUPINF_2:39; then SUM G0 <= (SUM (OS_Meas * F)) + (SUM E) by A17, A35, Th4; then SUM G0 <= (SUM (OS_Meas * F)) + eps by A24, XXREAL_0:2; then SUM (vol FF) <= (SUM (OS_Meas * F)) + eps by A36, XXREAL_0:2; hence contradiction by A15, A21, A33, XXREAL_0:2; ::_thesis: verum end; hence OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) by A15, Def10; ::_thesis: verum end; suppose ex n being Element of NAT st Svc (F . n) = {+infty} ; ::_thesis: OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) then consider n being Element of NAT such that A37: Svc (F . n) = {+infty} ; for n being Element of NAT holds 0. <= (OS_Meas * F) . n proof let n be Element of NAT ; ::_thesis: 0. <= (OS_Meas * F) . n (OS_Meas * F) . n = OS_Meas . (F . n) by FUNCT_2:15; hence 0. <= (OS_Meas * F) . n by A2; ::_thesis: verum end; then A38: OS_Meas * F is V93() by SUPINF_2:39; inf {+infty} = +infty by XXREAL_2:13; then OS_Meas . (F . n) = +infty by A37, Def10; then (OS_Meas * F) . n = +infty by FUNCT_2:15; then SUM (OS_Meas * F) = +infty by A38, SUPINF_2:45; hence OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) by XXREAL_0:4; ::_thesis: verum end; end; end; definition :: original: OS_Meas redefine func OS_Meas -> C_Measure of REAL ; correctness coherence OS_Meas is C_Measure of REAL ; by Th16; end; definition func Lmi_sigmaFIELD -> SigmaField of REAL equals :: MEASURE7:def 12 sigma_Field OS_Meas; coherence sigma_Field OS_Meas is SigmaField of REAL ; end; :: deftheorem defines Lmi_sigmaFIELD MEASURE7:def_12_:_ Lmi_sigmaFIELD = sigma_Field OS_Meas; definition func L_mi -> sigma_Measure of Lmi_sigmaFIELD equals :: MEASURE7:def 13 sigma_Meas OS_Meas; correctness coherence sigma_Meas OS_Meas is sigma_Measure of Lmi_sigmaFIELD; ; end; :: deftheorem defines L_mi MEASURE7:def_13_:_ L_mi = sigma_Meas OS_Meas;