:: INTEGRA7 semantic presentation begin theorem Th1: :: INTEGRA7:1 for a being real number for A being non empty set for f, g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds abs ((f . x) - (g . x)) <= a ) holds ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a ) proof let a be real number ; ::_thesis: for A being non empty set for f, g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds abs ((f . x) - (g . x)) <= a ) holds ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a ) let A be non empty set ; ::_thesis: for f, g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds abs ((f . x) - (g . x)) <= a ) holds ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a ) let f, g be Function of A,REAL; ::_thesis: ( rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds abs ((f . x) - (g . x)) <= a ) implies ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a ) ) assume that A1: rng f is bounded_above and A2: rng g is bounded_above and A3: for x being set st x in A holds abs ((f . x) - (g . x)) <= a ; ::_thesis: ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a ) A4: dom f = A by FUNCT_2:def_1; A5: for b being real number st b in rng g holds b <= (upper_bound (rng f)) + a proof let b be real number ; ::_thesis: ( b in rng g implies b <= (upper_bound (rng f)) + a ) assume b in rng g ; ::_thesis: b <= (upper_bound (rng f)) + a then consider x being Element of A such that x in dom g and A6: b = g . x by PARTFUN1:3; abs ((f . x) - (g . x)) <= a by A3; then abs ((g . x) - (f . x)) <= a by COMPLEX1:60; then (g . x) - (f . x) <= a by ABSVALUE:5; then A7: b <= a + (f . x) by A6, XREAL_1:20; f . x in rng f by A4, FUNCT_1:3; then f . x <= upper_bound (rng f) by A1, SEQ_4:def_1; then a + (f . x) <= a + (upper_bound (rng f)) by XREAL_1:6; hence b <= (upper_bound (rng f)) + a by A7, XXREAL_0:2; ::_thesis: verum end; A8: dom g = A by FUNCT_2:def_1; then rng g is non empty Subset of REAL by RELAT_1:42; then A9: upper_bound (rng g) <= (upper_bound (rng f)) + a by A5, SEQ_4:45; A10: for b being real number st b in rng f holds b <= (upper_bound (rng g)) + a proof let b be real number ; ::_thesis: ( b in rng f implies b <= (upper_bound (rng g)) + a ) assume b in rng f ; ::_thesis: b <= (upper_bound (rng g)) + a then consider x being Element of A such that x in dom f and A11: b = f . x by PARTFUN1:3; g . x in rng g by A8, FUNCT_1:3; then g . x <= upper_bound (rng g) by A2, SEQ_4:def_1; then A12: a + (g . x) <= a + (upper_bound (rng g)) by XREAL_1:6; abs ((f . x) - (g . x)) <= a by A3; then (f . x) - (g . x) <= a by ABSVALUE:5; then b <= a + (g . x) by A11, XREAL_1:20; hence b <= (upper_bound (rng g)) + a by A12, XXREAL_0:2; ::_thesis: verum end; rng f is non empty Subset of REAL by A4, RELAT_1:42; then upper_bound (rng f) <= (upper_bound (rng g)) + a by A10, SEQ_4:45; hence ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a ) by A9, XREAL_1:20; ::_thesis: verum end; theorem Th2: :: INTEGRA7:2 for a being real number for A being non empty set for f, g being Function of A,REAL st rng f is bounded_below & rng g is bounded_below & ( for x being set st x in A holds abs ((f . x) - (g . x)) <= a ) holds ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) proof let a be real number ; ::_thesis: for A being non empty set for f, g being Function of A,REAL st rng f is bounded_below & rng g is bounded_below & ( for x being set st x in A holds abs ((f . x) - (g . x)) <= a ) holds ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) let A be non empty set ; ::_thesis: for f, g being Function of A,REAL st rng f is bounded_below & rng g is bounded_below & ( for x being set st x in A holds abs ((f . x) - (g . x)) <= a ) holds ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) let f, g be Function of A,REAL; ::_thesis: ( rng f is bounded_below & rng g is bounded_below & ( for x being set st x in A holds abs ((f . x) - (g . x)) <= a ) implies ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) ) assume that A1: rng f is bounded_below and A2: rng g is bounded_below and A3: for x being set st x in A holds abs ((f . x) - (g . x)) <= a ; ::_thesis: ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) A4: dom f = A by FUNCT_2:def_1; A5: for b being real number st b in rng g holds (lower_bound (rng f)) - a <= b proof let b be real number ; ::_thesis: ( b in rng g implies (lower_bound (rng f)) - a <= b ) assume b in rng g ; ::_thesis: (lower_bound (rng f)) - a <= b then consider x being Element of A such that x in dom g and A6: b = g . x by PARTFUN1:3; f . x in rng f by A4, FUNCT_1:3; then lower_bound (rng f) <= f . x by A1, SEQ_4:def_2; then A7: (lower_bound (rng f)) - a <= (f . x) - a by XREAL_1:9; abs ((f . x) - (g . x)) <= a by A3; then (f . x) - (g . x) <= a by ABSVALUE:5; then (f . x) - a <= b by A6, XREAL_1:12; hence (lower_bound (rng f)) - a <= b by A7, XXREAL_0:2; ::_thesis: verum end; A8: dom g = A by FUNCT_2:def_1; then rng g is non empty Subset of REAL by RELAT_1:42; then A9: (lower_bound (rng f)) - a <= lower_bound (rng g) by A5, SEQ_4:43; A10: for b being real number st b in rng f holds (lower_bound (rng g)) - a <= b proof let b be real number ; ::_thesis: ( b in rng f implies (lower_bound (rng g)) - a <= b ) assume b in rng f ; ::_thesis: (lower_bound (rng g)) - a <= b then consider x being Element of A such that x in dom f and A11: b = f . x by PARTFUN1:3; abs ((f . x) - (g . x)) <= a by A3; then abs ((g . x) - (f . x)) <= a by COMPLEX1:60; then (g . x) - (f . x) <= a by ABSVALUE:5; then A12: (g . x) - a <= b by A11, XREAL_1:12; g . x in rng g by A8, FUNCT_1:3; then lower_bound (rng g) <= g . x by A2, SEQ_4:def_2; then (lower_bound (rng g)) - a <= (g . x) - a by XREAL_1:9; hence (lower_bound (rng g)) - a <= b by A12, XXREAL_0:2; ::_thesis: verum end; rng f is non empty Subset of REAL by A4, RELAT_1:42; then (lower_bound (rng g)) - a <= lower_bound (rng f) by A10, SEQ_4:43; hence ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) by A9, XREAL_1:12; ::_thesis: verum end; theorem :: INTEGRA7:3 for X being set for f being PartFunc of REAL,REAL st (f | X) | X is bounded holds f | X is bounded by RELAT_1:72; theorem Th4: :: INTEGRA7:4 for X being set for f being PartFunc of REAL,REAL for x being Real st x in X & f | X is_differentiable_in x holds f is_differentiable_in x proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL for x being Real st x in X & f | X is_differentiable_in x holds f is_differentiable_in x let f be PartFunc of REAL,REAL; ::_thesis: for x being Real st x in X & f | X is_differentiable_in x holds f is_differentiable_in x let x be Real; ::_thesis: ( x in X & f | X is_differentiable_in x implies f is_differentiable_in x ) assume that A1: x in X and A2: f | X is_differentiable_in x ; ::_thesis: f is_differentiable_in x consider N being Neighbourhood of x such that A3: N c= dom (f | X) and A4: ex L being LinearFunc ex R being RestFunc st for x1 being Real st x1 in N holds ((f | X) . x1) - ((f | X) . x) = (L . (x1 - x)) + (R . (x1 - x)) by A2, FDIFF_1:def_4; A5: (f | X) . x = f . x by A1, FUNCT_1:49; take N ; :: according to FDIFF_1:def_4 ::_thesis: ( N c= dom f & ex b1 being Element of K6(K7(REAL,REAL)) ex b2 being Element of K6(K7(REAL,REAL)) st for b3 being Element of REAL holds ( not b3 in N or (f . b3) - (f . x) = (b1 . (b3 - x)) + (b2 . (b3 - x)) ) ) N c= (dom f) /\ X by A3, RELAT_1:61; hence N c= dom f by XBOOLE_1:18; ::_thesis: ex b1 being Element of K6(K7(REAL,REAL)) ex b2 being Element of K6(K7(REAL,REAL)) st for b3 being Element of REAL holds ( not b3 in N or (f . b3) - (f . x) = (b1 . (b3 - x)) + (b2 . (b3 - x)) ) consider L being LinearFunc, R being RestFunc such that A6: for x1 being Real st x1 in N holds ((f | X) . x1) - ((f | X) . x) = (L . (x1 - x)) + (R . (x1 - x)) by A4; take L ; ::_thesis: ex b1 being Element of K6(K7(REAL,REAL)) st for b2 being Element of REAL holds ( not b2 in N or (f . b2) - (f . x) = (L . (b2 - x)) + (b1 . (b2 - x)) ) take R ; ::_thesis: for b1 being Element of REAL holds ( not b1 in N or (f . b1) - (f . x) = (L . (b1 - x)) + (R . (b1 - x)) ) let x1 be Real; ::_thesis: ( not x1 in N or (f . x1) - (f . x) = (L . (x1 - x)) + (R . (x1 - x)) ) assume A7: x1 in N ; ::_thesis: (f . x1) - (f . x) = (L . (x1 - x)) + (R . (x1 - x)) then (f | X) . x1 = f . x1 by A3, FUNCT_1:47; hence (f . x1) - (f . x) = (L . (x1 - x)) + (R . (x1 - x)) by A6, A7, A5; ::_thesis: verum end; theorem :: INTEGRA7:5 for X being set for f being PartFunc of REAL,REAL st f | X is_differentiable_on X holds f is_differentiable_on X proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is_differentiable_on X holds f is_differentiable_on X let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is_differentiable_on X implies f is_differentiable_on X ) assume A1: f | X is_differentiable_on X ; ::_thesis: f is_differentiable_on X A2: now__::_thesis:_for_x_being_Real_st_x_in_X_holds_ f_|_X_is_differentiable_in_x let x be Real; ::_thesis: ( x in X implies f | X is_differentiable_in x ) assume A3: x in X ; ::_thesis: f | X is_differentiable_in x then (f | X) | X is_differentiable_in x by A1, FDIFF_1:def_6; hence f | X is_differentiable_in x by A3, Th4; ::_thesis: verum end; X c= dom (f | X) by A1, FDIFF_1:def_6; then X c= (dom f) /\ X by RELAT_1:61; then X c= dom f by XBOOLE_1:18; hence f is_differentiable_on X by A2, FDIFF_1:def_6; ::_thesis: verum end; theorem Th6: :: INTEGRA7:6 for X being set for f, g being PartFunc of REAL,REAL st f is_differentiable_on X & g is_differentiable_on X holds ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X ) proof let X be set ; ::_thesis: for f, g being PartFunc of REAL,REAL st f is_differentiable_on X & g is_differentiable_on X holds ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X ) let f, g be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on X & g is_differentiable_on X implies ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X ) ) assume that A1: f is_differentiable_on X and A2: g is_differentiable_on X ; ::_thesis: ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X ) reconsider Z = X as Subset of REAL by A1, FDIFF_1:8; reconsider Z = Z as open Subset of REAL by A1, FDIFF_1:10; ( X c= dom f & X c= dom g ) by A1, A2, FDIFF_1:def_6; then A3: Z c= (dom f) /\ (dom g) by XBOOLE_1:19; then A4: Z c= dom (f (#) g) by VALUED_1:def_4; ( Z c= dom (f + g) & Z c= dom (f - g) ) by A3, VALUED_1:12, VALUED_1:def_1; hence ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X ) by A1, A2, A4, FDIFF_1:18, FDIFF_1:19, FDIFF_1:21; ::_thesis: verum end; theorem Th7: :: INTEGRA7:7 for r being real number for X being set for f being PartFunc of REAL,REAL st f is_differentiable_on X holds r (#) f is_differentiable_on X proof let r be real number ; ::_thesis: for X being set for f being PartFunc of REAL,REAL st f is_differentiable_on X holds r (#) f is_differentiable_on X let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on X holds r (#) f is_differentiable_on X let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on X implies r (#) f is_differentiable_on X ) reconsider r1 = r as Real by XREAL_0:def_1; assume A1: f is_differentiable_on X ; ::_thesis: r (#) f is_differentiable_on X then reconsider Z = X as Subset of REAL by FDIFF_1:8; reconsider Z = Z as open Subset of REAL by A1, FDIFF_1:10; X c= dom f by A1, FDIFF_1:def_6; then Z c= dom (r (#) f) by VALUED_1:def_5; then r1 (#) f is_differentiable_on X by A1, FDIFF_1:20; hence r (#) f is_differentiable_on X ; ::_thesis: verum end; theorem Th8: :: INTEGRA7:8 for X being set for g, f being PartFunc of REAL,REAL st ( for x being set st x in X holds g . x <> 0 ) & f is_differentiable_on X & g is_differentiable_on X holds f / g is_differentiable_on X proof let X be set ; ::_thesis: for g, f being PartFunc of REAL,REAL st ( for x being set st x in X holds g . x <> 0 ) & f is_differentiable_on X & g is_differentiable_on X holds f / g is_differentiable_on X let g, f be PartFunc of REAL,REAL; ::_thesis: ( ( for x being set st x in X holds g . x <> 0 ) & f is_differentiable_on X & g is_differentiable_on X implies f / g is_differentiable_on X ) assume that A1: for x being set st x in X holds g . x <> 0 and A2: f is_differentiable_on X and A3: g is_differentiable_on X ; ::_thesis: f / g is_differentiable_on X reconsider Z = X as Subset of REAL by A2, FDIFF_1:8; reconsider Z = Z as open Subset of REAL by A2, FDIFF_1:10; for x being Real st x in Z holds g . x <> 0 by A1; hence f / g is_differentiable_on X by A2, A3, FDIFF_2:21; ::_thesis: verum end; theorem :: INTEGRA7:9 for X being set for f being PartFunc of REAL,REAL st ( for x being set st x in X holds f . x <> 0 ) & f is_differentiable_on X holds f ^ is_differentiable_on X proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st ( for x being set st x in X holds f . x <> 0 ) & f is_differentiable_on X holds f ^ is_differentiable_on X let f be PartFunc of REAL,REAL; ::_thesis: ( ( for x being set st x in X holds f . x <> 0 ) & f is_differentiable_on X implies f ^ is_differentiable_on X ) assume that A1: for x being set st x in X holds f . x <> 0 and A2: f is_differentiable_on X ; ::_thesis: f ^ is_differentiable_on X reconsider Z = X as Subset of REAL by A2, FDIFF_1:8; reconsider Z = Z as open Subset of REAL by A2, FDIFF_1:10; for x being Real st x in Z holds f . x <> 0 by A1; hence f ^ is_differentiable_on X by A2, FDIFF_2:22; ::_thesis: verum end; theorem Th10: :: INTEGRA7:10 for a, b being real number for X being set for F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded holds F . b = (integral ((F `| X),a,b)) + (F . a) proof let a, b be real number ; ::_thesis: for X being set for F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded holds F . b = (integral ((F `| X),a,b)) + (F . a) let X be set ; ::_thesis: for F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded holds F . b = (integral ((F `| X),a,b)) + (F . a) let F be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded implies F . b = (integral ((F `| X),a,b)) + (F . a) ) assume that A1: a <= b and A2: ( ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded ) ; ::_thesis: F . b = (integral ((F `| X),a,b)) + (F . a) integral ((F `| X),a,b) = integral ((F `| X),['a,b']) by A1, INTEGRA5:def_4; then A3: integral ((F `| X),a,b) = (F . (upper_bound ['a,b'])) - (F . (lower_bound ['a,b'])) by A2, INTEGRA5:13; A4: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A5: [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] by INTEGRA1:4; then a = lower_bound [.a,b.] by A4, INTEGRA1:5; hence F . b = (integral ((F `| X),a,b)) + (F . a) by A4, A5, A3, INTEGRA1:5; ::_thesis: verum end; begin definition let X be set ; let f be PartFunc of REAL,REAL; func IntegralFuncs (f,X) -> set means :Def1: :: INTEGRA7:def 1 for x being set holds ( x in it iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) proof defpred S1[ set ] means ex F being PartFunc of REAL,REAL st ( \$1 = F & F is_differentiable_on X & F `| X = f | X ); consider Z being set such that A1: for x being set holds ( x in Z iff ( x in PFuncs (REAL,REAL) & S1[x] ) ) from XBOOLE_0:sch_1(); take Z ; ::_thesis: for x being set holds ( x in Z iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) let x be set ; ::_thesis: ( x in Z iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) thus ( x in Z implies ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) by A1; ::_thesis: ( ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) implies x in Z ) given F being PartFunc of REAL,REAL such that A2: ( x = F & F is_differentiable_on X & F `| X = f | X ) ; ::_thesis: x in Z F in PFuncs (REAL,REAL) by PARTFUN1:45; hence x in Z by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) & ( for x being set holds ( x in b2 iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) holds b1 = b2 proof let Z1, Z2 be set ; ::_thesis: ( ( for x being set holds ( x in Z1 iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) & ( for x being set holds ( x in Z2 iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) implies Z1 = Z2 ) assume that A3: for x being set holds ( x in Z1 iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) and A4: for x being set holds ( x in Z2 iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) ; ::_thesis: Z1 = Z2 for x being set holds ( x in Z1 iff x in Z2 ) proof let x be set ; ::_thesis: ( x in Z1 iff x in Z2 ) ( x in Z1 iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) by A3; hence ( x in Z1 iff x in Z2 ) by A4; ::_thesis: verum end; hence Z1 = Z2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def1 defines IntegralFuncs INTEGRA7:def_1_:_ for X being set for f being PartFunc of REAL,REAL for b3 being set holds ( b3 = IntegralFuncs (f,X) iff for x being set holds ( x in b3 iff ex F being PartFunc of REAL,REAL st ( x = F & F is_differentiable_on X & F `| X = f | X ) ) ); definition let X be set ; let F, f be PartFunc of REAL,REAL; predF is_integral_of f,X means :Def2: :: INTEGRA7:def 2 F in IntegralFuncs (f,X); end; :: deftheorem Def2 defines is_integral_of INTEGRA7:def_2_:_ for X being set for F, f being PartFunc of REAL,REAL holds ( F is_integral_of f,X iff F in IntegralFuncs (f,X) ); Lm1: for X being set for F, f being PartFunc of REAL,REAL holds ( F is_integral_of f,X iff ( F is_differentiable_on X & F `| X = f | X ) ) proof let X be set ; ::_thesis: for F, f being PartFunc of REAL,REAL holds ( F is_integral_of f,X iff ( F is_differentiable_on X & F `| X = f | X ) ) let F, f be PartFunc of REAL,REAL; ::_thesis: ( F is_integral_of f,X iff ( F is_differentiable_on X & F `| X = f | X ) ) hereby ::_thesis: ( F is_differentiable_on X & F `| X = f | X implies F is_integral_of f,X ) assume F is_integral_of f,X ; ::_thesis: ( F is_differentiable_on X & F `| X = f | X ) then F in IntegralFuncs (f,X) by Def2; then ex F9 being PartFunc of REAL,REAL st ( F = F9 & F9 is_differentiable_on X & F9 `| X = f | X ) by Def1; hence ( F is_differentiable_on X & F `| X = f | X ) ; ::_thesis: verum end; assume ( F is_differentiable_on X & F `| X = f | X ) ; ::_thesis: F is_integral_of f,X then F in IntegralFuncs (f,X) by Def1; hence F is_integral_of f,X by Def2; ::_thesis: verum end; theorem Th11: :: INTEGRA7:11 for X being set for F, f being PartFunc of REAL,REAL st F is_integral_of f,X holds X c= dom F proof let X be set ; ::_thesis: for F, f being PartFunc of REAL,REAL st F is_integral_of f,X holds X c= dom F let F, f be PartFunc of REAL,REAL; ::_thesis: ( F is_integral_of f,X implies X c= dom F ) assume F is_integral_of f,X ; ::_thesis: X c= dom F then F in IntegralFuncs (f,X) by Def2; then ex G being PartFunc of REAL,REAL st ( F = G & G is_differentiable_on X & G `| X = f | X ) by Def1; hence X c= dom F by FDIFF_1:def_6; ::_thesis: verum end; theorem :: INTEGRA7:12 for X being set for F, f, G, g being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds ( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X ) proof let X be set ; ::_thesis: for F, f, G, g being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds ( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X ) let F, f, G, g be PartFunc of REAL,REAL; ::_thesis: ( F is_integral_of f,X & G is_integral_of g,X implies ( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X ) ) assume that A1: F is_integral_of f,X and A2: G is_integral_of g,X ; ::_thesis: ( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X ) A3: G is_differentiable_on X by A2, Lm1; A4: G `| X = g | X by A2, Lm1; then dom (g | X) = X by A3, FDIFF_1:def_7; then (dom g) /\ X = X by RELAT_1:61; then A5: X c= dom g by XBOOLE_1:18; A6: F is_differentiable_on X by A1, Lm1; then A7: F + G is_differentiable_on X by A3, Th6; A8: F `| X = f | X by A1, Lm1; then dom (f | X) = X by A6, FDIFF_1:def_7; then (dom f) /\ X = X by RELAT_1:61; then X c= dom f by XBOOLE_1:18; then A9: X c= (dom f) /\ (dom g) by A5, XBOOLE_1:19; then A10: X c= dom (f + g) by VALUED_1:def_1; A11: now__::_thesis:_for_x_being_Element_of_REAL_st_x_in_dom_((F_+_G)_`|_X)_holds_ ((F_+_G)_`|_X)_._x_=_((f_+_g)_|_X)_._x let x be Element of REAL ; ::_thesis: ( x in dom ((F + G) `| X) implies ((F + G) `| X) . x = ((f + g) | X) . x ) assume x in dom ((F + G) `| X) ; ::_thesis: ((F + G) `| X) . x = ((f + g) | X) . x then A12: x in X by A7, FDIFF_1:def_7; then F | X is_differentiable_in x by A6, FDIFF_1:def_6; then A13: F is_differentiable_in x by A12, Th4; (G `| X) . x = diff (G,x) by A3, A12, FDIFF_1:def_7; then A14: g . x = diff (G,x) by A4, A12, FUNCT_1:49; (F `| X) . x = diff (F,x) by A6, A12, FDIFF_1:def_7; then A15: f . x = diff (F,x) by A8, A12, FUNCT_1:49; G | X is_differentiable_in x by A3, A12, FDIFF_1:def_6; then A16: G is_differentiable_in x by A12, Th4; ((F + G) `| X) . x = diff ((F + G),x) by A7, A12, FDIFF_1:def_7; then ((F + G) `| X) . x = (diff (F,x)) + (diff (G,x)) by A13, A16, FDIFF_1:13; then ((F + G) `| X) . x = (f + g) . x by A10, A12, A15, A14, VALUED_1:def_1; hence ((F + G) `| X) . x = ((f + g) | X) . x by A12, FUNCT_1:49; ::_thesis: verum end; A17: F - G is_differentiable_on X by A6, A3, Th6; A18: X c= dom (f - g) by A9, VALUED_1:12; A19: now__::_thesis:_for_x_being_Element_of_REAL_st_x_in_dom_((F_-_G)_`|_X)_holds_ ((F_-_G)_`|_X)_._x_=_((f_-_g)_|_X)_._x let x be Element of REAL ; ::_thesis: ( x in dom ((F - G) `| X) implies ((F - G) `| X) . x = ((f - g) | X) . x ) assume x in dom ((F - G) `| X) ; ::_thesis: ((F - G) `| X) . x = ((f - g) | X) . x then A20: x in X by A17, FDIFF_1:def_7; then F | X is_differentiable_in x by A6, FDIFF_1:def_6; then A21: F is_differentiable_in x by A20, Th4; (G `| X) . x = diff (G,x) by A3, A20, FDIFF_1:def_7; then A22: g . x = diff (G,x) by A4, A20, FUNCT_1:49; (F `| X) . x = diff (F,x) by A6, A20, FDIFF_1:def_7; then A23: f . x = diff (F,x) by A8, A20, FUNCT_1:49; G | X is_differentiable_in x by A3, A20, FDIFF_1:def_6; then A24: G is_differentiable_in x by A20, Th4; ((F - G) `| X) . x = diff ((F - G),x) by A17, A20, FDIFF_1:def_7; then ((F - G) `| X) . x = (diff (F,x)) - (diff (G,x)) by A21, A24, FDIFF_1:14; then ((F - G) `| X) . x = (f - g) . x by A18, A20, A23, A22, VALUED_1:13; hence ((F - G) `| X) . x = ((f - g) | X) . x by A20, FUNCT_1:49; ::_thesis: verum end; X = dom ((f + g) | X) by A10, RELAT_1:62; then dom ((F + G) `| X) = dom ((f + g) | X) by A7, FDIFF_1:def_7; then (F + G) `| X = (f + g) | X by A11, PARTFUN1:5; hence F + G is_integral_of f + g,X by A7, Lm1; ::_thesis: F - G is_integral_of f - g,X X = dom ((f - g) | X) by A18, RELAT_1:62; then dom ((F - G) `| X) = dom ((f - g) | X) by A17, FDIFF_1:def_7; then (F - G) `| X = (f - g) | X by A19, PARTFUN1:5; hence F - G is_integral_of f - g,X by A17, Lm1; ::_thesis: verum end; theorem :: INTEGRA7:13 for r being real number for X being set for F, f being PartFunc of REAL,REAL st F is_integral_of f,X holds r (#) F is_integral_of r (#) f,X proof let r be real number ; ::_thesis: for X being set for F, f being PartFunc of REAL,REAL st F is_integral_of f,X holds r (#) F is_integral_of r (#) f,X let X be set ; ::_thesis: for F, f being PartFunc of REAL,REAL st F is_integral_of f,X holds r (#) F is_integral_of r (#) f,X let F, f be PartFunc of REAL,REAL; ::_thesis: ( F is_integral_of f,X implies r (#) F is_integral_of r (#) f,X ) assume A1: F is_integral_of f,X ; ::_thesis: r (#) F is_integral_of r (#) f,X then A2: F is_differentiable_on X by Lm1; then A3: r (#) F is_differentiable_on X by Th7; A4: F `| X = f | X by A1, Lm1; then dom (f | X) = X by A2, FDIFF_1:def_7; then (dom f) /\ X = X by RELAT_1:61; then X c= dom f by XBOOLE_1:18; then A5: X c= dom (r (#) f) by VALUED_1:def_5; A6: now__::_thesis:_for_x_being_Element_of_REAL_st_x_in_dom_((r_(#)_F)_`|_X)_holds_ ((r_(#)_F)_`|_X)_._x_=_((r_(#)_f)_|_X)_._x reconsider r1 = r as Real by XREAL_0:def_1; let x be Element of REAL ; ::_thesis: ( x in dom ((r (#) F) `| X) implies ((r (#) F) `| X) . x = ((r (#) f) | X) . x ) assume x in dom ((r (#) F) `| X) ; ::_thesis: ((r (#) F) `| X) . x = ((r (#) f) | X) . x then A7: x in X by A3, FDIFF_1:def_7; then F | X is_differentiable_in x by A2, FDIFF_1:def_6; then A8: F is_differentiable_in x by A7, Th4; ((r (#) F) `| X) . x = diff ((r (#) F),x) by A3, A7, FDIFF_1:def_7; then A9: ((r1 (#) F) `| X) . x = r1 * (diff (F,x)) by A8, FDIFF_1:15; (F `| X) . x = diff (F,x) by A2, A7, FDIFF_1:def_7; then f . x = diff (F,x) by A4, A7, FUNCT_1:49; then ((r (#) F) `| X) . x = (r (#) f) . x by A5, A7, A9, VALUED_1:def_5; hence ((r (#) F) `| X) . x = ((r (#) f) | X) . x by A7, FUNCT_1:49; ::_thesis: verum end; X = dom ((r (#) f) | X) by A5, RELAT_1:62; then dom ((r (#) F) `| X) = dom ((r (#) f) | X) by A3, FDIFF_1:def_7; then (r (#) F) `| X = (r (#) f) | X by A6, PARTFUN1:5; hence r (#) F is_integral_of r (#) f,X by A3, Lm1; ::_thesis: verum end; theorem :: INTEGRA7:14 for X being set for F, f, G, g being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds F (#) G is_integral_of (f (#) G) + (F (#) g),X proof let X be set ; ::_thesis: for F, f, G, g being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds F (#) G is_integral_of (f (#) G) + (F (#) g),X let F, f, G, g be PartFunc of REAL,REAL; ::_thesis: ( F is_integral_of f,X & G is_integral_of g,X implies F (#) G is_integral_of (f (#) G) + (F (#) g),X ) assume that A1: F is_integral_of f,X and A2: G is_integral_of g,X ; ::_thesis: F (#) G is_integral_of (f (#) G) + (F (#) g),X A3: G is_differentiable_on X by A2, Lm1; A4: X c= dom F by A1, Th11; A5: G `| X = g | X by A2, Lm1; then dom (g | X) = X by A3, FDIFF_1:def_7; then (dom g) /\ X = X by RELAT_1:61; then X c= dom g by XBOOLE_1:18; then X c= (dom F) /\ (dom g) by A4, XBOOLE_1:19; then A6: X c= dom (F (#) g) by VALUED_1:def_4; A7: X c= dom G by A2, Th11; A8: F is_differentiable_on X by A1, Lm1; then A9: F (#) G is_differentiable_on X by A3, Th6; A10: F `| X = f | X by A1, Lm1; then dom (f | X) = X by A8, FDIFF_1:def_7; then (dom f) /\ X = X by RELAT_1:61; then X c= dom f by XBOOLE_1:18; then X c= (dom f) /\ (dom G) by A7, XBOOLE_1:19; then X c= dom (f (#) G) by VALUED_1:def_4; then X c= (dom (f (#) G)) /\ (dom (F (#) g)) by A6, XBOOLE_1:19; then A11: X c= dom ((f (#) G) + (F (#) g)) by VALUED_1:def_1; A12: now__::_thesis:_for_x_being_Element_of_REAL_st_x_in_dom_((F_(#)_G)_`|_X)_holds_ ((F_(#)_G)_`|_X)_._x_=_(((F_(#)_g)_+_(f_(#)_G))_|_X)_._x let x be Element of REAL ; ::_thesis: ( x in dom ((F (#) G) `| X) implies ((F (#) G) `| X) . x = (((F (#) g) + (f (#) G)) | X) . x ) assume x in dom ((F (#) G) `| X) ; ::_thesis: ((F (#) G) `| X) . x = (((F (#) g) + (f (#) G)) | X) . x then A13: x in X by A9, FDIFF_1:def_7; then F | X is_differentiable_in x by A8, FDIFF_1:def_6; then A14: F is_differentiable_in x by A13, Th4; (G `| X) . x = diff (G,x) by A3, A13, FDIFF_1:def_7; then g . x = diff (G,x) by A5, A13, FUNCT_1:49; then A15: (F (#) g) . x = (F . x) * (diff (G,x)) by VALUED_1:5; (F `| X) . x = diff (F,x) by A8, A13, FDIFF_1:def_7; then f . x = diff (F,x) by A10, A13, FUNCT_1:49; then A16: (f (#) G) . x = (G . x) * (diff (F,x)) by VALUED_1:5; G | X is_differentiable_in x by A3, A13, FDIFF_1:def_6; then A17: G is_differentiable_in x by A13, Th4; ((F (#) G) `| X) . x = diff ((F (#) G),x) by A9, A13, FDIFF_1:def_7; then ((F (#) G) `| X) . x = ((G . x) * (diff (F,x))) + ((F . x) * (diff (G,x))) by A14, A17, FDIFF_1:16; then ((F (#) G) `| X) . x = ((F (#) g) + (f (#) G)) . x by A11, A13, A15, A16, VALUED_1:def_1; hence ((F (#) G) `| X) . x = (((F (#) g) + (f (#) G)) | X) . x by A13, FUNCT_1:49; ::_thesis: verum end; X = dom (((f (#) G) + (F (#) g)) | X) by A11, RELAT_1:62; then dom ((F (#) G) `| X) = dom (((f (#) G) + (F (#) g)) | X) by A9, FDIFF_1:def_7; then (F (#) G) `| X = ((F (#) g) + (f (#) G)) | X by A12, PARTFUN1:5; hence F (#) G is_integral_of (f (#) G) + (F (#) g),X by A9, Lm1; ::_thesis: verum end; theorem :: INTEGRA7:15 for X being set for G, F, f, g being PartFunc of REAL,REAL st ( for x being set st x in X holds G . x <> 0 ) & F is_integral_of f,X & G is_integral_of g,X holds F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X proof let X be set ; ::_thesis: for G, F, f, g being PartFunc of REAL,REAL st ( for x being set st x in X holds G . x <> 0 ) & F is_integral_of f,X & G is_integral_of g,X holds F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X let G, F, f, g be PartFunc of REAL,REAL; ::_thesis: ( ( for x being set st x in X holds G . x <> 0 ) & F is_integral_of f,X & G is_integral_of g,X implies F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X ) assume that A1: for x being set st x in X holds G . x <> 0 and A2: F is_integral_of f,X and A3: G is_integral_of g,X ; ::_thesis: F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X A4: G is_differentiable_on X by A3, Lm1; A5: X c= dom F by A2, Th11; A6: G `| X = g | X by A3, Lm1; then dom (g | X) = X by A4, FDIFF_1:def_7; then (dom g) /\ X = X by RELAT_1:61; then X c= dom g by XBOOLE_1:18; then X c= (dom F) /\ (dom g) by A5, XBOOLE_1:19; then A7: X c= dom (F (#) g) by VALUED_1:def_4; A8: X c= dom G by A3, Th11; A9: F is_differentiable_on X by A2, Lm1; then A10: F / G is_differentiable_on X by A1, A4, Th8; A11: F `| X = f | X by A2, Lm1; then dom (f | X) = X by A9, FDIFF_1:def_7; then (dom f) /\ X = X by RELAT_1:61; then X c= dom f by XBOOLE_1:18; then X c= (dom f) /\ (dom G) by A8, XBOOLE_1:19; then X c= dom (f (#) G) by VALUED_1:def_4; then X c= (dom (f (#) G)) /\ (dom (F (#) g)) by A7, XBOOLE_1:19; then A12: X c= dom ((f (#) G) - (F (#) g)) by VALUED_1:12; A13: now__::_thesis:_for_x_being_Element_of_REAL_st_x_in_dom_((F_/_G)_`|_X)_holds_ ((F_/_G)_`|_X)_._x_=_((((f_(#)_G)_-_(F_(#)_g))_/_(G_(#)_G))_|_X)_._x let x be Element of REAL ; ::_thesis: ( x in dom ((F / G) `| X) implies ((F / G) `| X) . x = ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) . x ) X = (dom G) /\ X by A3, Th11, XBOOLE_1:28; then A14: X = dom (G | X) by RELAT_1:61; assume x in dom ((F / G) `| X) ; ::_thesis: ((F / G) `| X) . x = ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) . x then A15: x in X by A10, FDIFF_1:def_7; then F | X is_differentiable_in x by A9, FDIFF_1:def_6; then A16: F is_differentiable_in x by A15, Th4; G | X is_differentiable_in x by A4, A15, FDIFF_1:def_6; then A17: G is_differentiable_in x by A15, Th4; G . x = (G | X) . x by A15, FUNCT_1:49; then A18: (G . x) ^2 = ((G | X) (#) (G | X)) . x by VALUED_1:5; now__::_thesis:_for_y_being_set_st_y_in_dom_(G_|_X)_holds_ not_y_in_(G_|_X)_"_{0} let y be set ; ::_thesis: ( y in dom (G | X) implies not y in (G | X) " {0} ) assume A19: y in dom (G | X) ; ::_thesis: not y in (G | X) " {0} then y in (dom G) /\ X by RELAT_1:61; then y in X by XBOOLE_0:def_4; then A20: G . y <> 0 by A1; (G | X) . y = G . y by A19, FUNCT_1:47; then not (G | X) . y in {0} by A20, TARSKI:def_1; hence not y in (G | X) " {0} by FUNCT_1:def_7; ::_thesis: verum end; then not x in (G | X) " {0} by A15, A14; then x in ((dom (G | X)) \ ((G | X) " {0})) /\ ((dom (G | X)) \ ((G | X) " {0})) by A15, A14, XBOOLE_0:def_5; then x in (dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0}) by RFUNCT_1:2; then x in (dom ((f (#) G) - (F (#) g))) /\ ((dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0})) by A12, A15, XBOOLE_0:def_4; then A21: x in dom (((f (#) G) - (F (#) g)) / ((G | X) (#) (G | X))) by RFUNCT_1:def_1; (G `| X) . x = diff (G,x) by A4, A15, FDIFF_1:def_7; then g . x = diff (G,x) by A6, A15, FUNCT_1:49; then A22: (F (#) g) . x = (F . x) * (diff (G,x)) by VALUED_1:5; (F `| X) . x = diff (F,x) by A9, A15, FDIFF_1:def_7; then f . x = diff (F,x) by A11, A15, FUNCT_1:49; then (f (#) G) . x = (G . x) * (diff (F,x)) by VALUED_1:5; then A23: ((f (#) G) - (F (#) g)) . x = ((diff (F,x)) * (G . x)) - ((diff (G,x)) * (F . x)) by A12, A15, A22, VALUED_1:13; ( ((F / G) `| X) . x = diff ((F / G),x) & G . x <> 0 ) by A1, A10, A15, FDIFF_1:def_7; then ((F / G) `| X) . x = (((diff (F,x)) * (G . x)) - ((diff (G,x)) * (F . x))) / ((G . x) ^2) by A16, A17, FDIFF_2:14; then ((F / G) `| X) . x = (((f (#) G) - (F (#) g)) / ((G | X) (#) (G | X))) . x by A21, A23, A18, RFUNCT_1:def_1; then ((F / G) `| X) . x = (((f (#) G) - (F (#) g)) / ((G (#) G) | X)) . x by RFUNCT_1:45; hence ((F / G) `| X) . x = ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) . x by RFUNCT_1:48; ::_thesis: verum end; now__::_thesis:_not_(G_|_X)_"_{0}_<>_{} assume (G | X) " {0} <> {} ; ::_thesis: contradiction then consider y being set such that A24: y in (G | X) " {0} by XBOOLE_0:def_1; A25: y in dom (G | X) by A24, FUNCT_1:def_7; then A26: (G | X) . y = G . y by FUNCT_1:47; y in (dom G) /\ X by A25, RELAT_1:61; then y in X by XBOOLE_0:def_4; then A27: G . y <> 0 by A1; (G | X) . y in {0} by A24, FUNCT_1:def_7; hence contradiction by A27, A26, TARSKI:def_1; ::_thesis: verum end; then ((dom (G | X)) \ ((G | X) " {0})) /\ ((dom (G | X)) \ ((G | X) " {0})) = dom (G | X) ; then (dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0}) = dom (G | X) by RFUNCT_1:2; then (dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0}) = (dom G) /\ X by RELAT_1:61; then A28: (dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0}) = X by A3, Th11, XBOOLE_1:28; X = dom (((f (#) G) - (F (#) g)) | X) by A12, RELAT_1:62; then (dom (((f (#) G) - (F (#) g)) | X)) /\ ((dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0})) = X by A28; then dom ((((f (#) G) - (F (#) g)) | X) / ((G | X) (#) (G | X))) = X by RFUNCT_1:def_1; then dom ((((f (#) G) - (F (#) g)) | X) / ((G (#) G) | X)) = X by RFUNCT_1:45; then dom ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) = X by RFUNCT_1:48; then dom ((F / G) `| X) = dom ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) by A10, FDIFF_1:def_7; then (F / G) `| X = (((f (#) G) - (F (#) g)) / (G (#) G)) | X by A13, PARTFUN1:5; hence F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X by A10, Lm1; ::_thesis: verum end; theorem :: INTEGRA7:16 for a, b being real number for f, F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f | ['a,b'] is continuous & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = (integral (f,a,x)) + (F . a) ) holds F is_integral_of f,].a,b.[ proof let a, b be real number ; ::_thesis: for f, F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f | ['a,b'] is continuous & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = (integral (f,a,x)) + (F . a) ) holds F is_integral_of f,].a,b.[ let f, F be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & f | ['a,b'] is continuous & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = (integral (f,a,x)) + (F . a) ) implies F is_integral_of f,].a,b.[ ) set O = ].a,b.[; assume that A1: a <= b and A2: ['a,b'] c= dom f and A3: f | ['a,b'] is continuous and A4: ].a,b.[ c= dom F and A5: for x being real number st x in ].a,b.[ holds F . x = (integral (f,a,x)) + (F . a) ; ::_thesis: F is_integral_of f,].a,b.[ dom (F | ].a,b.[) = (dom F) /\ ].a,b.[ by PARTFUN2:15; then A6: dom (F | ].a,b.[) = ].a,b.[ by A4, XBOOLE_1:28; set H1 = REAL --> (F . a); deffunc H1( Element of REAL ) -> Element of REAL = integral (f,a,\$1); consider G1 being Function of REAL,REAL such that A7: for h being Real holds G1 . h = H1(h) from FUNCT_2:sch_4(); reconsider H = (REAL --> (F . a)) | ].a,b.[ as PartFunc of REAL,REAL ; reconsider G = G1 | ].a,b.[ as PartFunc of REAL,REAL ; dom H = (dom (REAL --> (F . a))) /\ ].a,b.[ by RELAT_1:61; then A8: dom H = REAL /\ ].a,b.[ by FUNCT_2:def_1; then A9: dom H = ].a,b.[ by XBOOLE_1:28; now__::_thesis:_for_x_being_Element_of_REAL_st_x_in_].a,b.[_/\_(dom_H)_holds_ H_/._x_=_F_._a let x be Element of REAL ; ::_thesis: ( x in ].a,b.[ /\ (dom H) implies H /. x = F . a ) reconsider z = x as real number ; assume A10: x in ].a,b.[ /\ (dom H) ; ::_thesis: H /. x = F . a then H . x = (REAL --> (F . a)) . z by A9, FUNCT_1:47; then H . x = F . a by FUNCOP_1:7; hence H /. x = F . a by A9, A10, PARTFUN1:def_6; ::_thesis: verum end; then A11: H | ].a,b.[ is V20() by PARTFUN2:35; then A12: H is_differentiable_on ].a,b.[ by A9, FDIFF_1:22; dom G = (dom G1) /\ ].a,b.[ by RELAT_1:61; then A13: dom G = REAL /\ ].a,b.[ by FUNCT_2:def_1; then A14: ].a,b.[ = dom G by XBOOLE_1:28; A15: now__::_thesis:_for_x_being_real_number_st_x_in_].a,b.[_holds_ G_._x_=_integral_(f,a,x) let x be real number ; ::_thesis: ( x in ].a,b.[ implies G . x = integral (f,a,x) ) reconsider z = x as Real by XREAL_0:def_1; assume x in ].a,b.[ ; ::_thesis: G . x = integral (f,a,x) then G . x = G1 . x by A14, FUNCT_1:47; then G . x = integral (f,a,z) by A7; hence G . x = integral (f,a,x) ; ::_thesis: verum end; A16: now__::_thesis:_for_x_being_set_st_x_in_dom_(F_|_].a,b.[)_holds_ (F_|_].a,b.[)_._x_=_(G_._x)_+_(H_._x) let x be set ; ::_thesis: ( x in dom (F | ].a,b.[) implies (F | ].a,b.[) . x = (G . x) + (H . x) ) assume A17: x in dom (F | ].a,b.[) ; ::_thesis: (F | ].a,b.[) . x = (G . x) + (H . x) then reconsider z = x as real number ; reconsider z1 = z as Real by XREAL_0:def_1; H . x = (REAL --> (F . a)) . z1 by A9, A6, A17, FUNCT_1:47; then A18: H . x = F . a by FUNCOP_1:7; (F | ].a,b.[) . x = F . z by A17, FUNCT_1:47; then (F | ].a,b.[) . x = (integral (f,a,z)) + (F . a) by A5, A6, A17; hence (F | ].a,b.[) . x = (G . x) + (H . x) by A15, A6, A17, A18; ::_thesis: verum end; A19: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A20: ].a,b.[ c= ['a,b'] by XXREAL_1:25; then A21: ].a,b.[ c= dom f by A2, XBOOLE_1:1; A22: for x being Real st x in ].a,b.[ holds ( G is_differentiable_in x & diff (G,x) = f . x ) proof let x be Real; ::_thesis: ( x in ].a,b.[ implies ( G is_differentiable_in x & diff (G,x) = f . x ) ) reconsider z = x as real number ; A23: f | ].a,b.[ is continuous by A3, A19, FCONT_1:16, XXREAL_1:25; assume A24: x in ].a,b.[ ; ::_thesis: ( G is_differentiable_in x & diff (G,x) = f . x ) then x in dom (f | ].a,b.[) by A21, RELAT_1:57; then A25: f | ].a,b.[ is_continuous_in z by A23, FCONT_1:def_2; for r being real number st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - z) < s holds abs ((f . x1) - (f . z)) < r ) ) proof let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - z) < s holds abs ((f . x1) - (f . z)) < r ) ) ) consider ss1 being real number such that A26: 0 < ss1 and A27: ].(z - ss1),(z + ss1).[ c= ].a,b.[ by A24, RCOMP_1:19; assume 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - z) < s holds abs ((f . x1) - (f . z)) < r ) ) then consider s being real number such that A28: 0 < s and A29: for x1 being real number st x1 in dom (f | ].a,b.[) & abs (x1 - z) < s holds abs (((f | ].a,b.[) . x1) - ((f | ].a,b.[) . z)) < r by A25, FCONT_1:3; set s1 = min (ss1,s); take min (ss1,s) ; ::_thesis: ( 0 < min (ss1,s) & ( for x1 being real number st x1 in dom f & abs (x1 - z) < min (ss1,s) holds abs ((f . x1) - (f . z)) < r ) ) now__::_thesis:_for_x1_being_real_number_st_x1_in_dom_f_&_abs_(x1_-_z)_<_min_(ss1,s)_holds_ abs_((f_._x1)_-_(f_._z))_<_r let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - z) < min (ss1,s) implies abs ((f . x1) - (f . z)) < r ) assume that x1 in dom f and A30: abs (x1 - z) < min (ss1,s) ; ::_thesis: abs ((f . x1) - (f . z)) < r min (ss1,s) <= s by XXREAL_0:17; then A31: abs (x1 - z) < s by A30, XXREAL_0:2; ].a,b.[ = ].a,b.[ /\ (dom f) by A2, A20, XBOOLE_1:1, XBOOLE_1:28; then A32: ].a,b.[ = dom (f | ].a,b.[) by PARTFUN2:15; min (ss1,s) <= ss1 by XXREAL_0:17; then abs (x1 - z) < ss1 by A30, XXREAL_0:2; then A33: x1 in ].(z - ss1),(z + ss1).[ by RCOMP_1:1; then abs ((f . x1) - (f . z)) = abs (((f | ].a,b.[) . x1) - (f . z)) by A27, A32, FUNCT_1:47; then abs ((f . x1) - (f . z)) = abs (((f | ].a,b.[) . x1) - ((f | ].a,b.[) . z)) by A24, A32, FUNCT_1:47; hence abs ((f . x1) - (f . z)) < r by A29, A27, A31, A33, A32; ::_thesis: verum end; hence ( 0 < min (ss1,s) & ( for x1 being real number st x1 in dom f & abs (x1 - z) < min (ss1,s) holds abs ((f . x1) - (f . z)) < r ) ) by A28, A26, XXREAL_0:15; ::_thesis: verum end; then A34: f is_continuous_in z by FCONT_1:3; ( f | ['a,b'] is bounded & f is_integrable_on ['a,b'] ) by A2, A3, INTEGRA5:10, INTEGRA5:11; hence ( G is_differentiable_in x & diff (G,x) = f . x ) by A1, A2, A14, A15, A24, A34, INTEGRA6:28; ::_thesis: verum end; then for x being Real st x in ].a,b.[ holds G is_differentiable_in x ; then A35: G is_differentiable_on ].a,b.[ by A14, FDIFF_1:9; dom (F | ].a,b.[) = (dom G) /\ (dom H) by A13, A8, A6, XBOOLE_1:28; then A36: F | ].a,b.[ = G + H by A16, VALUED_1:def_1; then F | ].a,b.[ is_differentiable_on ].a,b.[ by A35, A12, A6, FDIFF_1:18; then for x being Real st x in ].a,b.[ holds F | ].a,b.[ is_differentiable_in x by FDIFF_1:9; then A37: F is_differentiable_on ].a,b.[ by A4, FDIFF_1:def_6; A38: now__::_thesis:_for_x_being_Real_st_x_in_dom_(F_`|_].a,b.[)_holds_ (F_`|_].a,b.[)_._x_=_(f_|_].a,b.[)_._x let x be Real; ::_thesis: ( x in dom (F `| ].a,b.[) implies (F `| ].a,b.[) . x = (f | ].a,b.[) . x ) assume x in dom (F `| ].a,b.[) ; ::_thesis: (F `| ].a,b.[) . x = (f | ].a,b.[) . x then A39: x in ].a,b.[ by A37, FDIFF_1:def_7; then x in (dom f) /\ ].a,b.[ by A21, XBOOLE_0:def_4; then A40: x in dom (f | ].a,b.[) by PARTFUN2:15; (F `| ].a,b.[) . x = ((F | ].a,b.[) `| ].a,b.[) . x by A37, FDIFF_2:16; then (F `| ].a,b.[) . x = (diff (G,x)) + (diff (H,x)) by A35, A12, A6, A36, A39, FDIFF_1:18; then A41: (F `| ].a,b.[) . x = (f . x) + (diff (H,x)) by A22, A39; (H `| ].a,b.[) . x = 0 by A9, A11, A39, FDIFF_1:22; then diff (H,x) = 0 by A12, A39, FDIFF_1:def_7; hence (F `| ].a,b.[) . x = (f | ].a,b.[) . x by A40, A41, FUNCT_1:47; ::_thesis: verum end; dom (F `| ].a,b.[) = ].a,b.[ by A37, FDIFF_1:def_7; then dom (F `| ].a,b.[) = ].a,b.[ /\ (dom f) by A2, A20, XBOOLE_1:1, XBOOLE_1:28; then dom (F `| ].a,b.[) = dom (f | ].a,b.[) by PARTFUN2:15; then F `| ].a,b.[ = f | ].a,b.[ by A38, PARTFUN1:5; hence F is_integral_of f,].a,b.[ by A37, Lm1; ::_thesis: verum end; theorem :: INTEGRA7:17 for a, b being real number for f, F being PartFunc of REAL,REAL for x, x0 being real number st f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds F . x = (integral (f,x0,x)) + (F . x0) proof let a, b be real number ; ::_thesis: for f, F being PartFunc of REAL,REAL for x, x0 being real number st f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds F . x = (integral (f,x0,x)) + (F . x0) let f, F be PartFunc of REAL,REAL; ::_thesis: for x, x0 being real number st f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds F . x = (integral (f,x0,x)) + (F . x0) let x, x0 be real number ; ::_thesis: ( f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ implies F . x = (integral (f,x0,x)) + (F . x0) ) set O = ].a,b.[; assume that A1: f | [.a,b.] is continuous and A2: [.a,b.] c= dom f and A3: ( x in ].a,b.[ & x0 in ].a,b.[ ) and A4: F is_integral_of f,].a,b.[ ; ::_thesis: F . x = (integral (f,x0,x)) + (F . x0) A5: ( F is_differentiable_on ].a,b.[ & F `| ].a,b.[ = f | ].a,b.[ ) by A4, Lm1; A6: ].a,b.[ c= [.a,b.] by XXREAL_1:25; A7: [.x,x0.] c= ].a,b.[ by A3, XXREAL_2:def_12; A8: now__::_thesis:_(_x_<_x0_implies_F_._x_=_(integral_(f,x0,x))_+_(F_._x0)_) assume A9: x < x0 ; ::_thesis: F . x = (integral (f,x0,x)) + (F . x0) then A10: ['x,x0'] c= ].a,b.[ by A7, INTEGRA5:def_3; then A11: f | ['x,x0'] is continuous by A1, A6, FCONT_1:16, XBOOLE_1:1; (F `| ].a,b.[) || ['x,x0'] = (f | ].a,b.[) | ['x,x0'] by A4, Lm1; then A12: (F `| ].a,b.[) || ['x,x0'] = f || ['x,x0'] by A10, FUNCT_1:51; A13: ['x,x0'] c= [.a,b.] by A6, A10, XBOOLE_1:1; then ['x,x0'] c= dom f by A2, XBOOLE_1:1; then f is_integrable_on ['x,x0'] by A11, INTEGRA5:17; then f || ['x,x0'] is integrable by INTEGRA5:def_1; then A14: F `| ].a,b.[ is_integrable_on ['x,x0'] by A12, INTEGRA5:def_1; (F `| ].a,b.[) | ['x,x0'] is bounded by A2, A12, A13, A11, INTEGRA5:10, XBOOLE_1:1; then F . x0 = (integral ((f | ].a,b.[),x,x0)) + (F . x) by A5, A9, A10, A14, Th10; then F . x0 = (integral ((f | ].a,b.[),['x,x0'])) + (F . x) by A9, INTEGRA5:def_4; then F . x0 = (integral (f,['x,x0'])) + (F . x) by A10, FUNCT_1:51; then A15: F . x0 = (integral (f,x,x0)) + (F . x) by A9, INTEGRA5:def_4; integral (f,x0,x) = - (integral (f,['x,x0'])) by A9, INTEGRA5:def_4; then integral (f,x0,x) = - (integral (f,x,x0)) by A9, INTEGRA5:def_4; hence F . x = (integral (f,x0,x)) + (F . x0) by A15; ::_thesis: verum end; A16: [.x0,x.] c= ].a,b.[ by A3, XXREAL_2:def_12; now__::_thesis:_(_x0_<=_x_implies_F_._x_=_(integral_(f,x0,x))_+_(F_._x0)_) assume A17: x0 <= x ; ::_thesis: F . x = (integral (f,x0,x)) + (F . x0) then A18: ['x0,x'] c= ].a,b.[ by A16, INTEGRA5:def_3; then A19: f | ['x0,x'] is continuous by A1, A6, FCONT_1:16, XBOOLE_1:1; (F `| ].a,b.[) || ['x0,x'] = (f | ].a,b.[) | ['x0,x'] by A4, Lm1; then A20: (F `| ].a,b.[) || ['x0,x'] = f || ['x0,x'] by A18, FUNCT_1:51; ['x0,x'] c= [.a,b.] by A6, A18, XBOOLE_1:1; then A21: ['x0,x'] c= dom f by A2, XBOOLE_1:1; f | ['x0,x'] is continuous by A1, A6, A18, FCONT_1:16, XBOOLE_1:1; then f is_integrable_on ['x0,x'] by A21, INTEGRA5:17; then f || ['x0,x'] is integrable by INTEGRA5:def_1; then F `| ].a,b.[ is_integrable_on ['x0,x'] by A20, INTEGRA5:def_1; then F . x = (integral ((f | ].a,b.[),x0,x)) + (F . x0) by A5, A17, A18, A20, A21, A19, Th10, INTEGRA5:10; then F . x = (integral ((f | ].a,b.[),['x0,x'])) + (F . x0) by A17, INTEGRA5:def_4; then F . x = (integral (f,['x0,x'])) + (F . x0) by A18, FUNCT_1:51; hence F . x = (integral (f,x0,x)) + (F . x0) by A17, INTEGRA5:def_4; ::_thesis: verum end; hence F . x = (integral (f,x0,x)) + (F . x0) by A8; ::_thesis: verum end; theorem Th18: :: INTEGRA7:18 for a, b being real number for X being set for F, f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_integral_of f,X & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds F . b = (integral (f,a,b)) + (F . a) proof let a, b be real number ; ::_thesis: for X being set for F, f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_integral_of f,X & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds F . b = (integral (f,a,b)) + (F . a) let X be set ; ::_thesis: for F, f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_integral_of f,X & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds F . b = (integral (f,a,b)) + (F . a) let F, f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= X & F is_integral_of f,X & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies F . b = (integral (f,a,b)) + (F . a) ) assume that A1: a <= b and A2: ['a,b'] c= X ; ::_thesis: ( not F is_integral_of f,X or not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or F . b = (integral (f,a,b)) + (F . a) ) assume A3: F is_integral_of f,X ; ::_thesis: ( not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or F . b = (integral (f,a,b)) + (F . a) ) then A4: ( F is_differentiable_on X & F `| X = f | X ) by Lm1; assume f is_integrable_on ['a,b'] ; ::_thesis: ( not f | ['a,b'] is bounded or F . b = (integral (f,a,b)) + (F . a) ) then A5: f || ['a,b'] is integrable by INTEGRA5:def_1; assume A6: f | ['a,b'] is bounded ; ::_thesis: F . b = (integral (f,a,b)) + (F . a) (F `| X) || ['a,b'] = (f | X) | ['a,b'] by A3, Lm1; then A7: (F `| X) || ['a,b'] = f || ['a,b'] by A2, FUNCT_1:51; then F `| X is_integrable_on ['a,b'] by A5, INTEGRA5:def_1; then F . b = (integral ((f | X),a,b)) + (F . a) by A1, A2, A4, A7, A6, Th10; then F . b = (integral ((f | X),['a,b'])) + (F . a) by A1, INTEGRA5:def_4; then F . b = (integral (f,['a,b'])) + (F . a) by A2, FUNCT_1:51; hence F . b = (integral (f,a,b)) + (F . a) by A1, INTEGRA5:def_4; ::_thesis: verum end; theorem Th19: :: INTEGRA7:19 for a, b being real number for X being set for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous holds ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) proof let a, b be real number ; ::_thesis: for X being set for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous holds ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous holds ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous implies ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) assume a <= b ; ::_thesis: ( not [.a,b.] c= X or not X c= dom f or not f | X is continuous or ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) then A1: [.a,b.] = ['a,b'] by INTEGRA5:def_3; assume that A2: [.a,b.] c= X and A3: X c= dom f and A4: f | X is continuous ; ::_thesis: ( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) thus A5: f | ['a,b'] is continuous by A1, A2, A4, FCONT_1:16; ::_thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) [.a,b.] c= dom f by A2, A3, XBOOLE_1:1; hence ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, A5, INTEGRA5:10, INTEGRA5:17; ::_thesis: verum end; theorem Th20: :: INTEGRA7:20 for a, b being real number for X being set for f, F being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous & F is_integral_of f,X holds F . b = (integral (f,a,b)) + (F . a) proof let a, b be real number ; ::_thesis: for X being set for f, F being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous & F is_integral_of f,X holds F . b = (integral (f,a,b)) + (F . a) let X be set ; ::_thesis: for f, F being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous & F is_integral_of f,X holds F . b = (integral (f,a,b)) + (F . a) let f, F be PartFunc of REAL,REAL; ::_thesis: ( a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous & F is_integral_of f,X implies F . b = (integral (f,a,b)) + (F . a) ) assume that A1: a <= b and A2: [.a,b.] c= X and A3: X c= dom f ; ::_thesis: ( not f | X is continuous or not F is_integral_of f,X or F . b = (integral (f,a,b)) + (F . a) ) assume f | X is continuous ; ::_thesis: ( not F is_integral_of f,X or F . b = (integral (f,a,b)) + (F . a) ) then A4: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, A2, A3, Th19; A5: [.a,b.] = ['a,b'] by A1, INTEGRA5:def_3; assume F is_integral_of f,X ; ::_thesis: F . b = (integral (f,a,b)) + (F . a) hence F . b = (integral (f,a,b)) + (F . a) by A1, A2, A5, A4, Th18; ::_thesis: verum end; theorem Th21: :: INTEGRA7:21 for b, a being real number for X being set for f, g, F, G being PartFunc of REAL,REAL st b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X holds ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) proof let b, a be real number ; ::_thesis: for X being set for f, g, F, G being PartFunc of REAL,REAL st b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X holds ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) let X be set ; ::_thesis: for f, g, F, G being PartFunc of REAL,REAL st b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X holds ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) let f, g, F, G be PartFunc of REAL,REAL; ::_thesis: ( b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X implies ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) ) assume that A1: b <= a and A2: ['b,a'] c= X and A3: f is_integrable_on ['b,a'] and A4: g is_integrable_on ['b,a'] and A5: f | ['b,a'] is bounded and A6: g | ['b,a'] is bounded ; ::_thesis: ( not X c= dom f or not X c= dom g or not F is_integral_of f,X or not G is_integral_of g,X or ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) ) set I = ['b,a']; assume that A7: X c= dom f and A8: X c= dom g and A9: F is_integral_of f,X and A10: G is_integral_of g,X ; ::_thesis: ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) A11: X c= dom G by A10, Th11; then A12: ['b,a'] c= dom G by A2, XBOOLE_1:1; A13: G is_differentiable_on X by A10, Lm1; then A14: G | X is continuous by FDIFF_1:25; then A15: G | ['b,a'] is bounded by A2, A12, FCONT_1:16, INTEGRA5:10; then A16: (f (#) G) | (['b,a'] /\ ['b,a']) is bounded by A5, RFUNCT_1:84; A17: X c= dom F by A9, Th11; then A18: ['b,a'] c= dom F by A2, XBOOLE_1:1; A19: F is_differentiable_on X by A9, Lm1; then A20: X is open Subset of REAL by FDIFF_1:8, FDIFF_1:10; A21: F | X is continuous by A19, FDIFF_1:25; then A22: F | ['b,a'] is bounded by A2, A18, FCONT_1:16, INTEGRA5:10; then A23: (F (#) g) | (['b,a'] /\ ['b,a']) is bounded by A6, RFUNCT_1:84; then A24: ((f (#) G) + (F (#) g)) | (['b,a'] /\ ['b,a']) is bounded by A16, RFUNCT_1:83; F | ['b,a'] is continuous by A2, A21, FCONT_1:16; then A25: F is_integrable_on ['b,a'] by A18, INTEGRA5:17; ['b,a'] c= dom g by A2, A8, XBOOLE_1:1; then A26: F (#) g is_integrable_on ['b,a'] by A4, A6, A18, A25, A22, INTEGRA6:14; ( F `| X = f | X & G `| X = g | X ) by A9, A10, Lm1; then (F (#) G) `| X = ((f | X) (#) G) + (F (#) (g | X)) by A19, A13, A20, FDIFF_2:20; then (F (#) G) `| X = ((f (#) G) | X) + (F (#) (g | X)) by RFUNCT_1:45; then (F (#) G) `| X = ((f (#) G) | X) + ((F (#) g) | X) by RFUNCT_1:45; then A27: (F (#) G) `| X = ((f (#) G) + (F (#) g)) | X by RFUNCT_1:44; F (#) G is_differentiable_on X by A19, A13, A20, FDIFF_2:20; then A28: F (#) G is_integral_of (f (#) G) + (F (#) g),X by A27, Lm1; min (b,a) = b by A1, XXREAL_0:def_9; then A29: max (b,a) = a by XXREAL_0:36; ( b <= max (b,a) & [.b,a.] = ['b,a'] ) by A1, INTEGRA5:def_3, XXREAL_0:25; then A30: ( b in ['b,a'] & a in ['b,a'] ) by A29, XXREAL_1:1; X c= (dom F) /\ (dom g) by A8, A17, XBOOLE_1:19; then X c= dom (F (#) g) by VALUED_1:def_4; then A31: ['b,a'] c= dom (F (#) g) by A2, XBOOLE_1:1; G | ['b,a'] is continuous by A2, A14, FCONT_1:16; then A32: G is_integrable_on ['b,a'] by A12, INTEGRA5:17; X c= (dom f) /\ (dom G) by A7, A11, XBOOLE_1:19; then X c= dom (f (#) G) by VALUED_1:def_4; then A33: ['b,a'] c= dom (f (#) G) by A2, XBOOLE_1:1; ['b,a'] c= dom f by A2, A7, XBOOLE_1:1; then A34: f (#) G is_integrable_on ['b,a'] by A3, A5, A12, A32, A15, INTEGRA6:14; then (f (#) G) + (F (#) g) is_integrable_on ['b,a'] by A33, A31, A26, A16, A23, INTEGRA6:11; then (F (#) G) . a = (integral (((f (#) G) + (F (#) g)),b,a)) + ((F (#) G) . b) by A1, A2, A24, A28, Th18; then ( (F (#) G) . b = (F . b) * (G . b) & ((F (#) G) . a) - ((F (#) G) . b) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) ) by A1, A33, A31, A34, A26, A16, A23, A30, INTEGRA6:24, VALUED_1:5; hence ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) by VALUED_1:5; ::_thesis: verum end; theorem :: INTEGRA7:22 for b, a being real number for X being set for f, g, F, G being PartFunc of REAL,REAL st b <= a & [.b,a.] c= X & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & F is_integral_of f,X & G is_integral_of g,X holds ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) proof let b, a be real number ; ::_thesis: for X being set for f, g, F, G being PartFunc of REAL,REAL st b <= a & [.b,a.] c= X & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & F is_integral_of f,X & G is_integral_of g,X holds ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) let X be set ; ::_thesis: for f, g, F, G being PartFunc of REAL,REAL st b <= a & [.b,a.] c= X & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & F is_integral_of f,X & G is_integral_of g,X holds ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) let f, g, F, G be PartFunc of REAL,REAL; ::_thesis: ( b <= a & [.b,a.] c= X & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & F is_integral_of f,X & G is_integral_of g,X implies ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) ) assume that A1: b <= a and A2: [.b,a.] c= X ; ::_thesis: ( not X c= dom f or not X c= dom g or not f | X is continuous or not g | X is continuous or not F is_integral_of f,X or not G is_integral_of g,X or ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) ) assume that A3: X c= dom f and A4: X c= dom g and A5: f | X is continuous and A6: g | X is continuous and A7: ( F is_integral_of f,X & G is_integral_of g,X ) ; ::_thesis: ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) A8: [.b,a.] c= dom f by A2, A3, XBOOLE_1:1; A9: [.b,a.] = ['b,a'] by A1, INTEGRA5:def_3; then f | ['b,a'] is continuous by A2, A5, FCONT_1:16; then A10: f is_integrable_on ['b,a'] by A8, A9, INTEGRA5:17; A11: [.b,a.] c= dom g by A2, A4, XBOOLE_1:1; then A12: g | ['b,a'] is bounded by A2, A6, A9, FCONT_1:16, INTEGRA5:10; g | ['b,a'] is continuous by A2, A6, A9, FCONT_1:16; then A13: g is_integrable_on ['b,a'] by A11, A9, INTEGRA5:17; f | ['b,a'] is bounded by A2, A5, A8, A9, FCONT_1:16, INTEGRA5:10; hence ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) by A1, A2, A3, A4, A7, A9, A10, A13, A12, Th21; ::_thesis: verum end; begin theorem Th23: :: INTEGRA7:23 sin is_integral_of cos , REAL proof A1: dom (cos | REAL) = REAL /\ REAL by RELAT_1:61, SIN_COS:24; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(sin_`|_REAL)_holds_ (sin_`|_REAL)_._x_=_(cos_|_REAL)_._x let x be set ; ::_thesis: ( x in dom (sin `| REAL) implies (sin `| REAL) . x = (cos | REAL) . x ) assume A3: x in dom (sin `| REAL) ; ::_thesis: (sin `| REAL) . x = (cos | REAL) . x then reconsider z = x as real number ; (sin `| REAL) . x = diff (sin,z) by A3, FDIFF_1:def_7, SIN_COS:68; then (sin `| REAL) . x = cos . z by SIN_COS:64; hence (sin `| REAL) . x = (cos | REAL) . x by A1, A3, FUNCT_1:47; ::_thesis: verum end; dom (sin `| REAL) = REAL by FDIFF_1:def_7, SIN_COS:68; then sin `| REAL = cos | REAL by A1, A2, FUNCT_1:2; hence sin is_integral_of cos , REAL by Lm1, SIN_COS:68; ::_thesis: verum end; theorem :: INTEGRA7:24 for b, a being real number holds (sin . b) - (sin . a) = integral (cos,a,b) proof let b, a be real number ; ::_thesis: (sin . b) - (sin . a) = integral (cos,a,b) A1: min (a,b) <= a by XXREAL_0:17; A2: ( REAL = dom cos & [.(min (a,b)),(max (a,b)).] c= REAL ) by FUNCT_2:def_1; ( cos | REAL is continuous & a <= max (a,b) ) by FDIFF_1:25, SIN_COS:67, XXREAL_0:25; then A3: sin . (max (a,b)) = (integral (cos,(min (a,b)),(max (a,b)))) + (sin . (min (a,b))) by A1, A2, Th20, Th23, XXREAL_0:2; A4: now__::_thesis:_(_min_(a,b)_=_a_implies_(sin_._b)_-_(sin_._a)_=_integral_(cos,a,b)_) assume A5: min (a,b) = a ; ::_thesis: (sin . b) - (sin . a) = integral (cos,a,b) then max (a,b) = b by XXREAL_0:36; hence (sin . b) - (sin . a) = integral (cos,a,b) by A3, A5; ::_thesis: verum end; now__::_thesis:_(_min_(a,b)_=_b_implies_(sin_._b)_-_(sin_._a)_=_integral_(cos,a,b)_) assume A6: min (a,b) = b ; ::_thesis: (sin . b) - (sin . a) = integral (cos,a,b) then A7: max (a,b) = a by XXREAL_0:36; now__::_thesis:_(_b_<_a_implies_(sin_._b)_-_(sin_._a)_=_integral_(cos,a,b)_) assume b < a ; ::_thesis: (sin . b) - (sin . a) = integral (cos,a,b) then integral (cos,a,b) = - (integral (cos,['b,a'])) by INTEGRA5:def_4; then sin . a = (- (integral (cos,a,b))) + (sin . b) by A1, A3, A6, A7, INTEGRA5:def_4; hence (sin . b) - (sin . a) = integral (cos,a,b) ; ::_thesis: verum end; hence (sin . b) - (sin . a) = integral (cos,a,b) by A1, A4, A6, XXREAL_0:1; ::_thesis: verum end; hence (sin . b) - (sin . a) = integral (cos,a,b) by A4, XXREAL_0:15; ::_thesis: verum end; theorem Th25: :: INTEGRA7:25 (- 1) (#) cos is_integral_of sin , REAL proof A1: dom (sin | REAL) = REAL /\ REAL by RELAT_1:61, SIN_COS:24; A2: dom ((- 1) (#) cos) = [#] REAL by SIN_COS:24, VALUED_1:def_5; A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(((-_1)_(#)_cos)_`|_REAL)_holds_ (((-_1)_(#)_cos)_`|_REAL)_._x_=_(sin_|_REAL)_._x let x be set ; ::_thesis: ( x in dom (((- 1) (#) cos) `| REAL) implies (((- 1) (#) cos) `| REAL) . x = (sin | REAL) . x ) assume A4: x in dom (((- 1) (#) cos) `| REAL) ; ::_thesis: (((- 1) (#) cos) `| REAL) . x = (sin | REAL) . x then reconsider z = x as real number ; (((- 1) (#) cos) `| REAL) . x = (- 1) * (diff (cos,z)) by A2, A4, FDIFF_1:20, SIN_COS:67; then (((- 1) (#) cos) `| REAL) . x = (- 1) * (- (sin . z)) by SIN_COS:63; hence (((- 1) (#) cos) `| REAL) . x = (sin | REAL) . x by A1, A4, FUNCT_1:47; ::_thesis: verum end; A5: (- 1) (#) cos is_differentiable_on REAL by A2, FDIFF_1:20, SIN_COS:67; then dom (((- 1) (#) cos) `| REAL) = REAL by FDIFF_1:def_7; then ((- 1) (#) cos) `| REAL = sin | REAL by A1, A3, FUNCT_1:2; hence (- 1) (#) cos is_integral_of sin , REAL by A5, Lm1; ::_thesis: verum end; theorem :: INTEGRA7:26 for a, b being real number holds (cos . a) - (cos . b) = integral (sin,a,b) proof let a, b be real number ; ::_thesis: (cos . a) - (cos . b) = integral (sin,a,b) A1: min (a,b) <= a by XXREAL_0:17; max (a,b) in REAL by XREAL_0:def_1; then A2: max (a,b) in dom ((- 1) (#) cos) by SIN_COS:24, VALUED_1:def_5; min (a,b) in REAL by XREAL_0:def_1; then A3: min (a,b) in dom ((- 1) (#) cos) by SIN_COS:24, VALUED_1:def_5; A4: ( a <= max (a,b) & [.(min (a,b)),(max (a,b)).] c= REAL ) by XXREAL_0:25; ( sin | REAL is continuous & REAL c= dom sin ) by FDIFF_1:25, FUNCT_2:def_1, SIN_COS:68; then ((- 1) (#) cos) . (max (a,b)) = (integral (sin,(min (a,b)),(max (a,b)))) + (((- 1) (#) cos) . (min (a,b))) by A1, A4, Th20, Th25, XXREAL_0:2; then (- 1) * (cos . (max (a,b))) = (integral (sin,(min (a,b)),(max (a,b)))) + (((- 1) (#) cos) . (min (a,b))) by A2, VALUED_1:def_5; then (- 1) * (cos . (max (a,b))) = (integral (sin,(min (a,b)),(max (a,b)))) + ((- 1) * (cos . (min (a,b)))) by A3, VALUED_1:def_5; then A5: (cos . (min (a,b))) - (cos . (max (a,b))) = integral (sin,(min (a,b)),(max (a,b))) ; A6: now__::_thesis:_(_min_(a,b)_=_a_implies_(cos_._a)_-_(cos_._b)_=_integral_(sin,a,b)_) assume A7: min (a,b) = a ; ::_thesis: (cos . a) - (cos . b) = integral (sin,a,b) then max (a,b) = b by XXREAL_0:36; hence (cos . a) - (cos . b) = integral (sin,a,b) by A5, A7; ::_thesis: verum end; now__::_thesis:_(_min_(a,b)_=_b_implies_(cos_._a)_-_(cos_._b)_=_integral_(sin,a,b)_) assume A8: min (a,b) = b ; ::_thesis: (cos . a) - (cos . b) = integral (sin,a,b) then A9: max (a,b) = a by XXREAL_0:36; ( b < a implies (cos . a) - (cos . b) = integral (sin,a,b) ) proof assume A10: b < a ; ::_thesis: (cos . a) - (cos . b) = integral (sin,a,b) then integral (sin,a,b) = - (integral (sin,['b,a'])) by INTEGRA5:def_4; then integral (sin,a,b) = - (integral (sin,b,a)) by A10, INTEGRA5:def_4; hence (cos . a) - (cos . b) = integral (sin,a,b) by A5, A8, A9; ::_thesis: verum end; hence (cos . a) - (cos . b) = integral (sin,a,b) by A1, A6, A8, XXREAL_0:1; ::_thesis: verum end; hence (cos . a) - (cos . b) = integral (sin,a,b) by A6, XXREAL_0:15; ::_thesis: verum end; theorem Th27: :: INTEGRA7:27 exp_R is_integral_of exp_R , REAL proof A1: dom (exp_R | REAL) = REAL /\ REAL by RELAT_1:61, TAYLOR_1:16; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(exp_R_`|_REAL)_holds_ (exp_R_`|_REAL)_._x_=_(exp_R_|_REAL)_._x let x be set ; ::_thesis: ( x in dom (exp_R `| REAL) implies (exp_R `| REAL) . x = (exp_R | REAL) . x ) assume A3: x in dom (exp_R `| REAL) ; ::_thesis: (exp_R `| REAL) . x = (exp_R | REAL) . x then reconsider z = x as real number ; reconsider z1 = z as Real by XREAL_0:def_1; (exp_R `| REAL) . x = diff (exp_R,z) by A3, FDIFF_1:def_7, TAYLOR_1:16; then (exp_R `| REAL) . x = exp_R . z1 by TAYLOR_1:16; hence (exp_R `| REAL) . x = (exp_R | REAL) . x by A1, FUNCT_1:47; ::_thesis: verum end; dom (exp_R `| REAL) = REAL by FDIFF_1:def_7, TAYLOR_1:16; then exp_R `| REAL = exp_R | REAL by A1, A2, FUNCT_1:2; hence exp_R is_integral_of exp_R , REAL by Lm1, TAYLOR_1:16; ::_thesis: verum end; theorem :: INTEGRA7:28 for b, a being real number holds (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) proof let b, a be real number ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) A1: min (a,b) <= a by XXREAL_0:17; A2: [.(min (a,b)),(max (a,b)).] c= REAL ; ( exp_R | REAL is continuous & a <= max (a,b) ) by FDIFF_1:25, TAYLOR_1:16, XXREAL_0:25; then A3: exp_R . (max (a,b)) = (integral (exp_R,(min (a,b)),(max (a,b)))) + (exp_R . (min (a,b))) by A1, A2, Th20, Th27, SIN_COS:47, XXREAL_0:2; A4: ( min (a,b) = a implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) ) proof assume A5: min (a,b) = a ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) then max (a,b) = b by XXREAL_0:36; hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) by A3, A5; ::_thesis: verum end; ( min (a,b) = b implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) ) proof assume A6: min (a,b) = b ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) then A7: max (a,b) = a by XXREAL_0:36; ( b < a implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) ) proof assume b < a ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) then integral (exp_R,a,b) = - (integral (exp_R,['b,a'])) by INTEGRA5:def_4; then exp_R . a = (- (integral (exp_R,a,b))) + (exp_R . b) by A1, A3, A6, A7, INTEGRA5:def_4; hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) ; ::_thesis: verum end; hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) by A1, A4, A6, XXREAL_0:1; ::_thesis: verum end; hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) by A4, XXREAL_0:15; ::_thesis: verum end; theorem Th29: :: INTEGRA7:29 for n being Element of NAT holds #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL proof let n be Element of NAT ; ::_thesis: #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL reconsider m = n + 1 as Nat ; dom (((n + 1) (#) (#Z n)) | REAL) = (dom ((n + 1) (#) (#Z n))) /\ REAL by RELAT_1:61; then A1: dom (((n + 1) (#) (#Z n)) | REAL) = REAL /\ REAL by FUNCT_2:def_1; A2: dom (#Z (n + 1)) = REAL by FUNCT_2:def_1; for x being Real st x in REAL holds (#Z (n + 1)) | REAL is_differentiable_in x proof let x be Real; ::_thesis: ( x in REAL implies (#Z (n + 1)) | REAL is_differentiable_in x ) assume x in REAL ; ::_thesis: (#Z (n + 1)) | REAL is_differentiable_in x #Z (n + 1) is_differentiable_in x by TAYLOR_1:2; hence (#Z (n + 1)) | REAL is_differentiable_in x by A2, RELAT_1:68; ::_thesis: verum end; then A3: #Z (n + 1) is_differentiable_on REAL by A2, FDIFF_1:def_6; A4: dom (#Z n) = REAL by FUNCT_2:def_1; A5: now__::_thesis:_for_x_being_set_st_x_in_dom_((#Z_(n_+_1))_`|_REAL)_holds_ ((#Z_(n_+_1))_`|_REAL)_._x_=_(((n_+_1)_(#)_(#Z_n))_|_REAL)_._x let x be set ; ::_thesis: ( x in dom ((#Z (n + 1)) `| REAL) implies ((#Z (n + 1)) `| REAL) . x = (((n + 1) (#) (#Z n)) | REAL) . x ) assume A6: x in dom ((#Z (n + 1)) `| REAL) ; ::_thesis: ((#Z (n + 1)) `| REAL) . x = (((n + 1) (#) (#Z n)) | REAL) . x then reconsider z = x as real number ; ((#Z (n + 1)) `| REAL) . x = diff ((#Z (n + 1)),z) by A3, A6, FDIFF_1:def_7; then ((#Z (n + 1)) `| REAL) . x = m * (z #Z (m - 1)) by TAYLOR_1:2; then A7: ((#Z (n + 1)) `| REAL) . x = (n + 1) * ((#Z n) . x) by TAYLOR_1:def_1; x in dom (#Z n) by A4, A6; then x in dom ((n + 1) (#) (#Z n)) by VALUED_1:def_5; then ((#Z (n + 1)) `| REAL) . x = ((n + 1) (#) (#Z n)) . x by A7, VALUED_1:def_5; hence ((#Z (n + 1)) `| REAL) . x = (((n + 1) (#) (#Z n)) | REAL) . x by A1, A6, FUNCT_1:47; ::_thesis: verum end; dom ((#Z (n + 1)) `| REAL) = REAL by A3, FDIFF_1:def_7; then (#Z (n + 1)) `| REAL = ((n + 1) (#) (#Z n)) | REAL by A1, A5, FUNCT_1:2; hence #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL by A3, Lm1; ::_thesis: verum end; theorem :: INTEGRA7:30 for b, a being real number for n being Element of NAT holds ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) proof let b, a be real number ; ::_thesis: for n being Element of NAT holds ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) let n be Element of NAT ; ::_thesis: ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) A1: [#] REAL c= dom ((n + 1) (#) (#Z n)) by FUNCT_2:def_1; A2: dom (#Z n) = REAL by FUNCT_2:def_1; for x being Real st x in REAL holds (#Z n) | REAL is_differentiable_in x proof let x be Real; ::_thesis: ( x in REAL implies (#Z n) | REAL is_differentiable_in x ) assume x in REAL ; ::_thesis: (#Z n) | REAL is_differentiable_in x #Z n is_differentiable_in x by TAYLOR_1:2; hence (#Z n) | REAL is_differentiable_in x by A2, RELAT_1:68; ::_thesis: verum end; then #Z n is_differentiable_on REAL by A2, FDIFF_1:def_6; then A3: ((n + 1) (#) (#Z n)) | REAL is continuous by A1, FDIFF_1:20, FDIFF_1:25; A4: min (a,b) <= a by XXREAL_0:17; A5: [.(min (a,b)),(max (a,b)).] c= REAL ; a <= max (a,b) by XXREAL_0:25; then min (a,b) <= max (a,b) by A4, XXREAL_0:2; then A6: (#Z (n + 1)) . (max (a,b)) = (integral (((n + 1) (#) (#Z n)),(min (a,b)),(max (a,b)))) + ((#Z (n + 1)) . (min (a,b))) by A1, A3, A5, Th20, Th29; A7: ( min (a,b) = a implies ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) ) proof assume A8: min (a,b) = a ; ::_thesis: ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) then max (a,b) = b by XXREAL_0:36; hence ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) by A6, A8; ::_thesis: verum end; ( min (a,b) = b implies ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) ) proof assume A9: min (a,b) = b ; ::_thesis: ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) then A10: max (a,b) = a by XXREAL_0:36; ( b < a implies ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) ) proof assume b < a ; ::_thesis: ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) then integral (((n + 1) (#) (#Z n)),a,b) = - (integral (((n + 1) (#) (#Z n)),['b,a'])) by INTEGRA5:def_4; then (#Z (n + 1)) . a = (- (integral (((n + 1) (#) (#Z n)),a,b))) + ((#Z (n + 1)) . b) by A4, A6, A9, A10, INTEGRA5:def_4; hence ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) ; ::_thesis: verum end; hence ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) by A4, A7, A9, XXREAL_0:1; ::_thesis: verum end; hence ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) by A7, XXREAL_0:15; ::_thesis: verum end; begin theorem :: INTEGRA7:31 for a, b being real number for H being Functional_Sequence of REAL,REAL for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds ( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) ) ) & H is_unif_conv_on ['a,b'] holds ( (lim (H,['a,b'])) | ['a,b'] is bounded & lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) ) proof let a, b be real number ; ::_thesis: for H being Functional_Sequence of REAL,REAL for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds ( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) ) ) & H is_unif_conv_on ['a,b'] holds ( (lim (H,['a,b'])) | ['a,b'] is bounded & lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) ) let H be Functional_Sequence of REAL,REAL; ::_thesis: for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds ( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) ) ) & H is_unif_conv_on ['a,b'] holds ( (lim (H,['a,b'])) | ['a,b'] is bounded & lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) ) let rseq be Real_Sequence; ::_thesis: ( a < b & ( for n being Element of NAT holds ( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) ) ) & H is_unif_conv_on ['a,b'] implies ( (lim (H,['a,b'])) | ['a,b'] is bounded & lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) ) ) set AB = ['a,b']; assume that A1: a < b and A2: for n being Element of NAT holds ( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) ) and A3: H is_unif_conv_on ['a,b'] ; ::_thesis: ( (lim (H,['a,b'])) | ['a,b'] is bounded & lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) ) consider T being DivSequence of ['a,b'] such that A4: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11; A5: ['a,b'] common_on_dom H by A3, SEQFUNC:43; A6: for n being Element of NAT holds ( (H . n) || ['a,b'] is Function of ['a,b'],REAL & ((H . n) || ['a,b']) | ['a,b'] is bounded & lower_sum (((H . n) || ['a,b']),T) is convergent & lim (lower_sum (((H . n) || ['a,b']),T)) = lower_integral ((H . n) || ['a,b']) & upper_sum (((H . n) || ['a,b']),T) is convergent & lim (upper_sum (((H . n) || ['a,b']),T)) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) ) proof let n be Element of NAT ; ::_thesis: ( (H . n) || ['a,b'] is Function of ['a,b'],REAL & ((H . n) || ['a,b']) | ['a,b'] is bounded & lower_sum (((H . n) || ['a,b']),T) is convergent & lim (lower_sum (((H . n) || ['a,b']),T)) = lower_integral ((H . n) || ['a,b']) & upper_sum (((H . n) || ['a,b']),T) is convergent & lim (upper_sum (((H . n) || ['a,b']),T)) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) ) ['a,b'] c= dom (H . n) by A5, SEQFUNC:def_9; hence A7: (H . n) || ['a,b'] is Function of ['a,b'],REAL by FUNCT_2:68, INTEGRA5:6; ::_thesis: ( ((H . n) || ['a,b']) | ['a,b'] is bounded & lower_sum (((H . n) || ['a,b']),T) is convergent & lim (lower_sum (((H . n) || ['a,b']),T)) = lower_integral ((H . n) || ['a,b']) & upper_sum (((H . n) || ['a,b']),T) is convergent & lim (upper_sum (((H . n) || ['a,b']),T)) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) ) thus ((H . n) || ['a,b']) | ['a,b'] is bounded by A2, INTEGRA5:9; ::_thesis: ( lower_sum (((H . n) || ['a,b']),T) is convergent & lim (lower_sum (((H . n) || ['a,b']),T)) = lower_integral ((H . n) || ['a,b']) & upper_sum (((H . n) || ['a,b']),T) is convergent & lim (upper_sum (((H . n) || ['a,b']),T)) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) ) hence ( lower_sum (((H . n) || ['a,b']),T) is convergent & lim (lower_sum (((H . n) || ['a,b']),T)) = lower_integral ((H . n) || ['a,b']) & upper_sum (((H . n) || ['a,b']),T) is convergent & lim (upper_sum (((H . n) || ['a,b']),T)) = upper_integral ((H . n) || ['a,b']) ) by A4, A7, INTEGRA4:8, INTEGRA4:9; ::_thesis: ( lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) ) H . n is_integrable_on ['a,b'] by A2; then (H . n) || ['a,b'] is integrable by INTEGRA5:def_1; hence lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) by INTEGRA1:def_16; ::_thesis: rseq . n = integral ((H . n) || ['a,b']) rseq . n = integral ((H . n),a,b) by A2; then rseq . n = integral ((H . n),['a,b']) by A1, INTEGRA5:def_4; hence rseq . n = integral ((H . n) || ['a,b']) ; ::_thesis: verum end; set L1 = lower_integral ((lim (H,['a,b'])) || ['a,b']); set K1 = upper_integral ((lim (H,['a,b'])) || ['a,b']); A8: 0 < b - a by A1, XREAL_1:50; consider K being Element of NAT such that A9: for n being Element of NAT for x being Element of REAL st n >= K & x in ['a,b'] holds abs (((H . n) . x) - ((lim (H,['a,b'])) . x)) < 1 by A3, SEQFUNC:43; (H . K) | ['a,b'] is bounded by A2; then consider r being real number such that A10: for c being set st c in ['a,b'] /\ (dom (H . K)) holds abs ((H . K) . c) <= r by RFUNCT_1:73; set H0 = (lim (H,['a,b'])) || ['a,b']; H is_point_conv_on ['a,b'] by A3, SEQFUNC:22; then A11: dom (lim (H,['a,b'])) = ['a,b'] by SEQFUNC:21; then A12: (lim (H,['a,b'])) || ['a,b'] is Function of ['a,b'],REAL by FUNCT_2:68, INTEGRA5:6; dom (lim (H,['a,b'])) c= dom (H . K) by A5, A11, SEQFUNC:def_9; then A13: ['a,b'] /\ (dom (lim (H,['a,b']))) c= ['a,b'] /\ (dom (H . K)) by XBOOLE_1:26; now__::_thesis:_for_c_being_set_st_c_in_['a,b']_/\_(dom_(lim_(H,['a,b'])))_holds_ abs_((lim_(H,['a,b']))_._c)_<=_r_+_1 let c be set ; ::_thesis: ( c in ['a,b'] /\ (dom (lim (H,['a,b']))) implies abs ((lim (H,['a,b'])) . c) <= r + 1 ) (lim (H,['a,b'])) . c = ((H . K) . c) - (((H . K) . c) - ((lim (H,['a,b'])) . c)) ; then A14: abs ((lim (H,['a,b'])) . c) <= (abs ((H . K) . c)) + (abs (((H . K) . c) - ((lim (H,['a,b'])) . c))) by COMPLEX1:57; assume A15: c in ['a,b'] /\ (dom (lim (H,['a,b']))) ; ::_thesis: abs ((lim (H,['a,b'])) . c) <= r + 1 then c in ['a,b'] by XBOOLE_0:def_4; then A16: abs (((H . K) . c) - ((lim (H,['a,b'])) . c)) < 1 by A9; abs ((H . K) . c) <= r by A10, A13, A15; then (abs ((H . K) . c)) + (abs (((H . K) . c) - ((lim (H,['a,b'])) . c))) <= r + 1 by A16, XREAL_1:7; hence abs ((lim (H,['a,b'])) . c) <= r + 1 by A14, XXREAL_0:2; ::_thesis: verum end; hence A17: (lim (H,['a,b'])) | ['a,b'] is bounded by RFUNCT_1:73; ::_thesis: ( lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) ) then A18: ((lim (H,['a,b'])) || ['a,b']) | ['a,b'] is bounded_above by INTEGRA5:7; A19: ((lim (H,['a,b'])) || ['a,b']) | ['a,b'] is bounded_below by A17, INTEGRA5:8; then A20: upper_sum (((lim (H,['a,b'])) || ['a,b']),T) is convergent by A4, A18, A12, INTEGRA4:9; A21: for e being Element of REAL st 0 < e holds ex N being Element of NAT st for n, k being Element of NAT st N <= n holds abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) proof let e be Element of REAL ; ::_thesis: ( 0 < e implies ex N being Element of NAT st for n, k being Element of NAT st N <= n holds abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) ) assume 0 < e ; ::_thesis: ex N being Element of NAT st for n, k being Element of NAT st N <= n holds abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) then consider N being Element of NAT such that A22: for n being Element of NAT for x being Element of REAL st n >= N & x in ['a,b'] holds abs (((H . n) . x) - ((lim (H,['a,b'])) . x)) < e by A3, SEQFUNC:43; take N ; ::_thesis: for n, k being Element of NAT st N <= n holds abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) now__::_thesis:_for_n,_k_being_Element_of_NAT_st_N_<=_n_holds_ abs_(((upper_sum_(((H_._n)_||_['a,b']),T))_._k)_-_((upper_sum_(((lim_(H,['a,b']))_||_['a,b']),T))_._k))_<=_e_*_(b_-_a) let n, k be Element of NAT ; ::_thesis: ( N <= n implies abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) ) reconsider Tk = T . k as Division of ['a,b'] ; set l0 = len Tk; A23: dom Tk = Seg (len Tk) by FINSEQ_1:def_3; set Hn = (H . n) || ['a,b']; len (upper_volume (((H . n) || ['a,b']),(T . k))) = len Tk by INTEGRA1:def_6; then reconsider R1 = upper_volume (((H . n) || ['a,b']),(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92; len (upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . k))) = len Tk by INTEGRA1:def_6; then reconsider R2 = upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92; ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((upper_sum (((H . n) || ['a,b']),T)) . k) = (upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . k))) - ((upper_sum (((H . n) || ['a,b']),T)) . k) by INTEGRA2:def_2; then ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((upper_sum (((H . n) || ['a,b']),T)) . k) = (upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . k))) - (upper_sum (((H . n) || ['a,b']),(T . k))) by INTEGRA2:def_2; then A24: ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((upper_sum (((H . n) || ['a,b']),T)) . k) = Sum (R2 - R1) by RVSUM_1:90; consider H1 being Function of ['a,b'],REAL such that A25: rng H1 = {e} and A26: H1 | ['a,b'] is bounded by INTEGRA4:5; len (upper_volume (H1,(T . k))) = len Tk by INTEGRA1:def_6; then reconsider R3 = upper_volume (H1,(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92; A27: vol ['a,b'] = b - a by A1, INTEGRA6:5; upper_bound (rng H1) = e by A25, SEQ_4:9; then A28: upper_sum (H1,(T . k)) <= e * (b - a) by A26, A27, INTEGRA1:27; assume A29: N <= n ; ::_thesis: abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) A30: for i being Element of NAT st i in dom Tk holds ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) proof let i be Element of NAT ; ::_thesis: ( i in dom Tk implies ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) ) A31: 0 <= vol (divset ((T . k),i)) by INTEGRA1:9; assume A32: i in dom Tk ; ::_thesis: ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) A33: ( (upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) - (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) <= upper_bound (rng (H1 | (divset ((T . k),i)))) & (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) <= upper_bound (rng (H1 | (divset ((T . k),i)))) ) proof A34: divset ((T . k),i) c= ['a,b'] by A32, INTEGRA1:8; then reconsider g = ((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i)) as Function of (divset ((T . k),i)),REAL by A12, FUNCT_2:32; consider x0 being set such that A35: x0 in divset ((T . k),i) by XBOOLE_0:def_1; (H . n) || ['a,b'] is Function of ['a,b'],REAL by A6; then reconsider f = ((H . n) || ['a,b']) | (divset ((T . k),i)) as Function of (divset ((T . k),i)),REAL by A34, FUNCT_2:32; A36: for x being set st x in divset ((T . k),i) holds abs ((f . x) - (g . x)) <= e proof let x be set ; ::_thesis: ( x in divset ((T . k),i) implies abs ((f . x) - (g . x)) <= e ) assume A37: x in divset ((T . k),i) ; ::_thesis: abs ((f . x) - (g . x)) <= e then abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (g . x)) by FUNCT_1:49; then abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)) by A37, FUNCT_1:49; then abs ((f . x) - (g . x)) = abs (((H . n) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)) by A34, A37, FUNCT_1:49; then abs ((f . x) - (g . x)) = abs (((H . n) . x) - ((lim (H,['a,b'])) . x)) by A34, A37, FUNCT_1:49; hence abs ((f . x) - (g . x)) <= e by A22, A29, A34, A37; ::_thesis: verum end; ((H . n) || ['a,b']) | ['a,b'] is bounded by A6; then f | (divset ((T . k),i)) is bounded_above by A32, INTEGRA1:8, INTEGRA2:5; then A38: rng f is bounded_above by INTEGRA1:13; H1 . x0 in {e} by A25, A34, A35, FUNCT_2:4; then H1 . x0 = e by TARSKI:def_1; then A39: (H1 | (divset ((T . k),i))) . x0 = e by A35, FUNCT_1:49; H1 | (divset ((T . k),i)) is Function of (divset ((T . k),i)),REAL by A34, FUNCT_2:32; then e in rng (H1 | (divset ((T . k),i))) by A35, A39, FUNCT_2:4; then A40: {e} c= rng (H1 | (divset ((T . k),i))) by ZFMISC_1:31; rng (H1 | (divset ((T . k),i))) c= {e} by A25, RELAT_1:70; then rng (H1 | (divset ((T . k),i))) = {e} by A40, XBOOLE_0:def_10; then A41: e = upper_bound (rng (H1 | (divset ((T . k),i)))) by SEQ_4:9; g | (divset ((T . k),i)) is bounded_above by A18, A32, INTEGRA1:8, INTEGRA2:5; then A42: rng g is bounded_above by INTEGRA1:13; hence (upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) - (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) <= upper_bound (rng (H1 | (divset ((T . k),i)))) by A38, A41, A36, Th1; ::_thesis: (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) <= upper_bound (rng (H1 | (divset ((T . k),i)))) for x being set st x in divset ((T . k),i) holds abs ((g . x) - (f . x)) <= upper_bound (rng (H1 | (divset ((T . k),i)))) proof let x be set ; ::_thesis: ( x in divset ((T . k),i) implies abs ((g . x) - (f . x)) <= upper_bound (rng (H1 | (divset ((T . k),i)))) ) assume x in divset ((T . k),i) ; ::_thesis: abs ((g . x) - (f . x)) <= upper_bound (rng (H1 | (divset ((T . k),i)))) then abs ((f . x) - (g . x)) <= upper_bound (rng (H1 | (divset ((T . k),i)))) by A41, A36; hence abs ((g . x) - (f . x)) <= upper_bound (rng (H1 | (divset ((T . k),i)))) by COMPLEX1:60; ::_thesis: verum end; hence (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) <= upper_bound (rng (H1 | (divset ((T . k),i)))) by A38, A42, Th1; ::_thesis: verum end; (R1 - R2) . i = (R1 . i) - (R2 . i) by RVSUM_1:27; then (R1 - R2) . i = ((upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) - ((upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . k))) . i) by A32, INTEGRA1:def_6; then (R1 - R2) . i = ((upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) - ((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) by A32, INTEGRA1:def_6; then (R1 - R2) . i = ((upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) - (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i)))))) * (vol (divset ((T . k),i))) ; then (R1 - R2) . i <= (upper_bound (rng (H1 | (divset ((T . k),i))))) * (vol (divset ((T . k),i))) by A33, A31, XREAL_1:64; hence (R1 - R2) . i <= R3 . i by A32, INTEGRA1:def_6; ::_thesis: (R2 - R1) . i <= R3 . i (R2 - R1) . i = (R2 . i) - (R1 . i) by RVSUM_1:27; then (R2 - R1) . i = ((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) - ((upper_volume (((H . n) || ['a,b']),(T . k))) . i) by A32, INTEGRA1:def_6; then (R2 - R1) . i = ((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) - ((upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) by A32, INTEGRA1:def_6; then (R2 - R1) . i = ((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i)))))) * (vol (divset ((T . k),i))) ; then (R2 - R1) . i <= (upper_bound (rng (H1 | (divset ((T . k),i))))) * (vol (divset ((T . k),i))) by A33, A31, XREAL_1:64; hence (R2 - R1) . i <= R3 . i by A32, INTEGRA1:def_6; ::_thesis: verum end; then for i being Nat st i in dom Tk holds (R2 - R1) . i <= R3 . i ; then ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((upper_sum (((H . n) || ['a,b']),T)) . k) <= Sum R3 by A23, A24, RVSUM_1:82; then ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((upper_sum (((H . n) || ['a,b']),T)) . k) <= e * (b - a) by A28, XXREAL_0:2; then A43: - (e * (b - a)) <= - (((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((upper_sum (((H . n) || ['a,b']),T)) . k)) by XREAL_1:24; ((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) = (upper_sum (((H . n) || ['a,b']),(T . k))) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) by INTEGRA2:def_2; then ((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) = (upper_sum (((H . n) || ['a,b']),(T . k))) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . k))) by INTEGRA2:def_2; then A44: ((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) = Sum (R1 - R2) by RVSUM_1:90; for i being Nat st i in Seg (len Tk) holds (R1 - R2) . i <= R3 . i by A23, A30; then ((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) <= Sum R3 by A44, RVSUM_1:82; then ((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) <= e * (b - a) by A28, XXREAL_0:2; hence abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) by A43, ABSVALUE:5; ::_thesis: verum end; hence for n, k being Element of NAT st N <= n holds abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) ; ::_thesis: verum end; A45: for e being Element of REAL st 0 < e holds ex N being Element of NAT st for n being Element of NAT st N <= n holds abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= e proof let e be Element of REAL ; ::_thesis: ( 0 < e implies ex N being Element of NAT st for n being Element of NAT st N <= n holds abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= e ) assume 0 < e ; ::_thesis: ex N being Element of NAT st for n being Element of NAT st N <= n holds abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= e then consider N being Element of NAT such that A46: for n, k being Element of NAT st N <= n holds abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= (e / (b - a)) * (b - a) by A21, A8, XREAL_1:139; take N ; ::_thesis: for n being Element of NAT st N <= n holds abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= e A47: now__::_thesis:_for_n,_k_being_Element_of_NAT_st_N_<=_n_holds_ abs_(((upper_sum_(((H_._n)_||_['a,b']),T))_._k)_-_((upper_sum_(((lim_(H,['a,b']))_||_['a,b']),T))_._k))_<=_e let n, k be Element of NAT ; ::_thesis: ( N <= n implies abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e ) assume N <= n ; ::_thesis: abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e then abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= (e / (b - a)) * (b - a) by A46; hence abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e by A8, XCMPLX_1:87; ::_thesis: verum end; hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: ( N <= n implies abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= e ) assume A48: N <= n ; ::_thesis: abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= e A49: now__::_thesis:_for_k_being_Element_of_NAT_holds_(abs_((upper_sum_(((H_._n)_||_['a,b']),T))_-_(upper_sum_(((lim_(H,['a,b']))_||_['a,b']),T))))_._k_<=_e let k be Element of NAT ; ::_thesis: (abs ((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k <= e abs (((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e by A47, A48; then abs (((upper_sum (((H . n) || ['a,b']),T)) . k) + ((- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) . k)) <= e by SEQ_1:10; then abs (((upper_sum (((H . n) || ['a,b']),T)) + (- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k) <= e by SEQ_1:7; hence (abs ((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k <= e by SEQ_1:12; ::_thesis: verum end; A50: upper_sum (((H . n) || ['a,b']),T) is convergent by A6; then lim ((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) = (lim (upper_sum (((H . n) || ['a,b']),T))) - (lim (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) by A20, SEQ_2:12; then lim ((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) = (upper_integral ((H . n) || ['a,b'])) - (lim (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) by A6; then A51: lim ((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) = (upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b'])) by A4, A18, A19, A12, INTEGRA4:9; A52: (upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) is convergent by A20, A50; then abs ((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) is convergent by SEQ_4:13; then lim (abs ((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) <= e by A49, PREPOWER:2; hence abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= e by A52, A51, SEQ_4:14; ::_thesis: verum end; end; A53: lower_sum (((lim (H,['a,b'])) || ['a,b']),T) is convergent by A4, A18, A19, A12, INTEGRA4:8; A54: for e being Element of REAL st 0 < e holds ex N being Element of NAT st for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) proof let e be Element of REAL ; ::_thesis: ( 0 < e implies ex N being Element of NAT st for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) ) assume 0 < e ; ::_thesis: ex N being Element of NAT st for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) then consider N being Element of NAT such that A55: for n being Element of NAT for x being Element of REAL st n >= N & x in ['a,b'] holds abs (((H . n) . x) - ((lim (H,['a,b'])) . x)) < e by A3, SEQFUNC:43; take N ; ::_thesis: for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) hereby ::_thesis: verum let n, k be Element of NAT ; ::_thesis: ( N <= n implies abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) ) set Hn = (H . n) || ['a,b']; reconsider Tk = T . k as Division of ['a,b'] ; set l0 = len Tk; consider H1 being Function of ['a,b'],REAL such that A56: rng H1 = {e} and A57: H1 | ['a,b'] is bounded by INTEGRA4:5; A58: lower_sum (H1,(T . k)) <= upper_sum (H1,(T . k)) by A57, INTEGRA1:28; len (lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . k))) = len Tk by INTEGRA1:def_7; then reconsider R2 = lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92; len (lower_volume (((H . n) || ['a,b']),(T . k))) = len Tk by INTEGRA1:def_7; then reconsider R1 = lower_volume (((H . n) || ['a,b']),(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92; len (lower_volume (H1,(T . k))) = len Tk by INTEGRA1:def_7; then reconsider R3 = lower_volume (H1,(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92; assume A59: N <= n ; ::_thesis: abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) A60: for i being Element of NAT st i in dom Tk holds ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) proof let i be Element of NAT ; ::_thesis: ( i in dom Tk implies ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) ) consider x0 being set such that A61: x0 in divset ((T . k),i) by XBOOLE_0:def_1; A62: rng (H1 | (divset ((T . k),i))) c= {e} by A56, RELAT_1:70; assume A63: i in dom Tk ; ::_thesis: ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) then A64: divset ((T . k),i) c= ['a,b'] by INTEGRA1:8; then reconsider g = ((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i)) as Function of (divset ((T . k),i)),REAL by A12, FUNCT_2:32; (H . n) || ['a,b'] is Function of ['a,b'],REAL by A6; then reconsider f = ((H . n) || ['a,b']) | (divset ((T . k),i)) as Function of (divset ((T . k),i)),REAL by A64, FUNCT_2:32; A65: 0 <= vol (divset ((T . k),i)) by INTEGRA1:9; H1 . x0 in {e} by A56, A64, A61, FUNCT_2:4; then H1 . x0 = e by TARSKI:def_1; then A66: (H1 | (divset ((T . k),i))) . x0 = e by A61, FUNCT_1:49; H1 | (divset ((T . k),i)) is Function of (divset ((T . k),i)),REAL by A64, FUNCT_2:32; then e in rng (H1 | (divset ((T . k),i))) by A61, A66, FUNCT_2:4; then {e} c= rng (H1 | (divset ((T . k),i))) by ZFMISC_1:31; then rng (H1 | (divset ((T . k),i))) = {e} by A62, XBOOLE_0:def_10; then A67: e = lower_bound (rng (H1 | (divset ((T . k),i)))) by SEQ_4:9; A68: now__::_thesis:_for_x_being_set_st_x_in_divset_((T_._k),i)_holds_ abs_((f_._x)_-_(g_._x))_<=_e let x be set ; ::_thesis: ( x in divset ((T . k),i) implies abs ((f . x) - (g . x)) <= e ) assume A69: x in divset ((T . k),i) ; ::_thesis: abs ((f . x) - (g . x)) <= e then abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (g . x)) by FUNCT_1:49; then abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)) by A69, FUNCT_1:49; then abs ((f . x) - (g . x)) = abs (((H . n) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)) by A64, A69, FUNCT_1:49; then abs ((f . x) - (g . x)) = abs (((H . n) . x) - ((lim (H,['a,b'])) . x)) by A64, A69, FUNCT_1:49; hence abs ((f . x) - (g . x)) <= e by A55, A59, A64, A69; ::_thesis: verum end; (R2 - R1) . i = (R2 . i) - (R1 . i) by RVSUM_1:27; then (R2 - R1) . i = ((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) - ((lower_volume (((H . n) || ['a,b']),(T . k))) . i) by A63, INTEGRA1:def_7; then (R2 - R1) . i = ((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) - ((lower_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) by A63, INTEGRA1:def_7; then A70: (R2 - R1) . i = ((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) - (lower_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i)))))) * (vol (divset ((T . k),i))) ; (R1 - R2) . i = (R1 . i) - (R2 . i) by RVSUM_1:27; then (R1 - R2) . i = ((lower_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) - ((lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . k))) . i) by A63, INTEGRA1:def_7; then (R1 - R2) . i = ((lower_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) - ((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) * (vol (divset ((T . k),i)))) by A63, INTEGRA1:def_7; then A71: (R1 - R2) . i = ((lower_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) - (lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i)))))) * (vol (divset ((T . k),i))) ; ((H . n) || ['a,b']) | ['a,b'] is bounded by A6; then f | (divset ((T . k),i)) is bounded_below by A63, INTEGRA1:8, INTEGRA2:6; then A72: rng f is bounded_below by INTEGRA1:11; g | (divset ((T . k),i)) is bounded_below by A19, A63, INTEGRA1:8, INTEGRA2:6; then A73: rng g is bounded_below by INTEGRA1:11; then (lower_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) - (lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) <= lower_bound (rng (H1 | (divset ((T . k),i)))) by A72, A67, A68, Th2; then (R1 - R2) . i <= (lower_bound (rng (H1 | (divset ((T . k),i))))) * (vol (divset ((T . k),i))) by A71, A65, XREAL_1:64; hence (R1 - R2) . i <= R3 . i by A63, INTEGRA1:def_7; ::_thesis: (R2 - R1) . i <= R3 . i now__::_thesis:_for_x_being_set_st_x_in_divset_((T_._k),i)_holds_ abs_((g_._x)_-_(f_._x))_<=_lower_bound_(rng_(H1_|_(divset_((T_._k),i)))) let x be set ; ::_thesis: ( x in divset ((T . k),i) implies abs ((g . x) - (f . x)) <= lower_bound (rng (H1 | (divset ((T . k),i)))) ) assume x in divset ((T . k),i) ; ::_thesis: abs ((g . x) - (f . x)) <= lower_bound (rng (H1 | (divset ((T . k),i)))) then abs ((f . x) - (g . x)) <= lower_bound (rng (H1 | (divset ((T . k),i)))) by A67, A68; hence abs ((g . x) - (f . x)) <= lower_bound (rng (H1 | (divset ((T . k),i)))) by COMPLEX1:60; ::_thesis: verum end; then (lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i))))) - (lower_bound (rng (((H . n) || ['a,b']) | (divset ((T . k),i))))) <= lower_bound (rng (H1 | (divset ((T . k),i)))) by A72, A73, Th2; then (R2 - R1) . i <= (lower_bound (rng (H1 | (divset ((T . k),i))))) * (vol (divset ((T . k),i))) by A70, A65, XREAL_1:64; hence (R2 - R1) . i <= R3 . i by A63, INTEGRA1:def_7; ::_thesis: verum end; ((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) = (lower_sum (((H . n) || ['a,b']),(T . k))) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) by INTEGRA2:def_3; then ((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) = (lower_sum (((H . n) || ['a,b']),(T . k))) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . k))) by INTEGRA2:def_3; then A74: ((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) = Sum (R1 - R2) by RVSUM_1:90; A75: vol ['a,b'] = b - a by A1, INTEGRA6:5; upper_bound (rng H1) = e by A56, SEQ_4:9; then upper_sum (H1,(T . k)) <= e * (b - a) by A57, A75, INTEGRA1:27; then A76: lower_sum (H1,(T . k)) <= e * (b - a) by A58, XXREAL_0:2; ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k) = (lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . k))) - ((lower_sum (((H . n) || ['a,b']),T)) . k) by INTEGRA2:def_3; then ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k) = (lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . k))) - (lower_sum (((H . n) || ['a,b']),(T . k))) by INTEGRA2:def_3; then A77: ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k) = Sum (R2 - R1) by RVSUM_1:90; A78: Seg (len Tk) = dom Tk by FINSEQ_1:def_3; then for i being Nat st i in Seg (len Tk) holds (R2 - R1) . i <= R3 . i by A60; then ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k) <= Sum R3 by A77, RVSUM_1:82; then ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k) <= e * (b - a) by A76, XXREAL_0:2; then A79: - (e * (b - a)) <= - (((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k)) by XREAL_1:24; for i being Nat st i in Seg (len Tk) holds (R1 - R2) . i <= R3 . i by A78, A60; then ((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) <= lower_sum (H1,(T . k)) by A74, RVSUM_1:82; then ((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) <= e * (b - a) by A76, XXREAL_0:2; hence abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e * (b - a) by A79, ABSVALUE:5; ::_thesis: verum end; end; A80: for e being Element of REAL st 0 < e holds ex N being Element of NAT st for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e proof let e be Element of REAL ; ::_thesis: ( 0 < e implies ex N being Element of NAT st for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e ) assume 0 < e ; ::_thesis: ex N being Element of NAT st for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e then consider N being Element of NAT such that A81: for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= (e / (b - a)) * (b - a) by A54, A8, XREAL_1:139; take N ; ::_thesis: for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e hereby ::_thesis: verum let n, k be Element of NAT ; ::_thesis: ( N <= n implies abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e ) assume N <= n ; ::_thesis: abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e then abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= (e / (b - a)) * (b - a) by A81; hence abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e by A8, XCMPLX_1:87; ::_thesis: verum end; end; A82: for e being Element of REAL st 0 < e holds ex N being Element of NAT st for n being Element of NAT st N <= n holds abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= e proof let e be Element of REAL ; ::_thesis: ( 0 < e implies ex N being Element of NAT st for n being Element of NAT st N <= n holds abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= e ) assume 0 < e ; ::_thesis: ex N being Element of NAT st for n being Element of NAT st N <= n holds abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= e then consider N being Element of NAT such that A83: for n, k being Element of NAT st N <= n holds abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e by A80; take N ; ::_thesis: for n being Element of NAT st N <= n holds abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= e hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: ( N <= n implies abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= e ) set LHT = lower_sum (((H . n) || ['a,b']),T); assume A84: N <= n ; ::_thesis: abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= e A85: now__::_thesis:_for_k_being_Element_of_NAT_holds_(abs_((lower_sum_(((H_._n)_||_['a,b']),T))_-_(lower_sum_(((lim_(H,['a,b']))_||_['a,b']),T))))_._k_<=_e let k be Element of NAT ; ::_thesis: (abs ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k <= e abs (((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)) <= e by A83, A84; then abs (((lower_sum (((H . n) || ['a,b']),T)) . k) + ((- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) . k)) <= e by SEQ_1:10; then abs (((lower_sum (((H . n) || ['a,b']),T)) + (- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k) <= e by SEQ_1:7; hence (abs ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k <= e by SEQ_1:12; ::_thesis: verum end; A86: lower_sum (((H . n) || ['a,b']),T) is convergent by A6; then lim ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) = (lim (lower_sum (((H . n) || ['a,b']),T))) - (lim (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) by A53, SEQ_2:12; then lim ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) = (lower_integral ((H . n) || ['a,b'])) - (lim (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) by A6; then A87: lim ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) = (lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b'])) by A4, A18, A19, A12, INTEGRA4:8; A88: (lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) is convergent by A53, A86; then abs ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) is convergent by SEQ_4:13; then lim (abs ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) <= e by A85, PREPOWER:2; hence abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= e by A87, A88, SEQ_4:14; ::_thesis: verum end; end; A89: now__::_thesis:_for_e1_being_Element_of_REAL_st_0_<_e1_holds_ abs_((lower_integral_((lim_(H,['a,b']))_||_['a,b']))_-_(upper_integral_((lim_(H,['a,b']))_||_['a,b'])))_<_e1 let e1 be Element of REAL ; ::_thesis: ( 0 < e1 implies abs ((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) < e1 ) set e = e1 / 2; assume A90: 0 < e1 ; ::_thesis: abs ((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) < e1 then A91: 0 < e1 / 2 by XREAL_1:215; then consider N1 being Element of NAT such that A92: for n being Element of NAT st N1 <= n holds abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= (e1 / 2) / 2 by A45, XREAL_1:215; consider N2 being Element of NAT such that A93: for n being Element of NAT st N2 <= n holds abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= (e1 / 2) / 2 by A82, A91, XREAL_1:215; reconsider n = max (N1,N2) as Element of NAT ; set K = upper_integral ((H . n) || ['a,b']); set L = lower_integral ((H . n) || ['a,b']); abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= (e1 / 2) / 2 by A93, XXREAL_0:25; then A94: abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) <= (e1 / 2) / 2 by A6; ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) - ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) = (lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b'])) ; then A95: abs ((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= (abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b'])))) + (abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b'])))) by COMPLEX1:57; abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= (e1 / 2) / 2 by A92, XXREAL_0:25; then (abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b'])))) + (abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b'])))) <= ((e1 / 2) / 2) + ((e1 / 2) / 2) by A94, XREAL_1:7; then A96: abs ((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= e1 / 2 by A95, XXREAL_0:2; e1 / 2 < e1 by A90, XREAL_1:216; hence abs ((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) < e1 by A96, XXREAL_0:2; ::_thesis: verum end; A97: now__::_thesis:_not_upper_integral_((lim_(H,['a,b']))_||_['a,b'])_<>_lower_integral_((lim_(H,['a,b']))_||_['a,b']) assume upper_integral ((lim (H,['a,b'])) || ['a,b']) <> lower_integral ((lim (H,['a,b'])) || ['a,b']) ; ::_thesis: contradiction then 0 < abs ((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) by COMPLEX1:62; hence contradiction by A89; ::_thesis: verum end; ( (lim (H,['a,b'])) || ['a,b'] is upper_integrable & (lim (H,['a,b'])) || ['a,b'] is lower_integrable ) by A18, A19, A12, INTEGRA4:10; then (lim (H,['a,b'])) || ['a,b'] is integrable by A97, INTEGRA1:def_16; hence lim (H,['a,b']) is_integrable_on ['a,b'] by INTEGRA5:def_1; ::_thesis: ( rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) ) A98: for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((rseq . m) - (integral ((lim (H,['a,b'])),a,b))) < p proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((rseq . m) - (integral ((lim (H,['a,b'])),a,b))) < p ) set e = p / 2; assume A99: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((rseq . m) - (integral ((lim (H,['a,b'])),a,b))) < p then consider N being Element of NAT such that A100: for n being Element of NAT st N <= n holds abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= p / 2 by A45, XREAL_1:215; take N ; ::_thesis: for m being Element of NAT st N <= m holds abs ((rseq . m) - (integral ((lim (H,['a,b'])),a,b))) < p A101: p / 2 < p by A99, XREAL_1:216; hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: ( N <= n implies abs ((rseq . n) - (integral ((lim (H,['a,b'])),a,b))) < p ) upper_integral ((H . n) || ['a,b']) = integral ((H . n) || ['a,b']) ; then A102: upper_integral ((H . n) || ['a,b']) = rseq . n by A6; upper_integral ((lim (H,['a,b'])) || ['a,b']) = integral ((lim (H,['a,b'])),['a,b']) ; then A103: upper_integral ((lim (H,['a,b'])) || ['a,b']) = integral ((lim (H,['a,b'])),a,b) by A1, INTEGRA5:def_4; assume N <= n ; ::_thesis: abs ((rseq . n) - (integral ((lim (H,['a,b'])),a,b))) < p then abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) <= p / 2 by A100; hence abs ((rseq . n) - (integral ((lim (H,['a,b'])),a,b))) < p by A101, A102, A103, XXREAL_0:2; ::_thesis: verum end; end; hence rseq is convergent by SEQ_2:def_6; ::_thesis: lim rseq = integral ((lim (H,['a,b'])),a,b) hence lim rseq = integral ((lim (H,['a,b'])),a,b) by A98, SEQ_2:def_7; ::_thesis: verum end;