:: Riemann Indefinite Integral of Functions of Real Variable :: by Yasunari Shidama , Noboru Endou , Katsumi Wasaki and Katuhiko Kanazashi :: :: Received June 6, 2007 :: Copyright (c) 2007-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, PARTFUN1, SUBSET_1, FUNCT_1, RELAT_1, XXREAL_2, COMPLEX1, ARYTM_1, XXREAL_0, SEQ_4, ARYTM_3, REAL_1, FDIFF_1, RCOMP_1, TARSKI, VALUED_1, CARD_1, ORDINAL4, INTEGRA5, INTEGRA1, XXREAL_1, SQUARE_1, ORDINAL2, FUNCOP_1, FCONT_1, REALSET1, SIN_COS, PREPOWER, SEQFUNC, SEQ_1, SEQ_2, INTEGRA2, FUNCT_3, FINSEQ_1, FINSEQ_2, CARD_3, MEASURE7, NAT_1, INTEGRA7, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, XXREAL_2, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCOP_1, RELSET_1, FUNCT_2, RCOMP_1, PARTFUN1, PARTFUN2, FINSEQ_1, VALUED_1, SEQ_1, RFUNCT_1, SEQ_2, SEQ_4, SQUARE_1, PREPOWER, FCONT_1, FDIFF_1, FINSEQ_2, RVSUM_1, INTEGRA1, INTEGRA2, SEQFUNC, SIN_COS, TAYLOR_1, INTEGRA3, INTEGRA5; constructors REAL_1, FDIFF_1, PARTFUN2, RFUNCT_1, INTEGRA2, LIMFUNC1, FCONT_1, BINOP_2, INTEGRA5, SIN_COS, PREPOWER, TAYLOR_1, SQUARE_1, SEQFUNC, RVSUM_1, SEQ_4, RELSET_1, SEQ_2, COMPLEX1, INTEGRA3, COMSEQ_2; registrations XREAL_0, RELSET_1, INTEGRA1, RCOMP_1, INT_1, MEMBERED, PREPOWER, XBOOLE_0, NUMBERS, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, SEQ_2, FCONT_3, MEASURE5, SQUARE_1, FINSEQ_2, RELAT_1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; definitions FDIFF_1; equalities XCMPLX_0, SUBSET_1, INTEGRA1, INTEGRA5, VALUED_1, SQUARE_1; expansions INTEGRA1, INTEGRA5, FDIFF_1; theorems TARSKI, PARTFUN1, RVSUM_1, ZFMISC_1, PREPOWER, INTEGRA1, INTEGRA2, RFUNCT_1, FUNCT_1, SEQ_1, SEQ_2, FDIFF_1, SEQFUNC, ABSVALUE, XCMPLX_1, FINSEQ_1, FINSEQ_2, RCOMP_1, FCONT_1, FDIFF_2, RELAT_1, XREAL_0, XXREAL_0, PARTFUN2, FUNCT_2, XBOOLE_0, XBOOLE_1, SEQ_4, XREAL_1, COMPLEX1, INTEGRA4, INTEGRA5, SIN_COS, INTEGRA6, TAYLOR_1, VALUED_1, XXREAL_1, XXREAL_2, FUNCOP_1, ORDINAL1; schemes FUNCT_2, XBOOLE_0; begin :: Preliminaries reserve a,b,r for Real; reserve A for non empty set; reserve X,x for set; reserve f,g,F,G for PartFunc of REAL,REAL; reserve n for Element of NAT; theorem Th1: for f,g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & (for x be set st x in A holds |.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 f,g be Function of A,REAL; assume that A1: rng f is bounded_above and A2: rng g is bounded_above and A3: for x be set st x in A holds |.f.x-g.x.|<=a; A4: dom f = A by FUNCT_2:def 1; A5: for b st b in rng g holds b <= upper_bound rng f + a proof let b; assume b in rng g; then consider x being Element of A such that x in dom g and A6: b=g.x by PARTFUN1:3; |.f.x-g.x.|<=a by A3; then |.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 thesis by A7,XXREAL_0:2; end; A8: dom g = A by FUNCT_2:def 1; A9: upper_bound rng g <= upper_bound rng f + a by A5,SEQ_4:45; A10: for b st b in rng f holds b <= upper_bound rng g + a proof let b; assume b in rng f; 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; |.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 thesis by A12,XXREAL_0:2; end; upper_bound rng f <= upper_bound rng g + a by A10,SEQ_4:45; hence thesis by A9,XREAL_1:20; end; theorem Th2: for f,g being Function of A,REAL st rng f is bounded_below & rng g is bounded_below & (for x be set st x in A holds |.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 f,g be Function of A,REAL; assume that A1: rng f is bounded_below and A2: rng g is bounded_below and A3: for x be set st x in A holds |.f.x-g.x.|<=a; A4: dom f = A by FUNCT_2:def 1; A5: for b st b in rng g holds lower_bound rng f -a <= b proof let b; assume b in rng g; 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; |.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 thesis by A7,XXREAL_0:2; end; A8: dom g = A by FUNCT_2:def 1; A9: lower_bound rng f -a <= lower_bound rng g by A5,SEQ_4:43; A10: for b st b in rng f holds lower_bound rng g -a <=b proof let b; assume b in rng f; then consider x being Element of A such that x in dom f and A11: b=f.x by PARTFUN1:3; |.f.x-g.x.|<=a by A3; then |.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 thesis by A12,XXREAL_0:2; end; lower_bound rng g-a <= lower_bound rng f by A10,SEQ_4:43; hence thesis by A9,XREAL_1:12; end; theorem f|X|X is bounded implies f|X is bounded; theorem Th4: for x be Real st x in X & f|X is_differentiable_in x holds f is_differentiable_in x proof let x be Real; assume that A1: x in X and A2: f|X is_differentiable_in x; consider N be Neighbourhood of x such that A3: N c= dom(f|X) and A4: ex L be LinearFunc, R be RestFunc st for x1 be Real st x1 in N holds (f|X). x1 - (f|X).x = L.(x1-x) + R.(x1-x) by A2; A5: (f|X).x = f.x by A1,FUNCT_1:49; take N; N c= dom f /\ X by A3,RELAT_1:61; hence N c= dom f by XBOOLE_1:18; consider L be LinearFunc, R be RestFunc such that A6: for x1 be Real st x1 in N holds (f|X).x1 - (f|X).x = L.(x1-x) + R.( x1-x) by A4; take L,R; let x1 be Real; assume A7: x1 in N; then (f|X).x1 = f.x1 by A3,FUNCT_1:47; hence thesis by A6,A7,A5; end; theorem f|X is_differentiable_on X implies f is_differentiable_on X proof assume A1: f|X is_differentiable_on X; then A2: for x being Real st x in X holds f|X is_differentiable_in x; X c= dom(f|X) by A1; then X c= dom f /\ X by RELAT_1:61; then X c= dom f by XBOOLE_1:18; hence thesis by A2; end; theorem Th6: 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 proof assume that A1: f is_differentiable_on X and A2: g is_differentiable_on X; reconsider Z = X as Subset of REAL by A1,FDIFF_1:8; reconsider Z as open Subset of REAL by A1,FDIFF_1:10; X c= dom f & X c= dom g by A1,A2; 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,def 1; hence thesis by A1,A2,A4,FDIFF_1:18,19,21; end; theorem Th7: f is_differentiable_on X implies r(#)f is_differentiable_on X proof reconsider r1 = r as Real; assume A1: f is_differentiable_on X; then reconsider Z = X as Subset of REAL by FDIFF_1:8; reconsider Z as open Subset of REAL by A1,FDIFF_1:10; X c= dom f by A1; then Z c= dom(r(#)f) by VALUED_1:def 5; then (r1(#)f) is_differentiable_on X by A1,FDIFF_1:20; hence thesis; end; theorem Th8: (for x be 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 proof assume that A1: for x be set st x in X holds g.x <> 0 and A2: f is_differentiable_on X and A3: g is_differentiable_on X; reconsider Z = X as Subset of REAL by A2,FDIFF_1:8; reconsider Z as open Subset of REAL by A2,FDIFF_1:10; for x be Real st x in Z holds g.x <> 0 by A1; hence thesis by A2,A3,FDIFF_2:21; end; theorem (for x be set st x in X holds f.x <> 0) & f is_differentiable_on X implies f^ is_differentiable_on X proof assume that A1: for x be set st x in X holds f.x <> 0 and A2: f is_differentiable_on X; reconsider Z = X as Subset of REAL by A2,FDIFF_1:8; reconsider Z as open Subset of REAL by A2,FDIFF_1:10; for x be Real st x in Z holds f.x <> 0 by A1; hence thesis by A2,FDIFF_2:22; end; theorem Th10: 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 proof 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; 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 thesis by A4,A5,A3,INTEGRA1:5; end; begin :: The Definition of Indefinite Integral definition let X be set, f be PartFunc of REAL,REAL; func IntegralFuncs(f,X) -> set means :Def1: x in it iff ex F be PartFunc of REAL,REAL st x = F & F is_differentiable_on X & F`|X = f|X; existence proof defpred P[object] means ex F be 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 object holds x in Z iff x in PFuncs(REAL,REAL) & P[x] from XBOOLE_0:sch 1; take Z; let 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; given F being PartFunc of REAL,REAL such that A2: x = F & F is_differentiable_on X & F`|X = f|X; F in PFuncs(REAL,REAL) by PARTFUN1:45; hence thesis by A1,A2; end; uniqueness proof let Z1,Z2 be set such that A3: x in Z1 iff ex F be PartFunc of REAL,REAL st x = F & F is_differentiable_on X & F`|X = f|X and A4: x in Z2 iff ex F be PartFunc of REAL,REAL st x = F & F is_differentiable_on X & F`|X = f|X; for x being object holds x in Z1 iff x in Z2 proof let x be object; x in Z1 iff ex F be PartFunc of REAL,REAL st x = F & F is_differentiable_on X & F`|X = f|X by A3; hence thesis by A4; end; hence thesis by TARSKI:2; end; end; definition let X be set, F,f be PartFunc of REAL,REAL; pred F is_integral_of f,X means F in IntegralFuncs(f,X); end; Lm1: F is_integral_of f,X iff F is_differentiable_on X & F`|X = f|X proof hereby assume F is_integral_of f,X; then F in IntegralFuncs(f,X); then ex F9 be 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; end; assume F is_differentiable_on X & F`|X = f|X; then F in IntegralFuncs(f,X) by Def1; hence thesis; end; theorem Th11: F is_integral_of f,X implies X c= dom F proof assume F is_integral_of f,X; then F in IntegralFuncs(f,X); then ex G be PartFunc of REAL,REAL st F = G & G is_differentiable_on X & G`|X = f|X by Def1; hence thesis; end; theorem 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 proof assume that A1: F is_integral_of f,X and A2: G is_integral_of 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 let x be Element of REAL; assume x in dom((F+G)`|X); then A12: x in X by A7,FDIFF_1:def 7; then F|X is_differentiable_in x by A6; 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; 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; 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 let x be Element of REAL; assume x in dom((F-G)`|X); then A20: x in X by A17,FDIFF_1:def 7; then F|X is_differentiable_in x by A6; 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; 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; 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; 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 thesis by A17,Lm1; end; theorem F is_integral_of f,X implies r(#)F is_integral_of r(#)f,X proof assume A1: F is_integral_of 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 reconsider r1 = r as Real; let x be Element of REAL; assume x in dom((r(#)F)`|X); then A7: x in X by A3,FDIFF_1:def 7; then F|X is_differentiable_in x by A2; 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; 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 thesis by A3,Lm1; end; theorem F is_integral_of f,X & G is_integral_of g,X implies F(#)G is_integral_of f(#)G+F(#)g,X proof assume that A1: F is_integral_of f,X and A2: G is_integral_of 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 let x be Element of REAL; assume x in dom((F(#)G)`|X); then A13: x in X by A9,FDIFF_1:def 7; then F|X is_differentiable_in x by A8; 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; 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; 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 thesis by A9,Lm1; end; theorem (for x be 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 proof assume that A1: for x be 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; 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 let x be Element of REAL; 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); then A15: x in X by A10,FDIFF_1:def 7; then F|X is_differentiable_in x by A9; then A16: F is_differentiable_in x by A15,Th4; G|X is_differentiable_in x by A4,A15; 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 let y be set; assume A19: y in dom(G|X); 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; 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; end; now assume (G|X)"{0} <> {}; then consider y be object 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; 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 thesis by A10,Lm1; end; theorem a <= b & [' a,b '] c= dom f & f|[' a,b '] is continuous & ]. a,b .[ c= dom F & (for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x) + F.a ) implies F is_integral_of f,]. a,b .[ proof 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 be Real st x in ].a,b.[ holds F.x = integral(f,a,x) +F. a; dom(F|O) = dom F /\ O by PARTFUN2:15; then A6: dom(F|O) = O by A4,XBOOLE_1:28; reconsider Fa = F.a as Element of REAL by XREAL_0:def 1; set H1 = REAL --> Fa; deffunc G0(Real) = In(integral(f,a,\$1),REAL); consider G1 be Function of REAL,REAL such that A7: for h be Element of REAL holds G1.h=G0(h) from FUNCT_2:sch 4; reconsider H=H1|O as PartFunc of REAL,REAL; reconsider G=G1|O as PartFunc of REAL,REAL; dom H = dom H1 /\ O by RELAT_1:61; then A8: dom H = REAL /\ O by FUNCT_2:def 1; then A9: dom H = O by XBOOLE_1:28; now let x be Element of REAL; reconsider z=x as Real; assume A10: x in O /\ dom H; then H.x = H1.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; end; then A11: H|O is constant by PARTFUN2:35; then A12: H is_differentiable_on O by A9,FDIFF_1:22; dom G = dom G1 /\ O by RELAT_1:61; then A13: dom G = REAL /\ O by FUNCT_2:def 1; then A14: O = dom G by XBOOLE_1:28; A15: now let x be Real; reconsider z = x as Element of REAL by XREAL_0:def 1; assume x in ].a,b.[; then G.x = G1.x by A14,FUNCT_1:47; then G.x = G0(z) by A7; hence G.x = integral(f,a,x); end; A16: now let x be object; assume A17: x in dom(F|O); then reconsider z=x as Real; reconsider z1=z as Element of REAL by XREAL_0:def 1; H.x = H1.z1 by A9,A6,A17,FUNCT_1:47; then A18: H.x = F.a by FUNCOP_1:7; (F|O).x = F.z by A17,FUNCT_1:47; then (F|O).x = integral(f,a,z) + F.a by A5,A6,A17; hence (F|O).x = G.x + H.x by A15,A6,A17,A18; end; A19: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3; then A20: O c= [' a,b '] by XXREAL_1:25; then A21: O c= dom f by A2,XBOOLE_1:1; A22: for x be Real st x in O holds G is_differentiable_in x & diff(G,x)=f.x proof let x be Real; reconsider z = x as Real; A23: f|O is continuous by A3,A19,FCONT_1:16,XXREAL_1:25; assume A24: x in ]. a,b .[; then x in dom(f|O) by A21,RELAT_1:57; then A25: f|O is_continuous_in z by A23,FCONT_1:def 2; for r be Real st 0 < r ex s be Real st 0 < s & for x1 be Real st x1 in dom f & |.x1-z.| < s holds |.f.x1 - f.z.| < r proof let r be Real; consider ss1 be Real such that A26: 0 < ss1 and A27: ].z-ss1,z+ss1.[ c= O by A24,RCOMP_1:19; assume 0 < r; then consider s be Real such that A28: 0 < s and A29: for x1 be Real st x1 in dom(f|O) & |.x1-z.|= K & x in AB holds |.(H.n).x-(lim(H,AB)).x.| < jj by A3,SEQFUNC:43; (H.K)|AB is bounded by A5; then consider r be Real such that A11: for c be object st c in AB /\ dom(H.K) holds |.(H.K).c.| <= r by RFUNCT_1:73; set H0 = lim(H,AB)||AB; H is_point_conv_on AB by A3,SEQFUNC:22; then A12: dom lim(H,AB) = AB by SEQFUNC:21; then A13: H0 is Function of AB,REAL by FUNCT_2:68,INTEGRA5:6; dom lim(H,AB) c= dom(H.K) by A6,A12,SEQFUNC:def 9; then A14: AB /\ dom lim(H,AB) c= AB /\ dom(H.K) by XBOOLE_1:26; now let c be object; (lim(H,AB)).c = (H.K).c - ((H.K).c - (lim(H,AB)).c); then A15: |.(lim(H,AB)).c.| <= |.(H.K).c.| + |.(H.K).c-(lim(H,AB)).c.| by COMPLEX1:57; assume A16: c in AB /\ dom lim(H,AB); then c in AB by XBOOLE_0:def 4; then A17: |.(H.K).c - (lim(H,AB)).c.| < 1 by A10; |.(H.K).c.| <= r by A11,A14,A16; then |.(H.K).c.| + |.(H.K).c-(lim(H,AB)).c.| <= r+1 by A17,XREAL_1:7; hence |.(lim(H,AB)).c.| <= r+1 by A15,XXREAL_0:2; end; hence A18: lim(H,AB)|AB is bounded by RFUNCT_1:73; then A19: H0|AB is bounded_above; A20: H0|AB is bounded_below by A18; then A21: upper_sum(H0,T) is convergent by A4,A19,A13,INTEGRA4:9; A22: for e be Real st 0 < e ex N be Element of NAT st for n,k be Element of NAT st N<=n holds |.upper_sum((H.n)||AB,T).k-upper_sum(H0,T).k.| <= e*(b-a) proof let e be Real; assume 0 < e; then consider N be Nat such that A23: for n be Nat,x be Element of REAL st n>=N & x in AB holds |.(H.n).x-(lim(H,AB)).x.|=N & x in AB holds |.(H.n).x-(lim(H,AB)).x.|