:: INTEGRA4 semantic presentation begin theorem Th1: :: INTEGRA4:1 for A being non empty closed_interval Subset of REAL for D being Division of A st vol A = 0 holds len D = 1 proof let A be non empty closed_interval Subset of REAL; ::_thesis: for D being Division of A st vol A = 0 holds len D = 1 let D be Division of A; ::_thesis: ( vol A = 0 implies len D = 1 ) assume that A1: vol A = 0 and A2: len D <> 1 ; ::_thesis: contradiction rng D <> {} ; then A3: 1 in dom D by FINSEQ_3:32; then A4: 1 <= len D by FINSEQ_3:25; then A5: len D in dom D by FINSEQ_3:25; D . 1 in A by A3, INTEGRA1:6; then A6: lower_bound A <= D . 1 by INTEGRA2:1; 1 < len D by A2, A4, XXREAL_0:1; then A7: D . 1 < D . (len D) by A3, A5, SEQM_3:def_1; (upper_bound A) - (lower_bound A) = 0 by A1, INTEGRA1:def_5; hence contradiction by A7, A6, INTEGRA1:def_2; ::_thesis: verum end; theorem Th2: :: INTEGRA4:2 for A being non empty closed_interval Subset of REAL holds ( chi (A,A) is integrable & integral (chi (A,A)) = vol A ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( chi (A,A) is integrable & integral (chi (A,A)) = vol A ) (divs A) /\ (dom (upper_sum_set (chi (A,A)))) = (divs A) /\ (divs A) by FUNCT_2:def_1; then A1: divs A meets dom (upper_sum_set (chi (A,A))) by XBOOLE_0:def_7; A2: for D1 being Element of divs A st D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) holds (upper_sum_set (chi (A,A))) /. D1 = vol A proof let D1 be Element of divs A; ::_thesis: ( D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) implies (upper_sum_set (chi (A,A))) /. D1 = vol A ) reconsider D2 = D1 as Division of A by INTEGRA1:def_3; assume D1 in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) ; ::_thesis: (upper_sum_set (chi (A,A))) /. D1 = vol A (upper_sum_set (chi (A,A))) /. D1 = (upper_sum_set (chi (A,A))) . D1 .= upper_sum ((chi (A,A)),D2) by INTEGRA1:def_10 .= Sum (upper_volume ((chi (A,A)),D2)) by INTEGRA1:def_8 ; hence (upper_sum_set (chi (A,A))) /. D1 = vol A by INTEGRA1:24; ::_thesis: verum end; then (upper_sum_set (chi (A,A))) | (divs A) is constant by PARTFUN2:35; then consider x being Element of REAL such that A3: rng ((upper_sum_set (chi (A,A))) | (divs A)) = {x} by A1, PARTFUN2:37; A4: chi (A,A) is upper_integrable by A3, INTEGRA1:def_12; vol A in rng (upper_sum_set (chi (A,A))) proof set D1 = the Element of divs A; the Element of divs A in divs A ; then A5: the Element of divs A in dom (upper_sum_set (chi (A,A))) by FUNCT_2:def_1; then A6: (upper_sum_set (chi (A,A))) . the Element of divs A in rng (upper_sum_set (chi (A,A))) by FUNCT_1:def_3; A7: (upper_sum_set (chi (A,A))) . the Element of divs A = (upper_sum_set (chi (A,A))) /. the Element of divs A ; the Element of divs A in (divs A) /\ (dom (upper_sum_set (chi (A,A)))) by A5, XBOOLE_0:def_4; hence vol A in rng (upper_sum_set (chi (A,A))) by A2, A6, A7; ::_thesis: verum end; then A8: x = vol A by A3, TARSKI:def_1; rng (upper_sum_set (chi (A,A))) = {x} by A3; then lower_bound (rng (upper_sum_set (chi (A,A)))) = vol A by A8, SEQ_4:9; then A9: upper_integral (chi (A,A)) = vol A by INTEGRA1:def_14; (divs A) /\ (dom (lower_sum_set (chi (A,A)))) = (divs A) /\ (divs A) by FUNCT_2:def_1; then A10: divs A meets dom (lower_sum_set (chi (A,A))) by XBOOLE_0:def_7; A11: for D1 being Element of divs A st D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) holds (lower_sum_set (chi (A,A))) /. D1 = vol A proof let D1 be Element of divs A; ::_thesis: ( D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) implies (lower_sum_set (chi (A,A))) /. D1 = vol A ) reconsider D2 = D1 as Division of A by INTEGRA1:def_3; assume D1 in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) ; ::_thesis: (lower_sum_set (chi (A,A))) /. D1 = vol A (lower_sum_set (chi (A,A))) /. D1 = (lower_sum_set (chi (A,A))) . D1 .= lower_sum ((chi (A,A)),D2) by INTEGRA1:def_11 .= Sum (lower_volume ((chi (A,A)),D2)) by INTEGRA1:def_9 ; hence (lower_sum_set (chi (A,A))) /. D1 = vol A by INTEGRA1:23; ::_thesis: verum end; then (lower_sum_set (chi (A,A))) | (divs A) is constant by PARTFUN2:35; then consider x being Element of REAL such that A12: rng ((lower_sum_set (chi (A,A))) | (divs A)) = {x} by A10, PARTFUN2:37; vol A in rng (lower_sum_set (chi (A,A))) proof set D1 = the Element of divs A; the Element of divs A in divs A ; then A13: the Element of divs A in dom (lower_sum_set (chi (A,A))) by FUNCT_2:def_1; then A14: (lower_sum_set (chi (A,A))) . the Element of divs A in rng (lower_sum_set (chi (A,A))) by FUNCT_1:def_3; A15: (lower_sum_set (chi (A,A))) . the Element of divs A = (lower_sum_set (chi (A,A))) /. the Element of divs A ; the Element of divs A in (divs A) /\ (dom (lower_sum_set (chi (A,A)))) by A13, XBOOLE_0:def_4; hence vol A in rng (lower_sum_set (chi (A,A))) by A11, A14, A15; ::_thesis: verum end; then A16: x = vol A by A12, TARSKI:def_1; rng (lower_sum_set (chi (A,A))) = {x} by A12; then upper_bound (rng (lower_sum_set (chi (A,A)))) = vol A by A16, SEQ_4:9; then A17: lower_integral (chi (A,A)) = vol A by INTEGRA1:def_15; chi (A,A) is lower_integrable by A12, INTEGRA1:def_13; hence ( chi (A,A) is integrable & integral (chi (A,A)) = vol A ) by A4, A9, A17, INTEGRA1:def_16, INTEGRA1:def_17; ::_thesis: verum end; theorem Th3: :: INTEGRA4:3 for A being non empty closed_interval Subset of REAL for f being PartFunc of A,REAL for r being Real holds ( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of A,REAL for r being Real holds ( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) ) let f be PartFunc of A,REAL; ::_thesis: for r being Real holds ( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) ) let r be Real; ::_thesis: ( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) ) A1: ( f = r (#) (chi (A,A)) implies ( f is total & rng f = {r} ) ) proof assume A2: f = r (#) (chi (A,A)) ; ::_thesis: ( f is total & rng f = {r} ) A3: chi (A,A) is total by RFUNCT_1:62; hence f is total by A2; ::_thesis: rng f = {r} A4: dom f = A by A2, A3, PARTFUN1:def_2; for x being set st x in {r} holds x in rng f proof let x be set ; ::_thesis: ( x in {r} implies x in rng f ) assume x in {r} ; ::_thesis: x in rng f then A5: x = r by TARSKI:def_1; consider a being Real such that A6: a in dom f by A4, SUBSET_1:4; (chi (A,A)) . a = 1 by A6, RFUNCT_1:63; then f . a = r * 1 by A2, A6, VALUED_1:def_5; hence x in rng f by A5, A6, FUNCT_1:def_3; ::_thesis: verum end; then A7: {r} c= rng f by TARSKI:def_3; for x being set st x in rng f holds x in {r} proof let x be set ; ::_thesis: ( x in rng f implies x in {r} ) assume x in rng f ; ::_thesis: x in {r} then consider a being Element of A such that A8: a in dom f and A9: f . a = x by PARTFUN1:3; (chi (A,A)) . a = 1 by RFUNCT_1:63; then x = r * 1 by A2, A8, A9, VALUED_1:def_5 .= r ; hence x in {r} by TARSKI:def_1; ::_thesis: verum end; then rng f c= {r} by TARSKI:def_3; hence rng f = {r} by A7, XBOOLE_0:def_10; ::_thesis: verum end; ( f is total & rng f = {r} implies f = r (#) (chi (A,A)) ) proof reconsider g = r (#) (chi (A,A)) as PartFunc of A,REAL ; assume A10: f is total ; ::_thesis: ( not rng f = {r} or f = r (#) (chi (A,A)) ) A11: chi (A,A) is total by RFUNCT_1:62; A12: dom g = dom (chi (A,A)) by VALUED_1:def_5 .= A by A11, PARTFUN1:def_2 ; assume A13: rng f = {r} ; ::_thesis: f = r (#) (chi (A,A)) A14: for x being Element of A st x in dom f holds f /. x = g /. x proof let x be Element of A; ::_thesis: ( x in dom f implies f /. x = g /. x ) assume A15: x in dom f ; ::_thesis: f /. x = g /. x then f /. x = f . x by PARTFUN1:def_6; then A16: f /. x in rng f by A15, FUNCT_1:def_3; g /. x = g . x by A12, PARTFUN1:def_6 .= r * ((chi (A,A)) . x) by A12, VALUED_1:def_5 .= r * 1 by RFUNCT_1:63 .= r ; hence f /. x = g /. x by A13, A16, TARSKI:def_1; ::_thesis: verum end; dom f = dom g by A10, A12, PARTFUN1:def_2; hence f = r (#) (chi (A,A)) by A14, PARTFUN2:1; ::_thesis: verum end; hence ( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) ) by A1; ::_thesis: verum end; theorem Th4: :: INTEGRA4:4 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for r being Real st rng f = {r} holds ( f is integrable & integral f = r * (vol A) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for r being Real st rng f = {r} holds ( f is integrable & integral f = r * (vol A) ) let f be Function of A,REAL; ::_thesis: for r being Real st rng f = {r} holds ( f is integrable & integral f = r * (vol A) ) let r be Real; ::_thesis: ( rng f = {r} implies ( f is integrable & integral f = r * (vol A) ) ) A1: chi (A,A) is Function of A,REAL by FUNCT_2:68, RFUNCT_1:62; A2: integral (chi (A,A)) = vol A by Th2; assume rng f = {r} ; ::_thesis: ( f is integrable & integral f = r * (vol A) ) then A3: f = r (#) (chi (A,A)) by Th3; A4: rng (chi (A,A)) is real-bounded by INTEGRA1:17; then A5: (chi (A,A)) | A is bounded_above by INTEGRA1:14; A6: (chi (A,A)) | A is bounded_below by A4, INTEGRA1:12; chi (A,A) is integrable by Th2; hence ( f is integrable & integral f = r * (vol A) ) by A3, A2, A1, A5, A6, INTEGRA2:31; ::_thesis: verum end; theorem Th5: :: INTEGRA4:5 for A being non empty closed_interval Subset of REAL for r being Real ex f being Function of A,REAL st ( rng f = {r} & f | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real ex f being Function of A,REAL st ( rng f = {r} & f | A is bounded ) let r be Real; ::_thesis: ex f being Function of A,REAL st ( rng f = {r} & f | A is bounded ) r (#) (chi (A,A)) is total by Th3; then reconsider f = r (#) (chi (A,A)) as Function of A,REAL ; A1: rng f = {r} by Th3; then A2: f | A is bounded_below by INTEGRA1:12; f | A is bounded_above by A1, INTEGRA1:14; hence ex f being Function of A,REAL st ( rng f = {r} & f | A is bounded ) by A1, A2; ::_thesis: verum end; Lm1: for A being non empty closed_interval Subset of REAL for f being PartFunc of A,REAL for D being Element of divs A st vol A = 0 holds ( f is upper_integrable & upper_integral f = 0 ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of A,REAL for D being Element of divs A st vol A = 0 holds ( f is upper_integrable & upper_integral f = 0 ) let f be PartFunc of A,REAL; ::_thesis: for D being Element of divs A st vol A = 0 holds ( f is upper_integrable & upper_integral f = 0 ) let D be Element of divs A; ::_thesis: ( vol A = 0 implies ( f is upper_integrable & upper_integral f = 0 ) ) (divs A) /\ (dom (upper_sum_set f)) = (divs A) /\ (divs A) by FUNCT_2:def_1; then A1: divs A meets dom (upper_sum_set f) by XBOOLE_0:def_7; assume A2: vol A = 0 ; ::_thesis: ( f is upper_integrable & upper_integral f = 0 ) A3: for D1 being Element of divs A st D1 in (divs A) /\ (dom (upper_sum_set f)) holds (upper_sum_set f) /. D1 = 0 proof let D1 be Element of divs A; ::_thesis: ( D1 in (divs A) /\ (dom (upper_sum_set f)) implies (upper_sum_set f) /. D1 = 0 ) reconsider D2 = D1 as Division of A by INTEGRA1:def_3; A4: len (upper_volume (f,D2)) = len D2 by INTEGRA1:def_6 .= 1 by A2, Th1 ; A5: len D2 = 1 by A2, Th1; then 1 in Seg (len D1) by FINSEQ_1:1; then A6: 1 in dom D1 by FINSEQ_1:def_3; rng D2 <> {} ; then A7: 1 in dom D2 by FINSEQ_3:32; then A8: upper_bound (divset (D2,(len D2))) = D2 . (len D2) by A5, INTEGRA1:def_4 .= upper_bound A by INTEGRA1:def_2 ; divset (D2,1) = [.(lower_bound (divset (D2,(len D2)))),(upper_bound (divset (D2,(len D2)))).] by A5, INTEGRA1:4 .= [.(lower_bound A),(upper_bound A).] by A5, A7, A8, INTEGRA1:def_4 ; then divset (D2,1) = A by INTEGRA1:4; then (upper_volume (f,D2)) . 1 = (upper_bound (rng (f | (divset (D2,1))))) * (vol A) by A6, INTEGRA1:def_6 .= 0 by A2 ; then A9: upper_volume (f,D2) = <*0*> by A4, FINSEQ_1:40; assume D1 in (divs A) /\ (dom (upper_sum_set f)) ; ::_thesis: (upper_sum_set f) /. D1 = 0 (upper_sum_set f) /. D1 = (upper_sum_set f) . D1 .= upper_sum (f,D2) by INTEGRA1:def_10 .= Sum (upper_volume (f,D2)) by INTEGRA1:def_8 ; hence (upper_sum_set f) /. D1 = 0 by A9, FINSOP_1:11; ::_thesis: verum end; then (upper_sum_set f) | (divs A) is constant by PARTFUN2:35; then consider x being Element of REAL such that A10: rng ((upper_sum_set f) | (divs A)) = {x} by A1, PARTFUN2:37; thus f is upper_integrable by A10, INTEGRA1:def_12; ::_thesis: upper_integral f = 0 0 in rng (upper_sum_set f) proof set D1 = the Element of divs A; the Element of divs A in divs A ; then A11: the Element of divs A in dom (upper_sum_set f) by FUNCT_2:def_1; then A12: (upper_sum_set f) . the Element of divs A in rng (upper_sum_set f) by FUNCT_1:def_3; A13: (upper_sum_set f) . the Element of divs A = (upper_sum_set f) /. the Element of divs A ; the Element of divs A in (divs A) /\ (dom (upper_sum_set f)) by A11, XBOOLE_0:def_4; hence 0 in rng (upper_sum_set f) by A3, A12, A13; ::_thesis: verum end; then A14: x = 0 by A10, TARSKI:def_1; rng (upper_sum_set f) = {x} by A10; then lower_bound (rng (upper_sum_set f)) = 0 by A14, SEQ_4:9; hence upper_integral f = 0 by INTEGRA1:def_14; ::_thesis: verum end; Lm2: for A being non empty closed_interval Subset of REAL for f being PartFunc of A,REAL for D being Element of divs A st vol A = 0 holds ( f is lower_integrable & lower_integral f = 0 ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of A,REAL for D being Element of divs A st vol A = 0 holds ( f is lower_integrable & lower_integral f = 0 ) let f be PartFunc of A,REAL; ::_thesis: for D being Element of divs A st vol A = 0 holds ( f is lower_integrable & lower_integral f = 0 ) let D be Element of divs A; ::_thesis: ( vol A = 0 implies ( f is lower_integrable & lower_integral f = 0 ) ) (divs A) /\ (dom (lower_sum_set f)) = (divs A) /\ (divs A) by FUNCT_2:def_1; then A1: divs A meets dom (lower_sum_set f) by XBOOLE_0:def_7; assume A2: vol A = 0 ; ::_thesis: ( f is lower_integrable & lower_integral f = 0 ) A3: for D1 being Element of divs A st D1 in (divs A) /\ (dom (lower_sum_set f)) holds (lower_sum_set f) /. D1 = 0 proof let D1 be Element of divs A; ::_thesis: ( D1 in (divs A) /\ (dom (lower_sum_set f)) implies (lower_sum_set f) /. D1 = 0 ) reconsider D2 = D1 as Division of A by INTEGRA1:def_3; A4: len (lower_volume (f,D2)) = len D2 by INTEGRA1:def_7 .= 1 by A2, Th1 ; A5: len D2 = 1 by A2, Th1; then 1 in Seg (len D2) by FINSEQ_1:1; then A6: 1 in dom D2 by FINSEQ_1:def_3; rng D2 <> {} ; then A7: 1 in dom D2 by FINSEQ_3:32; then A8: upper_bound (divset (D2,(len D2))) = D2 . (len D2) by A5, INTEGRA1:def_4 .= upper_bound A by INTEGRA1:def_2 ; divset (D2,1) = [.(lower_bound (divset (D2,(len D2)))),(upper_bound (divset (D2,(len D2)))).] by A5, INTEGRA1:4 .= [.(lower_bound A),(upper_bound A).] by A5, A7, A8, INTEGRA1:def_4 ; then divset (D2,1) = A by INTEGRA1:4; then (lower_volume (f,D2)) . 1 = (lower_bound (rng (f | (divset (D2,1))))) * (vol A) by A6, INTEGRA1:def_7 .= 0 by A2 ; then A9: lower_volume (f,D2) = <*0*> by A4, FINSEQ_1:40; assume D1 in (divs A) /\ (dom (lower_sum_set f)) ; ::_thesis: (lower_sum_set f) /. D1 = 0 (lower_sum_set f) /. D1 = (lower_sum_set f) . D1 .= lower_sum (f,D2) by INTEGRA1:def_11 .= Sum (lower_volume (f,D2)) by INTEGRA1:def_9 ; hence (lower_sum_set f) /. D1 = 0 by A9, FINSOP_1:11; ::_thesis: verum end; then (lower_sum_set f) | (divs A) is constant by PARTFUN2:35; then consider x being Element of REAL such that A10: rng ((lower_sum_set f) | (divs A)) = {x} by A1, PARTFUN2:37; thus f is lower_integrable by A10, INTEGRA1:def_13; ::_thesis: lower_integral f = 0 0 in rng (lower_sum_set f) proof set D1 = the Element of divs A; the Element of divs A in divs A ; then A11: the Element of divs A in dom (lower_sum_set f) by FUNCT_2:def_1; then A12: (lower_sum_set f) . the Element of divs A in rng (lower_sum_set f) by FUNCT_1:def_3; A13: (lower_sum_set f) . the Element of divs A = (lower_sum_set f) /. the Element of divs A ; the Element of divs A in (divs A) /\ (dom (lower_sum_set f)) by A11, XBOOLE_0:def_4; hence 0 in rng (lower_sum_set f) by A3, A12, A13; ::_thesis: verum end; then A14: x = 0 by A10, TARSKI:def_1; rng (lower_sum_set f) = {x} by A10; then upper_bound (rng (lower_sum_set f)) = 0 by A14, SEQ_4:9; hence lower_integral f = 0 by INTEGRA1:def_15; ::_thesis: verum end; theorem Th6: :: INTEGRA4:6 for A being non empty closed_interval Subset of REAL for f being PartFunc of A,REAL for D being Element of divs A st vol A = 0 holds ( f is integrable & integral f = 0 ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of A,REAL for D being Element of divs A st vol A = 0 holds ( f is integrable & integral f = 0 ) let f be PartFunc of A,REAL; ::_thesis: for D being Element of divs A st vol A = 0 holds ( f is integrable & integral f = 0 ) let D be Element of divs A; ::_thesis: ( vol A = 0 implies ( f is integrable & integral f = 0 ) ) assume A1: vol A = 0 ; ::_thesis: ( f is integrable & integral f = 0 ) then A2: upper_integral f = 0 by Lm1; A3: lower_integral f = 0 by A1, Lm2; A4: f is lower_integrable by A1, Lm2; f is upper_integrable by A1, Lm1; hence ( f is integrable & integral f = 0 ) by A2, A4, A3, INTEGRA1:def_16, INTEGRA1:def_17; ::_thesis: verum end; theorem :: INTEGRA4:7 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded & f is integrable holds ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) ) consider g being Function of A,REAL such that A1: rng g = {(lower_bound (rng f))} and A2: g | A is bounded by Th5; consider h being Function of A,REAL such that A3: rng h = {(upper_bound (rng f))} and A4: h | A is bounded by Th5; A5: integral g = (lower_bound (rng f)) * (vol A) by A1, Th4; assume A6: f | A is bounded ; ::_thesis: ( not f is integrable or ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) ) A7: for x being Real st x in dom f holds ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) proof let x be Real; ::_thesis: ( x in dom f implies ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) ) assume x in dom f ; ::_thesis: ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) then A8: f . x in rng f by FUNCT_1:def_3; A9: rng f is bounded_below by A6, INTEGRA1:11; rng f is bounded_above by A6, INTEGRA1:13; hence ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) by A9, A8, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum end; A10: for x being Real st x in A holds f . x <= h . x proof let x be Real; ::_thesis: ( x in A implies f . x <= h . x ) assume A11: x in A ; ::_thesis: f . x <= h . x dom h = A by FUNCT_2:def_1; then A12: h . x in rng h by A11, FUNCT_1:def_3; dom f = A by FUNCT_2:def_1; then f . x <= upper_bound (rng f) by A7, A11; hence f . x <= h . x by A3, A12, TARSKI:def_1; ::_thesis: verum end; A13: for x being Real st x in A holds g . x <= f . x proof let x be Real; ::_thesis: ( x in A implies g . x <= f . x ) assume A14: x in A ; ::_thesis: g . x <= f . x dom g = A by FUNCT_2:def_1; then A15: g . x in rng g by A14, FUNCT_1:def_3; dom f = A by FUNCT_2:def_1; then lower_bound (rng f) <= f . x by A7, A14; hence g . x <= f . x by A1, A15, TARSKI:def_1; ::_thesis: verum end; assume A16: f is integrable ; ::_thesis: ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) A17: integral h = (upper_bound (rng f)) * (vol A) by A3, Th4; A18: h is integrable by A3, Th4; A19: g is integrable by A1, Th4; now__::_thesis:_ex_a_being_Real_st_ (_lower_bound_(rng_f)_<=_a_&_a_<=_upper_bound_(rng_f)_&_integral_f_=_a_*_(vol_A)_) percases ( vol A <> 0 or vol A = 0 ) ; supposeA20: vol A <> 0 ; ::_thesis: ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) reconsider a = (integral f) / (vol A) as Real ; A21: integral f = a * (vol A) by A20, XCMPLX_1:87; A22: vol A >= 0 by INTEGRA1:9; then A23: (integral f) / (vol A) <= upper_bound (rng f) by A6, A16, A4, A18, A17, A10, A20, INTEGRA2:34, XREAL_1:79; lower_bound (rng f) <= (integral f) / (vol A) by A6, A16, A2, A19, A5, A13, A20, A22, INTEGRA2:34, XREAL_1:77; hence ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) by A23, A21; ::_thesis: verum end; supposeA24: vol A = 0 ; ::_thesis: ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) A25: lower_bound (rng f) <= upper_bound (rng f) proof dom f = A by FUNCT_2:def_1; then consider x being Real such that A26: x in dom f by SUBSET_1:4; A27: f . x <= upper_bound (rng f) by A7, A26; lower_bound (rng f) <= f . x by A7, A26; hence lower_bound (rng f) <= upper_bound (rng f) by A27, XXREAL_0:2; ::_thesis: verum end; integral f = (lower_bound (rng f)) * (vol A) by A24, Th6; hence ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) by A25; ::_thesis: verum end; end; end; hence ex a being Real st ( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) ; ::_thesis: verum end; begin theorem Th8: :: INTEGRA4:8 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) let f be Function of A,REAL; ::_thesis: for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) let T be DivSequence of A; ::_thesis: ( f | A is bounded & delta T is convergent & lim (delta T) = 0 implies ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) ) assume A1: f | A is bounded ; ::_thesis: ( not delta T is convergent or not lim (delta T) = 0 or ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) ) assume A2: delta T is convergent ; ::_thesis: ( not lim (delta T) = 0 or ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) ) assume A3: lim (delta T) = 0 ; ::_thesis: ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) now__::_thesis:_(_lower_sum_(f,T)_is_convergent_&_lim_(lower_sum_(f,T))_=_lower_integral_f_) percases ( vol A <> 0 or vol A = 0 ) ; supposeA4: vol A <> 0 ; ::_thesis: ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) for n being Element of NAT holds (delta T) . n <> 0 proof let n be Element of NAT ; ::_thesis: (delta T) . n <> 0 reconsider mm = rng (upper_volume ((chi (A,A)),(T . n))) as non empty finite Subset of REAL ; reconsider D = T . n as Division of A ; assume (delta T) . n = 0 ; ::_thesis: contradiction then delta (T . n) = 0 by INTEGRA3:def_2; then A5: max mm = 0 by INTEGRA3:def_1; A6: for k being Element of NAT st k in dom D holds vol (divset (D,k)) = 0 proof let k be Element of NAT ; ::_thesis: ( k in dom D implies vol (divset (D,k)) = 0 ) assume A7: k in dom D ; ::_thesis: vol (divset (D,k)) = 0 then k in Seg (len D) by FINSEQ_1:def_3; then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6; then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3; then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3; then (upper_volume ((chi (A,A)),D)) . k <= 0 by A5, XXREAL_2:def_8; then vol (divset (D,k)) <= 0 by A7, INTEGRA1:20; hence vol (divset (D,k)) = 0 by INTEGRA1:9; ::_thesis: verum end; A8: for j being Nat st 1 <= j & j <= len (upper_volume ((chi (A,A)),D)) holds (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j proof let j be Nat; ::_thesis: ( 1 <= j & j <= len (upper_volume ((chi (A,A)),D)) implies (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j ) assume that A9: 1 <= j and A10: j <= len (upper_volume ((chi (A,A)),D)) ; ::_thesis: (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j j in Seg (len (upper_volume ((chi (A,A)),D))) by A9, A10, FINSEQ_1:1; then A11: j in Seg (len D) by INTEGRA1:def_6; then j in dom D by FINSEQ_1:def_3; then A12: (upper_volume ((chi (A,A)),D)) . j = vol (divset (D,j)) by INTEGRA1:20; j in dom D by A11, FINSEQ_1:def_3; then (upper_volume ((chi (A,A)),D)) . j = 0 by A6, A12; hence (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j by A11, FUNCOP_1:7; ::_thesis: verum end; len (upper_volume ((chi (A,A)),D)) = len D by INTEGRA1:def_6; then len (upper_volume ((chi (A,A)),D)) = len ((len D) |-> 0) by CARD_1:def_7; then upper_volume ((chi (A,A)),D) = (len D) |-> 0 by A8, FINSEQ_1:14; then Sum (upper_volume ((chi (A,A)),D)) = 0 by RVSUM_1:81; hence contradiction by A4, INTEGRA1:24; ::_thesis: verum end; then delta T is non-zero by SEQ_1:5; then ( delta T is 0 -convergent & delta T is non-zero ) by A2, A3, FDIFF_1:def_1; hence ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) by A1, A4, INTEGRA3:20; ::_thesis: verum end; supposeA13: vol A = 0 ; ::_thesis: ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) A14: for n being Nat holds (lower_sum (f,T)) . n = 0 proof let n be Nat; ::_thesis: (lower_sum (f,T)) . n = 0 reconsider nn = n as Element of NAT by ORDINAL1:def_12; reconsider D = T . nn as Division of A ; A15: len D = 1 by A13, Th1; then A16: len (lower_volume (f,D)) = 1 by INTEGRA1:def_7; rng D <> {} ; then A17: 1 in dom D by FINSEQ_3:32; then A18: upper_bound (divset (D,(len D))) = D . (len D) by A15, INTEGRA1:def_4 .= upper_bound A by INTEGRA1:def_2 ; 1 in Seg (len D) by A15, FINSEQ_1:1; then A19: 1 in dom D by FINSEQ_1:def_3; divset (D,1) = [.(lower_bound (divset (D,(len D)))),(upper_bound (divset (D,(len D)))).] by A15, INTEGRA1:4 .= [.(lower_bound A),(upper_bound A).] by A15, A17, A18, INTEGRA1:def_4 ; then divset (D,1) = A by INTEGRA1:4; then (lower_volume (f,D)) . 1 = (lower_bound (rng (f | (divset (D,1))))) * (vol A) by A19, INTEGRA1:def_7 .= 0 by A13 ; then lower_volume (f,D) = <*0*> by A16, FINSEQ_1:40; then Sum (lower_volume (f,D)) = 0 by FINSOP_1:11; then lower_sum (f,D) = 0 by INTEGRA1:def_9; hence (lower_sum (f,T)) . n = 0 by INTEGRA2:def_3; ::_thesis: verum end; then A20: lower_sum (f,T) is constant by VALUED_0:def_18; hence lower_sum (f,T) is convergent ; ::_thesis: lim (lower_sum (f,T)) = lower_integral f (lower_sum (f,T)) . 1 = 0 by A14; then lim (lower_sum (f,T)) = 0 by A20, SEQ_4:25; hence lim (lower_sum (f,T)) = lower_integral f by A13, Lm2; ::_thesis: verum end; end; end; hence ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) ; ::_thesis: verum end; theorem Th9: :: INTEGRA4:9 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) let f be Function of A,REAL; ::_thesis: for T being DivSequence of A st f | A is bounded & delta T is convergent & lim (delta T) = 0 holds ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) let T be DivSequence of A; ::_thesis: ( f | A is bounded & delta T is convergent & lim (delta T) = 0 implies ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) ) assume A1: f | A is bounded ; ::_thesis: ( not delta T is convergent or not lim (delta T) = 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) ) assume A2: delta T is convergent ; ::_thesis: ( not lim (delta T) = 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) ) assume A3: lim (delta T) = 0 ; ::_thesis: ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) now__::_thesis:_(_upper_sum_(f,T)_is_convergent_&_lim_(upper_sum_(f,T))_=_upper_integral_f_) percases ( vol A <> 0 or vol A = 0 ) ; supposeA4: vol A <> 0 ; ::_thesis: ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) for n being Element of NAT holds (delta T) . n <> 0 proof let n be Element of NAT ; ::_thesis: (delta T) . n <> 0 reconsider D = T . n as Division of A ; assume (delta T) . n = 0 ; ::_thesis: contradiction then delta (T . n) = 0 by INTEGRA3:def_2; then A5: max (rng (upper_volume ((chi (A,A)),(T . n)))) = 0 by INTEGRA3:def_1; A6: for k being Element of NAT st k in dom D holds vol (divset (D,k)) = 0 proof let k be Element of NAT ; ::_thesis: ( k in dom D implies vol (divset (D,k)) = 0 ) assume A7: k in dom D ; ::_thesis: vol (divset (D,k)) = 0 then k in Seg (len D) by FINSEQ_1:def_3; then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6; then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3; then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3; then (upper_volume ((chi (A,A)),D)) . k <= 0 by A5, XXREAL_2:def_8; then vol (divset (D,k)) <= 0 by A7, INTEGRA1:20; hence vol (divset (D,k)) = 0 by INTEGRA1:9; ::_thesis: verum end; A8: for j being Nat st 1 <= j & j <= len (upper_volume ((chi (A,A)),D)) holds (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j proof let j be Nat; ::_thesis: ( 1 <= j & j <= len (upper_volume ((chi (A,A)),D)) implies (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j ) assume that A9: 1 <= j and A10: j <= len (upper_volume ((chi (A,A)),D)) ; ::_thesis: (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j j in Seg (len (upper_volume ((chi (A,A)),D))) by A9, A10, FINSEQ_1:1; then A11: j in Seg (len D) by INTEGRA1:def_6; then j in dom D by FINSEQ_1:def_3; then A12: (upper_volume ((chi (A,A)),D)) . j = vol (divset (D,j)) by INTEGRA1:20; j in dom D by A11, FINSEQ_1:def_3; then (upper_volume ((chi (A,A)),D)) . j = 0 by A6, A12; hence (upper_volume ((chi (A,A)),D)) . j = ((len D) |-> 0) . j by A11, FUNCOP_1:7; ::_thesis: verum end; len (upper_volume ((chi (A,A)),D)) = len D by INTEGRA1:def_6; then len (upper_volume ((chi (A,A)),D)) = len ((len D) |-> 0) by CARD_1:def_7; then upper_volume ((chi (A,A)),D) = (len D) |-> 0 by A8, FINSEQ_1:14; then Sum (upper_volume ((chi (A,A)),D)) = 0 by RVSUM_1:81; hence contradiction by A4, INTEGRA1:24; ::_thesis: verum end; then delta T is non-zero by SEQ_1:5; then ( delta T is 0 -convergent & delta T is non-zero ) by A2, A3, FDIFF_1:def_1; hence ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) by A1, A4, INTEGRA3:21; ::_thesis: verum end; supposeA13: vol A = 0 ; ::_thesis: ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) A14: for n being Nat holds (upper_sum (f,T)) . n = 0 proof let n be Nat; ::_thesis: (upper_sum (f,T)) . n = 0 reconsider nn = n as Element of NAT by ORDINAL1:def_12; reconsider D = T . nn as Division of A ; A15: len D = 1 by A13, Th1; then A16: len (upper_volume (f,D)) = 1 by INTEGRA1:def_6; rng D <> {} ; then A17: 1 in dom D by FINSEQ_3:32; then A18: upper_bound (divset (D,(len D))) = D . (len D) by A15, INTEGRA1:def_4 .= upper_bound A by INTEGRA1:def_2 ; 1 in Seg (len D) by A15, FINSEQ_1:1; then A19: 1 in dom D by FINSEQ_1:def_3; divset (D,1) = [.(lower_bound (divset (D,(len D)))),(upper_bound (divset (D,(len D)))).] by A15, INTEGRA1:4 .= [.(lower_bound A),(upper_bound A).] by A15, A17, A18, INTEGRA1:def_4 ; then divset (D,1) = A by INTEGRA1:4; then (upper_volume (f,D)) . 1 = (upper_bound (rng (f | (divset (D,1))))) * (vol A) by A19, INTEGRA1:def_6 .= 0 by A13 ; then upper_volume (f,D) = <*0*> by A16, FINSEQ_1:40; then Sum (upper_volume (f,D)) = 0 by FINSOP_1:11; then upper_sum (f,D) = 0 by INTEGRA1:def_8; hence (upper_sum (f,T)) . n = 0 by INTEGRA2:def_2; ::_thesis: verum end; then A20: upper_sum (f,T) is constant by VALUED_0:def_18; hence upper_sum (f,T) is convergent ; ::_thesis: lim (upper_sum (f,T)) = upper_integral f (upper_sum (f,T)) . 1 = 0 by A14; then lim (upper_sum (f,T)) = 0 by A20, SEQ_4:25; hence lim (upper_sum (f,T)) = upper_integral f by A13, Lm1; ::_thesis: verum end; end; end; hence ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) ; ::_thesis: verum end; theorem Th10: :: INTEGRA4:10 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded holds ( f is upper_integrable & f is lower_integrable ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded holds ( f is upper_integrable & f is lower_integrable ) let f be Function of A,REAL; ::_thesis: ( f | A is bounded implies ( f is upper_integrable & f is lower_integrable ) ) assume A1: f | A is bounded ; ::_thesis: ( f is upper_integrable & f is lower_integrable ) (lower_bound (rng f)) * (vol A) is LowerBound of rng (upper_sum_set f) proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in rng (upper_sum_set f) or (lower_bound (rng f)) * (vol A) <= r ) assume r in rng (upper_sum_set f) ; ::_thesis: (lower_bound (rng f)) * (vol A) <= r then consider D being Element of divs A such that D in dom (upper_sum_set f) and A2: (upper_sum_set f) . D = r by PARTFUN1:3; reconsider D = D as Division of A by INTEGRA1:def_3; r = upper_sum (f,D) by A2, INTEGRA1:def_10; then A3: lower_sum (f,D) <= r by A1, INTEGRA1:28; (lower_bound (rng f)) * (vol A) <= lower_sum (f,D) by A1, INTEGRA1:25; hence (lower_bound (rng f)) * (vol A) <= r by A3, XXREAL_0:2; ::_thesis: verum end; then rng (upper_sum_set f) is bounded_below by XXREAL_2:def_9; hence f is upper_integrable by INTEGRA1:def_12; ::_thesis: f is lower_integrable (upper_bound (rng f)) * (vol A) is UpperBound of rng (lower_sum_set f) proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in rng (lower_sum_set f) or r <= (upper_bound (rng f)) * (vol A) ) assume r in rng (lower_sum_set f) ; ::_thesis: r <= (upper_bound (rng f)) * (vol A) then consider D being Element of divs A such that D in dom (lower_sum_set f) and A4: (lower_sum_set f) . D = r by PARTFUN1:3; reconsider D = D as Division of A by INTEGRA1:def_3; r = lower_sum (f,D) by A4, INTEGRA1:def_11; then A5: upper_sum (f,D) >= r by A1, INTEGRA1:28; (upper_bound (rng f)) * (vol A) >= upper_sum (f,D) by A1, INTEGRA1:27; hence r <= (upper_bound (rng f)) * (vol A) by A5, XXREAL_0:2; ::_thesis: verum end; then rng (lower_sum_set f) is bounded_above by XXREAL_2:def_10; hence f is lower_integrable by INTEGRA1:def_13; ::_thesis: verum end; definition let A be non empty closed_interval Subset of REAL; let IT be Division of A; let n be Element of NAT ; predIT divide_into_equal n means :Def1: :: INTEGRA4:def 1 ( len IT = n & ( for i being Element of NAT st i in dom IT holds IT . i = (lower_bound A) + (((vol A) / (len IT)) * i) ) ); end; :: deftheorem Def1 defines divide_into_equal INTEGRA4:def_1_:_ for A being non empty closed_interval Subset of REAL for IT being Division of A for n being Element of NAT holds ( IT divide_into_equal n iff ( len IT = n & ( for i being Element of NAT st i in dom IT holds IT . i = (lower_bound A) + (((vol A) / (len IT)) * i) ) ) ); Lm3: for A being non empty closed_interval Subset of REAL for n being Element of NAT st n > 0 & vol A > 0 holds ex D being Division of A st ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being Element of NAT st n > 0 & vol A > 0 holds ex D being Division of A st ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) let n be Element of NAT ; ::_thesis: ( n > 0 & vol A > 0 implies ex D being Division of A st ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) ) assume that A1: n > 0 and A2: vol A > 0 ; ::_thesis: ex D being Division of A st ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) deffunc H1( Nat) -> Element of REAL = (lower_bound A) + (((vol A) / n) * \$1); consider D being FinSequence of REAL such that A3: ( len D = n & ( for i being Nat st i in dom D holds D . i = H1(i) ) ) from FINSEQ_2:sch_1(); A4: for i, j being Element of NAT st i in dom D & j in dom D & i < j holds D . i < D . j proof let i, j be Element of NAT ; ::_thesis: ( i in dom D & j in dom D & i < j implies D . i < D . j ) assume that A5: i in dom D and A6: j in dom D and A7: i < j ; ::_thesis: D . i < D . j (vol A) / n > 0 by A1, A2, XREAL_1:139; then ((vol A) / n) * i < ((vol A) / n) * j by A7, XREAL_1:68; then (lower_bound A) + (((vol A) / n) * i) < (lower_bound A) + (((vol A) / n) * j) by XREAL_1:6; then D . i < (lower_bound A) + (((vol A) / n) * j) by A3, A5; hence D . i < D . j by A3, A6; ::_thesis: verum end; A8: dom D = Seg n by A3, FINSEQ_1:def_3; reconsider D = D as non empty increasing FinSequence of REAL by A1, A3, A4, SEQM_3:def_1; D . (len D) = (lower_bound A) + (((vol A) / n) * n) by A3, A8, FINSEQ_1:3; then A9: D . (len D) = (lower_bound A) + (vol A) by A1, XCMPLX_1:87; for x1 being set st x1 in rng D holds x1 in A proof let x1 be set ; ::_thesis: ( x1 in rng D implies x1 in A ) A10: (lower_bound A) + (vol A) = (lower_bound A) + ((upper_bound A) - (lower_bound A)) by INTEGRA1:def_5 .= upper_bound A ; assume A11: x1 in rng D ; ::_thesis: x1 in A then reconsider x1 = x1 as Real ; consider i being Element of NAT such that A12: i in dom D and A13: D . i = x1 by A11, PARTFUN1:3; A14: 1 <= i by A12, FINSEQ_3:25; i <= len D by A12, FINSEQ_3:25; then ((vol A) / n) * i <= ((vol A) / n) * n by A2, A3, XREAL_1:64; then ((vol A) / n) * i <= vol A by A1, XCMPLX_1:87; then A15: (lower_bound A) + (((vol A) / n) * i) <= (lower_bound A) + (vol A) by XREAL_1:6; (vol A) / n > 0 by A1, A2, XREAL_1:139; then A16: lower_bound A <= (lower_bound A) + (((vol A) / n) * i) by A14, XREAL_1:29, XREAL_1:129; x1 = (lower_bound A) + (((vol A) / n) * i) by A3, A12, A13; hence x1 in A by A16, A15, A10, INTEGRA2:1; ::_thesis: verum end; then A17: rng D c= A by TARSKI:def_3; vol A = (upper_bound A) - (lower_bound A) by INTEGRA1:def_5; then reconsider D = D as Division of A by A17, A9, INTEGRA1:def_2; take D ; ::_thesis: ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) thus ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) by A3; ::_thesis: verum end; Lm4: for A being non empty closed_interval Subset of REAL st vol A > 0 holds ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( vol A > 0 implies ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) ) defpred S1[ set , set ] means ex n being Element of NAT ex e being Division of A st ( n = \$1 & e = \$2 & e divide_into_equal n + 1 ); assume A1: vol A > 0 ; ::_thesis: ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) A2: for n being Element of NAT ex D being Element of divs A st S1[n,D] proof let n be Element of NAT ; ::_thesis: ex D being Element of divs A st S1[n,D] consider D being Division of A such that A3: len D = n + 1 and A4: for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / (n + 1)) * i) by A1, Lm3; A5: D is Element of divs A by INTEGRA1:def_3; D divide_into_equal n + 1 by A3, A4, Def1; hence ex D being Element of divs A st S1[n,D] by A5; ::_thesis: verum end; consider T being Function of NAT,(divs A) such that A6: for n being Element of NAT holds S1[n,T . n] from FUNCT_2:sch_3(A2); reconsider T = T as DivSequence of A ; A7: for i being Element of NAT holds (delta T) . i = (vol A) / (i + 1) proof let i be Element of NAT ; ::_thesis: (delta T) . i = (vol A) / (i + 1) (delta T) . i = delta (T . i) by INTEGRA3:def_2; then A8: (delta T) . i = max (rng (upper_volume ((chi (A,A)),(T . i)))) by INTEGRA3:def_1; for x1 being set st x1 in rng (upper_volume ((chi (A,A)),(T . i))) holds x1 in {((vol A) / (i + 1))} proof reconsider D = T . i as Division of A ; let x1 be set ; ::_thesis: ( x1 in rng (upper_volume ((chi (A,A)),(T . i))) implies x1 in {((vol A) / (i + 1))} ) assume x1 in rng (upper_volume ((chi (A,A)),(T . i))) ; ::_thesis: x1 in {((vol A) / (i + 1))} then consider k being Element of NAT such that A9: k in dom (upper_volume ((chi (A,A)),(T . i))) and A10: (upper_volume ((chi (A,A)),(T . i))) . k = x1 by PARTFUN1:3; A11: ex n being Element of NAT ex e being Division of A st ( n = i & e = D & e divide_into_equal n + 1 ) by A6; k in Seg (len (upper_volume ((chi (A,A)),(T . i)))) by A9, FINSEQ_1:def_3; then A12: k in Seg (len D) by INTEGRA1:def_6; A13: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) proof A14: 1 <= k by A9, FINSEQ_3:25; now__::_thesis:_(upper_bound_(divset_(D,k)))_-_(lower_bound_(divset_(D,k)))_=_(vol_A)_/_(i_+_1) percases ( k = 1 or k > 1 ) by A14, XXREAL_0:1; supposeA15: k = 1 ; ::_thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) A16: len D = i + 1 by A11, Def1; A17: 1 in dom D by A12, A15, FINSEQ_1:def_3; then upper_bound (divset (D,k)) = D . 1 by A15, INTEGRA1:def_4; then upper_bound (divset (D,k)) = (lower_bound A) + (((vol A) / (i + 1)) * 1) by A11, A17, A16, Def1; then (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = ((lower_bound A) + ((vol A) / (i + 1))) - (lower_bound A) by A15, A17, INTEGRA1:def_4 .= ((vol A) / (i + 1)) - ((lower_bound A) - (lower_bound A)) ; hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) ; ::_thesis: verum end; supposeA18: k > 1 ; ::_thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) A19: k in dom D by A12, FINSEQ_1:def_3; then A20: lower_bound (divset (D,k)) = D . (k - 1) by A18, INTEGRA1:def_4; k - 1 in dom D by A18, A19, INTEGRA1:7; then A21: D . (k - 1) = (lower_bound A) + (((vol A) / (len D)) * (k - 1)) by A11, Def1; A22: upper_bound (divset (D,k)) = D . k by A18, A19, INTEGRA1:def_4; D . k = (lower_bound A) + (((vol A) / (len D)) * k) by A11, A19, Def1; hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A11, A20, A22, A21, Def1; ::_thesis: verum end; end; end; hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) ; ::_thesis: verum end; k in dom D by A12, FINSEQ_1:def_3; then x1 = vol (divset (D,k)) by A10, INTEGRA1:20; then x1 = (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by INTEGRA1:def_5; hence x1 in {((vol A) / (i + 1))} by A13, TARSKI:def_1; ::_thesis: verum end; then A23: rng (upper_volume ((chi (A,A)),(T . i))) c= {((vol A) / (i + 1))} by TARSKI:def_3; for x1 being set st x1 in {((vol A) / (i + 1))} holds x1 in rng (upper_volume ((chi (A,A)),(T . i))) proof reconsider D = T . i as Division of A ; let x1 be set ; ::_thesis: ( x1 in {((vol A) / (i + 1))} implies x1 in rng (upper_volume ((chi (A,A)),(T . i))) ) A24: vol (divset (D,1)) = (upper_bound (divset (D,1))) - (lower_bound (divset (D,1))) by INTEGRA1:def_5; A25: ex n being Element of NAT ex e being Division of A st ( n = i & e = D & e divide_into_equal n + 1 ) by A6; rng D <> {} ; then A26: 1 in dom D by FINSEQ_3:32; then upper_bound (divset (D,1)) = D . 1 by INTEGRA1:def_4; then upper_bound (divset (D,1)) = (lower_bound A) + (((vol A) / (len D)) * 1) by A26, A25, Def1; then A27: vol (divset (D,1)) = ((lower_bound A) + ((vol A) / (len D))) - (lower_bound A) by A26, A24, INTEGRA1:def_4 .= (vol A) / (len D) ; assume x1 in {((vol A) / (i + 1))} ; ::_thesis: x1 in rng (upper_volume ((chi (A,A)),(T . i))) then A28: x1 = (vol A) / (i + 1) by TARSKI:def_1; 1 in Seg (len D) by A26, FINSEQ_1:def_3; then 1 in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6; then 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3; then A29: (upper_volume ((chi (A,A)),D)) . 1 in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3; (upper_volume ((chi (A,A)),D)) . 1 = vol (divset (D,1)) by A26, INTEGRA1:20; hence x1 in rng (upper_volume ((chi (A,A)),(T . i))) by A28, A29, A25, A27, Def1; ::_thesis: verum end; then {((vol A) / (i + 1))} c= rng (upper_volume ((chi (A,A)),(T . i))) by TARSKI:def_3; then rng (upper_volume ((chi (A,A)),(T . i))) = {((vol A) / (i + 1))} by A23, XBOOLE_0:def_10; then (delta T) . i in {((vol A) / (i + 1))} by A8, XXREAL_2:def_8; hence (delta T) . i = (vol A) / (i + 1) by TARSKI:def_1; ::_thesis: verum end; A30: for a being Real st 0 < a holds ex i being Element of NAT st abs (((delta T) . i) - 0) < a proof let a be Real; ::_thesis: ( 0 < a implies ex i being Element of NAT st abs (((delta T) . i) - 0) < a ) A31: vol A >= 0 by INTEGRA1:9; reconsider i1 = [\((vol A) / a)/] + 1 as Integer ; assume A32: 0 < a ; ::_thesis: ex i being Element of NAT st abs (((delta T) . i) - 0) < a then [\((vol A) / a)/] + 1 > 0 by A31, INT_1:29; then reconsider i1 = i1 as Element of NAT by INT_1:3; i1 < i1 + 1 by NAT_1:13; then (vol A) / a < 1 * (i1 + 1) by INT_1:29, XXREAL_0:2; then A33: (vol A) / (i1 + 1) < 1 * a by A32, XREAL_1:113; A34: (delta T) . i1 = (vol A) / (i1 + 1) by A7; ((vol A) / (i1 + 1)) - 0 = abs (((vol A) / (i1 + 1)) - 0) by A31, ABSVALUE:def_1; hence ex i being Element of NAT st abs (((delta T) . i) - 0) < a by A33, A34; ::_thesis: verum end; A35: for i being Element of NAT holds (delta T) . i >= 0 proof let i be Element of NAT ; ::_thesis: (delta T) . i >= 0 (delta T) . i = delta (T . i) by INTEGRA3:def_2; hence (delta T) . i >= 0 by INTEGRA3:9; ::_thesis: verum end; A36: for i, j being Element of NAT st i <= j holds (delta T) . i >= (delta T) . j proof let i, j be Element of NAT ; ::_thesis: ( i <= j implies (delta T) . i >= (delta T) . j ) assume i <= j ; ::_thesis: (delta T) . i >= (delta T) . j then A37: i + 1 <= j + 1 by XREAL_1:6; vol A >= 0 by INTEGRA1:9; then (vol A) / (i + 1) >= (vol A) / (j + 1) by A37, XREAL_1:118; then (delta T) . i >= (vol A) / (j + 1) by A7; hence (delta T) . i >= (delta T) . j by A7; ::_thesis: verum end; A38: for a being real number st 0 < a holds ex i being Element of NAT st for j being Element of NAT st i <= j holds abs (((delta T) . j) - 0) < a proof let a be real number ; ::_thesis: ( 0 < a implies ex i being Element of NAT st for j being Element of NAT st i <= j holds abs (((delta T) . j) - 0) < a ) assume A39: 0 < a ; ::_thesis: ex i being Element of NAT st for j being Element of NAT st i <= j holds abs (((delta T) . j) - 0) < a a is Real by XREAL_0:def_1; then consider i being Element of NAT such that A40: abs (((delta T) . i) - 0) < a by A30, A39; (delta T) . i >= 0 by A35; then A41: (delta T) . i < a by A40, ABSVALUE:def_1; for j being Element of NAT st i <= j holds abs (((delta T) . j) - 0) < a proof let j be Element of NAT ; ::_thesis: ( i <= j implies abs (((delta T) . j) - 0) < a ) assume i <= j ; ::_thesis: abs (((delta T) . j) - 0) < a then (delta T) . j <= (delta T) . i by A36; then A42: (delta T) . j < a by A41, XXREAL_0:2; (delta T) . j >= 0 by A35; hence abs (((delta T) . j) - 0) < a by A42, ABSVALUE:def_1; ::_thesis: verum end; hence ex i being Element of NAT st for j being Element of NAT st i <= j holds abs (((delta T) . j) - 0) < a ; ::_thesis: verum end; then A43: delta T is convergent by SEQ_2:def_6; then lim (delta T) = 0 by A38, SEQ_2:def_7; hence ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) by A43; ::_thesis: verum end; Lm5: for A being non empty closed_interval Subset of REAL st vol A = 0 holds ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( vol A = 0 implies ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) ) set T = the DivSequence of A; assume A1: vol A = 0 ; ::_thesis: ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) A2: for i being Nat holds (delta the DivSequence of A) . i = 0 proof let i be Nat; ::_thesis: (delta the DivSequence of A) . i = 0 reconsider ii = i as Element of NAT by ORDINAL1:def_12; reconsider D = the DivSequence of A . ii as Division of A ; A3: (delta the DivSequence of A) . i = delta D by INTEGRA3:def_2 .= max (rng (upper_volume ((chi (A,A)),D))) by INTEGRA3:def_1 ; A4: len D = 1 proof assume len D <> 1 ; ::_thesis: contradiction then not len D is trivial by NAT_2:def_1; then A5: len D >= 2 by NAT_2:29; then 1 <= len D by XXREAL_0:2; then A6: 1 in dom D by FINSEQ_3:25; then A7: D . 1 in A by INTEGRA1:6; then A8: lower_bound A <= D . 1 by INTEGRA2:1; A9: 2 in dom D by A5, FINSEQ_3:25; then D . 2 in A by INTEGRA1:6; then A10: D . 2 <= upper_bound A by INTEGRA2:1; A11: D . 1 <= upper_bound A by A7, INTEGRA2:1; A12: (upper_bound A) - (lower_bound A) = 0 by A1, INTEGRA1:def_5; D . 1 < D . 2 by A6, A9, SEQM_3:def_1; hence contradiction by A8, A11, A10, A12, XXREAL_0:1; ::_thesis: verum end; for x1 being set st x1 in {0} holds x1 in rng (upper_volume ((chi (A,A)),D)) proof let x1 be set ; ::_thesis: ( x1 in {0} implies x1 in rng (upper_volume ((chi (A,A)),D)) ) A13: 1 in Seg (len D) by A4, FINSEQ_1:3; then 1 in dom D by FINSEQ_1:def_3; then A14: (upper_volume ((chi (A,A)),D)) . 1 = vol (divset (D,1)) by INTEGRA1:20; 1 in Seg (len (upper_volume ((chi (A,A)),D))) by A13, INTEGRA1:def_6; then 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3; then A15: (upper_volume ((chi (A,A)),D)) . 1 in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3; A16: 1 in dom D by A13, FINSEQ_1:def_3; then upper_bound (divset (D,1)) = D . (len D) by A4, INTEGRA1:def_4; then A17: upper_bound (divset (D,1)) = upper_bound A by INTEGRA1:def_2; lower_bound (divset (D,1)) = lower_bound A by A16, INTEGRA1:def_4; then A18: vol (divset (D,1)) = (upper_bound A) - (lower_bound A) by A17, INTEGRA1:def_5 .= 0 by A1, INTEGRA1:def_5 ; assume x1 in {0} ; ::_thesis: x1 in rng (upper_volume ((chi (A,A)),D)) hence x1 in rng (upper_volume ((chi (A,A)),D)) by A15, A14, A18, TARSKI:def_1; ::_thesis: verum end; then A19: {0} c= rng (upper_volume ((chi (A,A)),D)) by TARSKI:def_3; for x1 being set st x1 in rng (upper_volume ((chi (A,A)),D)) holds x1 in {0} proof let x1 be set ; ::_thesis: ( x1 in rng (upper_volume ((chi (A,A)),D)) implies x1 in {0} ) assume A20: x1 in rng (upper_volume ((chi (A,A)),D)) ; ::_thesis: x1 in {0} then consider k being Element of NAT such that A21: k in dom (upper_volume ((chi (A,A)),D)) and A22: (upper_volume ((chi (A,A)),D)) . k = x1 by PARTFUN1:3; reconsider x1 = x1 as Real by A20; k in Seg (len (upper_volume ((chi (A,A)),D))) by A21, FINSEQ_1:def_3; then A23: k in Seg (len D) by INTEGRA1:def_6; then A24: k in dom D by FINSEQ_1:def_3; k in dom D by A23, FINSEQ_1:def_3; then A25: x1 = vol (divset (D,k)) by A22, INTEGRA1:20; then x1 >= 0 by INTEGRA1:9; then x1 = 0 by A1, A25, A24, INTEGRA1:8, INTEGRA2:38; hence x1 in {0} by TARSKI:def_1; ::_thesis: verum end; then rng (upper_volume ((chi (A,A)),D)) c= {0} by TARSKI:def_3; then rng (upper_volume ((chi (A,A)),D)) = {0} by A19, XBOOLE_0:def_10; then (delta the DivSequence of A) . i in {0} by A3, XXREAL_2:def_8; hence (delta the DivSequence of A) . i = 0 by TARSKI:def_1; ::_thesis: verum end; then A26: delta the DivSequence of A is constant by VALUED_0:def_18; (delta the DivSequence of A) . 1 = 0 by A2; then lim (delta the DivSequence of A) = 0 by A26, SEQ_4:25; hence ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) by A26; ::_thesis: verum end; theorem Th11: :: INTEGRA4:11 for A being non empty closed_interval Subset of REAL ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) now__::_thesis:_ex_T_being_DivSequence_of_A_st_ (_delta_T_is_convergent_&_lim_(delta_T)_=_0_) percases ( vol A <> 0 or vol A = 0 ) ; supposeA1: vol A <> 0 ; ::_thesis: ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) vol A >= 0 by INTEGRA1:9; hence ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) by A1, Lm4; ::_thesis: verum end; suppose vol A = 0 ; ::_thesis: ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) hence ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) by Lm5; ::_thesis: verum end; end; end; hence ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: verum end; theorem Th12: :: INTEGRA4:12 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded holds ( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded holds ( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) let f be Function of A,REAL; ::_thesis: ( f | A is bounded implies ( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) ) assume A1: f | A is bounded ; ::_thesis: ( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) A2: ( f is integrable implies for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) proof assume A3: f is integrable ; ::_thesis: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 proof A4: upper_integral f = lower_integral f by A3, INTEGRA1:def_16; let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) assume that A5: delta T is convergent and A6: lim (delta T) = 0 ; ::_thesis: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 A7: lim (lower_sum (f,T)) = lower_integral f by A1, A5, A6, Th8; lim (upper_sum (f,T)) = upper_integral f by A1, A5, A6, Th9; hence (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A7, A4; ::_thesis: verum end; hence for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ; ::_thesis: verum end; ( ( for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) implies f is integrable ) proof consider T being DivSequence of A such that A8: delta T is convergent and A9: lim (delta T) = 0 by Th11; assume for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ; ::_thesis: f is integrable then (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A8, A9; then (upper_integral f) - (lim (lower_sum (f,T))) = 0 by A1, A8, A9, Th9; then A10: (upper_integral f) - (lower_integral f) = 0 by A1, A8, A9, Th8; A11: f is lower_integrable by A1, Th10; f is upper_integrable by A1, Th10; hence f is integrable by A11, A10, INTEGRA1:def_16; ::_thesis: verum end; hence ( f is integrable iff for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) by A2; ::_thesis: verum end; theorem Th13: :: INTEGRA4:13 for C being non empty set for f being Function of C,REAL holds ( max+ f is total & max- f is total ) proof let C be non empty set ; ::_thesis: for f being Function of C,REAL holds ( max+ f is total & max- f is total ) let f be Function of C,REAL; ::_thesis: ( max+ f is total & max- f is total ) A1: dom f = C by FUNCT_2:def_1; then A2: dom (max- f) = C by RFUNCT_3:def_11; dom (max+ f) = C by A1, RFUNCT_3:def_10; hence ( max+ f is total & max- f is total ) by A2, PARTFUN1:def_2; ::_thesis: verum end; theorem Th14: :: INTEGRA4:14 for C being non empty set for X being set for f being PartFunc of C,REAL st f | X is bounded_above holds (max+ f) | X is bounded_above proof let C be non empty set ; ::_thesis: for X being set for f being PartFunc of C,REAL st f | X is bounded_above holds (max+ f) | X is bounded_above let X be set ; ::_thesis: for f being PartFunc of C,REAL st f | X is bounded_above holds (max+ f) | X is bounded_above let f be PartFunc of C,REAL; ::_thesis: ( f | X is bounded_above implies (max+ f) | X is bounded_above ) assume f | X is bounded_above ; ::_thesis: (max+ f) | X is bounded_above then consider b being real number such that A1: for c being set st c in X /\ (dom f) holds f . c <= b by RFUNCT_1:70; A2: dom (max+ f) = dom f by RFUNCT_3:def_10; ex r being Real st for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c <= r proof now__::_thesis:_ex_r_being_Real_st_ for_c_being_set_st_c_in_X_/\_(dom_(max+_f))_holds_ (max+_f)_._c_<=_r percases ( b < 0 or b >= 0 ) ; supposeA3: b < 0 ; ::_thesis: ex r being Real st for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c <= r for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c <= 0 proof let c be set ; ::_thesis: ( c in X /\ (dom (max+ f)) implies (max+ f) . c <= 0 ) assume c in X /\ (dom (max+ f)) ; ::_thesis: (max+ f) . c <= 0 then A4: c in X /\ (dom f) by RFUNCT_3:def_10; then f . c <= b by A1; then max ((f . c),0) = 0 by A3, XXREAL_0:def_10; then A5: max+ (f . c) = 0 by RFUNCT_3:def_1; c in dom f by A4, XBOOLE_0:def_4; hence (max+ f) . c <= 0 by A2, A5, RFUNCT_3:def_10; ::_thesis: verum end; hence ex r being Real st for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c <= r ; ::_thesis: verum end; supposeA6: b >= 0 ; ::_thesis: ex r being Real st for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c <= r for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c <= b proof let c be set ; ::_thesis: ( c in X /\ (dom (max+ f)) implies (max+ f) . c <= b ) assume c in X /\ (dom (max+ f)) ; ::_thesis: (max+ f) . c <= b then A7: c in X /\ (dom f) by RFUNCT_3:def_10; then f . c <= b by A1; then max ((f . c),0) <= b by A6, XXREAL_0:28; then A8: max+ (f . c) <= b by RFUNCT_3:def_1; c in dom f by A7, XBOOLE_0:def_4; hence (max+ f) . c <= b by A2, A8, RFUNCT_3:def_10; ::_thesis: verum end; then consider r being real number such that r = b and A9: for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c <= r ; r is Real by XREAL_0:def_1; hence ex r being Real st for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c <= r by A9; ::_thesis: verum end; end; end; hence ex r being Real st for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c <= r ; ::_thesis: verum end; hence (max+ f) | X is bounded_above by RFUNCT_1:70; ::_thesis: verum end; theorem Th15: :: INTEGRA4:15 for C being non empty set for X being set for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below proof let C be non empty set ; ::_thesis: for X being set for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below let X be set ; ::_thesis: for f being PartFunc of C,REAL holds (max+ f) | X is bounded_below let f be PartFunc of C,REAL; ::_thesis: (max+ f) | X is bounded_below for c being set st c in X /\ (dom (max+ f)) holds (max+ f) . c >= 0 by RFUNCT_3:37; hence (max+ f) | X is bounded_below by RFUNCT_1:71; ::_thesis: verum end; theorem Th16: :: INTEGRA4:16 for C being non empty set for X being set for f being PartFunc of C,REAL st f | X is bounded_below holds (max- f) | X is bounded_above proof let C be non empty set ; ::_thesis: for X being set for f being PartFunc of C,REAL st f | X is bounded_below holds (max- f) | X is bounded_above let X be set ; ::_thesis: for f being PartFunc of C,REAL st f | X is bounded_below holds (max- f) | X is bounded_above let f be PartFunc of C,REAL; ::_thesis: ( f | X is bounded_below implies (max- f) | X is bounded_above ) assume f | X is bounded_below ; ::_thesis: (max- f) | X is bounded_above then consider b being real number such that A1: for c being set st c in X /\ (dom f) holds f . c >= b by RFUNCT_1:71; A2: dom (max- f) = dom f by RFUNCT_3:def_11; ex r being Real st for c being set st c in X /\ (dom (max- f)) holds (max- f) . c <= r proof now__::_thesis:_ex_r_being_Real_st_ for_c_being_set_st_c_in_X_/\_(dom_(max-_f))_holds_ (max-_f)_._c_<=_r percases ( b > 0 or b <= 0 ) ; supposeA3: b > 0 ; ::_thesis: ex r being Real st for c being set st c in X /\ (dom (max- f)) holds (max- f) . c <= r for c being set st c in X /\ (dom (max- f)) holds (max- f) . c <= 0 proof let c be set ; ::_thesis: ( c in X /\ (dom (max- f)) implies (max- f) . c <= 0 ) assume c in X /\ (dom (max- f)) ; ::_thesis: (max- f) . c <= 0 then A4: c in X /\ (dom f) by RFUNCT_3:def_11; then f . c >= b by A1; then max ((- (f . c)),0) = 0 by A3, XXREAL_0:def_10; then A5: max- (f . c) = 0 by RFUNCT_3:def_2; c in dom f by A4, XBOOLE_0:def_4; hence (max- f) . c <= 0 by A2, A5, RFUNCT_3:def_11; ::_thesis: verum end; hence ex r being Real st for c being set st c in X /\ (dom (max- f)) holds (max- f) . c <= r ; ::_thesis: verum end; supposeA6: b <= 0 ; ::_thesis: ex r being Real st for c being set st c in X /\ (dom (max- f)) holds (max- f) . c <= r for c being set st c in X /\ (dom (max- f)) holds (max- f) . c <= - b proof let c be set ; ::_thesis: ( c in X /\ (dom (max- f)) implies (max- f) . c <= - b ) assume c in X /\ (dom (max- f)) ; ::_thesis: (max- f) . c <= - b then A7: c in X /\ (dom f) by RFUNCT_3:def_11; then f . c >= b by A1; then - (f . c) <= - b by XREAL_1:24; then max ((- (f . c)),0) <= - b by A6, XXREAL_0:28; then A8: max- (f . c) <= - b by RFUNCT_3:def_2; c in dom f by A7, XBOOLE_0:def_4; hence (max- f) . c <= - b by A2, A8, RFUNCT_3:def_11; ::_thesis: verum end; then consider r being real number such that r = - b and A9: for c being set st c in X /\ (dom (max- f)) holds (max- f) . c <= r ; r is Real by XREAL_0:def_1; hence ex r being Real st for c being set st c in X /\ (dom (max- f)) holds (max- f) . c <= r by A9; ::_thesis: verum end; end; end; hence ex r being Real st for c being set st c in X /\ (dom (max- f)) holds (max- f) . c <= r ; ::_thesis: verum end; hence (max- f) | X is bounded_above by RFUNCT_1:70; ::_thesis: verum end; theorem Th17: :: INTEGRA4:17 for C being non empty set for X being set for f being PartFunc of C,REAL holds (max- f) | X is bounded_below proof let C be non empty set ; ::_thesis: for X being set for f being PartFunc of C,REAL holds (max- f) | X is bounded_below let X be set ; ::_thesis: for f being PartFunc of C,REAL holds (max- f) | X is bounded_below let f be PartFunc of C,REAL; ::_thesis: (max- f) | X is bounded_below for c being set st c in X /\ (dom (max- f)) holds (max- f) . c >= 0 by RFUNCT_3:40; hence (max- f) | X is bounded_below by RFUNCT_1:71; ::_thesis: verum end; theorem Th18: :: INTEGRA4:18 for A being non empty closed_interval Subset of REAL for X being set for f being PartFunc of A,REAL st f | A is bounded_above holds rng (f | X) is bounded_above proof let A be non empty closed_interval Subset of REAL; ::_thesis: for X being set for f being PartFunc of A,REAL st f | A is bounded_above holds rng (f | X) is bounded_above let X be set ; ::_thesis: for f being PartFunc of A,REAL st f | A is bounded_above holds rng (f | X) is bounded_above let f be PartFunc of A,REAL; ::_thesis: ( f | A is bounded_above implies rng (f | X) is bounded_above ) assume f | A is bounded_above ; ::_thesis: rng (f | X) is bounded_above then rng f is bounded_above by INTEGRA1:13; hence rng (f | X) is bounded_above by RELAT_1:70, XXREAL_2:43; ::_thesis: verum end; theorem Th19: :: INTEGRA4:19 for A being non empty closed_interval Subset of REAL for X being set for f being PartFunc of A,REAL st f | A is bounded_below holds rng (f | X) is bounded_below proof let A be non empty closed_interval Subset of REAL; ::_thesis: for X being set for f being PartFunc of A,REAL st f | A is bounded_below holds rng (f | X) is bounded_below let X be set ; ::_thesis: for f being PartFunc of A,REAL st f | A is bounded_below holds rng (f | X) is bounded_below let f be PartFunc of A,REAL; ::_thesis: ( f | A is bounded_below implies rng (f | X) is bounded_below ) assume f | A is bounded_below ; ::_thesis: rng (f | X) is bounded_below then rng f is bounded_below by INTEGRA1:11; hence rng (f | X) is bounded_below by RELAT_1:70, XXREAL_2:44; ::_thesis: verum end; theorem Th20: :: INTEGRA4:20 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded & f is integrable holds max+ f is integrable proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds max+ f is integrable let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies max+ f is integrable ) assume that A1: f | A is bounded and A2: f is integrable ; ::_thesis: max+ f is integrable A3: max+ f is total by Th13; A4: (max+ f) | A is bounded_below by Th15; A5: (max+ f) | A is bounded_above by A1, Th14; for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0 proof let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0 ) assume that A6: delta T is convergent and A7: lim (delta T) = 0 ; ::_thesis: (lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0 A8: lower_sum (f,T) is convergent by A1, A6, A7, Th8; A9: upper_sum (f,T) is convergent by A1, A6, A7, Th9; then A10: (upper_sum (f,T)) - (lower_sum (f,T)) is convergent by A8; reconsider osc1 = (upper_sum ((max+ f),T)) - (lower_sum ((max+ f),T)) as Real_Sequence ; reconsider osc = (upper_sum (f,T)) - (lower_sum (f,T)) as Real_Sequence ; (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A1, A2, A6, A7, Th12; then A11: lim ((upper_sum (f,T)) - (lower_sum (f,T))) = 0 by A9, A8, SEQ_2:12; A12: for a being real number st 0 < a holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < a proof let a be real number ; ::_thesis: ( 0 < a implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < a ) assume 0 < a ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < a then consider n being Element of NAT such that A13: for m being Element of NAT st n <= m holds abs ((osc . m) - 0) < a by A10, A11, SEQ_2:def_7; for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < a proof let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((osc1 . m) - 0) < a ) reconsider D = T . m as Division of A ; len (upper_volume (f,D)) = len D by INTEGRA1:def_6; then reconsider UV = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; len (lower_volume (f,D)) = len D by INTEGRA1:def_7; then reconsider LV = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; len (upper_volume ((max+ f),D)) = len D by INTEGRA1:def_6; then reconsider UV1 = upper_volume ((max+ f),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; len (lower_volume ((max+ f),D)) = len D by INTEGRA1:def_7; then reconsider LV1 = lower_volume ((max+ f),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; reconsider F = UV1 - LV1 as FinSequence of REAL ; osc1 . m = ((upper_sum ((max+ f),T)) . m) + ((- (lower_sum ((max+ f),T))) . m) by SEQ_1:7 .= ((upper_sum ((max+ f),T)) . m) + (- ((lower_sum ((max+ f),T)) . m)) by SEQ_1:10 .= ((upper_sum ((max+ f),T)) . m) - ((lower_sum ((max+ f),T)) . m) .= (upper_sum ((max+ f),(T . m))) - ((lower_sum ((max+ f),T)) . m) by INTEGRA2:def_2 .= (upper_sum ((max+ f),(T . m))) - (lower_sum ((max+ f),(T . m))) by INTEGRA2:def_3 .= (Sum (upper_volume ((max+ f),D))) - (lower_sum ((max+ f),(T . m))) by INTEGRA1:def_8 .= (Sum (upper_volume ((max+ f),D))) - (Sum (lower_volume ((max+ f),D))) by INTEGRA1:def_9 ; then A14: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:90; A15: for j being Nat st j in Seg (len D) holds (UV1 - LV1) . j <= (UV - LV) . j proof let j be Nat; ::_thesis: ( j in Seg (len D) implies (UV1 - LV1) . j <= (UV - LV) . j ) set x = (UV1 - LV1) . j; set y = (UV - LV) . j; assume A16: j in Seg (len D) ; ::_thesis: (UV1 - LV1) . j <= (UV - LV) . j then A17: j in dom D by FINSEQ_1:def_3; then A18: LV1 . j = (lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7; A19: ( rng (f | (divset (D,j))) is real-bounded & ex r being Real st r in rng (f | (divset (D,j))) ) proof A20: rng f is bounded_below by A1, INTEGRA1:11; rng f is bounded_above by A1, INTEGRA1:13; hence rng (f | (divset (D,j))) is real-bounded by A20, RELAT_1:70, XXREAL_2:45; ::_thesis: ex r being Real st r in rng (f | (divset (D,j))) consider r being Real such that A21: r in divset (D,j) by SUBSET_1:4; j in dom D by A16, FINSEQ_1:def_3; then divset (D,j) c= A by INTEGRA1:8; then r in A by A21; then r in dom f by FUNCT_2:def_1; then f . r in rng (f | (divset (D,j))) by A21, FUNCT_1:50; hence ex r being Real st r in rng (f | (divset (D,j))) ; ::_thesis: verum end; A22: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) proof set m1 = lower_bound (rng ((max+ f) | (divset (D,j)))); set M1 = upper_bound (rng ((max+ f) | (divset (D,j)))); set m = lower_bound (rng (f | (divset (D,j)))); set M = upper_bound (rng (f | (divset (D,j)))); A23: dom f = dom (max+ f) by RFUNCT_3:def_10; A24: j in dom D by A16, FINSEQ_1:def_3; A25: rng (f | (divset (D,j))) is bounded_above by A1, Th18; dom (f | (divset (D,j))) = (dom f) /\ (divset (D,j)) by RELAT_1:61; then dom (f | (divset (D,j))) = A /\ (divset (D,j)) by FUNCT_2:def_1; then dom (f | (divset (D,j))) <> {} by A24, INTEGRA1:8, XBOOLE_1:28; then A26: rng (f | (divset (D,j))) <> {} by RELAT_1:42; dom f = A by FUNCT_2:def_1; then dom ((max+ f) | (divset (D,j))) = A /\ (divset (D,j)) by A23, RELAT_1:61; then dom ((max+ f) | (divset (D,j))) <> {} by A24, INTEGRA1:8, XBOOLE_1:28; then A27: rng ((max+ f) | (divset (D,j))) <> {} by RELAT_1:42; (max+ f) | A is bounded_below by Th15; then A28: rng ((max+ f) | (divset (D,j))) is bounded_below by Th19; A29: rng (f | (divset (D,j))) is bounded_below by A1, Th19; (max+ f) | A is bounded_above by A1, Th14; then A30: rng ((max+ f) | (divset (D,j))) is bounded_above by Th18; now__::_thesis:_(upper_bound_(rng_(f_|_(divset_(D,j)))))_-_(lower_bound_(rng_(f_|_(divset_(D,j)))))_>=_(upper_bound_(rng_((max+_f)_|_(divset_(D,j)))))_-_(lower_bound_(rng_((max+_f)_|_(divset_(D,j))))) percases ( ( upper_bound (rng (f | (divset (D,j)))) > 0 & lower_bound (rng (f | (divset (D,j)))) >= 0 ) or ( upper_bound (rng (f | (divset (D,j)))) > 0 & lower_bound (rng (f | (divset (D,j)))) <= 0 ) or ( upper_bound (rng (f | (divset (D,j)))) <= 0 & lower_bound (rng (f | (divset (D,j)))) <= 0 ) ) by A19, SEQ_4:11; supposeA31: ( upper_bound (rng (f | (divset (D,j)))) > 0 & lower_bound (rng (f | (divset (D,j)))) >= 0 ) ; ::_thesis: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) A32: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds r <= upper_bound (rng (f | (divset (D,j)))) proof let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies r <= upper_bound (rng (f | (divset (D,j)))) ) assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j)))) then consider x being Element of A such that A33: x in dom ((max+ f) | (divset (D,j))) and A34: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3; A35: r = (max+ (f | (divset (D,j)))) . x by A34, RFUNCT_3:44; A36: x in dom (max+ (f | (divset (D,j)))) by A33, RFUNCT_3:44; then A37: x in dom (f | (divset (D,j))) by RFUNCT_3:def_10; now__::_thesis:_r_<=_upper_bound_(rng_(f_|_(divset_(D,j)))) percases ( r = 0 or r > 0 ) by A35, RFUNCT_3:37; suppose r = 0 ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j)))) hence r <= upper_bound (rng (f | (divset (D,j)))) by A31; ::_thesis: verum end; supposeA38: r > 0 ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j)))) r = max+ ((f | (divset (D,j))) . x) by A35, A36, RFUNCT_3:def_10; then r = max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1; then r = (f | (divset (D,j))) . x by A38, XXREAL_0:def_10; then r in rng (f | (divset (D,j))) by A37, FUNCT_1:def_3; hence r <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def_1; ::_thesis: verum end; end; end; hence r <= upper_bound (rng (f | (divset (D,j)))) ; ::_thesis: verum end; A39: for s being real number st 0 < s holds ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < (lower_bound (rng (f | (divset (D,j))))) + s ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < (lower_bound (rng (f | (divset (D,j))))) + s ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < (lower_bound (rng (f | (divset (D,j))))) + s ) then consider r being real number such that A40: r in rng (f | (divset (D,j))) and A41: r < (lower_bound (rng (f | (divset (D,j))))) + s by A26, A29, SEQ_4:def_2; reconsider r = r as Real by XREAL_0:def_1; r in rng ((max+ f) | (divset (D,j))) proof A42: r >= lower_bound (rng (f | (divset (D,j)))) by A29, A40, SEQ_4:def_2; consider x being Element of A such that A43: x in dom (f | (divset (D,j))) and A44: r = (f | (divset (D,j))) . x by A40, PARTFUN1:3; A45: x in dom (max+ (f | (divset (D,j)))) by A43, RFUNCT_3:def_10; then (max+ (f | (divset (D,j)))) . x = max+ r by A44, RFUNCT_3:def_10 .= max (r,0) by RFUNCT_3:def_1 .= r by A31, A42, XXREAL_0:def_10 ; then r in rng (max+ (f | (divset (D,j)))) by A45, FUNCT_1:def_3; hence r in rng ((max+ f) | (divset (D,j))) by RFUNCT_3:44; ::_thesis: verum end; hence ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < (lower_bound (rng (f | (divset (D,j))))) + s ) by A41; ::_thesis: verum end; A46: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds lower_bound (rng (f | (divset (D,j)))) <= r proof let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies lower_bound (rng (f | (divset (D,j)))) <= r ) assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: lower_bound (rng (f | (divset (D,j)))) <= r then consider x being Element of A such that A47: x in dom ((max+ f) | (divset (D,j))) and A48: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3; A49: x in dom (max+ (f | (divset (D,j)))) by A47, RFUNCT_3:44; x in dom (max+ (f | (divset (D,j)))) by A47, RFUNCT_3:44; then x in dom (f | (divset (D,j))) by RFUNCT_3:def_10; then (f | (divset (D,j))) . x in rng (f | (divset (D,j))) by FUNCT_1:def_3; then A50: (f | (divset (D,j))) . x >= lower_bound (rng (f | (divset (D,j)))) by A29, SEQ_4:def_2; r = (max+ (f | (divset (D,j)))) . x by A48, RFUNCT_3:44 .= max+ ((f | (divset (D,j))) . x) by A49, RFUNCT_3:def_10 .= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1 ; hence lower_bound (rng (f | (divset (D,j)))) <= r by A31, A50, XXREAL_0:def_10; ::_thesis: verum end; for s being real number st 0 < s holds ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r ) then consider r being real number such that A51: r in rng (f | (divset (D,j))) and A52: (upper_bound (rng (f | (divset (D,j))))) - s < r by A26, A25, SEQ_4:def_1; r in rng ((max+ f) | (divset (D,j))) proof reconsider r1 = r as Real by XREAL_0:def_1; consider x being Element of A such that A53: x in dom (f | (divset (D,j))) and A54: r = (f | (divset (D,j))) . x by A51, PARTFUN1:3; A55: r >= lower_bound (rng (f | (divset (D,j)))) by A29, A51, SEQ_4:def_2; A56: x in dom (max+ (f | (divset (D,j)))) by A53, RFUNCT_3:def_10; then (max+ (f | (divset (D,j)))) . x = max+ r1 by A54, RFUNCT_3:def_10 .= max (r,0) by RFUNCT_3:def_1 .= r by A31, A55, XXREAL_0:def_10 ; then r in rng (max+ (f | (divset (D,j)))) by A56, FUNCT_1:def_3; hence r in rng ((max+ f) | (divset (D,j))) by RFUNCT_3:44; ::_thesis: verum end; hence ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r ) by A52; ::_thesis: verum end; then upper_bound (rng ((max+ f) | (divset (D,j)))) = upper_bound (rng (f | (divset (D,j)))) by A27, A30, A32, SEQ_4:def_1; hence (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) by A27, A28, A46, A39, SEQ_4:def_2; ::_thesis: verum end; supposeA57: ( upper_bound (rng (f | (divset (D,j)))) > 0 & lower_bound (rng (f | (divset (D,j)))) <= 0 ) ; ::_thesis: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) A58: for s being real number st 0 < s holds ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) ) assume A59: s > 0 ; ::_thesis: ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) then consider r being real number such that A60: r in rng (f | (divset (D,j))) and A61: r < (lower_bound (rng (f | (divset (D,j))))) + s by A26, A29, SEQ_4:def_2; consider x being Element of A such that A62: x in dom (f | (divset (D,j))) and A63: r = (f | (divset (D,j))) . x by A60, PARTFUN1:3; A64: x in dom (max+ (f | (divset (D,j)))) by A62, RFUNCT_3:def_10; then A65: (max+ (f | (divset (D,j)))) . x = max+ ((f | (divset (D,j))) . x) by RFUNCT_3:def_10 .= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1 ; (max+ (f | (divset (D,j)))) . x in rng (max+ (f | (divset (D,j)))) by A64, FUNCT_1:def_3; then A66: (max+ (f | (divset (D,j)))) . x in rng ((max+ f) | (divset (D,j))) by RFUNCT_3:44; A67: r - s < lower_bound (rng (f | (divset (D,j)))) by A61, XREAL_1:19; now__::_thesis:_ex_r_being_Real_st_ (_r_in_rng_((max+_f)_|_(divset_(D,j)))_&_r_<_0_+_s_) percases ( r < 0 or r >= 0 ) ; suppose r < 0 ; ::_thesis: ex r being Real st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) then 0 in rng ((max+ f) | (divset (D,j))) by A63, A66, A65, XXREAL_0:def_10; hence ex r being Real st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) by A59; ::_thesis: verum end; supposeA68: r >= 0 ; ::_thesis: ex r being Real st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) A69: r < 0 + s by A57, A67, XREAL_1:19; r in rng ((max+ f) | (divset (D,j))) by A63, A66, A65, A68, XXREAL_0:def_10; hence ex r being Real st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) by A69; ::_thesis: verum end; end; end; hence ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) ; ::_thesis: verum end; for r being real number st r in rng ((max+ f) | (divset (D,j))) holds 0 <= r proof let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies 0 <= r ) assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: 0 <= r then r in rng (max+ (f | (divset (D,j)))) by RFUNCT_3:44; then ex x being Element of A st ( x in dom (max+ (f | (divset (D,j)))) & r = (max+ (f | (divset (D,j)))) . x ) by PARTFUN1:3; hence 0 <= r by RFUNCT_3:37; ::_thesis: verum end; then A70: lower_bound (rng ((max+ f) | (divset (D,j)))) = 0 by A27, A28, A58, SEQ_4:def_2; for r being Real st r in rng ((max+ f) | (divset (D,j))) holds r <= upper_bound (rng (f | (divset (D,j)))) proof let r be Real; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies r <= upper_bound (rng (f | (divset (D,j)))) ) assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j)))) then consider x being Element of A such that A71: x in dom ((max+ f) | (divset (D,j))) and A72: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3; A73: r = (max+ (f | (divset (D,j)))) . x by A72, RFUNCT_3:44; A74: x in dom (max+ (f | (divset (D,j)))) by A71, RFUNCT_3:44; then A75: x in dom (f | (divset (D,j))) by RFUNCT_3:def_10; now__::_thesis:_r_<=_upper_bound_(rng_(f_|_(divset_(D,j)))) percases ( r = 0 or r > 0 ) by A73, RFUNCT_3:37; suppose r = 0 ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j)))) hence r <= upper_bound (rng (f | (divset (D,j)))) by A57; ::_thesis: verum end; supposeA76: r > 0 ; ::_thesis: r <= upper_bound (rng (f | (divset (D,j)))) r = max+ ((f | (divset (D,j))) . x) by A73, A74, RFUNCT_3:def_10; then r = max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1; then r = (f | (divset (D,j))) . x by A76, XXREAL_0:def_10; then r in rng (f | (divset (D,j))) by A75, FUNCT_1:def_3; hence r <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def_1; ::_thesis: verum end; end; end; hence r <= upper_bound (rng (f | (divset (D,j)))) ; ::_thesis: verum end; then A77: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds r <= upper_bound (rng (f | (divset (D,j)))) ; for s being real number st 0 < s holds ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r ) proof assume ex s being real number st ( 0 < s & ( for r being real number holds ( not r in rng ((max+ f) | (divset (D,j))) or not (upper_bound (rng (f | (divset (D,j))))) - s < r ) ) ) ; ::_thesis: contradiction then consider s being real number such that A78: s > 0 and A79: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds (upper_bound (rng (f | (divset (D,j))))) - s >= r ; consider r1 being real number such that A80: r1 in rng (f | (divset (D,j))) and A81: (upper_bound (rng (f | (divset (D,j))))) - s < r1 by A26, A25, A78, SEQ_4:def_1; consider x being Element of A such that A82: x in dom (f | (divset (D,j))) and A83: r1 = (f | (divset (D,j))) . x by A80, PARTFUN1:3; A84: x in dom (max+ (f | (divset (D,j)))) by A82, RFUNCT_3:def_10; then x in dom ((max+ f) | (divset (D,j))) by RFUNCT_3:44; then A85: ((max+ f) | (divset (D,j))) . x in rng ((max+ f) | (divset (D,j))) by FUNCT_1:def_3; (max+ (f | (divset (D,j)))) . x >= 0 by RFUNCT_3:37; then ((max+ f) | (divset (D,j))) . x >= 0 by RFUNCT_3:44; then A86: (upper_bound (rng (f | (divset (D,j))))) - s >= 0 by A79, A85; ((max+ f) | (divset (D,j))) . x = (max+ (f | (divset (D,j)))) . x by RFUNCT_3:44 .= max+ ((f | (divset (D,j))) . x) by A84, RFUNCT_3:def_10 .= max (r1,0) by A83, RFUNCT_3:def_1 .= r1 by A81, A86, XXREAL_0:def_10 ; hence contradiction by A79, A81, A85; ::_thesis: verum end; then upper_bound (rng ((max+ f) | (divset (D,j)))) = upper_bound (rng (f | (divset (D,j)))) by A27, A30, A77, SEQ_4:def_1; hence (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) by A57, A70, XREAL_1:13; ::_thesis: verum end; supposeA87: ( upper_bound (rng (f | (divset (D,j)))) <= 0 & lower_bound (rng (f | (divset (D,j)))) <= 0 ) ; ::_thesis: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) A88: for s being real number st 0 < s holds ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) ) assume A89: s > 0 ; ::_thesis: ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) consider r being Real such that A90: r in rng ((max+ f) | (divset (D,j))) by A27, SUBSET_1:4; consider x being Element of A such that A91: x in dom ((max+ f) | (divset (D,j))) and A92: r = ((max+ f) | (divset (D,j))) . x by A90, PARTFUN1:3; A93: x in dom (max+ (f | (divset (D,j)))) by A91, RFUNCT_3:44; then x in dom (f | (divset (D,j))) by RFUNCT_3:def_10; then (f | (divset (D,j))) . x in rng (f | (divset (D,j))) by FUNCT_1:def_3; then A94: (f | (divset (D,j))) . x <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def_1; r = (max+ (f | (divset (D,j)))) . x by A92, RFUNCT_3:44; then r = max+ ((f | (divset (D,j))) . x) by A93, RFUNCT_3:def_10 .= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1 ; then r = 0 by A87, A94, XXREAL_0:def_10; hence ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) by A89, A90; ::_thesis: verum end; for r being real number st r in rng ((max+ f) | (divset (D,j))) holds 0 <= r proof let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies 0 <= r ) assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: 0 <= r then consider x being Element of A such that x in dom ((max+ f) | (divset (D,j))) and A95: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3; r = (max+ (f | (divset (D,j)))) . x by A95, RFUNCT_3:44; hence 0 <= r by RFUNCT_3:37; ::_thesis: verum end; then A96: lower_bound (rng ((max+ f) | (divset (D,j)))) = 0 by A27, A28, A88, SEQ_4:def_2; A97: for r being real number st r in rng ((max+ f) | (divset (D,j))) holds r <= 0 proof let r be real number ; ::_thesis: ( r in rng ((max+ f) | (divset (D,j))) implies r <= 0 ) assume r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: r <= 0 then consider x being Element of A such that A98: x in dom ((max+ f) | (divset (D,j))) and A99: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3; A100: x in dom (max+ (f | (divset (D,j)))) by A98, RFUNCT_3:44; then x in dom (f | (divset (D,j))) by RFUNCT_3:def_10; then (f | (divset (D,j))) . x in rng (f | (divset (D,j))) by FUNCT_1:def_3; then A101: (f | (divset (D,j))) . x <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def_1; r = (max+ (f | (divset (D,j)))) . x by A99, RFUNCT_3:44; then r = max+ ((f | (divset (D,j))) . x) by A100, RFUNCT_3:def_10 .= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def_1 .= 0 by A87, A101, XXREAL_0:def_10 ; hence r <= 0 ; ::_thesis: verum end; for s being real number st 0 < s holds ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r ) ) assume A102: s > 0 ; ::_thesis: ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r ) consider r being Real such that A103: r in rng ((max+ f) | (divset (D,j))) by A27, SUBSET_1:4; consider x being Element of A such that x in dom ((max+ f) | (divset (D,j))) and A104: r = ((max+ f) | (divset (D,j))) . x by A103, PARTFUN1:3; r = (max+ (f | (divset (D,j)))) . x by A104, RFUNCT_3:44; then r >= 0 by RFUNCT_3:37; hence ex r being real number st ( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r ) by A102, A103; ::_thesis: verum end; then upper_bound (rng ((max+ f) | (divset (D,j)))) = 0 by A27, A30, A97, SEQ_4:def_1; hence (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) by A19, A96, SEQ_4:11, XREAL_1:48; ::_thesis: verum end; end; end; hence (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) ; ::_thesis: verum end; A105: LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A17, INTEGRA1:def_7; UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A17, INTEGRA1:def_6; then A106: (UV - LV) . j = ((upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) by A105, RVSUM_1:27 .= ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) * (vol (divset (D,j))) ; UV1 . j = (upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by A17, INTEGRA1:def_6; then A107: (UV1 - LV1) . j = ((upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j)))) by A18, RVSUM_1:27 .= ((upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))) * (vol (divset (D,j))) ; vol (divset (D,j)) >= 0 by INTEGRA1:9; hence (UV1 - LV1) . j <= (UV - LV) . j by A107, A106, A22, XREAL_1:64; ::_thesis: verum end; assume n <= m ; ::_thesis: abs ((osc1 . m) - 0) < a then A108: abs ((osc . m) - 0) < a by A13; for j being Nat st j in dom F holds 0 <= F . j proof let j be Nat; ::_thesis: ( j in dom F implies 0 <= F . j ) set r = F . j; (max+ f) | A is bounded_below by Th15; then A109: rng (max+ f) is bounded_below by INTEGRA1:11; assume A110: j in dom F ; ::_thesis: 0 <= F . j j in Seg (len F) by A110, FINSEQ_1:def_3; then A111: j in Seg (len D) by CARD_1:def_7; then A112: j in dom D by FINSEQ_1:def_3; then A113: LV1 . j = (lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7; A114: ex r being Real st r in rng ((max+ f) | (divset (D,j))) proof consider r being Real such that A115: r in divset (D,j) by SUBSET_1:4; j in dom D by A111, FINSEQ_1:def_3; then divset (D,j) c= A by INTEGRA1:8; then r in A by A115; then r in dom f by FUNCT_2:def_1; then r in (dom f) /\ (divset (D,j)) by A115, XBOOLE_0:def_4; then r in dom (f | (divset (D,j))) by RELAT_1:61; then r in dom (max+ (f | (divset (D,j)))) by RFUNCT_3:def_10; then r in dom ((max+ f) | (divset (D,j))) by RFUNCT_3:44; then ((max+ f) | (divset (D,j))) . r in rng ((max+ f) | (divset (D,j))) by FUNCT_1:def_3; hence ex r being Real st r in rng ((max+ f) | (divset (D,j))) ; ::_thesis: verum end; (max+ f) | A is bounded_above by A1, Th14; then rng (max+ f) is bounded_above by INTEGRA1:13; then rng ((max+ f) | (divset (D,j))) is real-bounded by A109, RELAT_1:70, XXREAL_2:45; then A116: (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) >= 0 by A114, SEQ_4:11, XREAL_1:48; UV1 . j = (upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by A112, INTEGRA1:def_6; then A117: F . j = ((upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j)))) by A110, A113, VALUED_1:13 .= ((upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))) * (vol (divset (D,j))) ; vol (divset (D,j)) >= 0 by INTEGRA1:9; hence 0 <= F . j by A117, A116; ::_thesis: verum end; then A118: osc1 . m >= 0 by A14, RVSUM_1:84; then A119: abs ((osc1 . m) - 0) = osc1 . m by ABSVALUE:def_1; osc . m = ((upper_sum (f,T)) . m) + ((- (lower_sum (f,T))) . m) by SEQ_1:7 .= ((upper_sum (f,T)) . m) + (- ((lower_sum (f,T)) . m)) by SEQ_1:10 .= ((upper_sum (f,T)) . m) - ((lower_sum (f,T)) . m) .= (upper_sum (f,(T . m))) - ((lower_sum (f,T)) . m) by INTEGRA2:def_2 .= (upper_sum (f,(T . m))) - (lower_sum (f,(T . m))) by INTEGRA2:def_3 .= (Sum (upper_volume (f,D))) - (lower_sum (f,(T . m))) by INTEGRA1:def_8 .= (Sum (upper_volume (f,D))) - (Sum (lower_volume (f,D))) by INTEGRA1:def_9 ; then osc . m = Sum (UV - LV) by RVSUM_1:90; then A120: osc1 . m <= osc . m by A14, A15, RVSUM_1:82; then abs (osc . m) = osc . m by A118, ABSVALUE:def_1; hence abs ((osc1 . m) - 0) < a by A108, A120, A119, XXREAL_0:2; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < a ; ::_thesis: verum end; then osc1 is convergent by SEQ_2:def_6; then A121: lim ((upper_sum ((max+ f),T)) - (lower_sum ((max+ f),T))) = 0 by A12, SEQ_2:def_7; A122: lower_sum ((max+ f),T) is convergent by A3, A5, A4, A6, A7, Th8; upper_sum ((max+ f),T) is convergent by A3, A5, A4, A6, A7, Th9; hence (lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0 by A122, A121, SEQ_2:12; ::_thesis: verum end; hence max+ f is integrable by A3, A5, A4, Th12; ::_thesis: verum end; theorem Th21: :: INTEGRA4:21 for C being non empty set for f being PartFunc of C,REAL holds max- f = max+ (- f) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL holds max- f = max+ (- f) let f be PartFunc of C,REAL; ::_thesis: max- f = max+ (- f) dom (max+ (- f)) = dom (- f) by RFUNCT_3:def_10; then A1: dom (max+ (- f)) = dom f by VALUED_1:8; A2: dom (max- f) = dom f by RFUNCT_3:def_11; for x1 being Element of C st x1 in dom f holds (max- f) . x1 = (max+ (- f)) . x1 proof let x1 be Element of C; ::_thesis: ( x1 in dom f implies (max- f) . x1 = (max+ (- f)) . x1 ) assume A3: x1 in dom f ; ::_thesis: (max- f) . x1 = (max+ (- f)) . x1 then A4: (max+ (- f)) . x1 = max+ ((- f) . x1) by A1, RFUNCT_3:def_10 .= max (((- f) . x1),0) by RFUNCT_3:def_1 .= max ((- (f . x1)),0) by VALUED_1:8 ; (max- f) . x1 = max- (f . x1) by A2, A3, RFUNCT_3:def_11 .= max ((- (f . x1)),0) by RFUNCT_3:def_2 ; hence (max- f) . x1 = (max+ (- f)) . x1 by A4; ::_thesis: verum end; hence max- f = max+ (- f) by A2, A1, PARTFUN1:5; ::_thesis: verum end; theorem Th22: :: INTEGRA4:22 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded & f is integrable holds max- f is integrable proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds max- f is integrable let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies max- f is integrable ) assume that A1: f | A is bounded and A2: f is integrable ; ::_thesis: max- f is integrable A3: (- f) | A is bounded by A1, RFUNCT_1:82; (- 1) (#) f is integrable by A1, A2, INTEGRA2:31; then max+ (- f) is integrable by A3, Th20; hence max- f is integrable by Th21; ::_thesis: verum end; theorem :: INTEGRA4:23 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded & f is integrable holds ( abs f is integrable & abs (integral f) <= integral (abs f) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds ( abs f is integrable & abs (integral f) <= integral (abs f) ) let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies ( abs f is integrable & abs (integral f) <= integral (abs f) ) ) assume that A1: f | A is bounded and A2: f is integrable ; ::_thesis: ( abs f is integrable & abs (integral f) <= integral (abs f) ) A3: max- f is integrable by A1, A2, Th22; A4: (max+ f) | A is bounded_above by A1, Th14; A5: (max- f) | A is bounded_above by A1, Th16; A6: max+ f is total by Th13; A7: (max- f) | A is bounded_below by Th17; A8: (max+ f) | A is bounded_below by Th15; A9: max- f is total by Th13; A10: max+ f is integrable by A1, A2, Th20; then (max+ f) + (max- f) is integrable by A6, A9, A4, A8, A5, A7, A3, INTEGRA1:57; hence abs f is integrable by RFUNCT_3:34; ::_thesis: abs (integral f) <= integral (abs f) A11: (integral (max+ f)) - (integral (max- f)) = integral ((max+ f) - (max- f)) by A6, A9, A4, A8, A5, A7, A10, A3, INTEGRA2:33 .= integral f by RFUNCT_3:34 ; A12: (integral (max+ f)) + (integral (max- f)) = integral ((max+ f) + (max- f)) by A6, A9, A4, A8, A5, A7, A10, A3, INTEGRA1:57 .= integral (abs f) by RFUNCT_3:34 ; then A13: (integral (abs f)) - (integral f) = 2 * (integral (max- f)) by A11; for x being Real st x in A holds (max- f) . x >= 0 by RFUNCT_3:40; then integral (max- f) >= 0 by A9, A5, A7, INTEGRA2:32; then A14: integral (abs f) >= integral f by A13, XREAL_1:49; A15: (integral (abs f)) + (integral f) = 2 * (integral (max+ f)) by A12, A11; for x being Real st x in A holds (max+ f) . x >= 0 by RFUNCT_3:37; then integral (max+ f) >= 0 by A6, A4, A8, INTEGRA2:32; then - (integral (abs f)) <= integral f by A15, XREAL_1:61; hence abs (integral f) <= integral (abs f) by A14, ABSVALUE:5; ::_thesis: verum end; theorem Th24: :: INTEGRA4:24 for a being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds abs ((f . x) - (f . y)) <= a ) holds (upper_bound (rng f)) - (lower_bound (rng f)) <= a proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds abs ((f . x) - (f . y)) <= a ) holds (upper_bound (rng f)) - (lower_bound (rng f)) <= a let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds abs ((f . x) - (f . y)) <= a ) holds (upper_bound (rng f)) - (lower_bound (rng f)) <= a let f be Function of A,REAL; ::_thesis: ( ( for x, y being Real st x in A & y in A holds abs ((f . x) - (f . y)) <= a ) implies (upper_bound (rng f)) - (lower_bound (rng f)) <= a ) assume A1: for x, y being Real st x in A & y in A holds abs ((f . x) - (f . y)) <= a ; ::_thesis: (upper_bound (rng f)) - (lower_bound (rng f)) <= a A2: for y being real number st y in A holds (upper_bound (rng f)) - a <= f . y proof let y be real number ; ::_thesis: ( y in A implies (upper_bound (rng f)) - a <= f . y ) assume A3: y in A ; ::_thesis: (upper_bound (rng f)) - a <= f . y for b being real number st b in rng f holds b <= a + (f . y) proof let b be real number ; ::_thesis: ( b in rng f implies b <= a + (f . y) ) assume b in rng f ; ::_thesis: b <= a + (f . y) then consider x being Element of A such that x in dom f and A4: b = f . x by PARTFUN1:3; abs ((f . x) - (f . y)) <= a by A1, A3; then (f . x) - (f . y) <= a by ABSVALUE:5; hence b <= a + (f . y) by A4, XREAL_1:20; ::_thesis: verum end; then upper_bound (rng f) <= a + (f . y) by SEQ_4:45; hence (upper_bound (rng f)) - a <= f . y by XREAL_1:20; ::_thesis: verum end; for b being real number st b in rng f holds (upper_bound (rng f)) - a <= b proof let b be real number ; ::_thesis: ( b in rng f implies (upper_bound (rng f)) - a <= b ) assume b in rng f ; ::_thesis: (upper_bound (rng f)) - a <= b then ex x being Element of A st ( x in dom f & b = f . x ) by PARTFUN1:3; hence (upper_bound (rng f)) - a <= b by A2; ::_thesis: verum end; then (upper_bound (rng f)) - a <= lower_bound (rng f) by SEQ_4:43; then upper_bound (rng f) <= a + (lower_bound (rng f)) by XREAL_1:20; hence (upper_bound (rng f)) - (lower_bound (rng f)) <= a by XREAL_1:20; ::_thesis: verum end; theorem Th25: :: INTEGRA4:25 for a being Real for A being non empty closed_interval Subset of REAL for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) let f, g be Function of A,REAL; ::_thesis: ( f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) implies (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) ) assume that A1: f | A is bounded and A2: a >= 0 and A3: for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ; ::_thesis: (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) A4: rng f is bounded_above by A1, INTEGRA1:13; A5: dom f = A by FUNCT_2:def_1; A6: rng f is bounded_below by A1, INTEGRA1:11; A7: for x, y being Real st x in A & y in A holds abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) proof let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) ) assume that A8: x in A and A9: y in A ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) now__::_thesis:_abs_((f_._x)_-_(f_._y))_<=_(upper_bound_(rng_f))_-_(lower_bound_(rng_f)) percases ( f . x >= f . y or f . x < f . y ) ; suppose f . x >= f . y ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) then (f . x) - (f . y) >= 0 by XREAL_1:48; then abs ((f . x) - (f . y)) = (f . x) - (f . y) by ABSVALUE:def_1; then A10: (abs ((f . x) - (f . y))) + (f . y) = f . x ; f . y in rng f by A5, A9, FUNCT_1:def_3; then A11: lower_bound (rng f) <= f . y by A6, SEQ_4:def_2; f . x in rng f by A5, A8, FUNCT_1:def_3; then f . x <= upper_bound (rng f) by A4, SEQ_4:def_1; then f . y <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A10, XREAL_1:19; then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A11, XXREAL_0:2; then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:19; hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; ::_thesis: verum end; suppose f . x < f . y ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) then (f . x) - (f . y) < 0 by XREAL_1:49; then abs ((f . x) - (f . y)) = - ((f . x) - (f . y)) by ABSVALUE:def_1 .= (f . y) - (f . x) ; then A12: (abs ((f . x) - (f . y))) + (f . x) = f . y ; f . x in rng f by A5, A8, FUNCT_1:def_3; then A13: lower_bound (rng f) <= f . x by A6, SEQ_4:def_2; f . y in rng f by A5, A9, FUNCT_1:def_3; then f . y <= upper_bound (rng f) by A4, SEQ_4:def_1; then f . x <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A12, XREAL_1:19; then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A13, XXREAL_0:2; then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:19; hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; ::_thesis: verum end; end; end; hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) ; ::_thesis: verum end; for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) proof let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) ) assume that A14: x in A and A15: y in A ; ::_thesis: abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) A16: abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) by A3, A14, A15; a * (abs ((f . x) - (f . y))) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A2, A7, A14, A15, XREAL_1:64; hence abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A16, XXREAL_0:2; ::_thesis: verum end; hence (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by Th24; ::_thesis: verum end; theorem Th26: :: INTEGRA4:26 for a being Real for A being non empty closed_interval Subset of REAL for f, g, h being Function of A,REAL st f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, g, h being Function of A,REAL st f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g, h being Function of A,REAL st f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) let f, g, h be Function of A,REAL; ::_thesis: ( f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) implies (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) ) assume that A1: f | A is bounded and A2: g | A is bounded and A3: a >= 0 and A4: for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ; ::_thesis: (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) A5: rng g is bounded_above by A2, INTEGRA1:13; A6: rng f is bounded_above by A1, INTEGRA1:13; A7: dom g = A by FUNCT_2:def_1; A8: rng g is bounded_below by A2, INTEGRA1:11; A9: for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) proof let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) ) assume that A10: x in A and A11: y in A ; ::_thesis: abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) now__::_thesis:_abs_((g_._x)_-_(g_._y))_<=_(upper_bound_(rng_g))_-_(lower_bound_(rng_g)) percases ( g . x >= g . y or g . x < g . y ) ; suppose g . x >= g . y ; ::_thesis: abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) then (g . x) - (g . y) >= 0 by XREAL_1:48; then abs ((g . x) - (g . y)) = (g . x) - (g . y) by ABSVALUE:def_1; then A12: (abs ((g . x) - (g . y))) + (g . y) = g . x ; g . y in rng g by A7, A11, FUNCT_1:def_3; then A13: lower_bound (rng g) <= g . y by A8, SEQ_4:def_2; g . x in rng g by A7, A10, FUNCT_1:def_3; then g . x <= upper_bound (rng g) by A5, SEQ_4:def_1; then g . y <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A12, XREAL_1:19; then lower_bound (rng g) <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A13, XXREAL_0:2; then (lower_bound (rng g)) + (abs ((g . x) - (g . y))) <= upper_bound (rng g) by XREAL_1:19; hence abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) by XREAL_1:19; ::_thesis: verum end; suppose g . x < g . y ; ::_thesis: abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) then (g . x) - (g . y) < 0 by XREAL_1:49; then abs ((g . x) - (g . y)) = - ((g . x) - (g . y)) by ABSVALUE:def_1 .= (g . y) - (g . x) ; then A14: (abs ((g . x) - (g . y))) + (g . x) = g . y ; g . x in rng g by A7, A10, FUNCT_1:def_3; then A15: lower_bound (rng g) <= g . x by A8, SEQ_4:def_2; g . y in rng g by A7, A11, FUNCT_1:def_3; then g . y <= upper_bound (rng g) by A5, SEQ_4:def_1; then g . x <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A14, XREAL_1:19; then lower_bound (rng g) <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A15, XXREAL_0:2; then (lower_bound (rng g)) + (abs ((g . x) - (g . y))) <= upper_bound (rng g) by XREAL_1:19; hence abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) by XREAL_1:19; ::_thesis: verum end; end; end; hence abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) ; ::_thesis: verum end; A16: dom f = A by FUNCT_2:def_1; A17: rng f is bounded_below by A1, INTEGRA1:11; A18: for x, y being Real st x in A & y in A holds abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) proof let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) ) assume that A19: x in A and A20: y in A ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) now__::_thesis:_abs_((f_._x)_-_(f_._y))_<=_(upper_bound_(rng_f))_-_(lower_bound_(rng_f)) percases ( f . x >= f . y or f . x < f . y ) ; suppose f . x >= f . y ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) then (f . x) - (f . y) >= 0 by XREAL_1:48; then abs ((f . x) - (f . y)) = (f . x) - (f . y) by ABSVALUE:def_1; then A21: (abs ((f . x) - (f . y))) + (f . y) = f . x ; f . y in rng f by A16, A20, FUNCT_1:def_3; then A22: lower_bound (rng f) <= f . y by A17, SEQ_4:def_2; f . x in rng f by A16, A19, FUNCT_1:def_3; then f . x <= upper_bound (rng f) by A6, SEQ_4:def_1; then f . y <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A21, XREAL_1:19; then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A22, XXREAL_0:2; then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:19; hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; ::_thesis: verum end; suppose f . x < f . y ; ::_thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) then (f . x) - (f . y) < 0 by XREAL_1:49; then abs ((f . x) - (f . y)) = - ((f . x) - (f . y)) by ABSVALUE:def_1 .= (f . y) - (f . x) ; then A23: (abs ((f . x) - (f . y))) + (f . x) = f . y ; f . x in rng f by A16, A19, FUNCT_1:def_3; then A24: lower_bound (rng f) <= f . x by A17, SEQ_4:def_2; f . y in rng f by A16, A20, FUNCT_1:def_3; then f . y <= upper_bound (rng f) by A6, SEQ_4:def_1; then f . x <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A23, XREAL_1:19; then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A24, XXREAL_0:2; then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:19; hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; ::_thesis: verum end; end; end; hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) ; ::_thesis: verum end; for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) proof let x, y be Real; ::_thesis: ( x in A & y in A implies abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) ) assume that A25: x in A and A26: y in A ; ::_thesis: abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) A27: a * (abs ((g . x) - (g . y))) <= a * ((upper_bound (rng g)) - (lower_bound (rng g))) by A3, A9, A25, A26, XREAL_1:64; a * (abs ((f . x) - (f . y))) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A3, A18, A25, A26, XREAL_1:64; then A28: (a * (abs ((f . x) - (f . y)))) + (a * (abs ((g . x) - (g . y)))) <= (a * ((upper_bound (rng f)) - (lower_bound (rng f)))) + (a * ((upper_bound (rng g)) - (lower_bound (rng g)))) by A27, XREAL_1:7; abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) by A4, A25, A26; hence abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) by A28, XXREAL_0:2; ::_thesis: verum end; hence (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) by Th24; ::_thesis: verum end; theorem Th27: :: INTEGRA4:27 for a being Real for A being non empty closed_interval Subset of REAL for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds g is integrable proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds g is integrable let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds g is integrable let f, g be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) implies g is integrable ) assume that A1: f | A is bounded and A2: f is integrable and A3: g | A is bounded and A4: a > 0 and A5: for x, y being Real st x in A & y in A holds abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ; ::_thesis: g is integrable for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 proof let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 ) assume that A6: delta T is convergent and A7: lim (delta T) = 0 ; ::_thesis: (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 A8: lower_sum (f,T) is convergent by A1, A6, A7, Th8; A9: upper_sum (f,T) is convergent by A1, A6, A7, Th9; then A10: (upper_sum (f,T)) - (lower_sum (f,T)) is convergent by A8; reconsider osc1 = (upper_sum (g,T)) - (lower_sum (g,T)) as Real_Sequence ; reconsider osc = (upper_sum (f,T)) - (lower_sum (f,T)) as Real_Sequence ; (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A1, A2, A6, A7, Th12; then A11: lim ((upper_sum (f,T)) - (lower_sum (f,T))) = 0 by A9, A8, SEQ_2:12; A12: for b being real number st 0 < b holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < b proof let b be real number ; ::_thesis: ( 0 < b implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < b ) assume b > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < b then b / a > 0 by A4, XREAL_1:139; then consider n being Element of NAT such that A13: for m being Element of NAT st n <= m holds abs ((osc . m) - 0) < b / a by A10, A11, SEQ_2:def_7; for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < b proof let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((osc1 . m) - 0) < b ) reconsider D = T . m as Division of A ; len (upper_volume (f,D)) = len D by INTEGRA1:def_6; then reconsider UV = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; len (lower_volume (f,D)) = len D by INTEGRA1:def_7; then reconsider LV = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; osc . m = ((upper_sum (f,T)) . m) + ((- (lower_sum (f,T))) . m) by SEQ_1:7 .= ((upper_sum (f,T)) . m) + (- ((lower_sum (f,T)) . m)) by SEQ_1:10 .= ((upper_sum (f,T)) . m) - ((lower_sum (f,T)) . m) .= (upper_sum (f,(T . m))) - ((lower_sum (f,T)) . m) by INTEGRA2:def_2 .= (upper_sum (f,(T . m))) - (lower_sum (f,(T . m))) by INTEGRA2:def_3 .= (Sum (upper_volume (f,D))) - (lower_sum (f,(T . m))) by INTEGRA1:def_8 .= (Sum (upper_volume (f,D))) - (Sum (lower_volume (f,D))) by INTEGRA1:def_9 ; then A14: osc . m = Sum (UV - LV) by RVSUM_1:90; assume n <= m ; ::_thesis: abs ((osc1 . m) - 0) < b then A15: abs ((osc . m) - 0) < b / a by A13; len (lower_volume (g,D)) = len D by INTEGRA1:def_7; then reconsider LV1 = lower_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; len (upper_volume (g,D)) = len D by INTEGRA1:def_6; then reconsider UV1 = upper_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; reconsider F = UV1 - LV1 as FinSequence of REAL ; osc1 . m = ((upper_sum (g,T)) . m) + ((- (lower_sum (g,T))) . m) by SEQ_1:7 .= ((upper_sum (g,T)) . m) + (- ((lower_sum (g,T)) . m)) by SEQ_1:10 .= ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) .= (upper_sum (g,(T . m))) - ((lower_sum (g,T)) . m) by INTEGRA2:def_2 .= (upper_sum (g,(T . m))) - (lower_sum (g,(T . m))) by INTEGRA2:def_3 .= (Sum (upper_volume (g,D))) - (lower_sum (g,(T . m))) by INTEGRA1:def_8 .= (Sum (upper_volume (g,D))) - (Sum (lower_volume (g,D))) by INTEGRA1:def_9 ; then A16: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:90; for j being Nat st j in dom F holds 0 <= F . j proof let j be Nat; ::_thesis: ( j in dom F implies 0 <= F . j ) set r = F . j; A17: rng g is bounded_below by A3, INTEGRA1:11; assume A18: j in dom F ; ::_thesis: 0 <= F . j j in Seg (len F) by A18, FINSEQ_1:def_3; then A19: j in Seg (len D) by CARD_1:def_7; then A20: j in dom D by FINSEQ_1:def_3; then A21: LV1 . j = (lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7; A22: ex r being Real st r in rng (g | (divset (D,j))) proof consider r being Real such that A23: r in divset (D,j) by SUBSET_1:4; j in dom D by A19, FINSEQ_1:def_3; then divset (D,j) c= A by INTEGRA1:8; then r in A by A23; then r in dom g by FUNCT_2:def_1; then r in (dom g) /\ (divset (D,j)) by A23, XBOOLE_0:def_4; then r in dom (g | (divset (D,j))) by RELAT_1:61; then (g | (divset (D,j))) . r in rng (g | (divset (D,j))) by FUNCT_1:def_3; hence ex r being Real st r in rng (g | (divset (D,j))) ; ::_thesis: verum end; rng g is bounded_above by A3, INTEGRA1:13; then rng (g | (divset (D,j))) is real-bounded by A17, RELAT_1:70, XXREAL_2:45; then A24: (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))) >= 0 by A22, SEQ_4:11, XREAL_1:48; UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A20, INTEGRA1:def_6; then A25: F . j = ((upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) by A18, A21, VALUED_1:13 .= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) ; vol (divset (D,j)) >= 0 by INTEGRA1:9; hence 0 <= F . j by A25, A24; ::_thesis: verum end; then A26: osc1 . m >= 0 by A16, RVSUM_1:84; then A27: abs (osc1 . m) = osc1 . m by ABSVALUE:def_1; for j being Nat st j in Seg (len D) holds (UV1 - LV1) . j <= (a * (UV - LV)) . j proof let j be Nat; ::_thesis: ( j in Seg (len D) implies (UV1 - LV1) . j <= (a * (UV - LV)) . j ) set x = (UV1 - LV1) . j; set y = (a * (UV - LV)) . j; A28: (a * (UV - LV)) . j = a * ((UV - LV) . j) by RVSUM_1:45; assume A29: j in Seg (len D) ; ::_thesis: (UV1 - LV1) . j <= (a * (UV - LV)) . j then A30: j in dom D by FINSEQ_1:def_3; then A31: LV1 . j = (lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7; A32: a * ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) >= (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))) proof A33: j in dom D by A29, FINSEQ_1:def_3; then A34: (f | (divset (D,j))) | (divset (D,j)) is bounded_below by A1, INTEGRA1:8, INTEGRA2:6; A35: dom (g | (divset (D,j))) = (dom g) /\ (divset (D,j)) by RELAT_1:61 .= A /\ (divset (D,j)) by FUNCT_2:def_1 .= divset (D,j) by A33, INTEGRA1:8, XBOOLE_1:28 ; then reconsider g1 = g | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5; A36: dom (f | (divset (D,j))) = (dom f) /\ (divset (D,j)) by RELAT_1:61 .= A /\ (divset (D,j)) by FUNCT_2:def_1 .= divset (D,j) by A33, INTEGRA1:8, XBOOLE_1:28 ; then reconsider f1 = f | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5; reconsider g1 = g1 as Function of (divset (D,j)),REAL by A35, FUNCT_2:def_1; reconsider f1 = f1 as Function of (divset (D,j)),REAL by A36, FUNCT_2:def_1; A37: divset (D,j) c= A by A33, INTEGRA1:8; A38: for x, y being Real st x in divset (D,j) & y in divset (D,j) holds abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y))) proof let x, y be Real; ::_thesis: ( x in divset (D,j) & y in divset (D,j) implies abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y))) ) assume that A39: x in divset (D,j) and A40: y in divset (D,j) ; ::_thesis: abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y))) A41: g . y = g1 . y by A35, A40, FUNCT_1:47; A42: f . y = f1 . y by A36, A40, FUNCT_1:47; A43: f . x = f1 . x by A36, A39, FUNCT_1:47; g . x = g1 . x by A35, A39, FUNCT_1:47; hence abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y))) by A5, A37, A39, A40, A41, A43, A42; ::_thesis: verum end; (f | (divset (D,j))) | (divset (D,j)) is bounded_above by A1, A33, INTEGRA1:8, INTEGRA2:5; then f1 | (divset (D,j)) is bounded by A34; hence a * ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) >= (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))) by A4, A38, Th25; ::_thesis: verum end; vol (divset (D,j)) >= 0 by INTEGRA1:9; then A44: (a * ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))))) * (vol (divset (D,j))) >= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) by A32, XREAL_1:64; UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def_6; then A45: (UV1 - LV1) . j = ((upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) by A31, RVSUM_1:27 .= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) ; A46: LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def_7; UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def_6; then (a * (UV - LV)) . j = a * (((upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))))) by A46, A28, RVSUM_1:27 .= a * (((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) * (vol (divset (D,j)))) ; hence (UV1 - LV1) . j <= (a * (UV - LV)) . j by A45, A44; ::_thesis: verum end; then osc1 . m <= Sum (a * (UV - LV)) by A16, RVSUM_1:82; then A47: osc1 . m <= a * (osc . m) by A14, RVSUM_1:87; then osc . m >= 0 / a by A4, A26, XREAL_1:79; then abs (osc . m) = osc . m by ABSVALUE:def_1; then a * (osc . m) < a * (b / a) by A4, A15, XREAL_1:68; then a * (osc . m) < b by A4, XCMPLX_1:87; hence abs ((osc1 . m) - 0) < b by A47, A27, XXREAL_0:2; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc1 . m) - 0) < b ; ::_thesis: verum end; then osc1 is convergent by SEQ_2:def_6; then A48: lim ((upper_sum (g,T)) - (lower_sum (g,T))) = 0 by A12, SEQ_2:def_7; A49: lower_sum (g,T) is convergent by A3, A6, A7, Th8; upper_sum (g,T) is convergent by A3, A6, A7, Th9; hence (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 by A49, A48, SEQ_2:12; ::_thesis: verum end; hence g is integrable by A3, Th12; ::_thesis: verum end; theorem Th28: :: INTEGRA4:28 for a being Real for A being non empty closed_interval Subset of REAL for f, g, h being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds h is integrable proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, g, h being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds h is integrable let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g, h being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds h is integrable let f, g, h be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) implies h is integrable ) assume that A1: f | A is bounded and A2: f is integrable and A3: g | A is bounded and A4: g is integrable and A5: h | A is bounded and A6: a > 0 and A7: for x, y being Real st x in A & y in A holds abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ; ::_thesis: h is integrable for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds (lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0 proof let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0 ) assume that A8: delta T is convergent and A9: lim (delta T) = 0 ; ::_thesis: (lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0 A10: lower_sum (g,T) is convergent by A3, A8, A9, Th8; A11: upper_sum (g,T) is convergent by A3, A8, A9, Th9; then A12: (upper_sum (g,T)) - (lower_sum (g,T)) is convergent by A10; (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 by A3, A4, A8, A9, Th12; then A13: lim ((upper_sum (g,T)) - (lower_sum (g,T))) = 0 by A11, A10, SEQ_2:12; A14: lower_sum (f,T) is convergent by A1, A8, A9, Th8; reconsider osc2 = (upper_sum (h,T)) - (lower_sum (h,T)) as Real_Sequence ; reconsider osc1 = (upper_sum (g,T)) - (lower_sum (g,T)) as Real_Sequence ; reconsider osc = (upper_sum (f,T)) - (lower_sum (f,T)) as Real_Sequence ; A15: upper_sum (f,T) is convergent by A1, A8, A9, Th9; (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A1, A2, A8, A9, Th12; then A16: lim ((upper_sum (f,T)) - (lower_sum (f,T))) = 0 by A15, A14, SEQ_2:12; A17: (upper_sum (f,T)) - (lower_sum (f,T)) is convergent by A15, A14; A18: for b being real number st 0 < b holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc2 . m) - 0) < b proof let b be real number ; ::_thesis: ( 0 < b implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc2 . m) - 0) < b ) assume b > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc2 . m) - 0) < b then b / a > 0 by A6, XREAL_1:139; then A19: (b / a) / 2 > 0 by XREAL_1:139; then consider n1 being Element of NAT such that A20: for m being Element of NAT st n1 <= m holds abs ((osc . m) - 0) < (b / a) / 2 by A17, A16, SEQ_2:def_7; consider n2 being Element of NAT such that A21: for m being Element of NAT st n2 <= m holds abs ((osc1 . m) - 0) < (b / a) / 2 by A12, A13, A19, SEQ_2:def_7; ex n being Element of NAT st ( n1 <= n & n2 <= n ) proof take n = max (n1,n2); ::_thesis: ( n is Element of REAL & n is Element of NAT & n1 <= n & n2 <= n ) reconsider n = n as Element of NAT by XXREAL_0:16; n1 <= n by XXREAL_0:25; hence ( n is Element of REAL & n is Element of NAT & n1 <= n & n2 <= n ) by XXREAL_0:25; ::_thesis: verum end; then consider n being Element of NAT such that A22: n1 <= n and A23: n2 <= n ; for m being Element of NAT st n <= m holds abs ((osc2 . m) - 0) < b proof let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((osc2 . m) - 0) < b ) reconsider D = T . m as Division of A ; len (upper_volume (f,D)) = len D by INTEGRA1:def_6; then reconsider UV = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; len (lower_volume (f,D)) = len D by INTEGRA1:def_7; then reconsider LV = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; osc . m = ((upper_sum (f,T)) . m) + ((- (lower_sum (f,T))) . m) by SEQ_1:7 .= ((upper_sum (f,T)) . m) + (- ((lower_sum (f,T)) . m)) by SEQ_1:10 .= ((upper_sum (f,T)) . m) - ((lower_sum (f,T)) . m) .= (upper_sum (f,(T . m))) - ((lower_sum (f,T)) . m) by INTEGRA2:def_2 .= (upper_sum (f,(T . m))) - (lower_sum (f,(T . m))) by INTEGRA2:def_3 .= (Sum (upper_volume (f,D))) - (lower_sum (f,(T . m))) by INTEGRA1:def_8 .= (Sum (upper_volume (f,D))) - (Sum (lower_volume (f,D))) by INTEGRA1:def_9 ; then A24: osc . m = Sum (UV - LV) by RVSUM_1:90; len (lower_volume (h,D)) = len D by INTEGRA1:def_7; then reconsider LV2 = lower_volume (h,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; len (upper_volume (h,D)) = len D by INTEGRA1:def_6; then reconsider UV2 = upper_volume (h,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; len (lower_volume (g,D)) = len D by INTEGRA1:def_7; then reconsider LV1 = lower_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; len (upper_volume (g,D)) = len D by INTEGRA1:def_6; then reconsider UV1 = upper_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133; reconsider H = UV - LV as FinSequence of REAL ; reconsider G = UV1 - LV1 as FinSequence of REAL ; reconsider F = UV2 - LV2 as FinSequence of REAL ; osc1 . m = ((upper_sum (g,T)) . m) + ((- (lower_sum (g,T))) . m) by SEQ_1:7 .= ((upper_sum (g,T)) . m) + (- ((lower_sum (g,T)) . m)) by SEQ_1:10 .= ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) .= (upper_sum (g,(T . m))) - ((lower_sum (g,T)) . m) by INTEGRA2:def_2 .= (upper_sum (g,(T . m))) - (lower_sum (g,(T . m))) by INTEGRA2:def_3 .= (Sum (upper_volume (g,D))) - (lower_sum (g,(T . m))) by INTEGRA1:def_8 .= (Sum (upper_volume (g,D))) - (Sum (lower_volume (g,D))) by INTEGRA1:def_9 ; then A25: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:90; for j being Nat st j in dom G holds 0 <= G . j proof let j be Nat; ::_thesis: ( j in dom G implies 0 <= G . j ) set r = G . j; A26: rng g is bounded_below by A3, INTEGRA1:11; assume A27: j in dom G ; ::_thesis: 0 <= G . j j in Seg (len G) by A27, FINSEQ_1:def_3; then A28: j in Seg (len D) by CARD_1:def_7; then A29: j in dom D by FINSEQ_1:def_3; then A30: LV1 . j = (lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7; A31: ex r being Real st r in rng (g | (divset (D,j))) proof consider r being Real such that A32: r in divset (D,j) by SUBSET_1:4; j in dom D by A28, FINSEQ_1:def_3; then divset (D,j) c= A by INTEGRA1:8; then r in A by A32; then r in dom g by FUNCT_2:def_1; then r in (dom g) /\ (divset (D,j)) by A32, XBOOLE_0:def_4; then r in dom (g | (divset (D,j))) by RELAT_1:61; then (g | (divset (D,j))) . r in rng (g | (divset (D,j))) by FUNCT_1:def_3; hence ex r being Real st r in rng (g | (divset (D,j))) ; ::_thesis: verum end; rng g is bounded_above by A3, INTEGRA1:13; then rng (g | (divset (D,j))) is real-bounded by A26, RELAT_1:70, XXREAL_2:45; then A33: (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))) >= 0 by A31, SEQ_4:11, XREAL_1:48; UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A29, INTEGRA1:def_6; then A34: G . j = ((upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) by A27, A30, VALUED_1:13 .= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) ; vol (divset (D,j)) >= 0 by INTEGRA1:9; hence 0 <= G . j by A34, A33; ::_thesis: verum end; then A35: osc1 . m >= 0 by A25, RVSUM_1:84; assume A36: n <= m ; ::_thesis: abs ((osc2 . m) - 0) < b then n1 <= m by A22, XXREAL_0:2; then A37: abs ((osc . m) - 0) < (b / a) / 2 by A20; n2 <= m by A23, A36, XXREAL_0:2; then A38: abs ((osc1 . m) - 0) < (b / a) / 2 by A21; for j being Nat st j in dom H holds 0 <= H . j proof let j be Nat; ::_thesis: ( j in dom H implies 0 <= H . j ) set r = H . j; A39: rng f is bounded_below by A1, INTEGRA1:11; assume A40: j in dom H ; ::_thesis: 0 <= H . j j in Seg (len H) by A40, FINSEQ_1:def_3; then A41: j in Seg (len D) by CARD_1:def_7; then A42: j in dom D by FINSEQ_1:def_3; then A43: LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7; A44: ex r being Real st r in rng (f | (divset (D,j))) proof consider r being Real such that A45: r in divset (D,j) by SUBSET_1:4; j in dom D by A41, FINSEQ_1:def_3; then divset (D,j) c= A by INTEGRA1:8; then r in A by A45; then r in dom f by FUNCT_2:def_1; then r in (dom f) /\ (divset (D,j)) by A45, XBOOLE_0:def_4; then r in dom (f | (divset (D,j))) by RELAT_1:61; then (f | (divset (D,j))) . r in rng (f | (divset (D,j))) by FUNCT_1:def_3; hence ex r being Real st r in rng (f | (divset (D,j))) ; ::_thesis: verum end; rng f is bounded_above by A1, INTEGRA1:13; then rng (f | (divset (D,j))) is real-bounded by A39, RELAT_1:70, XXREAL_2:45; then A46: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= 0 by A44, SEQ_4:11, XREAL_1:48; UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A42, INTEGRA1:def_6; then A47: H . j = ((upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) by A40, A43, VALUED_1:13 .= ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) * (vol (divset (D,j))) ; vol (divset (D,j)) >= 0 by INTEGRA1:9; hence 0 <= H . j by A47, A46; ::_thesis: verum end; then A48: osc . m >= 0 by A24, RVSUM_1:84; then (osc . m) * (osc1 . m) >= 0 by A35; then (abs (osc . m)) + (abs (osc1 . m)) = abs ((osc . m) + (osc1 . m)) by ABSVALUE:11; then (abs ((osc . m) - 0)) + (abs (osc1 . m)) = (osc . m) + (osc1 . m) by A48, A35, ABSVALUE:def_1; then (osc . m) + (osc1 . m) < ((b / a) / 2) + ((b / a) / 2) by A37, A38, XREAL_1:8; then a * ((osc . m) + (osc1 . m)) < a * (b / a) by A6, XREAL_1:68; then A49: a * ((osc . m) + (osc1 . m)) < b by A6, XCMPLX_1:87; osc2 . m = ((upper_sum (h,T)) . m) + ((- (lower_sum (h,T))) . m) by SEQ_1:7 .= ((upper_sum (h,T)) . m) + (- ((lower_sum (h,T)) . m)) by SEQ_1:10 .= ((upper_sum (h,T)) . m) - ((lower_sum (h,T)) . m) .= (upper_sum (h,(T . m))) - ((lower_sum (h,T)) . m) by INTEGRA2:def_2 .= (upper_sum (h,(T . m))) - (lower_sum (h,(T . m))) by INTEGRA2:def_3 .= (Sum (upper_volume (h,D))) - (lower_sum (h,(T . m))) by INTEGRA1:def_8 .= (Sum (upper_volume (h,D))) - (Sum (lower_volume (h,D))) by INTEGRA1:def_9 ; then A50: osc2 . m = Sum (UV2 - LV2) by RVSUM_1:90; for j being Nat st j in dom F holds 0 <= F . j proof let j be Nat; ::_thesis: ( j in dom F implies 0 <= F . j ) set r = F . j; A51: rng h is bounded_below by A5, INTEGRA1:11; assume A52: j in dom F ; ::_thesis: 0 <= F . j j in Seg (len F) by A52, FINSEQ_1:def_3; then A53: j in Seg (len D) by CARD_1:def_7; then A54: j in dom D by FINSEQ_1:def_3; then A55: LV2 . j = (lower_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7; A56: ex r being Real st r in rng (h | (divset (D,j))) proof consider r being Real such that A57: r in divset (D,j) by SUBSET_1:4; j in dom D by A53, FINSEQ_1:def_3; then divset (D,j) c= A by INTEGRA1:8; then r in A by A57; then r in dom h by FUNCT_2:def_1; then r in (dom h) /\ (divset (D,j)) by A57, XBOOLE_0:def_4; then r in dom (h | (divset (D,j))) by RELAT_1:61; then (h | (divset (D,j))) . r in rng (h | (divset (D,j))) by FUNCT_1:def_3; hence ex r being Real st r in rng (h | (divset (D,j))) ; ::_thesis: verum end; rng h is bounded_above by A5, INTEGRA1:13; then rng (h | (divset (D,j))) is real-bounded by A51, RELAT_1:70, XXREAL_2:45; then A58: (upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j))))) >= 0 by A56, SEQ_4:11, XREAL_1:48; UV2 . j = (upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by A54, INTEGRA1:def_6; then A59: F . j = ((upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j)))) by A52, A55, VALUED_1:13 .= ((upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j)))))) * (vol (divset (D,j))) ; vol (divset (D,j)) >= 0 by INTEGRA1:9; hence 0 <= F . j by A59, A58; ::_thesis: verum end; then osc2 . m >= 0 by A50, RVSUM_1:84; then A60: abs (osc2 . m) = osc2 . m by ABSVALUE:def_1; for j being Nat st j in Seg (len D) holds (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j proof let j be Nat; ::_thesis: ( j in Seg (len D) implies (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j ) set x = (UV2 - LV2) . j; set y = (a * ((UV - LV) + (UV1 - LV1))) . j; A61: (a * ((UV - LV) + (UV1 - LV1))) . j = a * (((UV - LV) + (UV1 - LV1)) . j) by RVSUM_1:45 .= a * (((UV - LV) . j) + ((UV1 - LV1) . j)) by RVSUM_1:11 .= a * (((UV . j) - (LV . j)) + ((UV1 - LV1) . j)) by RVSUM_1:27 .= a * (((UV . j) - (LV . j)) + ((UV1 . j) - (LV1 . j))) by RVSUM_1:27 ; A62: vol (divset (D,j)) >= 0 by INTEGRA1:9; assume A63: j in Seg (len D) ; ::_thesis: (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j then A64: j in dom D by FINSEQ_1:def_3; then A65: LV2 . j = (lower_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def_7; UV2 . j = (upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def_6; then A66: (UV2 - LV2) . j = ((upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j)))) by A65, RVSUM_1:27 .= ((upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j)))))) * (vol (divset (D,j))) ; A67: LV1 . j = (lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def_7; A68: UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def_6; A69: a * (((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) + ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))))) >= (upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j))))) proof A70: j in dom D by A63, FINSEQ_1:def_3; A71: dom (g | (divset (D,j))) = (dom g) /\ (divset (D,j)) by RELAT_1:61 .= A /\ (divset (D,j)) by FUNCT_2:def_1 .= divset (D,j) by A70, INTEGRA1:8, XBOOLE_1:28 ; then reconsider g1 = g | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5; reconsider g1 = g1 as Function of (divset (D,j)),REAL by A71, FUNCT_2:def_1; A72: (g | (divset (D,j))) | (divset (D,j)) is bounded_below by A3, A71, INTEGRA2:6; A73: dom (h | (divset (D,j))) = (dom h) /\ (divset (D,j)) by RELAT_1:61 .= A /\ (divset (D,j)) by FUNCT_2:def_1 .= divset (D,j) by A70, INTEGRA1:8, XBOOLE_1:28 ; then reconsider h1 = h | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5; reconsider h1 = h1 as Function of (divset (D,j)),REAL by A73, FUNCT_2:def_1; A74: dom (f | (divset (D,j))) = (dom f) /\ (divset (D,j)) by RELAT_1:61 .= A /\ (divset (D,j)) by FUNCT_2:def_1 .= divset (D,j) by A70, INTEGRA1:8, XBOOLE_1:28 ; then reconsider f1 = f | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5; A75: (f | (divset (D,j))) | (divset (D,j)) is bounded_below by A1, A74, INTEGRA2:6; A76: for x, y being Real st x in divset (D,j) & y in divset (D,j) holds abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) proof let x, y be Real; ::_thesis: ( x in divset (D,j) & y in divset (D,j) implies abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) ) assume that A77: x in divset (D,j) and A78: y in divset (D,j) ; ::_thesis: abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) A79: g . y = g1 . y by A71, A78, FUNCT_1:47; A80: h . y = h1 . y by A73, A78, FUNCT_1:47; A81: h . x = h1 . x by A73, A77, FUNCT_1:47; A82: f . y = f1 . y by A74, A78, FUNCT_1:47; A83: f . x = f1 . x by A74, A77, FUNCT_1:47; g . x = g1 . x by A71, A77, FUNCT_1:47; hence abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) by A7, A74, A77, A78, A79, A83, A82, A81, A80; ::_thesis: verum end; (g | (divset (D,j))) | (divset (D,j)) is bounded_above by A3, A71, INTEGRA2:5; then A84: g1 | (divset (D,j)) is bounded by A72; (f | (divset (D,j))) | (divset (D,j)) is bounded_above by A1, A74, INTEGRA2:5; then A85: f1 | (divset (D,j)) is bounded by A75; f1 is total by A74, PARTFUN1:def_2; hence a * (((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) + ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))))) >= (upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j))))) by A6, A85, A84, A76, Th26; ::_thesis: verum end; LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def_7; then (a * ((UV - LV) + (UV1 - LV1))) . j = a * ((((upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))))) + (((upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))))) by A64, A68, A67, A61, INTEGRA1:def_6 .= (a * (((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) + ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))))) * (vol (divset (D,j))) ; hence (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j by A66, A69, A62, XREAL_1:64; ::_thesis: verum end; then osc2 . m <= Sum (a * ((UV - LV) + (UV1 - LV1))) by A50, RVSUM_1:82; then osc2 . m <= a * (Sum ((UV - LV) + (UV1 - LV1))) by RVSUM_1:87; then osc2 . m <= a * ((osc . m) + (osc1 . m)) by A24, A25, RVSUM_1:89; hence abs ((osc2 . m) - 0) < b by A60, A49, XXREAL_0:2; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((osc2 . m) - 0) < b ; ::_thesis: verum end; then osc2 is convergent by SEQ_2:def_6; then A86: lim ((upper_sum (h,T)) - (lower_sum (h,T))) = 0 by A18, SEQ_2:def_7; A87: lower_sum (h,T) is convergent by A5, A8, A9, Th8; upper_sum (h,T) is convergent by A5, A8, A9, Th9; hence (lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0 by A87, A86, SEQ_2:12; ::_thesis: verum end; hence h is integrable by A5, Th12; ::_thesis: verum end; theorem :: INTEGRA4:29 for A being non empty closed_interval Subset of REAL for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds f (#) g is integrable proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds f (#) g is integrable let f, g be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable implies f (#) g is integrable ) assume that A1: f | A is bounded and A2: f is integrable and A3: g | A is bounded and A4: g is integrable ; ::_thesis: f (#) g is integrable A5: (f (#) g) | (A /\ A) is bounded by A1, A3, RFUNCT_1:84; consider r2 being real number such that A6: for x being set st x in A /\ (dom g) holds abs (g . x) <= r2 by A3, RFUNCT_1:73; A7: A /\ (dom g) = A /\ A by FUNCT_2:def_1 .= A ; A8: A /\ (dom f) = A /\ A by FUNCT_2:def_1 .= A ; then consider a being Element of REAL such that A9: a in A /\ (dom f) by SUBSET_1:4; reconsider a = a as Element of A by A9; A10: abs (f . a) >= 0 by COMPLEX1:46; consider r1 being real number such that A11: for x being set st x in A /\ (dom f) holds abs (f . x) <= r1 by A1, RFUNCT_1:73; reconsider r = max (r1,r2) as Real by XREAL_0:def_1; A12: r2 <= r by XXREAL_0:25; A13: r1 <= r by XXREAL_0:25; A14: for x, y being Real st x in A & y in A holds abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) proof let x, y be Real; ::_thesis: ( x in A & y in A implies abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) ) assume that A15: x in A and A16: y in A ; ::_thesis: abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) A17: (f (#) g) . y = (f . y) * (g . y) by VALUED_1:5; abs (g . y) <= r2 by A6, A7, A16; then A18: abs (g . y) <= r by A12, XXREAL_0:2; A19: abs ((f . x) - (f . y)) >= 0 by COMPLEX1:46; abs (((f . x) - (f . y)) * (g . y)) = (abs ((f . x) - (f . y))) * (abs (g . y)) by COMPLEX1:65; then A20: abs (((f . x) - (f . y)) * (g . y)) <= r * (abs ((f . x) - (f . y))) by A19, A18, XREAL_1:64; (f (#) g) . x = (f . x) * (g . x) by VALUED_1:5; then abs (((f (#) g) . x) - ((f (#) g) . y)) = abs (((f . x) * ((g . x) - (g . y))) + (((f . x) - (f . y)) * (g . y))) by A17; then A21: abs (((f (#) g) . x) - ((f (#) g) . y)) <= (abs ((f . x) * ((g . x) - (g . y)))) + (abs (((f . x) - (f . y)) * (g . y))) by COMPLEX1:56; abs (f . x) <= r1 by A11, A8, A15; then A22: abs (f . x) <= r by A13, XXREAL_0:2; A23: abs ((g . x) - (g . y)) >= 0 by COMPLEX1:46; abs ((f . x) * ((g . x) - (g . y))) = (abs (f . x)) * (abs ((g . x) - (g . y))) by COMPLEX1:65; then abs ((f . x) * ((g . x) - (g . y))) <= r * (abs ((g . x) - (g . y))) by A23, A22, XREAL_1:64; then (abs ((f . x) * ((g . x) - (g . y)))) + (abs (((f . x) - (f . y)) * (g . y))) <= (r * (abs ((g . x) - (g . y)))) + (r * (abs ((f . x) - (f . y)))) by A20, XREAL_1:7; hence abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) by A21, XXREAL_0:2; ::_thesis: verum end; A24: abs (f . a) <= r1 by A11, A9; now__::_thesis:_f_(#)_g_is_integrable percases ( r = 0 or r > 0 ) by A24, A10, XXREAL_0:25; supposeA25: r = 0 ; ::_thesis: f (#) g is integrable for x, y being Real st x in A & y in A holds abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y))) proof let x, y be Real; ::_thesis: ( x in A & y in A implies abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y))) ) assume that A26: x in A and A27: y in A ; ::_thesis: abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y))) abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) by A14, A26, A27; hence abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y))) by A25, COMPLEX1:46; ::_thesis: verum end; hence f (#) g is integrable by A1, A2, A5, Th27; ::_thesis: verum end; suppose r > 0 ; ::_thesis: f (#) g is integrable hence f (#) g is integrable by A1, A2, A3, A4, A5, A14, Th28; ::_thesis: verum end; end; end; hence f (#) g is integrable ; ::_thesis: verum end; theorem :: INTEGRA4:30 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded & f is integrable & not 0 in rng f & (f ^) | A is bounded holds f ^ is integrable proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable & not 0 in rng f & (f ^) | A is bounded holds f ^ is integrable let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & not 0 in rng f & (f ^) | A is bounded implies f ^ is integrable ) assume that A1: f | A is bounded and A2: f is integrable and A3: not 0 in rng f and A4: (f ^) | A is bounded ; ::_thesis: f ^ is integrable consider r being real number such that A5: for x being set st x in A /\ (dom (f ^)) holds abs ((f ^) . x) <= r by A4, RFUNCT_1:73; reconsider r = r as Real by XREAL_0:def_1; f " {0} = {} by A3, FUNCT_1:72; then A6: f ^ is total by RFUNCT_1:54; A7: for x, y being Real st x in A & y in A holds abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y))) proof let x, y be Real; ::_thesis: ( x in A & y in A implies abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y))) ) assume that A8: x in A and A9: y in A ; ::_thesis: abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y))) A10: x in dom (f ^) by A6, A8, PARTFUN1:def_2; then A11: f . x <> 0 by RFUNCT_1:3; A12: y in dom (f ^) by A6, A9, PARTFUN1:def_2; then A13: f . y <> 0 by RFUNCT_1:3; ( 0 <= 1 / (abs (f . x)) & 0 <= 1 / (abs (f . y)) & 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r ) proof A14: abs (f . y) > 0 by A13, COMPLEX1:47; abs (f . x) > 0 by A11, COMPLEX1:47; hence ( 0 <= 1 / (abs (f . x)) & 0 <= 1 / (abs (f . y)) ) by A14; ::_thesis: ( 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r ) reconsider x = x, y = y as Element of A by A8, A9; y in A /\ (dom (f ^)) by A12, XBOOLE_0:def_4; then abs ((f ^) . y) <= r by A5; then abs (1 * ((f . y) ")) <= r by A12, RFUNCT_1:def_2; then A15: abs (1 / (f . y)) <= r by XCMPLX_0:def_9; x in A /\ (dom (f ^)) by A10, XBOOLE_0:def_4; then abs ((f ^) . x) <= r by A5; then abs (1 * ((f . x) ")) <= r by A10, RFUNCT_1:def_2; then abs (1 / (f . x)) <= r by XCMPLX_0:def_9; hence ( 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r ) by A15, ABSVALUE:7; ::_thesis: verum end; then A16: (1 / (abs (f . x))) * (1 / (abs (f . y))) <= r * r by XREAL_1:66; abs ((f . x) - (f . y)) >= 0 by COMPLEX1:46; then A17: (abs ((f . x) - (f . y))) * ((1 / (abs (f . x))) * (1 / (abs (f . y)))) <= (abs ((f . x) - (f . y))) * (r ^2) by A16, XREAL_1:64; ((f ^) . x) - ((f ^) . y) = ((f . x) ") - ((f ^) . y) by A10, RFUNCT_1:def_2 .= ((f . x) ") - ((f . y) ") by A12, RFUNCT_1:def_2 ; then abs (((f ^) . x) - ((f ^) . y)) = (abs ((f . x) - (f . y))) / ((abs (f . x)) * (abs (f . y))) by A13, A11, SEQ_2:2 .= ((abs ((f . x) - (f . y))) / (abs (f . x))) * (1 / (abs (f . y))) by XCMPLX_1:103 .= ((abs ((f . x) - (f . y))) * (1 / (abs (f . x)))) * (1 / (abs (f . y))) by XCMPLX_1:99 ; hence abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y))) by A17; ::_thesis: verum end; percases ( r ^2 = 0 or r ^2 > 0 ) by XREAL_1:63; supposeA18: r ^2 = 0 ; ::_thesis: f ^ is integrable for x, y being Real st x in A & y in A holds abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y))) proof let x, y be Real; ::_thesis: ( x in A & y in A implies abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y))) ) assume that A19: x in A and A20: y in A ; ::_thesis: abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y))) abs (((f ^) . x) - ((f ^) . y)) <= 0 * (abs ((f . x) - (f . y))) by A7, A18, A19, A20; hence abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y))) by COMPLEX1:46; ::_thesis: verum end; hence f ^ is integrable by A1, A2, A4, A6, Th27; ::_thesis: verum end; suppose r ^2 > 0 ; ::_thesis: f ^ is integrable hence f ^ is integrable by A1, A2, A4, A6, A7, Th27; ::_thesis: verum end; end; end;