:: INTEGR15 semantic presentation begin definition let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL; let D be Division of A; mode middle_volume of f,D -> FinSequence of REAL means :Def1: :: INTEGR15:def 1 ( len it = len D & ( for i being Nat st i in dom D holds ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & it . i = r * (vol (divset (D,i))) ) ) ); correctness existence ex b1 being FinSequence of REAL st ( len b1 = len D & ( for i being Nat st i in dom D holds ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & b1 . i = r * (vol (divset (D,i))) ) ) ); proof defpred S1[ Nat, Element of REAL ] means ex r being Element of REAL st ( r in rng (f | (divset (D,\$1))) & \$2 = r * (vol (divset (D,\$1))) ); A1: Seg (len D) = dom D by FINSEQ_1:def_3; A2: for k being Nat st k in Seg (len D) holds ex x being Element of REAL st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of REAL st S1[k,x] ) assume k in Seg (len D) ; ::_thesis: ex x being Element of REAL st S1[k,x] then A3: k in dom D by FINSEQ_1:def_3; dom f = A by FUNCT_2:def_1; then dom (f | (divset (D,k))) = divset (D,k) by A3, INTEGRA1:8, RELAT_1:62; then not rng (f | (divset (D,k))) is empty by RELAT_1:42; then consider r being set such that A4: r in rng (f | (divset (D,k))) by XBOOLE_0:def_1; reconsider r = r as Element of REAL by A4; r * (vol (divset (D,k))) is Element of REAL ; hence ex x being Element of REAL st S1[k,x] by A4; ::_thesis: verum end; consider p being FinSequence of REAL such that A5: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds S1[k,p . k] ) ) from FINSEQ_1:sch_5(A2); len p = len D by A5, FINSEQ_1:def_3; hence ex b1 being FinSequence of REAL st ( len b1 = len D & ( for i being Nat st i in dom D holds ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & b1 . i = r * (vol (divset (D,i))) ) ) ) by A5, A1; ::_thesis: verum end; end; :: deftheorem Def1 defines middle_volume INTEGR15:def_1_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for b4 being FinSequence of REAL holds ( b4 is middle_volume of f,D iff ( len b4 = len D & ( for i being Nat st i in dom D holds ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & b4 . i = r * (vol (divset (D,i))) ) ) ) ); Lm1: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for F being middle_volume of f,D for i being Nat st f | A is bounded_below & i in dom D holds (lower_volume (f,D)) . i <= F . i proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A for F being middle_volume of f,D for i being Nat st f | A is bounded_below & i in dom D holds (lower_volume (f,D)) . i <= F . i let f be Function of A,REAL; ::_thesis: for D being Division of A for F being middle_volume of f,D for i being Nat st f | A is bounded_below & i in dom D holds (lower_volume (f,D)) . i <= F . i let D be Division of A; ::_thesis: for F being middle_volume of f,D for i being Nat st f | A is bounded_below & i in dom D holds (lower_volume (f,D)) . i <= F . i let F be middle_volume of f,D; ::_thesis: for i being Nat st f | A is bounded_below & i in dom D holds (lower_volume (f,D)) . i <= F . i let i be Nat; ::_thesis: ( f | A is bounded_below & i in dom D implies (lower_volume (f,D)) . i <= F . i ) assume that A1: f | A is bounded_below and A2: i in dom D ; ::_thesis: (lower_volume (f,D)) . i <= F . i A3: (lower_volume (f,D)) . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A2, INTEGRA1:def_7; consider r being Element of REAL such that A4: r in rng (f | (divset (D,i))) and A5: F . i = r * (vol (divset (D,i))) by A2, Def1; rng f is bounded_below by A1, INTEGRA1:11; then rng (f | (divset (D,i))) is bounded_below by RELAT_1:70, XXREAL_2:44; then ( 0 <= vol (divset (D,i)) & lower_bound (rng (f | (divset (D,i)))) <= r ) by A4, INTEGRA1:9, SEQ_4:def_2; hence (lower_volume (f,D)) . i <= F . i by A5, A3, XREAL_1:64; ::_thesis: verum end; Lm2: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for e being Real st f | A is bounded_below & 0 < e holds ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A for e being Real st f | A is bounded_below & 0 < e holds ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) let f be Function of A,REAL; ::_thesis: for D being Division of A for e being Real st f | A is bounded_below & 0 < e holds ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) let D be Division of A; ::_thesis: for e being Real st f | A is bounded_below & 0 < e holds ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) let e be Real; ::_thesis: ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) ) assume that A1: f | A is bounded_below and A2: 0 < e ; ::_thesis: ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) defpred S1[ Nat, Element of REAL ] means ex r being Element of REAL st ( r in rng (f | (divset (D,\$1))) & \$2 = r * (vol (divset (D,\$1))) & (lower_volume (f,D)) . \$1 <= \$2 & \$2 < ((lower_volume (f,D)) . \$1) + e ); A3: for k being Nat st k in Seg (len D) holds ex x being Element of REAL st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of REAL st S1[k,x] ) assume k in Seg (len D) ; ::_thesis: ex x being Element of REAL st S1[k,x] then A4: k in dom D by FINSEQ_1:def_3; dom f = A by FUNCT_2:def_1; then dom (f | (divset (D,k))) = divset (D,k) by A4, INTEGRA1:8, RELAT_1:62; then A5: not rng (f | (divset (D,k))) is empty by RELAT_1:42; rng f is bounded_below by A1, INTEGRA1:11; then A6: rng (f | (divset (D,k))) is bounded_below by RELAT_1:70, XXREAL_2:44; percases ( vol (divset (D,k)) = 0 or vol (divset (D,k)) <> 0 ) ; supposeA7: vol (divset (D,k)) = 0 ; ::_thesis: ex x being Element of REAL st S1[k,x] consider r being set such that A8: r in rng (f | (divset (D,k))) by A5, XBOOLE_0:def_1; reconsider r = r as Element of REAL by A8; reconsider x = r * (vol (divset (D,k))) as Element of REAL ; A9: (lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def_7 .= 0 by A7 ; then x < ((lower_volume (f,D)) . k) + e by A2, A7; hence ex x being Element of REAL st S1[k,x] by A7, A8, A9; ::_thesis: verum end; supposeA10: vol (divset (D,k)) <> 0 ; ::_thesis: ex x being Element of REAL st S1[k,x] set l = lower_bound (rng (f | (divset (D,k)))); set e1 = e / (vol (divset (D,k))); A11: 0 < vol (divset (D,k)) by A10, INTEGRA1:9; then 0 < e / (vol (divset (D,k))) by A2, XREAL_1:139; then consider r being real number such that A12: r in rng (f | (divset (D,k))) and A13: r < (lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k)))) by A6, A5, SEQ_4:def_2; A14: (lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def_7; reconsider x = r * (vol (divset (D,k))) as Element of REAL ; x < ((lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k))))) * (vol (divset (D,k))) by A11, A13, XREAL_1:68; then x < ((lower_volume (f,D)) . k) + ((e / (vol (divset (D,k)))) * (vol (divset (D,k)))) by A14; then A15: x < ((lower_volume (f,D)) . k) + e by A10, XCMPLX_1:87; lower_bound (rng (f | (divset (D,k)))) <= r by A6, A12, SEQ_4:def_2; then (lower_volume (f,D)) . k <= x by A11, A14, XREAL_1:64; hence ex x being Element of REAL st S1[k,x] by A12, A15; ::_thesis: verum end; end; end; consider p being FinSequence of REAL such that A16: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds S1[k,p . k] ) ) from FINSEQ_1:sch_5(A3); A17: now__::_thesis:_for_i_being_Nat_st_i_in_dom_D_holds_ ex_r_being_Element_of_REAL_st_ (_r_in_rng_(f_|_(divset_(D,i)))_&_p_._i_=_r_*_(vol_(divset_(D,i)))_) let i be Nat; ::_thesis: ( i in dom D implies ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) ) assume i in dom D ; ::_thesis: ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) then i in Seg (len D) by FINSEQ_1:def_3; then consider r being Element of REAL such that A18: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) and (lower_volume (f,D)) . i <= p . i and p . i < ((lower_volume (f,D)) . i) + e by A16; take r = r; ::_thesis: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) thus ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) by A18; ::_thesis: verum end; len p = len D by A16, FINSEQ_1:def_3; then reconsider p = p as middle_volume of f,D by A17, Def1; now__::_thesis:_for_i_being_Nat_st_i_in_dom_D_holds_ (_(lower_volume_(f,D))_._i_<=_p_._i_&_p_._i_<_((lower_volume_(f,D))_._i)_+_e_) let i be Nat; ::_thesis: ( i in dom D implies ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) ) assume i in dom D ; ::_thesis: ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) then i in Seg (len D) by FINSEQ_1:def_3; then ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) & (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) by A16; hence ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) ; ::_thesis: verum end; hence ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) ; ::_thesis: verum end; Lm3: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for e being Real st f | A is bounded_above & 0 < e holds ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A for e being Real st f | A is bounded_above & 0 < e holds ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i ) let f be Function of A,REAL; ::_thesis: for D being Division of A for e being Real st f | A is bounded_above & 0 < e holds ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i ) let D be Division of A; ::_thesis: for e being Real st f | A is bounded_above & 0 < e holds ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i ) let e be Real; ::_thesis: ( f | A is bounded_above & 0 < e implies ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i ) ) assume that A1: f | A is bounded_above and A2: 0 < e ; ::_thesis: ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i ) defpred S1[ Nat, Element of REAL ] means ex r being Element of REAL st ( r in rng (f | (divset (D,\$1))) & \$2 = r * (vol (divset (D,\$1))) & \$2 <= (upper_volume (f,D)) . \$1 & ((upper_volume (f,D)) . \$1) - e < \$2 ); A3: for k being Nat st k in Seg (len D) holds ex x being Element of REAL st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of REAL st S1[k,x] ) assume k in Seg (len D) ; ::_thesis: ex x being Element of REAL st S1[k,x] then A4: k in dom D by FINSEQ_1:def_3; dom f = A by FUNCT_2:def_1; then dom (f | (divset (D,k))) = divset (D,k) by A4, INTEGRA1:8, RELAT_1:62; then A5: not rng (f | (divset (D,k))) is empty by RELAT_1:42; rng f is bounded_above by A1, INTEGRA1:13; then A6: rng (f | (divset (D,k))) is bounded_above by RELAT_1:70, XXREAL_2:43; percases ( vol (divset (D,k)) = 0 or vol (divset (D,k)) <> 0 ) ; supposeA7: vol (divset (D,k)) = 0 ; ::_thesis: ex x being Element of REAL st S1[k,x] consider r being set such that A8: r in rng (f | (divset (D,k))) by A5, XBOOLE_0:def_1; reconsider r = r as Element of REAL by A8; reconsider x = r * (vol (divset (D,k))) as Element of REAL ; A9: (upper_volume (f,D)) . k = (upper_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def_6 .= 0 by A7 ; then ((upper_volume (f,D)) . k) - e < x by A2, A7; hence ex x being Element of REAL st S1[k,x] by A7, A8, A9; ::_thesis: verum end; supposeA10: vol (divset (D,k)) <> 0 ; ::_thesis: ex x being Element of REAL st S1[k,x] set l = upper_bound (rng (f | (divset (D,k)))); set e1 = e / (vol (divset (D,k))); A11: 0 < vol (divset (D,k)) by A10, INTEGRA1:9; then 0 < e / (vol (divset (D,k))) by A2, XREAL_1:139; then consider r being real number such that A12: r in rng (f | (divset (D,k))) and A13: (upper_bound (rng (f | (divset (D,k))))) - (e / (vol (divset (D,k)))) < r by A6, A5, SEQ_4:def_1; A14: (upper_volume (f,D)) . k = (upper_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def_6; reconsider x = r * (vol (divset (D,k))) as Element of REAL ; ((upper_bound (rng (f | (divset (D,k))))) - (e / (vol (divset (D,k))))) * (vol (divset (D,k))) < x by A11, A13, XREAL_1:68; then ((upper_volume (f,D)) . k) - ((e / (vol (divset (D,k)))) * (vol (divset (D,k)))) < x by A14; then A15: ((upper_volume (f,D)) . k) - e < x by A10, XCMPLX_1:87; r <= upper_bound (rng (f | (divset (D,k)))) by A6, A12, SEQ_4:def_1; then x <= (upper_volume (f,D)) . k by A11, A14, XREAL_1:64; hence ex x being Element of REAL st S1[k,x] by A12, A15; ::_thesis: verum end; end; end; consider p being FinSequence of REAL such that A16: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds S1[k,p . k] ) ) from FINSEQ_1:sch_5(A3); A17: now__::_thesis:_for_i_being_Nat_st_i_in_dom_D_holds_ ex_r_being_Element_of_REAL_st_ (_r_in_rng_(f_|_(divset_(D,i)))_&_p_._i_=_r_*_(vol_(divset_(D,i)))_) let i be Nat; ::_thesis: ( i in dom D implies ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) ) assume i in dom D ; ::_thesis: ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) then i in Seg (len D) by FINSEQ_1:def_3; then consider r being Element of REAL such that A18: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) and p . i <= (upper_volume (f,D)) . i and ((upper_volume (f,D)) . i) - e < p . i by A16; take r = r; ::_thesis: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) thus ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) by A18; ::_thesis: verum end; len p = len D by A16, FINSEQ_1:def_3; then reconsider p = p as middle_volume of f,D by A17, Def1; now__::_thesis:_for_i_being_Nat_st_i_in_dom_D_holds_ (_p_._i_<=_(upper_volume_(f,D))_._i_&_((upper_volume_(f,D))_._i)_-_e_<_p_._i_) let i be Nat; ::_thesis: ( i in dom D implies ( p . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < p . i ) ) assume i in dom D ; ::_thesis: ( p . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < p . i ) then i in Seg (len D) by FINSEQ_1:def_3; then ex r being Element of REAL st ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) & p . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < p . i ) by A16; hence ( p . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < p . i ) ; ::_thesis: verum end; hence ex F being middle_volume of f,D st for i being Nat st i in dom D holds ( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i ) ; ::_thesis: verum end; Lm4: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for F being middle_volume of f,D for i being Nat st f | A is bounded_above & i in dom D holds F . i <= (upper_volume (f,D)) . i proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A for F being middle_volume of f,D for i being Nat st f | A is bounded_above & i in dom D holds F . i <= (upper_volume (f,D)) . i let f be Function of A,REAL; ::_thesis: for D being Division of A for F being middle_volume of f,D for i being Nat st f | A is bounded_above & i in dom D holds F . i <= (upper_volume (f,D)) . i let D be Division of A; ::_thesis: for F being middle_volume of f,D for i being Nat st f | A is bounded_above & i in dom D holds F . i <= (upper_volume (f,D)) . i let F be middle_volume of f,D; ::_thesis: for i being Nat st f | A is bounded_above & i in dom D holds F . i <= (upper_volume (f,D)) . i let i be Nat; ::_thesis: ( f | A is bounded_above & i in dom D implies F . i <= (upper_volume (f,D)) . i ) assume that A1: f | A is bounded_above and A2: i in dom D ; ::_thesis: F . i <= (upper_volume (f,D)) . i A3: (upper_volume (f,D)) . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A2, INTEGRA1:def_6; consider r being Element of REAL such that A4: r in rng (f | (divset (D,i))) and A5: F . i = r * (vol (divset (D,i))) by A2, Def1; rng f is bounded_above by A1, INTEGRA1:13; then rng (f | (divset (D,i))) is bounded_above by RELAT_1:70, XXREAL_2:43; then ( 0 <= vol (divset (D,i)) & r <= upper_bound (rng (f | (divset (D,i)))) ) by A4, INTEGRA1:9, SEQ_4:def_1; hence F . i <= (upper_volume (f,D)) . i by A5, A3, XREAL_1:64; ::_thesis: verum end; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL; let D be Division of A; let F be middle_volume of f,D; func middle_sum (f,F) -> Real equals :: INTEGR15:def 2 Sum F; correctness coherence Sum F is Real; ; end; :: deftheorem defines middle_sum INTEGR15:def_2_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for F being middle_volume of f,D holds middle_sum (f,F) = Sum F; theorem Th1: :: INTEGR15:1 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for F being middle_volume of f,D st f | A is bounded_below holds lower_sum (f,D) <= middle_sum (f,F) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A for F being middle_volume of f,D st f | A is bounded_below holds lower_sum (f,D) <= middle_sum (f,F) let f be Function of A,REAL; ::_thesis: for D being Division of A for F being middle_volume of f,D st f | A is bounded_below holds lower_sum (f,D) <= middle_sum (f,F) let D be Division of A; ::_thesis: for F being middle_volume of f,D st f | A is bounded_below holds lower_sum (f,D) <= middle_sum (f,F) let F be middle_volume of f,D; ::_thesis: ( f | A is bounded_below implies lower_sum (f,D) <= middle_sum (f,F) ) len (lower_volume (f,D)) = len D by INTEGRA1:def_7; then reconsider p = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92; len F = len D by Def1; then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92; assume A1: f | A is bounded_below ; ::_thesis: lower_sum (f,D) <= middle_sum (f,F) now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_D)_holds_ p_._i_<=_q_._i let i be Nat; ::_thesis: ( i in Seg (len D) implies p . i <= q . i ) assume i in Seg (len D) ; ::_thesis: p . i <= q . i then i in dom D by FINSEQ_1:def_3; hence p . i <= q . i by A1, Lm1; ::_thesis: verum end; hence lower_sum (f,D) <= middle_sum (f,F) by RVSUM_1:82; ::_thesis: verum end; theorem Th2: :: INTEGR15:2 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for F being middle_volume of f,D st f | A is bounded_above holds middle_sum (f,F) <= upper_sum (f,D) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A for F being middle_volume of f,D st f | A is bounded_above holds middle_sum (f,F) <= upper_sum (f,D) let f be Function of A,REAL; ::_thesis: for D being Division of A for F being middle_volume of f,D st f | A is bounded_above holds middle_sum (f,F) <= upper_sum (f,D) let D be Division of A; ::_thesis: for F being middle_volume of f,D st f | A is bounded_above holds middle_sum (f,F) <= upper_sum (f,D) let F be middle_volume of f,D; ::_thesis: ( f | A is bounded_above implies middle_sum (f,F) <= upper_sum (f,D) ) len (upper_volume (f,D)) = len D by INTEGRA1:def_6; then reconsider p = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92; len F = len D by Def1; then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92; assume A1: f | A is bounded_above ; ::_thesis: middle_sum (f,F) <= upper_sum (f,D) now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_D)_holds_ q_._i_<=_p_._i let i be Nat; ::_thesis: ( i in Seg (len D) implies q . i <= p . i ) assume i in Seg (len D) ; ::_thesis: q . i <= p . i then i in dom D by FINSEQ_1:def_3; hence q . i <= p . i by A1, Lm4; ::_thesis: verum end; hence middle_sum (f,F) <= upper_sum (f,D) by RVSUM_1:82; ::_thesis: verum end; theorem Th3: :: INTEGR15:3 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for e being Real st f | A is bounded_below & 0 < e holds ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A for e being Real st f | A is bounded_below & 0 < e holds ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e let f be Function of A,REAL; ::_thesis: for D being Division of A for e being Real st f | A is bounded_below & 0 < e holds ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e let D be Division of A; ::_thesis: for e being Real st f | A is bounded_below & 0 < e holds ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e let e be Real; ::_thesis: ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e ) len (lower_volume (f,D)) = len D by INTEGRA1:def_7; then reconsider p = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92; set e1 = e / (len D); assume ( f | A is bounded_below & 0 < e ) ; ::_thesis: ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e then consider F being middle_volume of f,D such that A1: for i being Nat st i in dom D holds ( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + (e / (len D)) ) by Lm2, XREAL_1:139; set s = (len D) |-> (e / (len D)); reconsider t = p + ((len D) |-> (e / (len D))) as Element of (len D) -tuples_on REAL ; take F ; ::_thesis: middle_sum (f,F) <= (lower_sum (f,D)) + e len F = len D by Def1; then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92; now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_D)_holds_ q_._i_<=_t_._i let i be Nat; ::_thesis: ( i in Seg (len D) implies q . i <= t . i ) assume A2: i in Seg (len D) ; ::_thesis: q . i <= t . i then i in dom D by FINSEQ_1:def_3; then q . i <= (p . i) + (e / (len D)) by A1; then q . i <= (p . i) + (((len D) |-> (e / (len D))) . i) by A2, FINSEQ_2:57; hence q . i <= t . i by RVSUM_1:11; ::_thesis: verum end; then Sum q <= Sum t by RVSUM_1:82; then Sum q <= (Sum p) + (Sum ((len D) |-> (e / (len D)))) by RVSUM_1:89; then Sum q <= (Sum p) + ((len D) * (e / (len D))) by RVSUM_1:80; hence middle_sum (f,F) <= (lower_sum (f,D)) + e by XCMPLX_1:87; ::_thesis: verum end; theorem Th4: :: INTEGR15:4 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A for e being Real st f | A is bounded_above & 0 < e holds ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A for e being Real st f | A is bounded_above & 0 < e holds ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F) let f be Function of A,REAL; ::_thesis: for D being Division of A for e being Real st f | A is bounded_above & 0 < e holds ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F) let D be Division of A; ::_thesis: for e being Real st f | A is bounded_above & 0 < e holds ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F) let e be Real; ::_thesis: ( f | A is bounded_above & 0 < e implies ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F) ) len (upper_volume (f,D)) = len D by INTEGRA1:def_6; then reconsider p = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92; set e1 = e / (len D); assume ( f | A is bounded_above & 0 < e ) ; ::_thesis: ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F) then consider F being middle_volume of f,D such that A1: for i being Nat st i in dom D holds ( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - (e / (len D)) < F . i ) by Lm3, XREAL_1:139; set s = (len D) |-> (e / (len D)); reconsider t = p - ((len D) |-> (e / (len D))) as Element of (len D) -tuples_on REAL ; take F ; ::_thesis: (upper_sum (f,D)) - e <= middle_sum (f,F) len F = len D by Def1; then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92; now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_D)_holds_ t_._i_<=_q_._i let i be Nat; ::_thesis: ( i in Seg (len D) implies t . i <= q . i ) assume A2: i in Seg (len D) ; ::_thesis: t . i <= q . i then i in dom D by FINSEQ_1:def_3; then (p . i) - (e / (len D)) <= q . i by A1; then (p . i) - (((len D) |-> (e / (len D))) . i) <= q . i by A2, FINSEQ_2:57; hence t . i <= q . i by RVSUM_1:27; ::_thesis: verum end; then Sum t <= Sum q by RVSUM_1:82; then (Sum p) - (Sum ((len D) |-> (e / (len D)))) <= Sum q by RVSUM_1:90; then (Sum p) - ((len D) * (e / (len D))) <= Sum q by RVSUM_1:80; hence (upper_sum (f,D)) - e <= middle_sum (f,F) by XCMPLX_1:87; ::_thesis: verum end; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL; let T be DivSequence of A; mode middle_volume_Sequence of f,T -> Function of NAT,(REAL *) means :Def3: :: INTEGR15:def 3 for k being Element of NAT holds it . k is middle_volume of f,T . k; correctness existence ex b1 being Function of NAT,(REAL *) st for k being Element of NAT holds b1 . k is middle_volume of f,T . k; proof defpred S1[ Element of NAT , set ] means \$2 is middle_volume of f,T . \$1; A1: for x being Element of NAT ex y being Element of REAL * st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y] set y = the middle_volume of f,T . x; reconsider y = the middle_volume of f,T . x as Element of REAL * by FINSEQ_1:def_11; y is middle_volume of f,T . x ; hence ex y being Element of REAL * st S1[x,y] ; ::_thesis: verum end; ex f being Function of NAT,(REAL *) st for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of NAT,(REAL *) st for k being Element of NAT holds b1 . k is middle_volume of f,T . k ; ::_thesis: verum end; end; :: deftheorem Def3 defines middle_volume_Sequence INTEGR15:def_3_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for T being DivSequence of A for b4 being Function of NAT,(REAL *) holds ( b4 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b4 . k is middle_volume of f,T . k ); definition let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL; let T be DivSequence of A; let S be middle_volume_Sequence of f,T; let k be Element of NAT ; :: original: . redefine funcS . k -> middle_volume of f,T . k; coherence S . k is middle_volume of f,T . k by Def3; end; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL; let T be DivSequence of A; let S be middle_volume_Sequence of f,T; func middle_sum (f,S) -> Real_Sequence means :Def4: :: INTEGR15:def 4 for i being Element of NAT holds it . i = middle_sum (f,(S . i)); existence ex b1 being Real_Sequence st for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) proof deffunc H1( Element of NAT ) -> Real = middle_sum (f,(S . \$1)); thus ex IT being Real_Sequence st for i being Element of NAT holds IT . i = H1(i) from SEQ_1:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds b1 = b2 proof let F1, F2 be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ) implies F1 = F2 ) assume that A1: for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) and A2: for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ; ::_thesis: F1 = F2 for i being Element of NAT holds F1 . i = F2 . i proof let i be Element of NAT ; ::_thesis: F1 . i = F2 . i F1 . i = middle_sum (f,(S . i)) by A1 .= F2 . i by A2 ; hence F1 . i = F2 . i ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines middle_sum INTEGR15:def_4_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for T being DivSequence of A for S being middle_volume_Sequence of f,T for b5 being Real_Sequence holds ( b5 = middle_sum (f,S) iff for i being Element of NAT holds b5 . i = middle_sum (f,(S . i)) ); theorem Th5: :: INTEGR15:5 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for T being DivSequence of A for S being middle_volume_Sequence of f,T for i being Element of NAT st f | A is bounded_below holds (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for T being DivSequence of A for S being middle_volume_Sequence of f,T for i being Element of NAT st f | A is bounded_below holds (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i let f be Function of A,REAL; ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T for i being Element of NAT st f | A is bounded_below holds (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T for i being Element of NAT st f | A is bounded_below holds (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i let S be middle_volume_Sequence of f,T; ::_thesis: for i being Element of NAT st f | A is bounded_below holds (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i let i be Element of NAT ; ::_thesis: ( f | A is bounded_below implies (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i ) assume A1: f | A is bounded_below ; ::_thesis: (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i ( (middle_sum (f,S)) . i = middle_sum (f,(S . i)) & (lower_sum (f,T)) . i = lower_sum (f,(T . i)) ) by Def4, INTEGRA2:def_3; hence (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i by A1, Th1; ::_thesis: verum end; theorem Th6: :: INTEGR15:6 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for T being DivSequence of A for S being middle_volume_Sequence of f,T for i being Element of NAT st f | A is bounded_above holds (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for T being DivSequence of A for S being middle_volume_Sequence of f,T for i being Element of NAT st f | A is bounded_above holds (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i let f be Function of A,REAL; ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T for i being Element of NAT st f | A is bounded_above holds (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T for i being Element of NAT st f | A is bounded_above holds (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i let S be middle_volume_Sequence of f,T; ::_thesis: for i being Element of NAT st f | A is bounded_above holds (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i let i be Element of NAT ; ::_thesis: ( f | A is bounded_above implies (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i ) assume A1: f | A is bounded_above ; ::_thesis: (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i ( (middle_sum (f,S)) . i = middle_sum (f,(S . i)) & (upper_sum (f,T)) . i = upper_sum (f,(T . i)) ) by Def4, INTEGRA2:def_2; hence (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i by A1, Th2; ::_thesis: verum end; theorem Th7: :: INTEGR15:7 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for T being DivSequence of A for e being Element of REAL st 0 < e & f | A is bounded_below holds ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for T being DivSequence of A for e being Element of REAL st 0 < e & f | A is bounded_below holds ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e let f be Function of A,REAL; ::_thesis: for T being DivSequence of A for e being Element of REAL st 0 < e & f | A is bounded_below holds ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e let T be DivSequence of A; ::_thesis: for e being Element of REAL st 0 < e & f | A is bounded_below holds ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e let e be Element of REAL ; ::_thesis: ( 0 < e & f | A is bounded_below implies ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e ) defpred S1[ Element of NAT , set ] means ( \$2 is middle_volume of f,T . \$1 & ex z being middle_volume of f,T . \$1 st ( z = \$2 & middle_sum (f,z) <= (lower_sum (f,(T . \$1))) + e ) ); assume A1: ( 0 < e & f | A is bounded_below ) ; ::_thesis: ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e A2: for x being Element of NAT ex y being Element of REAL * st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y] consider z being middle_volume of f,T . x such that A3: middle_sum (f,z) <= (lower_sum (f,(T . x))) + e by A1, Th3; reconsider y = z as Element of REAL * by FINSEQ_1:def_11; take y ; ::_thesis: S1[x,y] thus S1[x,y] by A3; ::_thesis: verum end; consider F being Function of NAT,(REAL *) such that A4: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A2); reconsider F = F as middle_volume_Sequence of f,T by A4, Def3; now__::_thesis:_for_x_being_Element_of_NAT_holds_(middle_sum_(f,F))_._x_<=_((lower_sum_(f,T))_._x)_+_e let x be Element of NAT ; ::_thesis: (middle_sum (f,F)) . x <= ((lower_sum (f,T)) . x) + e ex z being middle_volume of f,T . x st ( z = F . x & middle_sum (f,z) <= (lower_sum (f,(T . x))) + e ) by A4; then (middle_sum (f,F)) . x <= (lower_sum (f,(T . x))) + e by Def4; hence (middle_sum (f,F)) . x <= ((lower_sum (f,T)) . x) + e by INTEGRA2:def_3; ::_thesis: verum end; hence ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e ; ::_thesis: verum end; theorem Th8: :: INTEGR15:8 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for T being DivSequence of A for e being Element of REAL st 0 < e & f | A is bounded_above holds ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for T being DivSequence of A for e being Element of REAL st 0 < e & f | A is bounded_above holds ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i let f be Function of A,REAL; ::_thesis: for T being DivSequence of A for e being Element of REAL st 0 < e & f | A is bounded_above holds ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i let T be DivSequence of A; ::_thesis: for e being Element of REAL st 0 < e & f | A is bounded_above holds ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i let e be Element of REAL ; ::_thesis: ( 0 < e & f | A is bounded_above implies ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i ) defpred S1[ Element of NAT , set ] means ( \$2 is middle_volume of f,T . \$1 & ex z being middle_volume of f,T . \$1 st ( z = \$2 & (upper_sum (f,(T . \$1))) - e <= middle_sum (f,z) ) ); assume A1: ( 0 < e & f | A is bounded_above ) ; ::_thesis: ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i A2: for x being Element of NAT ex y being Element of REAL * st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y] consider z being middle_volume of f,T . x such that A3: (upper_sum (f,(T . x))) - e <= middle_sum (f,z) by A1, Th4; reconsider y = z as Element of REAL * by FINSEQ_1:def_11; take y ; ::_thesis: S1[x,y] thus S1[x,y] by A3; ::_thesis: verum end; consider F being Function of NAT,(REAL *) such that A4: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A2); reconsider F = F as middle_volume_Sequence of f,T by A4, Def3; now__::_thesis:_for_x_being_Element_of_NAT_holds_((upper_sum_(f,T))_._x)_-_e_<=_(middle_sum_(f,F))_._x let x be Element of NAT ; ::_thesis: ((upper_sum (f,T)) . x) - e <= (middle_sum (f,F)) . x ex z being middle_volume of f,T . x st ( z = F . x & (upper_sum (f,(T . x))) - e <= middle_sum (f,z) ) by A4; then (upper_sum (f,(T . x))) - e <= (middle_sum (f,F)) . x by Def4; hence ((upper_sum (f,T)) . x) - e <= (middle_sum (f,F)) . x by INTEGRA2:def_2; ::_thesis: verum end; hence ex S being middle_volume_Sequence of f,T st for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i ; ::_thesis: verum end; Lm5: for p, q, r being Real_Sequence st p is convergent & r is convergent & lim p = lim r & ( for i being Element of NAT holds p . i <= q . i ) & ( for i being Element of NAT holds q . i <= r . i ) holds ( q is convergent & lim p = lim q & lim r = lim q ) proof let p, q, r be Real_Sequence; ::_thesis: ( p is convergent & r is convergent & lim p = lim r & ( for i being Element of NAT holds p . i <= q . i ) & ( for i being Element of NAT holds q . i <= r . i ) implies ( q is convergent & lim p = lim q & lim r = lim q ) ) assume that A1: p is convergent and A2: r is convergent and A3: lim p = lim r and A4: for i being Element of NAT holds p . i <= q . i and A5: for i being Element of NAT holds q . i <= r . i ; ::_thesis: ( q is convergent & lim p = lim q & lim r = lim q ) A6: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((q_._m)_-_(lim_p))_<_e let e be real number ; ::_thesis: ( 0 < e implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((q . m) - (lim p)) < e ) assume A7: 0 < e ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((q . m) - (lim p)) < e then consider n1 being Element of NAT such that A8: for m being Element of NAT st n1 <= m holds abs ((p . m) - (lim p)) < e by A1, SEQ_2:def_7; consider n2 being Element of NAT such that A9: for m being Element of NAT st n2 <= m holds abs ((r . m) - (lim r)) < e by A2, A7, SEQ_2:def_7; reconsider n = max (n1,n2) as Element of NAT by ORDINAL1:def_12; take n = n; ::_thesis: for m being Element of NAT st n <= m holds abs ((q . m) - (lim p)) < e thus for m being Element of NAT st n <= m holds abs ((q . m) - (lim p)) < e ::_thesis: verum proof let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((q . m) - (lim p)) < e ) assume A10: n <= m ; ::_thesis: abs ((q . m) - (lim p)) < e n1 <= n by XXREAL_0:25; then n1 <= m by A10, XXREAL_0:2; then abs ((p . m) - (lim p)) < e by A8; then p . m in ].((lim p) - e),((lim p) + e).[ by RCOMP_1:1; then p . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by RCOMP_1:def_2; then A11: ex z being Real st ( z = p . m & (lim p) - e < z & z < (lim p) + e ) ; p . m <= q . m by A4; then A12: (lim p) - e < q . m by A11, XXREAL_0:2; n2 <= n by XXREAL_0:25; then n2 <= m by A10, XXREAL_0:2; then abs ((r . m) - (lim r)) < e by A9; then r . m in ].((lim r) - e),((lim r) + e).[ by RCOMP_1:1; then r . m in { z where z is Real : ( (lim r) - e < z & z < (lim r) + e ) } by RCOMP_1:def_2; then A13: ex z being Real st ( z = r . m & (lim r) - e < z & z < (lim r) + e ) ; q . m <= r . m by A5; then q . m < (lim p) + e by A3, A13, XXREAL_0:2; then q . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by A12; then q . m in ].((lim p) - e),((lim p) + e).[ by RCOMP_1:def_2; hence abs ((q . m) - (lim p)) < e by RCOMP_1:1; ::_thesis: verum end; end; hence q is convergent by SEQ_2:def_6; ::_thesis: ( lim p = lim q & lim r = lim q ) hence ( lim q = lim p & lim q = lim r ) by A3, A6, SEQ_2:def_7; ::_thesis: verum end; theorem Th9: :: INTEGR15:9 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let f be Function of A,REAL; ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let S be middle_volume_Sequence of f,T; ::_thesis: ( f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) ) assume that A1: f is bounded and A2: f is integrable and A3: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) A4: dom f = A by FUNCT_2:def_1; then f | A is bounded_below by A1, RELAT_1:69; then A5: for i being Element of NAT holds (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i by Th5; A6: f | A = f by A4, RELAT_1:69; then A7: ( lower_sum (f,T) is convergent & upper_sum (f,T) is convergent ) by A1, A3, INTEGRA4:8, INTEGRA4:9; f | A is bounded_above by A1, A4, RELAT_1:69; then A8: for i being Element of NAT holds (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i by Th6; A9: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A1, A2, A3, A6, INTEGRA4:12; then lim (lower_sum (f,T)) = integral f by A1, A3, A6, INTEGRA4:9; hence ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) by A7, A9, A5, A8, Lm5; ::_thesis: verum end; theorem Th10: :: INTEGR15:10 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f is bounded holds ( f is integrable iff ex I being Real st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f is bounded holds ( f is integrable iff ex I being Real st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) let f be Function of A,REAL; ::_thesis: ( f is bounded implies ( f is integrable iff ex I being Real st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) ) assume A1: f is bounded ; ::_thesis: ( f is integrable iff ex I being Real st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) hereby ::_thesis: ( ex I being Real st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) assume A2: f is integrable ; ::_thesis: ex I being Element of REAL st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) take I = integral f; ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) thus for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, A2, Th9; ::_thesis: verum end; dom f = A by FUNCT_2:def_1; then A3: f | A is bounded by A1, RELAT_1:69; now__::_thesis:_(_ex_I_being_Real_st_ for_T_being_DivSequence_of_A for_S_being_middle_volume_Sequence_of_f,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_ (_middle_sum_(f,S)_is_convergent_&_lim_(middle_sum_(f,S))_=_I_)_implies_f_is_integrable_) assume ex I being Real st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; ::_thesis: f is integrable then consider I being Real such that A4: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; A5: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds lim (upper_sum (f,T)) = I proof let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies lim (upper_sum (f,T)) = I ) set S = the middle_volume_Sequence of f,T; A6: now__::_thesis:_for_i_being_Element_of_NAT_holds_0_<=_((upper_sum_(f,T))_-_(middle_sum_(f,_the_middle_volume_Sequence_of_f,T)))_._i let i be Element of NAT ; ::_thesis: 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i (middle_sum (f, the middle_volume_Sequence of f,T)) . i <= (upper_sum (f,T)) . i by A3, Th6; then ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) <= ((upper_sum (f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) by XREAL_1:9; hence 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i by VALUED_1:15; ::_thesis: verum end; assume A7: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: lim (upper_sum (f,T)) = I then A8: upper_sum (f,T) is convergent by A3, INTEGRA4:9; A9: now__::_thesis:_for_e1_being_real_number_st_0_<_e1_holds_ (lim_(upper_sum_(f,T)))_-_I_<=_e1 let e1 be real number ; ::_thesis: ( 0 < e1 implies (lim (upper_sum (f,T))) - I <= e1 ) reconsider e = e1 as Real by XREAL_0:def_1; assume 0 < e1 ; ::_thesis: (lim (upper_sum (f,T))) - I <= e1 then consider S being middle_volume_Sequence of f,T such that A10: for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A3, Th8; A11: now__::_thesis:_for_i_being_Element_of_NAT_holds_((upper_sum_(f,T))_-_(middle_sum_(f,S)))_._i_<=_e let i be Element of NAT ; ::_thesis: ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A10; then (((upper_sum (f,T)) . i) - e) + e <= ((middle_sum (f,S)) . i) + e by XREAL_1:6; then ((upper_sum (f,T)) . i) - ((middle_sum (f,S)) . i) <= (((middle_sum (f,S)) . i) + e) - ((middle_sum (f,S)) . i) by XREAL_1:9; hence ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e by VALUED_1:15; ::_thesis: verum end; A12: middle_sum (f,S) is convergent by A4, A7; then A13: (upper_sum (f,T)) - (middle_sum (f,S)) is convergent by A8; lim ((upper_sum (f,T)) - (middle_sum (f,S))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f,S))) by A8, A12, SEQ_2:12 .= (lim (upper_sum (f,T))) - I by A4, A7 ; hence (lim (upper_sum (f,T))) - I <= e1 by A11, A13, PREPOWER:2; ::_thesis: verum end; A14: middle_sum (f, the middle_volume_Sequence of f,T) is convergent by A4, A7; then A15: (upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T)) is convergent by A8; lim ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f, the middle_volume_Sequence of f,T))) by A8, A14, SEQ_2:12 .= (lim (upper_sum (f,T))) - I by A4, A7 ; then 0 <= (lim (upper_sum (f,T))) - I by A6, A15, SEQ_2:17; then (lim (upper_sum (f,T))) - I = 0 by A9, XREAL_1:5; hence lim (upper_sum (f,T)) = I ; ::_thesis: verum end; A16: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds I = lim (lower_sum (f,T)) proof let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies I = lim (lower_sum (f,T)) ) set S = the middle_volume_Sequence of f,T; A17: now__::_thesis:_for_i_being_Element_of_NAT_holds_0_<=_((middle_sum_(f,_the_middle_volume_Sequence_of_f,T))_-_(lower_sum_(f,T)))_._i let i be Element of NAT ; ::_thesis: 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i (lower_sum (f,T)) . i <= (middle_sum (f, the middle_volume_Sequence of f,T)) . i by A3, Th5; then ((lower_sum (f,T)) . i) - ((lower_sum (f,T)) . i) <= ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((lower_sum (f,T)) . i) by XREAL_1:9; hence 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i by VALUED_1:15; ::_thesis: verum end; assume A18: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: I = lim (lower_sum (f,T)) then A19: lower_sum (f,T) is convergent by A3, INTEGRA4:8; A20: now__::_thesis:_for_e1_being_real_number_st_0_<_e1_holds_ I_-_(lim_(lower_sum_(f,T)))_<=_e1 let e1 be real number ; ::_thesis: ( 0 < e1 implies I - (lim (lower_sum (f,T))) <= e1 ) reconsider e = e1 as Real by XREAL_0:def_1; assume 0 < e1 ; ::_thesis: I - (lim (lower_sum (f,T))) <= e1 then consider S being middle_volume_Sequence of f,T such that A21: for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A3, Th7; A22: now__::_thesis:_for_i_being_Element_of_NAT_holds_((middle_sum_(f,S))_-_(lower_sum_(f,T)))_._i_<=_e let i be Element of NAT ; ::_thesis: ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A21; then ((middle_sum (f,S)) . i) - ((lower_sum (f,T)) . i) <= (((lower_sum (f,T)) . i) + e) - ((lower_sum (f,T)) . i) by XREAL_1:9; hence ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e by VALUED_1:15; ::_thesis: verum end; A23: middle_sum (f,S) is convergent by A4, A18; then A24: (middle_sum (f,S)) - (lower_sum (f,T)) is convergent by A19; lim ((middle_sum (f,S)) - (lower_sum (f,T))) = (lim (middle_sum (f,S))) - (lim (lower_sum (f,T))) by A19, A23, SEQ_2:12 .= I - (lim (lower_sum (f,T))) by A4, A18 ; hence I - (lim (lower_sum (f,T))) <= e1 by A22, A24, PREPOWER:2; ::_thesis: verum end; A25: middle_sum (f, the middle_volume_Sequence of f,T) is convergent by A4, A18; then A26: (middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T)) is convergent by A19; lim ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) = (lim (middle_sum (f, the middle_volume_Sequence of f,T))) - (lim (lower_sum (f,T))) by A19, A25, SEQ_2:12 .= I - (lim (lower_sum (f,T))) by A4, A18 ; then 0 <= I - (lim (lower_sum (f,T))) by A17, A26, SEQ_2:17; then I - (lim (lower_sum (f,T))) = 0 by A20, XREAL_1:5; hence I = lim (lower_sum (f,T)) ; ::_thesis: verum end; now__::_thesis:_for_T_being_DivSequence_of_A_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_ (lim_(upper_sum_(f,T)))_-_(lim_(lower_sum_(f,T)))_=_0 let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 ) assume A27: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 hence (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = (lim (upper_sum (f,T))) - I by A16 .= I - I by A5, A27 .= 0 ; ::_thesis: verum end; hence f is integrable by A3, INTEGRA4:12; ::_thesis: verum end; hence ( ex I being Real st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) ; ::_thesis: verum end; definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be Function of A,(REAL n); let D be Division of A; mode middle_volume of f,D -> FinSequence of REAL n means :Def5: :: INTEGR15:def 5 ( len it = len D & ( for i being Nat st i in dom D holds ex r being Element of REAL n st ( r in rng (f | (divset (D,i))) & it . i = (vol (divset (D,i))) * r ) ) ); correctness existence ex b1 being FinSequence of REAL n st ( len b1 = len D & ( for i being Nat st i in dom D holds ex r being Element of REAL n st ( r in rng (f | (divset (D,i))) & b1 . i = (vol (divset (D,i))) * r ) ) ); proof defpred S1[ Nat, set ] means ex r being Element of REAL n st ( r in rng (f | (divset (D,\$1))) & \$2 = (vol (divset (D,\$1))) * r ); A1: Seg (len D) = dom D by FINSEQ_1:def_3; A2: for k being Nat st k in Seg (len D) holds ex x being Element of REAL n st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of REAL n st S1[k,x] ) assume k in Seg (len D) ; ::_thesis: ex x being Element of REAL n st S1[k,x] then A3: k in dom D by FINSEQ_1:def_3; dom f = A by FUNCT_2:def_1; then dom (f | (divset (D,k))) = divset (D,k) by A3, INTEGRA1:8, RELAT_1:62; then not rng (f | (divset (D,k))) is empty by RELAT_1:42; then consider r being set such that A4: r in rng (f | (divset (D,k))) by XBOOLE_0:def_1; reconsider r = r as Element of REAL n by A4; (vol (divset (D,k))) * r is Element of REAL n ; hence ex x being Element of REAL n st S1[k,x] by A4; ::_thesis: verum end; consider p being FinSequence of REAL n such that A5: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds S1[k,p . k] ) ) from FINSEQ_1:sch_5(A2); len p = len D by A5, FINSEQ_1:def_3; hence ex b1 being FinSequence of REAL n st ( len b1 = len D & ( for i being Nat st i in dom D holds ex r being Element of REAL n st ( r in rng (f | (divset (D,i))) & b1 . i = (vol (divset (D,i))) * r ) ) ) by A5, A1; ::_thesis: verum end; end; :: deftheorem Def5 defines middle_volume INTEGR15:def_5_:_ for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for D being Division of A for b5 being FinSequence of REAL n holds ( b5 is middle_volume of f,D iff ( len b5 = len D & ( for i being Nat st i in dom D holds ex r being Element of REAL n st ( r in rng (f | (divset (D,i))) & b5 . i = (vol (divset (D,i))) * r ) ) ) ); definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be Function of A,(REAL n); let D be Division of A; let F be middle_volume of f,D; func middle_sum (f,F) -> Element of REAL n means :Def6: :: INTEGR15:def 6 for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & it . i = Sum Fi ); existence ex b1 being Element of REAL n st for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & b1 . i = Sum Fi ) proof defpred S1[ Nat, Element of REAL ] means ex i being Element of NAT ex Fi being FinSequence of REAL st ( \$1 = i & Fi = (proj (i,n)) * F & \$2 = Sum Fi ); A1: for i being Nat st i in Seg n holds ex x being Element of REAL st S1[i,x] proof let i be Nat; ::_thesis: ( i in Seg n implies ex x being Element of REAL st S1[i,x] ) assume i in Seg n ; ::_thesis: ex x being Element of REAL st S1[i,x] then reconsider ii = i as Element of NAT ; reconsider Fi = (proj (ii,n)) * F as FinSequence of REAL ; reconsider x = Sum Fi as Element of REAL ; take x ; ::_thesis: S1[i,x] thus ex ii being Element of NAT ex Fi being FinSequence of REAL st ( i = ii & Fi = (proj (ii,n)) * F & x = Sum Fi ) ; ::_thesis: verum end; consider p being FinSequence of REAL such that A2: ( dom p = Seg n & ( for i being Nat st i in Seg n holds S1[i,p . i] ) ) from FINSEQ_1:sch_5(A1); take p ; ::_thesis: ( p is Element of REAL n & ( for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ) ) A3: for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & p . i = Sum Fi ) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ) reconsider k = i as Nat ; assume i in Seg n ; ::_thesis: ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & p . i = Sum Fi ) then S1[k,p . k] by A2; hence ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ; ::_thesis: verum end; len p = n by A2, FINSEQ_1:def_3; hence ( p is Element of REAL n & ( for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ) ) by A3, FINSEQ_2:92; ::_thesis: verum end; uniqueness for b1, b2 being Element of REAL n st ( for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & b1 . i = Sum Fi ) ) & ( for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & b2 . i = Sum Fi ) ) holds b1 = b2 proof let x1, x2 be Element of REAL n; ::_thesis: ( ( for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & x1 . i = Sum Fi ) ) & ( for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & x2 . i = Sum Fi ) ) implies x1 = x2 ) assume A4: ( ( for i being Element of NAT st i in Seg n holds ex Fi1 being FinSequence of REAL st ( Fi1 = (proj (i,n)) * F & x1 . i = Sum Fi1 ) ) & ( for i being Element of NAT st i in Seg n holds ex Fi2 being FinSequence of REAL st ( Fi2 = (proj (i,n)) * F & x2 . i = Sum Fi2 ) ) ) ; ::_thesis: x1 = x2 A5: for k0 being Nat st k0 in dom x1 holds x1 . k0 = x2 . k0 proof let k0 be Nat; ::_thesis: ( k0 in dom x1 implies x1 . k0 = x2 . k0 ) assume A6: k0 in dom x1 ; ::_thesis: x1 . k0 = x2 . k0 then reconsider k = k0 as Element of NAT ; len x1 = n by CARD_1:def_7; then k0 in Seg n by A6, FINSEQ_1:def_3; then ( ex Fi1 being FinSequence of REAL st ( Fi1 = (proj (k,n)) * F & x1 . k = Sum Fi1 ) & ex Fi2 being FinSequence of REAL st ( Fi2 = (proj (k,n)) * F & x2 . k = Sum Fi2 ) ) by A4; hence x1 . k0 = x2 . k0 ; ::_thesis: verum end; A7: len x2 = n by CARD_1:def_7; len x1 = n by CARD_1:def_7; then dom x1 = Seg n by FINSEQ_1:def_3 .= dom x2 by A7, FINSEQ_1:def_3 ; hence x1 = x2 by A5, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def6 defines middle_sum INTEGR15:def_6_:_ for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for D being Division of A for F being middle_volume of f,D for b6 being Element of REAL n holds ( b6 = middle_sum (f,F) iff for i being Element of NAT st i in Seg n holds ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * F & b6 . i = Sum Fi ) ); definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be Function of A,(REAL n); let T be DivSequence of A; mode middle_volume_Sequence of f,T -> Function of NAT,((REAL n) *) means :Def7: :: INTEGR15:def 7 for k being Element of NAT holds it . k is middle_volume of f,T . k; correctness existence ex b1 being Function of NAT,((REAL n) *) st for k being Element of NAT holds b1 . k is middle_volume of f,T . k; proof defpred S1[ Element of NAT , set ] means \$2 is middle_volume of f,T . \$1; A1: for x being Element of NAT ex y being Element of (REAL n) * st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of (REAL n) * st S1[x,y] set y = the middle_volume of f,T . x; reconsider y = the middle_volume of f,T . x as Element of (REAL n) * by FINSEQ_1:def_11; y is middle_volume of f,T . x ; hence ex y being Element of (REAL n) * st S1[x,y] ; ::_thesis: verum end; ex f being Function of NAT,((REAL n) *) st for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of NAT,((REAL n) *) st for k being Element of NAT holds b1 . k is middle_volume of f,T . k ; ::_thesis: verum end; end; :: deftheorem Def7 defines middle_volume_Sequence INTEGR15:def_7_:_ for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for T being DivSequence of A for b5 being Function of NAT,((REAL n) *) holds ( b5 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b5 . k is middle_volume of f,T . k ); definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be Function of A,(REAL n); let T be DivSequence of A; let S be middle_volume_Sequence of f,T; let k be Element of NAT ; :: original: . redefine funcS . k -> middle_volume of f,T . k; coherence S . k is middle_volume of f,T . k by Def7; end; definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be Function of A,(REAL n); let T be DivSequence of A; let S be middle_volume_Sequence of f,T; func middle_sum (f,S) -> sequence of (REAL-NS n) means :Def8: :: INTEGR15:def 8 for i being Element of NAT holds it . i = middle_sum (f,(S . i)); existence ex b1 being sequence of (REAL-NS n) st for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) proof deffunc H1( Element of NAT ) -> Element of REAL n = middle_sum (f,(S . \$1)); A1: REAL n = the carrier of (REAL-NS n) by REAL_NS1:def_4; ex IT being sequence of (REAL n) st for i being Element of NAT holds IT . i = H1(i) from FUNCT_2:sch_4(); hence ex b1 being sequence of (REAL-NS n) st for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) by A1; ::_thesis: verum end; uniqueness for b1, b2 being sequence of (REAL-NS n) st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds b1 = b2 proof let F1, F2 be sequence of (REAL-NS n); ::_thesis: ( ( for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ) implies F1 = F2 ) assume that A2: for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) and A3: for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ; ::_thesis: F1 = F2 for i being Element of NAT holds F1 . i = F2 . i proof let i be Element of NAT ; ::_thesis: F1 . i = F2 . i thus F1 . i = middle_sum (f,(S . i)) by A2 .= F2 . i by A3 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def8 defines middle_sum INTEGR15:def_8_:_ for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for T being DivSequence of A for S being middle_volume_Sequence of f,T for b6 being sequence of (REAL-NS n) holds ( b6 = middle_sum (f,S) iff for i being Element of NAT holds b6 . i = middle_sum (f,(S . i)) ); definition let n be Nat; let Z be set ; let f, g be PartFunc of Z,(REAL n); funcf + g -> PartFunc of Z,(REAL n) equals :: INTEGR15:def 9 f <++> g; coherence f <++> g is PartFunc of Z,(REAL n) proof set F = f <++> g; rng (f <++> g) c= REAL n proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f <++> g) or y in REAL n ) assume y in rng (f <++> g) ; ::_thesis: y in REAL n then consider x being set such that A1: x in dom (f <++> g) and A2: (f <++> g) . x = y by FUNCT_1:def_3; dom (f <++> g) = (dom f) /\ (dom g) by VALUED_2:def_45; then ( x in dom f & x in dom g ) by A1, XBOOLE_0:def_4; then A3: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def_6; (f /. x) + (g /. x) in REAL n ; hence y in REAL n by A2, A3, A1, VALUED_2:def_45; ::_thesis: verum end; hence f <++> g is PartFunc of Z,(REAL n) by RELSET_1:6; ::_thesis: verum end; funcf - g -> PartFunc of Z,(REAL n) equals :: INTEGR15:def 10 f <--> g; coherence f <--> g is PartFunc of Z,(REAL n) proof set F = f <--> g; rng (f <--> g) c= REAL n proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f <--> g) or y in REAL n ) assume y in rng (f <--> g) ; ::_thesis: y in REAL n then consider x being set such that A4: x in dom (f <--> g) and A5: (f <--> g) . x = y by FUNCT_1:def_3; dom (f <--> g) = (dom f) /\ (dom g) by VALUED_2:def_46; then ( x in dom f & x in dom g ) by A4, XBOOLE_0:def_4; then A6: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def_6; (f /. x) - (g /. x) in REAL n ; hence y in REAL n by A5, A6, A4, VALUED_2:def_46; ::_thesis: verum end; hence f <--> g is PartFunc of Z,(REAL n) by RELSET_1:6; ::_thesis: verum end; end; :: deftheorem defines + INTEGR15:def_9_:_ for n being Nat for Z being set for f, g being PartFunc of Z,(REAL n) holds f + g = f <++> g; :: deftheorem defines - INTEGR15:def_10_:_ for n being Nat for Z being set for f, g being PartFunc of Z,(REAL n) holds f - g = f <--> g; definition let n be Nat; let r be real number ; let Z be set ; let f be PartFunc of Z,(REAL n); funcr (#) f -> PartFunc of Z,(REAL n) equals :: INTEGR15:def 11 f [#] r; coherence f [#] r is PartFunc of Z,(REAL n) proof set F = f [#] r; rng (f [#] r) c= REAL n proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f [#] r) or y in REAL n ) assume y in rng (f [#] r) ; ::_thesis: y in REAL n then consider x being set such that A1: x in dom (f [#] r) and A2: (f [#] r) . x = y by FUNCT_1:def_3; dom (f [#] r) = dom f by VALUED_2:def_39; then A3: f . x = f /. x by A1, PARTFUN1:def_6; r * (f /. x) in REAL n ; hence y in REAL n by A2, A3, A1, VALUED_2:def_39; ::_thesis: verum end; hence f [#] r is PartFunc of Z,(REAL n) by RELSET_1:6; ::_thesis: verum end; end; :: deftheorem defines (#) INTEGR15:def_11_:_ for n being Nat for r being real number for Z being set for f being PartFunc of Z,(REAL n) holds r (#) f = f [#] r; begin definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be Function of A,(REAL n); attrf is bounded means :Def12: :: INTEGR15:def 12 for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is bounded ; end; :: deftheorem Def12 defines bounded INTEGR15:def_12_:_ for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) holds ( f is bounded iff for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is bounded ); Lm6: for n, i being Element of NAT for f being PartFunc of REAL,(REAL n) for i being Element of NAT for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A proof let n, i be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for i being Element of NAT for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A let f be PartFunc of REAL,(REAL n); ::_thesis: for i being Element of NAT for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A let i be Element of NAT ; ::_thesis: for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A let A be Subset of REAL; ::_thesis: (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A A1: dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then A2: rng f c= dom (proj (i,n)) ; A3: rng (f | A) c= dom (proj (i,n)) by A1; A4: now__::_thesis:_for_c_being_set_st_c_in_dom_(((proj_(i,n))_*_f)_|_A)_holds_ (((proj_(i,n))_*_f)_|_A)_._c_=_((proj_(i,n))_*_(f_|_A))_._c let c be set ; ::_thesis: ( c in dom (((proj (i,n)) * f) | A) implies (((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c ) assume A5: c in dom (((proj (i,n)) * f) | A) ; ::_thesis: (((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c then A6: c in (dom ((proj (i,n)) * f)) /\ A by RELAT_1:61; then A7: c in A by XBOOLE_0:def_4; A8: c in dom ((proj (i,n)) * f) by A6, XBOOLE_0:def_4; then c in dom f by A2, RELAT_1:27; then c in (dom f) /\ A by A7, XBOOLE_0:def_4; then A9: c in dom (f | A) by RELAT_1:61; then c in dom ((proj (i,n)) * (f | A)) by A3, RELAT_1:27; then ((proj (i,n)) * (f | A)) . c = (proj (i,n)) . ((f | A) . c) by FUNCT_1:12 .= (proj (i,n)) . (f . c) by A9, FUNCT_1:47 .= ((proj (i,n)) * f) . c by A8, FUNCT_1:12 ; hence (((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c by A5, FUNCT_1:47; ::_thesis: verum end; dom (((proj (i,n)) * f) | A) = (dom ((proj (i,n)) * f)) /\ A by RELAT_1:61 .= (dom f) /\ A by A2, RELAT_1:27 .= dom (f | A) by RELAT_1:61 .= dom ((proj (i,n)) * (f | A)) by A3, RELAT_1:27 ; hence (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A by A4, FUNCT_1:2; ::_thesis: verum end; definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be Function of A,(REAL n); attrf is integrable means :Def13: :: INTEGR15:def 13 for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is integrable ; end; :: deftheorem Def13 defines integrable INTEGR15:def_13_:_ for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) holds ( f is integrable iff for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is integrable ); definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be Function of A,(REAL n); func integral f -> Element of REAL n means :Def14: :: INTEGR15:def 14 ( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds it . i = integral ((proj (i,n)) * f) ) ); existence ex b1 being Element of REAL n st ( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds b1 . i = integral ((proj (i,n)) * f) ) ) proof defpred S1[ Nat, Element of REAL ] means ex i being Element of NAT st ( \$1 = i & \$2 = integral ((proj (i,n)) * f) ); A1: for i being Nat st i in Seg n holds ex x being Element of REAL st S1[i,x] proof let i be Nat; ::_thesis: ( i in Seg n implies ex x being Element of REAL st S1[i,x] ) assume i in Seg n ; ::_thesis: ex x being Element of REAL st S1[i,x] then reconsider ii = i as Element of NAT ; consider x being Element of REAL such that A2: x = integral ((proj (ii,n)) * f) ; take x ; ::_thesis: S1[i,x] thus S1[i,x] by A2; ::_thesis: verum end; consider p being FinSequence of REAL such that A3: ( dom p = Seg n & ( for i being Nat st i in Seg n holds S1[i,p . i] ) ) from FINSEQ_1:sch_5(A1); take p ; ::_thesis: ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds p . i = integral ((proj (i,n)) * f) ) ) A4: for i being Element of NAT st i in Seg n holds p . i = integral ((proj (i,n)) * f) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies p . i = integral ((proj (i,n)) * f) ) assume i in Seg n ; ::_thesis: p . i = integral ((proj (i,n)) * f) then S1[i,p . i] by A3; hence p . i = integral ((proj (i,n)) * f) ; ::_thesis: verum end; len p = n by A3, FINSEQ_1:def_3; hence ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds p . i = integral ((proj (i,n)) * f) ) ) by A3, A4, FINSEQ_2:92; ::_thesis: verum end; uniqueness for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds b1 . i = integral ((proj (i,n)) * f) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds b2 . i = integral ((proj (i,n)) * f) ) holds b1 = b2 proof let x1, x2 be Element of REAL n; ::_thesis: ( dom x1 = Seg n & ( for i being Element of NAT st i in Seg n holds x1 . i = integral ((proj (i,n)) * f) ) & dom x2 = Seg n & ( for i being Element of NAT st i in Seg n holds x2 . i = integral ((proj (i,n)) * f) ) implies x1 = x2 ) assume that A5: dom x1 = Seg n and A6: for i being Element of NAT st i in Seg n holds x1 . i = integral ((proj (i,n)) * f) and A7: dom x2 = Seg n and A8: for i being Element of NAT st i in Seg n holds x2 . i = integral ((proj (i,n)) * f) ; ::_thesis: x1 = x2 now__::_thesis:_for_k_being_Nat_st_k_in_dom_x1_holds_ x1_._k_=_x2_._k let k be Nat; ::_thesis: ( k in dom x1 implies x1 . k = x2 . k ) assume A9: k in dom x1 ; ::_thesis: x1 . k = x2 . k then reconsider i = k as Element of NAT ; x1 . i = integral ((proj (i,n)) * f) by A5, A6, A9 .= x2 . i by A5, A8, A9 ; hence x1 . k = x2 . k ; ::_thesis: verum end; hence x1 = x2 by A5, A7, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def14 defines integral INTEGR15:def_14_:_ for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for b4 being Element of REAL n holds ( b4 = integral f iff ( dom b4 = Seg n & ( for i being Element of NAT st i in Seg n holds b4 . i = integral ((proj (i,n)) * f) ) ) ); theorem Th11: :: INTEGR15:11 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let f be Function of A,(REAL n); ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let S be middle_volume_Sequence of f,T; ::_thesis: ( f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) ) assume that A1: ( f is bounded & f is integrable ) and A2: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) set seq = middle_sum (f,S); set xs = integral f; REAL n = the carrier of (REAL-NS n) by REAL_NS1:def_4; then reconsider xseq = middle_sum (f,S) as Function of NAT,(REAL n) ; A3: for i being Element of NAT st i in Seg n holds ex rseqi being Real_Sequence st for k being Element of NAT holds ( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex rseqi being Real_Sequence st for k being Element of NAT holds ( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) ) reconsider pjinf = (proj (i,n)) * f as Function of A,REAL ; defpred S1[ Element of NAT , set ] means \$2 = (proj (i,n)) * (S . \$1); A4: for x being Element of NAT ex y being Element of REAL * st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y] (proj (i,n)) * (S . x) is Element of REAL * by FINSEQ_1:def_11; hence ex y being Element of REAL * st S1[x,y] ; ::_thesis: verum end; consider F being Function of NAT,(REAL *) such that A5: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A4); A6: for x being Element of NAT holds ( (proj (i,n)) * (S . x) is FinSequence of REAL & dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) & rng ((proj (i,n)) * (S . x)) c= REAL ) proof let x be Element of NAT ; ::_thesis: ( (proj (i,n)) * (S . x) is FinSequence of REAL & dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) & rng ((proj (i,n)) * (S . x)) c= REAL ) dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng (S . x) c= dom (proj (i,n)) ; then dom ((proj (i,n)) * (S . x)) = dom (S . x) by RELAT_1:27 .= Seg (len (S . x)) by FINSEQ_1:def_3 ; hence ( (proj (i,n)) * (S . x) is FinSequence of REAL & dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) & rng ((proj (i,n)) * (S . x)) c= REAL ) ; ::_thesis: verum end; for k being Element of NAT holds F . k is middle_volume of pjinf,T . k proof let k be Element of NAT ; ::_thesis: F . k is middle_volume of pjinf,T . k reconsider Tk = T . k as FinSequence ; reconsider Fk = F . k as FinSequence of REAL by FINSEQ_1:def_11; A7: F . k = (proj (i,n)) * (S . k) by A5; then A8: dom Fk = Seg (len (S . k)) by A6 .= Seg (len Tk) by Def5 ; then A9: dom Fk = dom Tk by FINSEQ_1:def_3; A10: now__::_thesis:_for_j_being_Nat_st_j_in_dom_Tk_holds_ ex_v_being_Element_of_REAL_st_ (_v_in_rng_(pjinf_|_(divset_((T_._k),j)))_&_Fk_._j_=_v_*_(vol_(divset_((T_._k),j)))_) let j be Nat; ::_thesis: ( j in dom Tk implies ex v being Element of REAL st ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) ) dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then A11: rng f c= dom (proj (i,n)) ; assume A12: j in dom Tk ; ::_thesis: ex v being Element of REAL st ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) then consider r being Element of REAL n such that A13: r in rng (f | (divset ((T . k),j))) and A14: (S . k) . j = (vol (divset ((T . k),j))) * r by Def5; reconsider v = (proj (i,n)) . r as Element of REAL ; take v = v; ::_thesis: ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) consider t being set such that A15: t in dom (f | (divset ((T . k),j))) and A16: r = (f | (divset ((T . k),j))) . t by A13, FUNCT_1:def_3; t in (dom f) /\ (divset ((T . k),j)) by A15, RELAT_1:61; then t in dom f by XBOOLE_0:def_4; then A17: t in dom ((proj (i,n)) * f) by A11, RELAT_1:27; A18: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61 .= (dom pjinf) /\ (divset ((T . k),j)) by A11, RELAT_1:27 .= dom (pjinf | (divset ((T . k),j))) by RELAT_1:61 ; (proj (i,n)) . r = (proj (i,n)) . (f . t) by A15, A16, FUNCT_1:47 .= ((proj (i,n)) * f) . t by A17, FUNCT_1:12 .= (pjinf | (divset ((T . k),j))) . t by A15, A18, FUNCT_1:47 ; hence v in rng (pjinf | (divset ((T . k),j))) by A15, A18, FUNCT_1:3; ::_thesis: Fk . j = v * (vol (divset ((T . k),j))) thus Fk . j = (proj (i,n)) . ((S . k) . j) by A7, A9, A12, FUNCT_1:12 .= ((vol (divset ((T . k),j))) * r) . i by A14, PDIFF_1:def_1 .= (vol (divset ((T . k),j))) * (r . i) by RVSUM_1:44 .= v * (vol (divset ((T . k),j))) by PDIFF_1:def_1 ; ::_thesis: verum end; len Fk = len Tk by A8, FINSEQ_1:def_3; hence F . k is middle_volume of pjinf,T . k by A10, Def1; ::_thesis: verum end; then reconsider pjis = F as middle_volume_Sequence of pjinf,T by Def3; reconsider rseqi = middle_sum (pjinf,pjis) as Real_Sequence ; assume A19: i in Seg n ; ::_thesis: ex rseqi being Real_Sequence st for k being Element of NAT holds ( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) A20: for k being Element of NAT holds rseqi . k = (xseq . k) . i proof let k be Element of NAT ; ::_thesis: rseqi . k = (xseq . k) . i A21: ex Fi being FinSequence of REAL st ( Fi = (proj (i,n)) * (S . k) & (middle_sum (f,(S . k))) . i = Sum Fi ) by A19, Def6; thus rseqi . k = middle_sum (pjinf,(pjis . k)) by Def4 .= (middle_sum (f,(S . k))) . i by A5, A21 .= (xseq . k) . i by Def8 ; ::_thesis: verum end; take rseqi ; ::_thesis: for k being Element of NAT holds ( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) A22: ( (proj (i,n)) * f is bounded & pjinf is integrable ) by A1, A19, Def12, Def13; then lim (middle_sum (pjinf,pjis)) = integral pjinf by A2, Th9; hence for k being Element of NAT holds ( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) by A2, A19, A22, A20, Def14, Th9; ::_thesis: verum end; reconsider x = integral f as Point of (REAL-NS n) by REAL_NS1:def_4; integral f = x ; hence ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) by A3, REAL_NS1:11; ::_thesis: verum end; theorem :: INTEGR15:12 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) st f is bounded holds ( f is integrable iff ex I being Element of REAL n st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,(REAL n) st f is bounded holds ( f is integrable iff ex I being Element of REAL n st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) st f is bounded holds ( f is integrable iff ex I being Element of REAL n st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) let f be Function of A,(REAL n); ::_thesis: ( f is bounded implies ( f is integrable iff ex I being Element of REAL n st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) ) assume A1: f is bounded ; ::_thesis: ( f is integrable iff ex I being Element of REAL n st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) hereby ::_thesis: ( ex I being Element of REAL n st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) reconsider I = integral f as Element of REAL n ; assume A2: f is integrable ; ::_thesis: ex I being Element of REAL n st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) take I = I; ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) thus for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, A2, Th11; ::_thesis: verum end; now__::_thesis:_(_ex_I_being_Element_of_REAL_n_st_ for_T_being_DivSequence_of_A for_S_being_middle_volume_Sequence_of_f,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_ (_middle_sum_(f,S)_is_convergent_&_lim_(middle_sum_(f,S))_=_I_)_implies_f_is_integrable_) assume ex I being Element of REAL n st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; ::_thesis: f is integrable then consider I being Element of REAL n such that A3: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ (proj_(i,n))_*_f_is_integrable let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * f is integrable ) reconsider Ii = I . i as Element of REAL ; assume A4: i in Seg n ; ::_thesis: (proj (i,n)) * f is integrable A5: now__::_thesis:_for_T_being_DivSequence_of_A for_Si_being_middle_volume_Sequence_of_(proj_(i,n))_*_f,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_ (_middle_sum_(((proj_(i,n))_*_f),Si)_is_convergent_&_lim_(middle_sum_(((proj_(i,n))_*_f),Si))_=_Ii_) set x = I; let T be DivSequence of A; ::_thesis: for Si being middle_volume_Sequence of (proj (i,n)) * f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) let Si be middle_volume_Sequence of (proj (i,n)) * f,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) ) defpred S1[ Element of NAT , set ] means ex H, z being FinSequence st ( H = T . \$1 & z = \$2 & len z = len H & ( for j being Element of NAT st j in dom H holds ex rji being Element of REAL n ex tji being Element of REAL st ( tji in dom (f | (divset ((T . \$1),j))) & (Si . \$1) . j = (vol (divset ((T . \$1),j))) * ((((proj (i,n)) * f) | (divset ((T . \$1),j))) . tji) & rji = (f | (divset ((T . \$1),j))) . tji & z . j = (vol (divset ((T . \$1),j))) * rji ) ) ); reconsider xs = I as Element of REAL n ; A6: for k being Element of NAT ex y being Element of (REAL n) * st S1[k,y] proof let k be Element of NAT ; ::_thesis: ex y being Element of (REAL n) * st S1[k,y] reconsider Tk = T . k as FinSequence ; defpred S2[ Nat, set ] means ex j being Element of NAT st ( \$1 = j & ex rji being Element of REAL n ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & \$2 = (vol (divset ((T . k),j))) * rji ) ); A7: for j being Nat st j in Seg (len Tk) holds ex x being Element of REAL n st S2[j,x] proof dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then A8: rng f c= dom (proj (i,n)) ; let j0 be Nat; ::_thesis: ( j0 in Seg (len Tk) implies ex x being Element of REAL n st S2[j0,x] ) assume A9: j0 in Seg (len Tk) ; ::_thesis: ex x being Element of REAL n st S2[j0,x] then reconsider j = j0 as Element of NAT ; j in dom Tk by A9, FINSEQ_1:def_3; then consider r being Element of REAL such that A10: r in rng (((proj (i,n)) * f) | (divset ((T . k),j))) and A11: (Si . k) . j = r * (vol (divset ((T . k),j))) by Def1; consider tji being set such that A12: tji in dom (((proj (i,n)) * f) | (divset ((T . k),j))) and A13: r = (((proj (i,n)) * f) | (divset ((T . k),j))) . tji by A10, FUNCT_1:def_3; tji in (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A12, RELAT_1:61; then reconsider tji = tji as Element of REAL ; A14: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61 .= (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A8, RELAT_1:27 .= dom (((proj (i,n)) * f) | (divset ((T . k),j))) by RELAT_1:61 ; then (f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j))) by A12, FUNCT_1:3; then reconsider rji = (f | (divset ((T . k),j))) . tji as Element of REAL n ; reconsider x = (vol (divset ((T . k),j))) * rji as Element of REAL n ; take x ; ::_thesis: S2[j0,x] thus S2[j0,x] by A11, A12, A13, A14; ::_thesis: verum end; consider p being FinSequence of REAL n such that A15: ( dom p = Seg (len Tk) & ( for j being Nat st j in Seg (len Tk) holds S2[j,p . j] ) ) from FINSEQ_1:sch_5(A7); reconsider x = p as Element of (REAL n) * by FINSEQ_1:def_11; take x ; ::_thesis: S1[k,x] A16: now__::_thesis:_for_jj0_being_Element_of_NAT_st_jj0_in_dom_Tk_holds_ ex_rji_being_Element_of_REAL_n_ex_tji_being_Element_of_REAL_st_ (_tji_in_dom_(f_|_(divset_((T_._k),jj0)))_&_(Si_._k)_._jj0_=_(vol_(divset_((T_._k),jj0)))_*_((((proj_(i,n))_*_f)_|_(divset_((T_._k),jj0)))_._tji)_&_rji_=_(f_|_(divset_((T_._k),jj0)))_._tji_&_p_._jj0_=_(vol_(divset_((T_._k),jj0)))_*_rji_) let jj0 be Element of NAT ; ::_thesis: ( jj0 in dom Tk implies ex rji being Element of REAL n ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) ) reconsider j0 = jj0 as Nat ; A17: dom Tk = Seg (len Tk) by FINSEQ_1:def_3; assume jj0 in dom Tk ; ::_thesis: ex rji being Element of REAL n ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) then S2[j0,p . j0] by A15, A17; hence ex rji being Element of REAL n ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) ; ::_thesis: verum end; len p = len Tk by A15, FINSEQ_1:def_3; hence S1[k,x] by A16; ::_thesis: verum end; consider S being Function of NAT,((REAL n) *) such that A18: for x being Element of NAT holds S1[x,S . x] from FUNCT_2:sch_3(A6); for k being Element of NAT holds S . k is middle_volume of f,T . k proof let k be Element of NAT ; ::_thesis: S . k is middle_volume of f,T . k consider H, z being FinSequence such that A19: ( H = T . k & z = S . k & len H = len z ) and A20: for j being Element of NAT st j in dom H holds ex rji being Element of REAL n ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A18; A21: now__::_thesis:_for_x_being_Nat_st_x_in_dom_H_holds_ ex_rji_being_Element_of_REAL_n_st_ (_rji_in_rng_(f_|_(divset_((T_._k),x)))_&_z_._x_=_(vol_(divset_((T_._k),x)))_*_rji_) let x be Nat; ::_thesis: ( x in dom H implies ex rji being Element of REAL n st ( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji ) ) assume A22: x in dom H ; ::_thesis: ex rji being Element of REAL n st ( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji ) then reconsider j = x as Element of NAT ; consider rji being Element of REAL n, tji being Element of REAL such that A23: tji in dom (f | (divset ((T . k),j))) and (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) and A24: rji = (f | (divset ((T . k),j))) . tji and A25: z . j = (vol (divset ((T . k),j))) * rji by A20, A22; take rji = rji; ::_thesis: ( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji ) thus rji in rng (f | (divset ((T . k),x))) by A23, A24, FUNCT_1:3; ::_thesis: z . x = (vol (divset ((T . k),x))) * rji thus z . x = (vol (divset ((T . k),x))) * rji by A25; ::_thesis: verum end; S . k is FinSequence of REAL n by FINSEQ_1:def_11; hence S . k is middle_volume of f,T . k by A19, A21, Def5; ::_thesis: verum end; then reconsider S = S as middle_volume_Sequence of f,T by Def7; set seq = middle_sum (f,S); REAL n = the carrier of (REAL-NS n) by REAL_NS1:def_4; then reconsider xseq = middle_sum (f,S) as Function of NAT,(REAL n) ; assume ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) then ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A3; then consider rseqi being Real_Sequence such that A26: for k being Element of NAT holds ( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) by A4, REAL_NS1:11; for k being Element of NAT holds rseqi . k = (middle_sum (((proj (i,n)) * f),Si)) . k proof let k be Element of NAT ; ::_thesis: rseqi . k = (middle_sum (((proj (i,n)) * f),Si)) . k consider H, z being FinSequence such that A27: H = T . k and A28: z = S . k and A29: len H = len z and A30: for j being Element of NAT st j in dom H holds ex rji being Element of REAL n ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A18; dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng (S . k) c= dom (proj (i,n)) ; then A31: dom ((proj (i,n)) * (S . k)) = dom (S . k) by RELAT_1:27 .= Seg (len H) by A28, A29, FINSEQ_1:def_3 .= Seg (len (Si . k)) by A27, Def1 .= dom (Si . k) by FINSEQ_1:def_3 ; A32: for j being Nat st j in dom ((proj (i,n)) * (S . k)) holds ((proj (i,n)) * (S . k)) . j = (Si . k) . j proof let j0 be Nat; ::_thesis: ( j0 in dom ((proj (i,n)) * (S . k)) implies ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0 ) reconsider j = j0 as Element of NAT by ORDINAL1:def_12; dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then A33: rng f c= dom (proj (i,n)) ; assume A34: j0 in dom ((proj (i,n)) * (S . k)) ; ::_thesis: ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0 then j0 in Seg (len (Si . k)) by A31, FINSEQ_1:def_3; then j0 in Seg (len H) by A27, Def1; then j in dom H by FINSEQ_1:def_3; then consider rji being Element of REAL n, tji being Element of REAL such that A35: tji in dom (f | (divset ((T . k),j))) and A36: (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) and A37: rji = (f | (divset ((T . k),j))) . tji and A38: z . j = (vol (divset ((T . k),j))) * rji by A30; A39: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61 .= (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A33, RELAT_1:27 .= dom (((proj (i,n)) * f) | (divset ((T . k),j))) by RELAT_1:61 ; then tji in (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A35, RELAT_1:61; then A40: tji in dom ((proj (i,n)) * f) by XBOOLE_0:def_4; A41: (((proj (i,n)) * f) | (divset ((T . k),j))) . tji = ((proj (i,n)) * f) . tji by A35, A39, FUNCT_1:47 .= (proj (i,n)) . (f . tji) by A40, FUNCT_1:12 .= (proj (i,n)) . rji by A35, A37, FUNCT_1:47 ; ((proj (i,n)) * (S . k)) . j = (proj (i,n)) . ((S . k) . j) by A34, FUNCT_1:12 .= ((vol (divset ((T . k),j))) * rji) . i by A28, A38, PDIFF_1:def_1 .= (vol (divset ((T . k),j))) * (rji . i) by RVSUM_1:44 .= (Si . k) . j by A36, A41, PDIFF_1:def_1 ; hence ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0 ; ::_thesis: verum end; consider Fi being FinSequence of REAL such that A42: Fi = (proj (i,n)) * (S . k) and A43: (middle_sum (f,(S . k))) . i = Sum Fi by A4, Def6; thus rseqi . k = (xseq . k) . i by A26 .= Sum Fi by A43, Def8 .= middle_sum (((proj (i,n)) * f),(Si . k)) by A31, A32, A42, FINSEQ_1:13 .= (middle_sum (((proj (i,n)) * f),Si)) . k by Def4 ; ::_thesis: verum end; hence ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) by A26, FUNCT_2:63; ::_thesis: verum end; (proj (i,n)) * f is bounded by A1, A4, Def12; hence (proj (i,n)) * f is integrable by A5, Th10; ::_thesis: verum end; hence f is integrable by Def13; ::_thesis: verum end; hence ( ex I being Element of REAL n st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) ; ::_thesis: verum end; definition let n be Element of NAT ; let f be PartFunc of REAL,(REAL n); attrf is bounded means :Def15: :: INTEGR15:def 15 for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is bounded ; end; :: deftheorem Def15 defines bounded INTEGR15:def_15_:_ for n being Element of NAT for f being PartFunc of REAL,(REAL n) holds ( f is bounded iff for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is bounded ); definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,(REAL n); predf is_integrable_on A means :Def16: :: INTEGR15:def 16 for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is_integrable_on A; end; :: deftheorem Def16 defines is_integrable_on INTEGR15:def_16_:_ for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) holds ( f is_integrable_on A iff for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is_integrable_on A ); definition let n be Element of NAT ; let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,(REAL n); func integral (f,A) -> Element of REAL n means :Def17: :: INTEGR15:def 17 ( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds it . i = integral (((proj (i,n)) * f),A) ) ); existence ex b1 being Element of REAL n st ( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds b1 . i = integral (((proj (i,n)) * f),A) ) ) proof defpred S1[ Nat, Element of REAL ] means ex i being Element of NAT st ( \$1 = i & \$2 = integral (((proj (i,n)) * f),A) ); A1: for i being Nat st i in Seg n holds ex x being Element of REAL st S1[i,x] proof let i be Nat; ::_thesis: ( i in Seg n implies ex x being Element of REAL st S1[i,x] ) assume i in Seg n ; ::_thesis: ex x being Element of REAL st S1[i,x] then reconsider ii = i as Element of NAT ; consider x being Element of REAL such that A2: x = integral (((proj (ii,n)) * f),A) ; take x ; ::_thesis: S1[i,x] thus S1[i,x] by A2; ::_thesis: verum end; consider p being FinSequence of REAL such that A3: ( dom p = Seg n & ( for i being Nat st i in Seg n holds S1[i,p . i] ) ) from FINSEQ_1:sch_5(A1); take p ; ::_thesis: ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds p . i = integral (((proj (i,n)) * f),A) ) ) A4: for i being Element of NAT st i in Seg n holds p . i = integral (((proj (i,n)) * f),A) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies p . i = integral (((proj (i,n)) * f),A) ) assume i in Seg n ; ::_thesis: p . i = integral (((proj (i,n)) * f),A) then S1[i,p . i] by A3; hence p . i = integral (((proj (i,n)) * f),A) ; ::_thesis: verum end; len p = n by A3, FINSEQ_1:def_3; hence ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds p . i = integral (((proj (i,n)) * f),A) ) ) by A3, A4, FINSEQ_2:92; ::_thesis: verum end; uniqueness for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds b1 . i = integral (((proj (i,n)) * f),A) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds b2 . i = integral (((proj (i,n)) * f),A) ) holds b1 = b2 proof let x1, x2 be Element of REAL n; ::_thesis: ( dom x1 = Seg n & ( for i being Element of NAT st i in Seg n holds x1 . i = integral (((proj (i,n)) * f),A) ) & dom x2 = Seg n & ( for i being Element of NAT st i in Seg n holds x2 . i = integral (((proj (i,n)) * f),A) ) implies x1 = x2 ) assume that A5: dom x1 = Seg n and A6: for i being Element of NAT st i in Seg n holds x1 . i = integral (((proj (i,n)) * f),A) and A7: dom x2 = Seg n and A8: for i being Element of NAT st i in Seg n holds x2 . i = integral (((proj (i,n)) * f),A) ; ::_thesis: x1 = x2 for k being Nat st k in dom x1 holds x1 . k = x2 . k proof let k be Nat; ::_thesis: ( k in dom x1 implies x1 . k = x2 . k ) assume A9: k in dom x1 ; ::_thesis: x1 . k = x2 . k then reconsider k = k as Element of NAT ; x2 . k = integral (((proj (k,n)) * f),A) by A5, A8, A9; hence x1 . k = x2 . k by A5, A6, A9; ::_thesis: verum end; hence x1 = x2 by A5, A7, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def17 defines integral INTEGR15:def_17_:_ for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for b4 being Element of REAL n holds ( b4 = integral (f,A) iff ( dom b4 = Seg n & ( for i being Element of NAT st i in Seg n holds b4 . i = integral (((proj (i,n)) * f),A) ) ) ); theorem :: INTEGR15:13 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f | A = g holds ( f is_integrable_on A iff g is integrable ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f | A = g holds ( f is_integrable_on A iff g is integrable ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f | A = g holds ( f is_integrable_on A iff g is integrable ) let f be PartFunc of REAL,(REAL n); ::_thesis: for g being Function of A,(REAL n) st f | A = g holds ( f is_integrable_on A iff g is integrable ) let g be Function of A,(REAL n); ::_thesis: ( f | A = g implies ( f is_integrable_on A iff g is integrable ) ) assume A1: f | A = g ; ::_thesis: ( f is_integrable_on A iff g is integrable ) thus ( f is_integrable_on A implies g is integrable ) ::_thesis: ( g is integrable implies f is_integrable_on A ) proof assume A2: f is_integrable_on A ; ::_thesis: g is integrable for i being Element of NAT st i in Seg n holds (proj (i,n)) * g is integrable proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * g is integrable ) dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng f c= dom (proj (i,n)) ; then A3: dom ((proj (i,n)) * f) = dom f by RELAT_1:27; A = dom g by FUNCT_2:def_1 .= (dom f) /\ A by A1, RELAT_1:61 ; then ((proj (i,n)) * f) || A is total by A3, INTEGRA5:6, XBOOLE_1:17; then reconsider F = ((proj (i,n)) * f) | A as Function of A,REAL ; assume i in Seg n ; ::_thesis: (proj (i,n)) * g is integrable then (proj (i,n)) * f is_integrable_on A by A2, Def16; then F is integrable by INTEGRA5:def_1; hence (proj (i,n)) * g is integrable by A1, Lm6; ::_thesis: verum end; hence g is integrable by Def13; ::_thesis: verum end; assume A4: g is integrable ; ::_thesis: f is_integrable_on A for i being Element of NAT st i in Seg n holds (proj (i,n)) * f is_integrable_on A proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * f is_integrable_on A ) assume A5: i in Seg n ; ::_thesis: (proj (i,n)) * f is_integrable_on A (proj (i,n)) * g = ((proj (i,n)) * f) | A by A1, Lm6; then ((proj (i,n)) * f) || A is integrable by A4, A5, Def13; hence (proj (i,n)) * f is_integrable_on A by INTEGRA5:def_1; ::_thesis: verum end; hence f is_integrable_on A by Def16; ::_thesis: verum end; theorem :: INTEGR15:14 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f | A = g holds integral (f,A) = integral g proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f | A = g holds integral (f,A) = integral g let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) for g being Function of A,(REAL n) st f | A = g holds integral (f,A) = integral g let f be PartFunc of REAL,(REAL n); ::_thesis: for g being Function of A,(REAL n) st f | A = g holds integral (f,A) = integral g let g be Function of A,(REAL n); ::_thesis: ( f | A = g implies integral (f,A) = integral g ) assume A1: f | A = g ; ::_thesis: integral (f,A) = integral g A2: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(integral_(f,A))_holds_ (integral_(f,A))_._k_=_(integral_g)_._k let k be Nat; ::_thesis: ( k in dom (integral (f,A)) implies (integral (f,A)) . k = (integral g) . k ) assume A3: k in dom (integral (f,A)) ; ::_thesis: (integral (f,A)) . k = (integral g) . k then reconsider i = k as Element of NAT ; dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng f c= dom (proj (i,n)) ; then A4: dom ((proj (i,n)) * f) = dom f by RELAT_1:27; A = dom g by FUNCT_2:def_1 .= (dom f) /\ A by A1, RELAT_1:61 ; then ((proj (i,n)) * f) || A is total by A4, INTEGRA5:6, XBOOLE_1:17; then reconsider F = ((proj (i,n)) * f) | A as Function of A,REAL ; A5: F = (proj (i,n)) * g by A1, Lm6; A6: i in Seg n by A3, Def17; then (integral (f,A)) . i = integral (((proj (i,n)) * f),A) by Def17 .= integral (((proj (i,n)) * f) || A) ; hence (integral (f,A)) . k = (integral g) . k by A6, A5, Def14; ::_thesis: verum end; dom (integral (f,A)) = Seg n by Def17 .= dom (integral g) by Def14 ; hence integral (f,A) = integral g by A2, FINSEQ_1:13; ::_thesis: verum end; definition let a, b be real number ; let n be Element of NAT ; let f be PartFunc of REAL,(REAL n); func integral (f,a,b) -> Element of REAL n means :Def18: :: INTEGR15:def 18 ( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds it . i = integral (((proj (i,n)) * f),a,b) ) ); existence ex b1 being Element of REAL n st ( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds b1 . i = integral (((proj (i,n)) * f),a,b) ) ) proof defpred S1[ Nat, Element of REAL ] means ex i being Element of NAT st ( \$1 = i & \$2 = integral (((proj (i,n)) * f),a,b) ); A1: for i being Nat st i in Seg n holds ex x being Element of REAL st S1[i,x] proof let i be Nat; ::_thesis: ( i in Seg n implies ex x being Element of REAL st S1[i,x] ) assume i in Seg n ; ::_thesis: ex x being Element of REAL st S1[i,x] then reconsider ii = i as Element of NAT ; consider x being Element of REAL such that A2: x = integral (((proj (ii,n)) * f),a,b) ; take x ; ::_thesis: S1[i,x] thus S1[i,x] by A2; ::_thesis: verum end; consider p being FinSequence of REAL such that A3: ( dom p = Seg n & ( for i being Nat st i in Seg n holds S1[i,p . i] ) ) from FINSEQ_1:sch_5(A1); take p ; ::_thesis: ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds p . i = integral (((proj (i,n)) * f),a,b) ) ) A4: for i being Element of NAT st i in Seg n holds p . i = integral (((proj (i,n)) * f),a,b) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies p . i = integral (((proj (i,n)) * f),a,b) ) assume i in Seg n ; ::_thesis: p . i = integral (((proj (i,n)) * f),a,b) then S1[i,p . i] by A3; hence p . i = integral (((proj (i,n)) * f),a,b) ; ::_thesis: verum end; len p = n by A3, FINSEQ_1:def_3; hence ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds p . i = integral (((proj (i,n)) * f),a,b) ) ) by A3, A4, FINSEQ_2:92; ::_thesis: verum end; uniqueness for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds b1 . i = integral (((proj (i,n)) * f),a,b) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds b2 . i = integral (((proj (i,n)) * f),a,b) ) holds b1 = b2 proof let x1, x2 be Element of REAL n; ::_thesis: ( dom x1 = Seg n & ( for i being Element of NAT st i in Seg n holds x1 . i = integral (((proj (i,n)) * f),a,b) ) & dom x2 = Seg n & ( for i being Element of NAT st i in Seg n holds x2 . i = integral (((proj (i,n)) * f),a,b) ) implies x1 = x2 ) assume that A5: dom x1 = Seg n and A6: for i being Element of NAT st i in Seg n holds x1 . i = integral (((proj (i,n)) * f),a,b) and A7: dom x2 = Seg n and A8: for i being Element of NAT st i in Seg n holds x2 . i = integral (((proj (i,n)) * f),a,b) ; ::_thesis: x1 = x2 for k being Nat st k in dom x1 holds x1 . k = x2 . k proof let k be Nat; ::_thesis: ( k in dom x1 implies x1 . k = x2 . k ) assume A9: k in dom x1 ; ::_thesis: x1 . k = x2 . k then reconsider k = k as Element of NAT ; x2 . k = integral (((proj (k,n)) * f),a,b) by A5, A8, A9; hence x1 . k = x2 . k by A5, A6, A9; ::_thesis: verum end; hence x1 = x2 by A5, A7, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def18 defines integral INTEGR15:def_18_:_ for a, b being real number for n being Element of NAT for f being PartFunc of REAL,(REAL n) for b5 being Element of REAL n holds ( b5 = integral (f,a,b) iff ( dom b5 = Seg n & ( for i being Element of NAT st i in Seg n holds b5 . i = integral (((proj (i,n)) * f),a,b) ) ) ); begin theorem Th15: :: INTEGR15:15 for Z being set for n, i being Element of NAT for f1, f2 being PartFunc of Z,(REAL n) holds ( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) ) proof let Z be set ; ::_thesis: for n, i being Element of NAT for f1, f2 being PartFunc of Z,(REAL n) holds ( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) ) let n, i be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of Z,(REAL n) holds ( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) ) let f1, f2 be PartFunc of Z,(REAL n); ::_thesis: ( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) ) A1: dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng f1 c= dom (proj (i,n)) ; then A2: dom ((proj (i,n)) * f1) = dom f1 by RELAT_1:27; A3: rng (f1 + f2) c= dom (proj (i,n)) by A1; then A4: dom ((proj (i,n)) * (f1 + f2)) = dom (f1 + f2) by RELAT_1:27; rng f2 c= dom (proj (i,n)) by A1; then A5: dom ((proj (i,n)) * f2) = dom f2 by RELAT_1:27; A6: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_2:def_45; A7: for z being Element of Z st z in dom ((proj (i,n)) * (f1 + f2)) holds ((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z proof let z be Element of Z; ::_thesis: ( z in dom ((proj (i,n)) * (f1 + f2)) implies ((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z ) reconsider f1z = f1 /. z as Element of n -tuples_on REAL ; reconsider f2z = f2 /. z as Element of n -tuples_on REAL ; assume A8: z in dom ((proj (i,n)) * (f1 + f2)) ; ::_thesis: ((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z then A9: z in dom (f1 + f2) by A3, RELAT_1:27; then A10: z in (dom f1) /\ (dom f2) by VALUED_2:def_45; then z in dom f1 by XBOOLE_0:def_4; then A11: f1 . z = f1z by PARTFUN1:def_6; z in dom f2 by A10, XBOOLE_0:def_4; then A12: f2 . z = f2z by PARTFUN1:def_6; (proj (i,n)) . ((f1 + f2) . z) = (proj (i,n)) . ((f1 . z) + (f2 . z)) by A9, VALUED_2:def_45; then (proj (i,n)) . ((f1 + f2) . z) = ((f1 /. z) + (f2 /. z)) . i by A11, A12, PDIFF_1:def_1; then A13: (proj (i,n)) . ((f1 + f2) . z) = (f1z . i) + (f2z . i) by RVSUM_1:11; A14: z in (dom ((proj (i,n)) * f1)) /\ (dom ((proj (i,n)) * f2)) by A2, A5, A4, A8, VALUED_2:def_45; then z in dom ((proj (i,n)) * f1) by XBOOLE_0:def_4; then ((proj (i,n)) * f1) . z = (proj (i,n)) . (f1 . z) by FUNCT_1:12; then A15: ((proj (i,n)) * f1) . z = f1z . i by A11, PDIFF_1:def_1; z in dom ((proj (i,n)) * f2) by A14, XBOOLE_0:def_4; then ((proj (i,n)) * f2) . z = (proj (i,n)) . (f2 . z) by FUNCT_1:12; then A16: ((proj (i,n)) * f2) . z = f2z . i by A12, PDIFF_1:def_1; z in dom (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) by A6, A2, A5, A4, A8, VALUED_1:def_1; then (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z = (f1z . i) + (f2z . i) by A15, A16, VALUED_1:def_1; hence ((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z by A8, A13, FUNCT_1:12; ::_thesis: verum end; dom ((proj (i,n)) * (f1 + f2)) = dom (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) by A6, A2, A5, A4, VALUED_1:def_1; hence (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) by A7, PARTFUN1:5; ::_thesis: (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) A17: rng (f1 - f2) c= dom (proj (i,n)) by A1; then A18: dom ((proj (i,n)) * (f1 - f2)) = dom (f1 - f2) by RELAT_1:27; A19: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_2:def_46; then A20: dom ((proj (i,n)) * (f1 - f2)) = dom (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) by A2, A5, A18, VALUED_1:12; for z being Element of Z st z in dom ((proj (i,n)) * (f1 - f2)) holds ((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z proof let z be Element of Z; ::_thesis: ( z in dom ((proj (i,n)) * (f1 - f2)) implies ((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z ) reconsider f1z = f1 /. z as Element of n -tuples_on REAL ; reconsider f2z = f2 /. z as Element of n -tuples_on REAL ; assume A21: z in dom ((proj (i,n)) * (f1 - f2)) ; ::_thesis: ((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z then A22: z in dom (f1 - f2) by A17, RELAT_1:27; then A23: z in (dom f1) /\ (dom f2) by VALUED_2:def_46; then z in dom f1 by XBOOLE_0:def_4; then A24: f1 . z = f1z by PARTFUN1:def_6; z in dom f2 by A23, XBOOLE_0:def_4; then A25: f2 . z = f2z by PARTFUN1:def_6; z in dom ((proj (i,n)) * f2) by A5, A19, A18, A21, XBOOLE_0:def_4; then ((proj (i,n)) * f2) . z = (proj (i,n)) . (f2 . z) by FUNCT_1:12; then A26: ((proj (i,n)) * f2) . z = f2z . i by A25, PDIFF_1:def_1; (proj (i,n)) . ((f1 - f2) . z) = (proj (i,n)) . ((f1 . z) - (f2 . z)) by A22, VALUED_2:def_46; then (proj (i,n)) . ((f1 - f2) . z) = ((f1 /. z) - (f2 /. z)) . i by A24, A25, PDIFF_1:def_1; then A27: (proj (i,n)) . ((f1 - f2) . z) = (f1z . i) - (f2z . i) by RVSUM_1:27; z in dom ((proj (i,n)) * f1) by A2, A19, A18, A21, XBOOLE_0:def_4; then ((proj (i,n)) * f1) . z = (proj (i,n)) . (f1 . z) by FUNCT_1:12; then A28: ((proj (i,n)) * f1) . z = f1z . i by A24, PDIFF_1:def_1; (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z = (((proj (i,n)) * f1) . z) - (((proj (i,n)) * f2) . z) by A20, A21, VALUED_1:13; hence ((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z by A21, A27, A28, A26, FUNCT_1:12; ::_thesis: verum end; hence (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) by A20, PARTFUN1:5; ::_thesis: verum end; theorem Th16: :: INTEGR15:16 for Z being set for n, i being Element of NAT for r being Real for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) proof let Z be set ; ::_thesis: for n, i being Element of NAT for r being Real for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) let n, i be Element of NAT ; ::_thesis: for r being Real for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) let r be Real; ::_thesis: for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) let f be PartFunc of Z,(REAL n); ::_thesis: (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) A1: dom (r (#) f) = dom f by VALUED_2:def_39; A2: dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then A3: rng (r (#) f) c= dom (proj (i,n)) ; rng f c= dom (proj (i,n)) by A2; then A4: dom ((proj (i,n)) * f) = dom f by RELAT_1:27; then dom (r (#) ((proj (i,n)) * f)) = dom f by VALUED_1:def_5; then A5: dom ((proj (i,n)) * (r (#) f)) = dom (r (#) ((proj (i,n)) * f)) by A1, A3, RELAT_1:27; for z being Element of Z st z in dom (r (#) ((proj (i,n)) * f)) holds ((proj (i,n)) * (r (#) f)) . z = (r (#) ((proj (i,n)) * f)) . z proof let z be Element of Z; ::_thesis: ( z in dom (r (#) ((proj (i,n)) * f)) implies ((proj (i,n)) * (r (#) f)) . z = (r (#) ((proj (i,n)) * f)) . z ) reconsider fz = f /. z as Element of n -tuples_on REAL ; reconsider rfz = (r (#) f) /. z as Element of n -tuples_on REAL ; assume A6: z in dom (r (#) ((proj (i,n)) * f)) ; ::_thesis: ((proj (i,n)) * (r (#) f)) . z = (r (#) ((proj (i,n)) * f)) . z then A7: z in dom ((proj (i,n)) * f) by VALUED_1:def_5; then A8: f . z = fz by A4, PARTFUN1:def_6; (r (#) ((proj (i,n)) * f)) . z = r * (((proj (i,n)) * f) . z) by A6, VALUED_1:def_5 .= r * ((proj (i,n)) . fz) by A7, A8, FUNCT_1:12 ; then A9: (r (#) ((proj (i,n)) * f)) . z = r * (fz . i) by PDIFF_1:def_1; A10: (r (#) f) . z = rfz by A1, A4, A7, PARTFUN1:def_6; thus ((proj (i,n)) * (r (#) f)) . z = (proj (i,n)) . ((r (#) f) . z) by A5, A6, FUNCT_1:12 .= rfz . i by A10, PDIFF_1:def_1 .= (r (#) fz) . i by A1, A4, A7, A8, A10, VALUED_2:def_39 .= (r (#) ((proj (i,n)) * f)) . z by A9, RVSUM_1:44 ; ::_thesis: verum end; hence (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) by A5, PARTFUN1:5; ::_thesis: verum end; theorem :: INTEGR15:17 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded implies ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) ) assume that A1: ( f1 is_integrable_on A & f2 is_integrable_on A ) and A2: ( A c= dom f1 & A c= dom f2 ) and A3: f1 | A is bounded and A4: f2 | A is bounded ; ::_thesis: ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) A5: for i being Element of NAT st i in Seg n holds ( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) ) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) ) ) assume i in Seg n ; ::_thesis: ( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) ) dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then ( rng f1 c= dom (proj (i,n)) & rng f2 c= dom (proj (i,n)) ) ; hence ( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) ) by A2, RELAT_1:27; ::_thesis: verum end; A6: for i being Element of NAT st i in Seg n holds ( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) ) assume A7: i in Seg n ; ::_thesis: ( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) then A8: ( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) ) by A5; (proj (i,n)) * (f2 | A) is bounded by A4, A7, Def15; then A9: ((proj (i,n)) * f2) | A is bounded by Lm6; (proj (i,n)) * (f1 | A) is bounded by A3, A7, Def15; then A10: ((proj (i,n)) * f1) | A is bounded by Lm6; A11: ( (proj (i,n)) * f1 is_integrable_on A & (proj (i,n)) * f2 is_integrable_on A ) by A1, A7, Def16; hence ( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) ) by A8, A10, A9, INTEGRA6:11; ::_thesis: ( ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) thus ( ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) by A8, A10, A9, A11, INTEGRA6:11; ::_thesis: verum end; A12: for i being Element of NAT st i in Seg n holds ( (proj (i,n)) * (f1 + f2) is_integrable_on A & (proj (i,n)) * (f1 - f2) is_integrable_on A ) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (proj (i,n)) * (f1 + f2) is_integrable_on A & (proj (i,n)) * (f1 - f2) is_integrable_on A ) ) assume i in Seg n ; ::_thesis: ( (proj (i,n)) * (f1 + f2) is_integrable_on A & (proj (i,n)) * (f1 - f2) is_integrable_on A ) then ( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A ) by A6; hence ( (proj (i,n)) * (f1 + f2) is_integrable_on A & (proj (i,n)) * (f1 - f2) is_integrable_on A ) by Th15; ::_thesis: verum end; then for i being Element of NAT st i in Seg n holds (proj (i,n)) * (f1 + f2) is_integrable_on A ; hence f1 + f2 is_integrable_on A by Def16; ::_thesis: ( f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) A13: for i being Element of NAT st i in Seg n holds ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) ) assume A14: i in Seg n ; ::_thesis: ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) then (integral (f1,A)) . i = integral (((proj (i,n)) * f1),A) by Def17; hence ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) by A14, Def17; ::_thesis: verum end; A15: for i being Element of NAT st i in Seg n holds ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) ) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) ) ) assume A16: i in Seg n ; ::_thesis: ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) ) then ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) by A13; hence ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) ) by A6, A16; ::_thesis: verum end; A17: for i being Element of NAT st i in Seg n holds ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) ) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) ) ) assume i in Seg n ; ::_thesis: ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) ) then ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) ) by A15; hence ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) ) by Th15; ::_thesis: verum end; A18: for i being Element of NAT st i in Seg n holds ( (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) & (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) ) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) & (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) ) ) assume A19: i in Seg n ; ::_thesis: ( (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) & (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) ) then ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) ) by A17; hence ( (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) & (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) ) by A19, Def17; ::_thesis: verum end; for i being Element of NAT st i in Seg n holds (proj (i,n)) * (f1 - f2) is_integrable_on A by A12; hence f1 - f2 is_integrable_on A by Def16; ::_thesis: ( integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) A20: dom (integral ((f1 + f2),A)) = Seg n by FINSEQ_1:89; A21: for i being Element of NAT st i in dom (integral ((f1 + f2),A)) holds (integral ((f1 + f2),A)) . i = ((integral (f1,A)) + (integral (f2,A))) . i proof let i be Element of NAT ; ::_thesis: ( i in dom (integral ((f1 + f2),A)) implies (integral ((f1 + f2),A)) . i = ((integral (f1,A)) + (integral (f2,A))) . i ) assume i in dom (integral ((f1 + f2),A)) ; ::_thesis: (integral ((f1 + f2),A)) . i = ((integral (f1,A)) + (integral (f2,A))) . i then (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) by A18, A20; hence (integral ((f1 + f2),A)) . i = ((integral (f1,A)) + (integral (f2,A))) . i by RVSUM_1:11; ::_thesis: verum end; dom ((integral (f1,A)) + (integral (f2,A))) = Seg n by FINSEQ_1:89; hence integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) by A21, FINSEQ_1:89, PARTFUN1:5; ::_thesis: integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) A22: dom (integral ((f1 - f2),A)) = Seg n by FINSEQ_1:89; A23: for i being Element of NAT st i in dom (integral ((f1 - f2),A)) holds (integral ((f1 - f2),A)) . i = ((integral (f1,A)) - (integral (f2,A))) . i proof let i be Element of NAT ; ::_thesis: ( i in dom (integral ((f1 - f2),A)) implies (integral ((f1 - f2),A)) . i = ((integral (f1,A)) - (integral (f2,A))) . i ) assume i in dom (integral ((f1 - f2),A)) ; ::_thesis: (integral ((f1 - f2),A)) . i = ((integral (f1,A)) - (integral (f2,A))) . i then (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) by A18, A22; hence (integral ((f1 - f2),A)) . i = ((integral (f1,A)) - (integral (f2,A))) . i by RVSUM_1:27; ::_thesis: verum end; dom ((integral (f1,A)) - (integral (f2,A))) = Seg n by FINSEQ_1:89; hence integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) by A23, FINSEQ_1:89, PARTFUN1:5; ::_thesis: verum end; theorem :: INTEGR15:18 for n being Element of NAT for r being Real for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) proof let n be Element of NAT ; ::_thesis: for r being Real for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) ) assume that A1: A c= dom f and A2: f is_integrable_on A and A3: f | A is bounded ; ::_thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) A4: now__::_thesis:_for_i_being_Element_of_NAT_holds_A_c=_dom_((proj_(i,n))_*_f) let i be Element of NAT ; ::_thesis: A c= dom ((proj (i,n)) * f) dom (proj (i,n)) = REAL n by FUNCT_2:def_1; then rng f c= dom (proj (i,n)) ; hence A c= dom ((proj (i,n)) * f) by A1, RELAT_1:27; ::_thesis: verum end; A5: for i being Element of NAT st i in Seg n holds integral ((r (#) ((proj (i,n)) * f)),A) = r * (integral (((proj (i,n)) * f),A)) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies integral ((r (#) ((proj (i,n)) * f)),A) = r * (integral (((proj (i,n)) * f),A)) ) assume A6: i in Seg n ; ::_thesis: integral ((r (#) ((proj (i,n)) * f)),A) = r * (integral (((proj (i,n)) * f),A)) ((proj (i,n)) * f) | A = (proj (i,n)) * (f | A) by Lm6; then A7: ((proj (i,n)) * f) | A is bounded by A3, A6, Def15; A8: A c= dom ((proj (i,n)) * f) by A4; (proj (i,n)) * f is_integrable_on A by A2, A6, Def16; hence integral ((r (#) ((proj (i,n)) * f)),A) = r * (integral (((proj (i,n)) * f),A)) by A7, A8, INTEGRA6:9; ::_thesis: verum end; A9: for i being Element of NAT st i in Seg n holds (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A)) proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A)) ) assume i in Seg n ; ::_thesis: (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A)) then r * ((integral (f,A)) . i) = r * (integral (((proj (i,n)) * f),A)) by Def17; hence (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A)) by RVSUM_1:45; ::_thesis: verum end; A10: for i being Element of NAT st i in Seg n holds (integral ((r (#) f),A)) . i = (r * (integral (f,A))) . i proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (integral ((r (#) f),A)) . i = (r * (integral (f,A))) . i ) A11: integral ((r (#) ((proj (i,n)) * f)),A) = integral (((proj (i,n)) * (r (#) f)),A) by Th16; assume A12: i in Seg n ; ::_thesis: (integral ((r (#) f),A)) . i = (r * (integral (f,A))) . i then ( (integral ((r (#) f),A)) . i = integral (((proj (i,n)) * (r (#) f)),A) & (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A)) ) by A9, Def17; hence (integral ((r (#) f),A)) . i = (r * (integral (f,A))) . i by A5, A12, A11; ::_thesis: verum end; for i being Element of NAT st i in Seg n holds (proj (i,n)) * (r (#) f) is_integrable_on A proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * (r (#) f) is_integrable_on A ) assume A13: i in Seg n ; ::_thesis: (proj (i,n)) * (r (#) f) is_integrable_on A ((proj (i,n)) * f) | A = (proj (i,n)) * (f | A) by Lm6; then A14: ((proj (i,n)) * f) | A is bounded by A3, A13, Def15; A15: A c= dom ((proj (i,n)) * f) by A4; (proj (i,n)) * f is_integrable_on A by A2, A13, Def16; then r (#) ((proj (i,n)) * f) is_integrable_on A by A14, A15, INTEGRA6:9; hence (proj (i,n)) * (r (#) f) is_integrable_on A by Th16; ::_thesis: verum end; hence r (#) f is_integrable_on A by Def16; ::_thesis: integral ((r (#) f),A) = r * (integral (f,A)) A16: dom (integral ((r (#) f),A)) = Seg n by FINSEQ_1:89; then dom (integral ((r (#) f),A)) = dom (r * (integral (f,A))) by FINSEQ_1:89; hence integral ((r (#) f),A) = r * (integral (f,A)) by A10, A16, PARTFUN1:5; ::_thesis: verum end; theorem :: INTEGR15:19 for n being Element of NAT for f being PartFunc of REAL,(REAL n) for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) let f be PartFunc of REAL,(REAL n); ::_thesis: for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) let a, b be Real; ::_thesis: ( A = [.a,b.] implies integral (f,A) = integral (f,a,b) ) assume A1: A = [.a,b.] ; ::_thesis: integral (f,A) = integral (f,a,b) A2: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_(f,A))_holds_ (integral_(f,A))_._i_=_(integral_(f,a,b))_._i let i be Nat; ::_thesis: ( i in dom (integral (f,A)) implies (integral (f,A)) . i = (integral (f,a,b)) . i ) assume A3: i in dom (integral (f,A)) ; ::_thesis: (integral (f,A)) . i = (integral (f,a,b)) . i then reconsider k = i as Element of NAT ; dom (integral (f,A)) = Seg n by Def17; then ( (integral (f,A)) . k = integral (((proj (k,n)) * f),A) & (integral (f,a,b)) . k = integral (((proj (k,n)) * f),a,b) ) by A3, Def17, Def18; hence (integral (f,A)) . i = (integral (f,a,b)) . i by A1, INTEGRA5:19; ::_thesis: verum end; dom (integral (f,A)) = Seg n by Def17 .= dom (integral (f,a,b)) by Def18 ; hence integral (f,A) = integral (f,a,b) by A2, FINSEQ_1:13; ::_thesis: verum end; theorem :: INTEGR15:20 for n being Element of NAT for f being PartFunc of REAL,(REAL n) for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) let f be PartFunc of REAL,(REAL n); ::_thesis: for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) let a, b be Real; ::_thesis: ( A = [.b,a.] implies - (integral (f,A)) = integral (f,a,b) ) assume A1: A = [.b,a.] ; ::_thesis: - (integral (f,A)) = integral (f,a,b) A2: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(-_(integral_(f,A)))_holds_ (-_(integral_(f,A)))_._i_=_(integral_(f,a,b))_._i let i be Nat; ::_thesis: ( i in dom (- (integral (f,A))) implies (- (integral (f,A))) . i = (integral (f,a,b)) . i ) assume A3: i in dom (- (integral (f,A))) ; ::_thesis: (- (integral (f,A))) . i = (integral (f,a,b)) . i then reconsider k = i as Element of NAT ; A4: dom (integral (f,A)) = Seg n by Def17; A5: k in dom (integral (f,A)) by A3, VALUED_1:8; then A6: (integral (f,a,b)) . k = integral (((proj (k,n)) * f),a,b) by A4, Def18; (- (integral (f,A))) . k = - ((integral (f,A)) . k) by VALUED_1:8 .= - (integral (((proj (k,n)) * f),A)) by A5, A4, Def17 ; hence (- (integral (f,A))) . i = (integral (f,a,b)) . i by A1, A6, INTEGRA5:20; ::_thesis: verum end; dom (- (integral (f,A))) = dom ((- 1) (#) (integral (f,A))) by VALUED_1:def_6 .= dom (integral (f,A)) by VALUED_1:def_5 .= Seg n by Def17 .= dom (integral (f,a,b)) by Def18 ; hence - (integral (f,A)) = integral (f,a,b) by A2, FINSEQ_1:13; ::_thesis: verum end; theorem :: INTEGR15:21 for n being Nat for Z, x being set for f, g being PartFunc of Z,(REAL n) st x in dom (f + g) holds (f + g) /. x = (f /. x) + (g /. x) proof let n be Nat; ::_thesis: for Z, x being set for f, g being PartFunc of Z,(REAL n) st x in dom (f + g) holds (f + g) /. x = (f /. x) + (g /. x) let Z, x be set ; ::_thesis: for f, g being PartFunc of Z,(REAL n) st x in dom (f + g) holds (f + g) /. x = (f /. x) + (g /. x) let f, g be PartFunc of Z,(REAL n); ::_thesis: ( x in dom (f + g) implies (f + g) /. x = (f /. x) + (g /. x) ) assume A1: x in dom (f + g) ; ::_thesis: (f + g) /. x = (f /. x) + (g /. x) dom (f + g) = (dom f) /\ (dom g) by VALUED_2:def_45; then ( x in dom f & x in dom g ) by A1, XBOOLE_0:def_4; then A2: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def_6; thus (f + g) /. x = (f + g) . x by A1, PARTFUN1:def_6 .= (f /. x) + (g /. x) by A1, A2, VALUED_2:def_45 ; ::_thesis: verum end; theorem :: INTEGR15:22 for n being Nat for Z, x being set for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds (f - g) /. x = (f /. x) - (g /. x) proof let n be Nat; ::_thesis: for Z, x being set for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds (f - g) /. x = (f /. x) - (g /. x) let Z, x be set ; ::_thesis: for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds (f - g) /. x = (f /. x) - (g /. x) let f, g be PartFunc of Z,(REAL n); ::_thesis: ( x in dom (f - g) implies (f - g) /. x = (f /. x) - (g /. x) ) assume A1: x in dom (f - g) ; ::_thesis: (f - g) /. x = (f /. x) - (g /. x) dom (f - g) = (dom f) /\ (dom g) by VALUED_2:def_46; then ( x in dom f & x in dom g ) by A1, XBOOLE_0:def_4; then A2: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def_6; thus (f - g) /. x = (f - g) . x by A1, PARTFUN1:def_6 .= (f /. x) - (g /. x) by A1, A2, VALUED_2:def_46 ; ::_thesis: verum end; theorem :: INTEGR15:23 for n being Nat for Z, x being set for f being PartFunc of Z,(REAL n) for r being real number st x in dom (r (#) f) holds (r (#) f) /. x = r * (f /. x) proof let n be Nat; ::_thesis: for Z, x being set for f being PartFunc of Z,(REAL n) for r being real number st x in dom (r (#) f) holds (r (#) f) /. x = r * (f /. x) let Z, x be set ; ::_thesis: for f being PartFunc of Z,(REAL n) for r being real number st x in dom (r (#) f) holds (r (#) f) /. x = r * (f /. x) let f be PartFunc of Z,(REAL n); ::_thesis: for r being real number st x in dom (r (#) f) holds (r (#) f) /. x = r * (f /. x) let r be real number ; ::_thesis: ( x in dom (r (#) f) implies (r (#) f) /. x = r * (f /. x) ) assume A1: x in dom (r (#) f) ; ::_thesis: (r (#) f) /. x = r * (f /. x) dom (r (#) f) = dom f by VALUED_2:def_39; then A2: f . x = f /. x by A1, PARTFUN1:def_6; thus (r (#) f) /. x = (r (#) f) . x by A1, PARTFUN1:def_6 .= r * (f /. x) by A1, A2, VALUED_2:def_39 ; ::_thesis: verum end;