:: INTEGR18 semantic presentation begin definition let X be RealNormSpace; let A be non empty closed_interval Subset of REAL; let f be Function of A, the carrier of X; let D be Division of A; mode middle_volume of f,D -> FinSequence of X means :Def1: :: INTEGR18:def 1 ( len it = len D & ( for i being Nat st i in dom D holds ex c being Point of X st ( c in rng (f | (divset (D,i))) & it . i = (vol (divset (D,i))) * c ) ) ); correctness existence ex b1 being FinSequence of X st ( len b1 = len D & ( for i being Nat st i in dom D holds ex c being Point of X st ( c in rng (f | (divset (D,i))) & b1 . i = (vol (divset (D,i))) * c ) ) ); proof defpred S1[ Nat, set ] means ex c being Point of X st ( c in rng (f | (divset (D,\$1))) & \$2 = (vol (divset (D,\$1))) * c ); 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 the carrier of X st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of the carrier of X st S1[k,x] ) assume k in Seg (len D) ; ::_thesis: ex x being Element of the carrier of X 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 c being set such that A4: c in rng (f | (divset (D,k))) by XBOOLE_0:def_1; reconsider c = c as Point of X by A4; (vol (divset (D,k))) * c is Element of the carrier of X ; hence ex x being Element of the carrier of X st S1[k,x] by A4; ::_thesis: verum end; consider p being FinSequence of the carrier of X 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 X st ( len b1 = len D & ( for i being Nat st i in dom D holds ex c being Point of X st ( c in rng (f | (divset (D,i))) & b1 . i = (vol (divset (D,i))) * c ) ) ) by A5, A1; ::_thesis: verum end; end; :: deftheorem Def1 defines middle_volume INTEGR18:def_1_:_ for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being Function of A, the carrier of X for D being Division of A for b5 being FinSequence of X holds ( b5 is middle_volume of f,D iff ( len b5 = len D & ( for i being Nat st i in dom D holds ex c being Point of X st ( c in rng (f | (divset (D,i))) & b5 . i = (vol (divset (D,i))) * c ) ) ) ); definition let X be RealNormSpace; let A be non empty closed_interval Subset of REAL; let f be Function of A, the carrier of X; let D be Division of A; let F be middle_volume of f,D; func middle_sum (f,F) -> Point of X equals :: INTEGR18:def 2 Sum F; coherence Sum F is Point of X ; end; :: deftheorem defines middle_sum INTEGR18:def_2_:_ for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being Function of A, the carrier of X for D being Division of A for F being middle_volume of f,D holds middle_sum (f,F) = Sum F; definition let X be RealNormSpace; let A be non empty closed_interval Subset of REAL; let f be Function of A, the carrier of X; let T be DivSequence of A; mode middle_volume_Sequence of f,T -> Function of NAT,( the carrier of X *) means :Def3: :: INTEGR18: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,( the carrier of X *) 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 the carrier of X * st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of the carrier of X * 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 the carrier of X * by FINSEQ_1:def_11; y is middle_volume of f,T . x ; hence ex y being Element of the carrier of X * st S1[x,y] ; ::_thesis: verum end; ex f being Function of NAT,( the carrier of X *) 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,( the carrier of X *) 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 INTEGR18:def_3_:_ for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being Function of A, the carrier of X for T being DivSequence of A for b5 being Function of NAT,( the carrier of X *) 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 X be RealNormSpace; let A be non empty closed_interval Subset of REAL; let f be Function of A, the carrier of X; 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 X be RealNormSpace; let A be non empty closed_interval Subset of REAL; let f be Function of A, the carrier of X; let T be DivSequence of A; let S be middle_volume_Sequence of f,T; func middle_sum (f,S) -> sequence of X means :Def4: :: INTEGR18:def 4 for i being Element of NAT holds it . i = middle_sum (f,(S . i)); existence ex b1 being sequence of X st for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) proof deffunc H1( Element of NAT ) -> Point of X = middle_sum (f,(S . \$1)); thus ex IT being sequence of the carrier of X st for i being Element of NAT holds IT . i = H1(i) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being sequence of X 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 X; ::_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 INTEGR18:def_4_:_ for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being Function of A, the carrier of X for T being DivSequence of A for S being middle_volume_Sequence of f,T for b6 being sequence of X holds ( b6 = middle_sum (f,S) iff for i being Element of NAT holds b6 . i = middle_sum (f,(S . i)) ); begin definition let X be RealNormSpace; let A be non empty closed_interval Subset of REAL; let f be Function of A, the carrier of X; attrf is integrable means :Def5: :: INTEGR18:def 5 ex I being Point of X 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 ); end; :: deftheorem Def5 defines integrable INTEGR18:def_5_:_ for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being Function of A, the carrier of X holds ( f is integrable iff ex I being Point of X 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 ) ); theorem Th1: :: INTEGR18:1 for X being RealNormSpace for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 + R2 holds Sum R3 = (Sum R1) + (Sum R2) proof let X be RealNormSpace; ::_thesis: for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 + R2 holds Sum R3 = (Sum R1) + (Sum R2) let R1, R2, R3 be FinSequence of X; ::_thesis: ( len R1 = len R2 & R3 = R1 + R2 implies Sum R3 = (Sum R1) + (Sum R2) ) assume A1: ( len R1 = len R2 & R3 = R1 + R2 ) ; ::_thesis: Sum R3 = (Sum R1) + (Sum R2) then dom R1 = dom R2 by FINSEQ_3:29; hence Sum R3 = (Sum R1) + (Sum R2) by A1, BINOM:7; ::_thesis: verum end; theorem :: INTEGR18:2 for X being RealNormSpace for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds Sum R3 = (Sum R1) - (Sum R2) proof let X be RealNormSpace; ::_thesis: for R1, R2, R3 being FinSequence of X st len R1 = len R2 & R3 = R1 - R2 holds Sum R3 = (Sum R1) - (Sum R2) let R1, R2, R3 be FinSequence of X; ::_thesis: ( len R1 = len R2 & R3 = R1 - R2 implies Sum R3 = (Sum R1) - (Sum R2) ) assume A1: ( len R1 = len R2 & R3 = R1 - R2 ) ; ::_thesis: Sum R3 = (Sum R1) - (Sum R2) then A2: dom R1 = dom R2 by FINSEQ_3:29; A3: dom R3 = (dom R1) /\ (dom R2) by A1, VFUNCT_1:def_2 .= dom R1 by A2 ; then A4: len R3 = len R1 by FINSEQ_3:29; A5: for k being Element of NAT st k in dom R1 holds R3 . k = (R1 /. k) - (R2 /. k) proof let k be Element of NAT ; ::_thesis: ( k in dom R1 implies R3 . k = (R1 /. k) - (R2 /. k) ) assume A6: k in dom R1 ; ::_thesis: R3 . k = (R1 /. k) - (R2 /. k) thus R3 . k = R3 /. k by A6, A3, PARTFUN1:def_6 .= (R1 /. k) - (R2 /. k) by A1, A6, A3, VFUNCT_1:def_2 ; ::_thesis: verum end; thus Sum R3 = (Sum R1) - (Sum R2) by A1, A4, A5, RLVECT_2:5; ::_thesis: verum end; theorem Th3: :: INTEGR18:3 for X being RealNormSpace for R1, R2 being FinSequence of X for a being Element of REAL st R2 = a (#) R1 holds Sum R2 = a * (Sum R1) proof let X be RealNormSpace; ::_thesis: for R1, R2 being FinSequence of X for a being Element of REAL st R2 = a (#) R1 holds Sum R2 = a * (Sum R1) let R1, R2 be FinSequence of X; ::_thesis: for a being Element of REAL st R2 = a (#) R1 holds Sum R2 = a * (Sum R1) let a be Element of REAL ; ::_thesis: ( R2 = a (#) R1 implies Sum R2 = a * (Sum R1) ) assume A1: R2 = a (#) R1 ; ::_thesis: Sum R2 = a * (Sum R1) dom R2 = dom R1 by A1, VFUNCT_1:def_4; then A2: len R2 = len R1 by FINSEQ_3:29; A3: for k being Element of NAT st k in dom R1 holds R2 . k = a * (R1 /. k) proof let k be Element of NAT ; ::_thesis: ( k in dom R1 implies R2 . k = a * (R1 /. k) ) assume k in dom R1 ; ::_thesis: R2 . k = a * (R1 /. k) then A4: k in dom R2 by A1, VFUNCT_1:def_4; thus R2 . k = R2 /. k by A4, PARTFUN1:def_6 .= a * (R1 /. k) by A4, A1, VFUNCT_1:def_4 ; ::_thesis: verum end; thus Sum R2 = a * (Sum R1) by A2, A3, RLVECT_2:3; ::_thesis: verum end; definition let X be RealNormSpace; let A be non empty closed_interval Subset of REAL; let f be Function of A, the carrier of X; assume A1: f is integrable ; func integral f -> Point of X means :Def6: :: INTEGR18:def 6 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)) = it ); existence ex b1 being Point of X 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)) = b1 ) by A1, Def5; uniqueness for b1, b2 being Point of X 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)) = b1 ) ) & ( 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)) = b2 ) ) holds b1 = b2 proof let I1, I2 be Point of X; ::_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)) = I1 ) ) & ( 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)) = I2 ) ) implies I1 = I2 ) assume A2: 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)) = I1 ) ; ::_thesis: ( ex T being DivSequence of A ex S being middle_volume_Sequence of f,T st ( delta T is convergent & lim (delta T) = 0 & not ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I2 ) ) or I1 = I2 ) assume 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)) = I2 ) ; ::_thesis: I1 = I2 consider T being DivSequence of A such that A4: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11; set S = the middle_volume_Sequence of f,T; thus I1 = lim (middle_sum (f, the middle_volume_Sequence of f,T)) by A2, A4 .= I2 by A3, A4 ; ::_thesis: verum end; end; :: deftheorem Def6 defines integral INTEGR18:def_6_:_ for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being Function of A, the carrier of X st f is integrable holds for b4 being Point of X holds ( b4 = integral f iff 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)) = b4 ) ); theorem Th4: :: INTEGR18:4 for X being RealNormSpace for A being non empty closed_interval Subset of REAL for r being Real for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds ( h is integrable & integral h = r * (integral f) ) proof let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL for r being Real for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds ( h is integrable & integral h = r * (integral f) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds ( h is integrable & integral h = r * (integral f) ) let r be Real; ::_thesis: for f, h being Function of A, the carrier of X st h = r (#) f & f is integrable holds ( h is integrable & integral h = r * (integral f) ) let f, h be Function of A, the carrier of X; ::_thesis: ( h = r (#) f & f is integrable implies ( h is integrable & integral h = r * (integral f) ) ) assume A1: ( h = r (#) f & f is integrable ) ; ::_thesis: ( h is integrable & integral h = r * (integral f) ) A2: ( dom h = A & dom f = A ) by FUNCT_2:def_1; A3: now__::_thesis:_for_T_being_DivSequence_of_A for_S_being_middle_volume_Sequence_of_h,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_ (_middle_sum_(h,S)_is_convergent_&_lim_(middle_sum_(h,S))_=_r_*_(integral_f)_) let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * (integral f) ) let S be middle_volume_Sequence of h,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * (integral f) ) ) assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = r * (integral f) ) defpred S1[ Element of NAT , set ] means ex p being FinSequence of REAL st ( p = \$2 & len p = len (T . \$1) & ( for i being Nat st i in dom (T . \$1) holds ( p . i in dom (h | (divset ((T . \$1),i))) & ex z being Point of X st ( z = (h | (divset ((T . \$1),i))) . (p . i) & (S . \$1) . i = (vol (divset ((T . \$1),i))) * z ) ) ) ); A5: for k being Element of NAT ex p being Element of REAL * st S1[k,p] proof let k be Element of NAT ; ::_thesis: ex p being Element of REAL * st S1[k,p] defpred S2[ Nat, set ] means ( \$2 in dom (h | (divset ((T . k),\$1))) & ex c being Point of X st ( c = (h | (divset ((T . k),\$1))) . \$2 & (S . k) . \$1 = (vol (divset ((T . k),\$1))) * c ) ); A6: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3; A7: for i being Nat st i in Seg (len (T . k)) holds ex x being Element of REAL st S2[i,x] proof let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] ) assume i in Seg (len (T . k)) ; ::_thesis: ex x being Element of REAL st S2[i,x] then i in dom (T . k) by FINSEQ_1:def_3; then consider c being Point of X such that A8: ( c in rng (h | (divset ((T . k),i))) & (S . k) . i = (vol (divset ((T . k),i))) * c ) by Def1; consider x being set such that A9: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def_3; ( x in dom h & x in divset ((T . k),i) ) by A9, RELAT_1:57; then reconsider x = x as Element of REAL ; take x ; ::_thesis: S2[i,x] thus S2[i,x] by A8, A9; ::_thesis: verum end; consider p being FinSequence of REAL such that A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds S2[i,p . i] ) ) from FINSEQ_1:sch_5(A7); take p ; ::_thesis: ( p is Element of REAL * & S1[k,p] ) len p = len (T . k) by A10, FINSEQ_1:def_3; hence ( p is Element of REAL * & S1[k,p] ) by A10, A6, FINSEQ_1:def_11; ::_thesis: verum end; consider F being Function of NAT,(REAL *) such that A11: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A5); defpred S2[ Element of NAT , set ] means ex q being middle_volume of f,T . \$1 st ( q = \$2 & ( for i being Nat st i in dom (T . \$1) holds ex z being Point of X st ( (F . \$1) . i in dom (f | (divset ((T . \$1),i))) & z = (f | (divset ((T . \$1),i))) . ((F . \$1) . i) & q . i = (vol (divset ((T . \$1),i))) * z ) ) ); A12: for k being Element of NAT ex y being Element of the carrier of X * st S2[k,y] proof let k be Element of NAT ; ::_thesis: ex y being Element of the carrier of X * st S2[k,y] defpred S3[ Nat, set ] means ex c being Point of X st ( (F . k) . \$1 in dom (f | (divset ((T . k),\$1))) & c = (f | (divset ((T . k),\$1))) . ((F . k) . \$1) & \$2 = (vol (divset ((T . k),\$1))) * c ); A13: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3; A14: for i being Nat st i in Seg (len (T . k)) holds ex x being Element of the carrier of X st S3[i,x] proof let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of the carrier of X st S3[i,x] ) assume i in Seg (len (T . k)) ; ::_thesis: ex x being Element of the carrier of X st S3[i,x] then A15: i in dom (T . k) by FINSEQ_1:def_3; consider p being FinSequence of REAL such that A16: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds ( p . i in dom (h | (divset ((T . k),i))) & ex z being Point of X st ( z = (h | (divset ((T . k),i))) . (p . i) & (S . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11; p . i in dom (h | (divset ((T . k),i))) by A15, A16; then A17: ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57; then p . i in dom (f | (divset ((T . k),i))) by A2, RELAT_1:57; then (f | (divset ((T . k),i))) . (p . i) in rng (f | (divset ((T . k),i))) by FUNCT_1:3; then reconsider x = (f | (divset ((T . k),i))) . (p . i) as Element of the carrier of X ; A18: (F . k) . i in dom (f | (divset ((T . k),i))) by A16, A17, A2, RELAT_1:57; (vol (divset ((T . k),i))) * x is Element of the carrier of X ; hence ex x being Element of the carrier of X st S3[i,x] by A16, A18; ::_thesis: verum end; consider q being FinSequence of the carrier of X such that A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds S3[i,q . i] ) ) from FINSEQ_1:sch_5(A14); A20: len q = len (T . k) by A19, FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(T_._k)_holds_ ex_c_being_Point_of_X_st_ (_c_in_rng_(f_|_(divset_((T_._k),i)))_&_q_._i_=_(vol_(divset_((T_._k),i)))_*_c_) let i be Nat; ::_thesis: ( i in dom (T . k) implies ex c being Point of X st ( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) ) assume i in dom (T . k) ; ::_thesis: ex c being Point of X st ( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) then i in Seg (len (T . k)) by FINSEQ_1:def_3; then consider c being Point of X such that A21: ( (F . k) . i in dom (f | (divset ((T . k),i))) & c = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A19; thus ex c being Point of X st ( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) by A21, FUNCT_1:3; ::_thesis: verum end; then reconsider q = q as middle_volume of f,T . k by A20, Def1; q is Element of the carrier of X * by FINSEQ_1:def_11; hence ex y being Element of the carrier of X * st S2[k,y] by A13, A19; ::_thesis: verum end; consider Sf being Function of NAT,( the carrier of X *) such that A22: for x being Element of NAT holds S2[x,Sf . x] from FUNCT_2:sch_3(A12); now__::_thesis:_for_k_being_Element_of_NAT_holds_Sf_._k_is_middle_volume_of_f,T_._k let k be Element of NAT ; ::_thesis: Sf . k is middle_volume of f,T . k ex q being middle_volume of f,T . k st ( q = Sf . k & ( for i being Nat st i in dom (T . k) holds ex z being Point of X st ( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A22; hence Sf . k is middle_volume of f,T . k ; ::_thesis: verum end; then reconsider Sf = Sf as middle_volume_Sequence of f,T by Def3; integral f is Point of X ; then A23: middle_sum (f,Sf) is convergent by Def6, A1, A4; A24: r * (middle_sum (f,Sf)) = middle_sum (h,S) proof now__::_thesis:_for_n_being_Element_of_NAT_holds_r_*_((middle_sum_(f,Sf))_._n)_=_(middle_sum_(h,S))_._n let n be Element of NAT ; ::_thesis: r * ((middle_sum (f,Sf)) . n) = (middle_sum (h,S)) . n consider p being FinSequence of REAL such that A25: ( p = F . n & len p = len (T . n) & ( for i being Nat st i in dom (T . n) holds ( p . i in dom (h | (divset ((T . n),i))) & ex z being Point of X st ( z = (h | (divset ((T . n),i))) . (p . i) & (S . n) . i = (vol (divset ((T . n),i))) * z ) ) ) ) by A11; consider q being middle_volume of f,T . n such that A26: ( q = Sf . n & ( for i being Nat st i in dom (T . n) holds ex z being Point of X st ( (F . n) . i in dom (f | (divset ((T . n),i))) & z = (f | (divset ((T . n),i))) . ((F . n) . i) & q . i = (vol (divset ((T . n),i))) * z ) ) ) by A22; ( len (Sf . n) = len (T . n) & len (S . n) = len (T . n) ) by Def1; then A27: ( dom (Sf . n) = dom (T . n) & dom (S . n) = dom (T . n) ) by FINSEQ_3:29; now__::_thesis:_for_x_being_Element_of_NAT_st_x_in_dom_(S_._n)_holds_ (S_._n)_/._x_=_r_*_((Sf_._n)_/._x) let x be Element of NAT ; ::_thesis: ( x in dom (S . n) implies (S . n) /. x = r * ((Sf . n) /. x) ) assume A28: x in dom (S . n) ; ::_thesis: (S . n) /. x = r * ((Sf . n) /. x) reconsider i = x as Nat ; consider t being Point of X such that A29: ( t = (h | (divset ((T . n),i))) . ((F . n) . i) & (S . n) . i = (vol (divset ((T . n),i))) * t ) by A28, A27, A25; consider z being Point of X such that A30: ( (F . n) . i in dom (f | (divset ((T . n),i))) & z = (f | (divset ((T . n),i))) . ((F . n) . i) & q . i = (vol (divset ((T . n),i))) * z ) by A26, A28, A27; A31: (F . n) . i in divset ((T . n),i) by A30, RELAT_1:57; (F . n) . i in A by A30; then A32: (F . n) . i in dom h by FUNCT_2:def_1; A33: (F . n) . i in dom f by A30, RELAT_1:57; A34: f /. ((F . n) . i) = f . ((F . n) . i) by A33, PARTFUN1:def_6 .= z by A30, A31, FUNCT_1:49 ; A35: t = (h | (divset ((T . n),i))) . ((F . n) . i) by A29 .= h . ((F . n) . i) by A31, FUNCT_1:49 .= h /. ((F . n) . i) by A32, PARTFUN1:def_6 .= r * (f /. ((F . n) . i)) by A32, A1, VFUNCT_1:def_4 .= r * z by A34 ; A36: (vol (divset ((T . n),i))) * z = (Sf . n) . x by A30, A26 .= (Sf . n) /. x by A28, A27, PARTFUN1:def_6 ; thus (S . n) /. x = (S . n) . x by A28, PARTFUN1:def_6 .= (vol (divset ((T . n),i))) * t by A29 .= (vol (divset ((T . n),i))) * (r * z) by A35 .= ((vol (divset ((T . n),i))) * r) * z by RLVECT_1:def_7 .= r * ((vol (divset ((T . n),i))) * z) by RLVECT_1:def_7 .= r * ((Sf . n) /. x) by A36 ; ::_thesis: verum end; then A37: r (#) (Sf . n) = S . n by A27, VFUNCT_1:def_4; thus r * ((middle_sum (f,Sf)) . n) = r * (middle_sum (f,(Sf . n))) by Def4 .= r * (Sum (Sf . n)) .= Sum (S . n) by A37, Th3 .= middle_sum (h,(S . n)) .= (middle_sum (h,S)) . n by Def4 ; ::_thesis: verum end; hence r * (middle_sum (f,Sf)) = middle_sum (h,S) by NORMSP_1:def_5; ::_thesis: verum end; A38: lim (r * (middle_sum (f,Sf))) = r * (lim (middle_sum (f,Sf))) by A23, NORMSP_1:28 .= r * (integral f) by Def6, A1, A4 ; thus middle_sum (h,S) is convergent by A23, A24, NORMSP_1:22; ::_thesis: lim (middle_sum (h,S)) = r * (integral f) thus lim (middle_sum (h,S)) = r * (integral f) by A24, A38; ::_thesis: verum end; hence h is integrable by Def5; ::_thesis: integral h = r * (integral f) hence integral h = r * (integral f) by Def6, A3; ::_thesis: verum end; theorem Th5: :: INTEGR18:5 for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f, h being Function of A, the carrier of X st h = - f & f is integrable holds ( h is integrable & integral h = - (integral f) ) proof let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL for f, h being Function of A, the carrier of X st h = - f & f is integrable holds ( h is integrable & integral h = - (integral f) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, h being Function of A, the carrier of X st h = - f & f is integrable holds ( h is integrable & integral h = - (integral f) ) let f, h be Function of A, the carrier of X; ::_thesis: ( h = - f & f is integrable implies ( h is integrable & integral h = - (integral f) ) ) assume A1: ( h = - f & f is integrable ) ; ::_thesis: ( h is integrable & integral h = - (integral f) ) then A2: h = (- 1) (#) f by VFUNCT_1:23; hence h is integrable by A1, Th4; ::_thesis: integral h = - (integral f) integral h = (- 1) * (integral f) by A1, A2, Th4; hence integral h = - (integral f) by RLVECT_1:16; ::_thesis: verum end; theorem Th6: :: INTEGR18:6 for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f, g, h being Function of A, the carrier of X st h = f + g & f is integrable & g is integrable holds ( h is integrable & integral h = (integral f) + (integral g) ) proof let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL for f, g, h being Function of A, the carrier of X st h = f + g & f is integrable & g is integrable holds ( h is integrable & integral h = (integral f) + (integral g) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g, h being Function of A, the carrier of X st h = f + g & f is integrable & g is integrable holds ( h is integrable & integral h = (integral f) + (integral g) ) let f, g, h be Function of A, the carrier of X; ::_thesis: ( h = f + g & f is integrable & g is integrable implies ( h is integrable & integral h = (integral f) + (integral g) ) ) assume A1: ( h = f + g & f is integrable & g is integrable ) ; ::_thesis: ( h is integrable & integral h = (integral f) + (integral g) ) A2: ( dom h = A & dom f = A & dom g = A ) by FUNCT_2:def_1; A3: now__::_thesis:_for_T_being_DivSequence_of_A for_S_being_middle_volume_Sequence_of_h,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_ (_middle_sum_(h,S)_is_convergent_&_lim_(middle_sum_(h,S))_=_(integral_f)_+_(integral_g)_) let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = (integral f) + (integral g) ) let S be middle_volume_Sequence of h,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = (integral f) + (integral g) ) ) assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = (integral f) + (integral g) ) defpred S1[ Element of NAT , set ] means ex p being FinSequence of REAL st ( p = \$2 & len p = len (T . \$1) & ( for i being Nat st i in dom (T . \$1) holds ( p . i in dom (h | (divset ((T . \$1),i))) & ex z being Point of X st ( z = (h | (divset ((T . \$1),i))) . (p . i) & (S . \$1) . i = (vol (divset ((T . \$1),i))) * z ) ) ) ); A5: for k being Element of NAT ex p being Element of REAL * st S1[k,p] proof let k be Element of NAT ; ::_thesis: ex p being Element of REAL * st S1[k,p] defpred S2[ Nat, set ] means ( \$2 in dom (h | (divset ((T . k),\$1))) & ex c being Point of X st ( c = (h | (divset ((T . k),\$1))) . \$2 & (S . k) . \$1 = (vol (divset ((T . k),\$1))) * c ) ); A6: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3; A7: for i being Nat st i in Seg (len (T . k)) holds ex x being Element of REAL st S2[i,x] proof let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] ) assume i in Seg (len (T . k)) ; ::_thesis: ex x being Element of REAL st S2[i,x] then i in dom (T . k) by FINSEQ_1:def_3; then consider c being Point of X such that A8: ( c in rng (h | (divset ((T . k),i))) & (S . k) . i = (vol (divset ((T . k),i))) * c ) by Def1; consider x being set such that A9: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def_3; ( x in dom h & x in divset ((T . k),i) ) by A9, RELAT_1:57; then reconsider x = x as Element of REAL ; take x ; ::_thesis: S2[i,x] thus S2[i,x] by A8, A9; ::_thesis: verum end; consider p being FinSequence of REAL such that A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds S2[i,p . i] ) ) from FINSEQ_1:sch_5(A7); take p ; ::_thesis: ( p is Element of REAL * & S1[k,p] ) len p = len (T . k) by A10, FINSEQ_1:def_3; hence ( p is Element of REAL * & S1[k,p] ) by A10, A6, FINSEQ_1:def_11; ::_thesis: verum end; consider F being Function of NAT,(REAL *) such that A11: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A5); defpred S2[ Element of NAT , set ] means ex q being middle_volume of f,T . \$1 st ( q = \$2 & ( for i being Nat st i in dom (T . \$1) holds ex z being Point of X st ( (F . \$1) . i in dom (f | (divset ((T . \$1),i))) & z = (f | (divset ((T . \$1),i))) . ((F . \$1) . i) & q . i = (vol (divset ((T . \$1),i))) * z ) ) ); A12: for k being Element of NAT ex y being Element of the carrier of X * st S2[k,y] proof let k be Element of NAT ; ::_thesis: ex y being Element of the carrier of X * st S2[k,y] defpred S3[ Nat, set ] means ex c being Point of X st ( (F . k) . \$1 in dom (f | (divset ((T . k),\$1))) & c = (f | (divset ((T . k),\$1))) . ((F . k) . \$1) & \$2 = (vol (divset ((T . k),\$1))) * c ); A13: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3; A14: for i being Nat st i in Seg (len (T . k)) holds ex x being Element of the carrier of X st S3[i,x] proof let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of the carrier of X st S3[i,x] ) assume i in Seg (len (T . k)) ; ::_thesis: ex x being Element of the carrier of X st S3[i,x] then A15: i in dom (T . k) by FINSEQ_1:def_3; consider p being FinSequence of REAL such that A16: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds ( p . i in dom (h | (divset ((T . k),i))) & ex z being Point of X st ( z = (h | (divset ((T . k),i))) . (p . i) & (S . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11; p . i in dom (h | (divset ((T . k),i))) by A15, A16; then A17: ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57; then p . i in dom (f | (divset ((T . k),i))) by A2, RELAT_1:57; then (f | (divset ((T . k),i))) . (p . i) in rng (f | (divset ((T . k),i))) by FUNCT_1:3; then reconsider x = (f | (divset ((T . k),i))) . (p . i) as Element of the carrier of X ; A18: (F . k) . i in dom (f | (divset ((T . k),i))) by A16, A17, A2, RELAT_1:57; (vol (divset ((T . k),i))) * x is Element of the carrier of X ; hence ex x being Element of the carrier of X st S3[i,x] by A16, A18; ::_thesis: verum end; consider q being FinSequence of the carrier of X such that A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds S3[i,q . i] ) ) from FINSEQ_1:sch_5(A14); A20: len q = len (T . k) by A19, FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(T_._k)_holds_ ex_c_being_Point_of_X_st_ (_c_in_rng_(f_|_(divset_((T_._k),i)))_&_q_._i_=_(vol_(divset_((T_._k),i)))_*_c_) let i be Nat; ::_thesis: ( i in dom (T . k) implies ex c being Point of X st ( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) ) assume i in dom (T . k) ; ::_thesis: ex c being Point of X st ( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) then i in Seg (len (T . k)) by FINSEQ_1:def_3; then consider c being Point of X such that A21: ( (F . k) . i in dom (f | (divset ((T . k),i))) & c = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A19; thus ex c being Point of X st ( c in rng (f | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) by A21, FUNCT_1:3; ::_thesis: verum end; then reconsider q = q as middle_volume of f,T . k by A20, Def1; q is Element of the carrier of X * by FINSEQ_1:def_11; hence ex y being Element of the carrier of X * st S2[k,y] by A13, A19; ::_thesis: verum end; consider Sf being Function of NAT,( the carrier of X *) such that A22: for x being Element of NAT holds S2[x,Sf . x] from FUNCT_2:sch_3(A12); now__::_thesis:_for_k_being_Element_of_NAT_holds_Sf_._k_is_middle_volume_of_f,T_._k let k be Element of NAT ; ::_thesis: Sf . k is middle_volume of f,T . k ex q being middle_volume of f,T . k st ( q = Sf . k & ( for i being Nat st i in dom (T . k) holds ex z being Point of X st ( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A22; hence Sf . k is middle_volume of f,T . k ; ::_thesis: verum end; then reconsider Sf = Sf as middle_volume_Sequence of f,T by Def3; defpred S3[ Element of NAT , set ] means ex q being middle_volume of g,T . \$1 st ( q = \$2 & ( for i being Nat st i in dom (T . \$1) holds ex z being Point of X st ( (F . \$1) . i in dom (g | (divset ((T . \$1),i))) & z = (g | (divset ((T . \$1),i))) . ((F . \$1) . i) & q . i = (vol (divset ((T . \$1),i))) * z ) ) ); A23: for k being Element of NAT ex y being Element of the carrier of X * st S3[k,y] proof let k be Element of NAT ; ::_thesis: ex y being Element of the carrier of X * st S3[k,y] defpred S4[ Nat, set ] means ex c being Point of X st ( (F . k) . \$1 in dom (g | (divset ((T . k),\$1))) & c = (g | (divset ((T . k),\$1))) . ((F . k) . \$1) & \$2 = (vol (divset ((T . k),\$1))) * c ); A24: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3; A25: for i being Nat st i in Seg (len (T . k)) holds ex x being Element of the carrier of X st S4[i,x] proof let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of the carrier of X st S4[i,x] ) assume i in Seg (len (T . k)) ; ::_thesis: ex x being Element of the carrier of X st S4[i,x] then A26: i in dom (T . k) by FINSEQ_1:def_3; consider p being FinSequence of REAL such that A27: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds ( p . i in dom (h | (divset ((T . k),i))) & ex z being Point of X st ( z = (h | (divset ((T . k),i))) . (p . i) & (S . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11; p . i in dom (h | (divset ((T . k),i))) by A26, A27; then A28: ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57; then p . i in dom (g | (divset ((T . k),i))) by A2, RELAT_1:57; then (g | (divset ((T . k),i))) . (p . i) in rng (g | (divset ((T . k),i))) by FUNCT_1:3; then reconsider x = (g | (divset ((T . k),i))) . (p . i) as Element of the carrier of X ; A29: (F . k) . i in dom (g | (divset ((T . k),i))) by A27, A28, A2, RELAT_1:57; (vol (divset ((T . k),i))) * x is Element of the carrier of X ; hence ex x being Element of the carrier of X st S4[i,x] by A27, A29; ::_thesis: verum end; consider q being FinSequence of the carrier of X such that A30: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds S4[i,q . i] ) ) from FINSEQ_1:sch_5(A25); A31: len q = len (T . k) by A30, FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(T_._k)_holds_ ex_c_being_Point_of_X_st_ (_c_in_rng_(g_|_(divset_((T_._k),i)))_&_q_._i_=_(vol_(divset_((T_._k),i)))_*_c_) let i be Nat; ::_thesis: ( i in dom (T . k) implies ex c being Point of X st ( c in rng (g | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) ) assume i in dom (T . k) ; ::_thesis: ex c being Point of X st ( c in rng (g | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) then i in Seg (len (T . k)) by FINSEQ_1:def_3; then consider c being Point of X such that A32: ( (F . k) . i in dom (g | (divset ((T . k),i))) & c = (g | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A30; thus ex c being Point of X st ( c in rng (g | (divset ((T . k),i))) & q . i = (vol (divset ((T . k),i))) * c ) by A32, FUNCT_1:3; ::_thesis: verum end; then reconsider q = q as middle_volume of g,T . k by A31, Def1; q is Element of the carrier of X * by FINSEQ_1:def_11; hence ex y being Element of the carrier of X * st S3[k,y] by A24, A30; ::_thesis: verum end; consider Sg being Function of NAT,( the carrier of X *) such that A33: for x being Element of NAT holds S3[x,Sg . x] from FUNCT_2:sch_3(A23); now__::_thesis:_for_k_being_Element_of_NAT_holds_Sg_._k_is_middle_volume_of_g,T_._k let k be Element of NAT ; ::_thesis: Sg . k is middle_volume of g,T . k ex q being middle_volume of g,T . k st ( q = Sg . k & ( for i being Nat st i in dom (T . k) holds ex z being Point of X st ( (F . k) . i in dom (g | (divset ((T . k),i))) & z = (g | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A33; hence Sg . k is middle_volume of g,T . k ; ::_thesis: verum end; then reconsider Sg = Sg as middle_volume_Sequence of g,T by Def3; integral f is Point of X ; then A34: ( middle_sum (f,Sf) is convergent & lim (middle_sum (f,Sf)) = integral f ) by Def6, A1, A4; integral g is Point of X ; then A35: ( middle_sum (g,Sg) is convergent & lim (middle_sum (g,Sg)) = integral g ) by Def6, A1, A4; A36: (middle_sum (f,Sf)) + (middle_sum (g,Sg)) = middle_sum (h,S) proof now__::_thesis:_for_n_being_Element_of_NAT_holds_((middle_sum_(f,Sf))_._n)_+_((middle_sum_(g,Sg))_._n)_=_(middle_sum_(h,S))_._n let n be Element of NAT ; ::_thesis: ((middle_sum (f,Sf)) . n) + ((middle_sum (g,Sg)) . n) = (middle_sum (h,S)) . n consider p being FinSequence of REAL such that A37: ( p = F . n & len p = len (T . n) & ( for i being Nat st i in dom (T . n) holds ( p . i in dom (h | (divset ((T . n),i))) & ex z being Point of X st ( z = (h | (divset ((T . n),i))) . (p . i) & (S . n) . i = (vol (divset ((T . n),i))) * z ) ) ) ) by A11; consider q being middle_volume of f,T . n such that A38: ( q = Sf . n & ( for i being Nat st i in dom (T . n) holds ex z being Point of X st ( (F . n) . i in dom (f | (divset ((T . n),i))) & z = (f | (divset ((T . n),i))) . ((F . n) . i) & q . i = (vol (divset ((T . n),i))) * z ) ) ) by A22; consider r being middle_volume of g,T . n such that A39: ( r = Sg . n & ( for i being Nat st i in dom (T . n) holds ex z being Point of X st ( (F . n) . i in dom (g | (divset ((T . n),i))) & z = (g | (divset ((T . n),i))) . ((F . n) . i) & r . i = (vol (divset ((T . n),i))) * z ) ) ) by A33; A40: ( len (Sf . n) = len (T . n) & len (Sg . n) = len (T . n) & len (S . n) = len (T . n) ) by Def1; A41: ( dom (Sf . n) = dom (T . n) & dom (Sg . n) = dom (T . n) & dom (S . n) = dom (T . n) ) by A40, FINSEQ_3:29; now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(S_._n)_holds_ (S_._n)_/._i_=_((Sf_._n)_/._i)_+_((Sg_._n)_/._i) let i be Nat; ::_thesis: ( 1 <= i & i <= len (S . n) implies (S . n) /. i = ((Sf . n) /. i) + ((Sg . n) /. i) ) assume ( 1 <= i & i <= len (S . n) ) ; ::_thesis: (S . n) /. i = ((Sf . n) /. i) + ((Sg . n) /. i) then i in Seg (len (S . n)) by FINSEQ_1:1; then A42: i in dom (S . n) by FINSEQ_1:def_3; consider t being Point of X such that A43: ( t = (h | (divset ((T . n),i))) . ((F . n) . i) & (S . n) . i = (vol (divset ((T . n),i))) * t ) by A42, A41, A37; consider z being Point of X such that A44: ( (F . n) . i in dom (f | (divset ((T . n),i))) & z = (f | (divset ((T . n),i))) . ((F . n) . i) & q . i = (vol (divset ((T . n),i))) * z ) by A38, A42, A41; consider w being Point of X such that A45: ( (F . n) . i in dom (g | (divset ((T . n),i))) & w = (g | (divset ((T . n),i))) . ((F . n) . i) & r . i = (vol (divset ((T . n),i))) * w ) by A39, A42, A41; A46: (F . n) . i in divset ((T . n),i) by A45, RELAT_1:57; A47: (F . n) . i in dom g by A45, RELAT_1:57; A48: (F . n) . i in A by A45; then A49: (F . n) . i in dom h by FUNCT_2:def_1; A50: (F . n) . i in dom f by A48, FUNCT_2:def_1; A51: f /. ((F . n) . i) = f . ((F . n) . i) by A50, PARTFUN1:def_6 .= z by A44, A46, FUNCT_1:49 ; A52: g /. ((F . n) . i) = g . ((F . n) . i) by A47, PARTFUN1:def_6 .= w by A45, A46, FUNCT_1:49 ; A53: t = (h | (divset ((T . n),i))) . ((F . n) . i) by A43 .= h . ((F . n) . i) by A46, FUNCT_1:49 .= h /. ((F . n) . i) by A49, PARTFUN1:def_6 .= (f /. ((F . n) . i)) + (g /. ((F . n) . i)) by A49, A1, VFUNCT_1:def_1 .= z + w by A51, A52 ; A54: (vol (divset ((T . n),i))) * z = (Sf . n) . i by A44, A38 .= (Sf . n) /. i by A42, A41, PARTFUN1:def_6 ; A55: (vol (divset ((T . n),i))) * w = (Sg . n) . i by A45, A39 .= (Sg . n) /. i by A42, A41, PARTFUN1:def_6 ; thus (S . n) /. i = (S . n) . i by A42, PARTFUN1:def_6 .= (vol (divset ((T . n),i))) * t by A43 .= ((vol (divset ((T . n),i))) * z) + ((vol (divset ((T . n),i))) * w) by A53, RLVECT_1:def_5 .= ((Sf . n) /. i) + ((Sg . n) /. i) by A54, A55 ; ::_thesis: verum end; then A56: (Sf . n) + (Sg . n) = S . n by A41, BINOM:def_1; thus ((middle_sum (f,Sf)) . n) + ((middle_sum (g,Sg)) . n) = (middle_sum (f,(Sf . n))) + ((middle_sum (g,Sg)) . n) by Def4 .= (middle_sum (f,(Sf . n))) + (middle_sum (g,(Sg . n))) by Def4 .= (Sum (Sf . n)) + (middle_sum (g,(Sg . n))) .= (Sum (Sf . n)) + (Sum (Sg . n)) .= Sum (S . n) by A56, A40, Th1 .= middle_sum (h,(S . n)) .= (middle_sum (h,S)) . n by Def4 ; ::_thesis: verum end; hence (middle_sum (f,Sf)) + (middle_sum (g,Sg)) = middle_sum (h,S) by NORMSP_1:def_2; ::_thesis: verum end; hence middle_sum (h,S) is convergent by A34, A35, NORMSP_1:19; ::_thesis: lim (middle_sum (h,S)) = (integral f) + (integral g) thus lim (middle_sum (h,S)) = (integral f) + (integral g) by A34, A35, A36, NORMSP_1:25; ::_thesis: verum end; hence h is integrable by Def5; ::_thesis: integral h = (integral f) + (integral g) hence integral h = (integral f) + (integral g) by Def6, A3; ::_thesis: verum end; theorem :: INTEGR18:7 for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f, g, h being Function of A, the carrier of X st h = f - g & f is integrable & g is integrable holds ( h is integrable & integral h = (integral f) - (integral g) ) proof let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL for f, g, h being Function of A, the carrier of X st h = f - g & f is integrable & g is integrable holds ( h is integrable & integral h = (integral f) - (integral g) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g, h being Function of A, the carrier of X st h = f - g & f is integrable & g is integrable holds ( h is integrable & integral h = (integral f) - (integral g) ) let f, g, h be Function of A, the carrier of X; ::_thesis: ( h = f - g & f is integrable & g is integrable implies ( h is integrable & integral h = (integral f) - (integral g) ) ) assume A1: ( h = f - g & f is integrable & g is integrable ) ; ::_thesis: ( h is integrable & integral h = (integral f) - (integral g) ) then A2: h = f + (- g) by VFUNCT_1:25; dom (- g) = dom g by VFUNCT_1:def_5 .= A by FUNCT_2:def_1 ; then reconsider gg = - g as Function of A, the carrier of X by FUNCT_2:def_1; A3: gg is integrable by A1, Th5; hence h is integrable by A1, A2, Th6; ::_thesis: integral h = (integral f) - (integral g) integral h = (integral f) + (integral gg) by A1, A2, A3, Th6; then integral h = (integral f) + (- (integral g)) by A1, Th5; hence integral h = (integral f) - (integral g) by RLVECT_1:def_11; ::_thesis: verum end; definition let X be RealNormSpace; let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL, the carrier of X; predf is_integrable_on A means :Def7: :: INTEGR18:def 7 ex g being Function of A, the carrier of X st ( g = f | A & g is integrable ); end; :: deftheorem Def7 defines is_integrable_on INTEGR18:def_7_:_ for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL, the carrier of X holds ( f is_integrable_on A iff ex g being Function of A, the carrier of X st ( g = f | A & g is integrable ) ); definition let X be RealNormSpace; let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL, the carrier of X; assume A1: A c= dom f ; func integral (f,A) -> Element of X means :Def8: :: INTEGR18:def 8 ex g being Function of A, the carrier of X st ( g = f | A & it = integral g ); correctness existence ex b1 being Element of X ex g being Function of A, the carrier of X st ( g = f | A & b1 = integral g ); uniqueness for b1, b2 being Element of X st ex g being Function of A, the carrier of X st ( g = f | A & b1 = integral g ) & ex g being Function of A, the carrier of X st ( g = f | A & b2 = integral g ) holds b1 = b2; proof A2: dom (f | A) = A by A1, RELAT_1:62; rng (f | A) c= the carrier of X ; then reconsider g = f | A as Function of A, the carrier of X by A2, FUNCT_2:2; integral g is Point of X ; hence ( ex b1 being Element of X ex g being Function of A, the carrier of X st ( g = f | A & b1 = integral g ) & ( for b1, b2 being Element of X st ex g being Function of A, the carrier of X st ( g = f | A & b1 = integral g ) & ex g being Function of A, the carrier of X st ( g = f | A & b2 = integral g ) holds b1 = b2 ) ) ; ::_thesis: verum end; end; :: deftheorem Def8 defines integral INTEGR18:def_8_:_ for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL, the carrier of X st A c= dom f holds for b4 being Element of X holds ( b4 = integral (f,A) iff ex g being Function of A, the carrier of X st ( g = f | A & b4 = integral g ) ); theorem Th8: :: INTEGR18:8 for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL, the carrier of X for g being Function of A, the carrier of X st f | A = g holds ( f is_integrable_on A iff g is integrable ) proof let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL, the carrier of X for g being Function of A, the carrier of X 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, the carrier of X for g being Function of A, the carrier of X st f | A = g holds ( f is_integrable_on A iff g is integrable ) let f be PartFunc of REAL, the carrier of X; ::_thesis: for g being Function of A, the carrier of X st f | A = g holds ( f is_integrable_on A iff g is integrable ) let g be Function of A, the carrier of X; ::_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 ) hereby ::_thesis: ( g is integrable implies f is_integrable_on A ) assume f is_integrable_on A ; ::_thesis: g is integrable then ex g being Function of A, the carrier of X st ( g = f | A & g is integrable ) by Def7; hence g is integrable by A1; ::_thesis: verum end; assume g is integrable ; ::_thesis: f is_integrable_on A hence f is_integrable_on A by A1, Def7; ::_thesis: verum end; theorem :: INTEGR18:9 for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL, the carrier of X for g being Function of A, the carrier of X st A c= dom f & f | A = g holds integral (f,A) = integral g by Def8; theorem Th10: :: INTEGR18:10 for X, Y being non empty set for V being RealNormSpace for g, f being PartFunc of X, the carrier of V for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds g1 + f1 = g + f proof let X, Y be non empty set ; ::_thesis: for V being RealNormSpace for g, f being PartFunc of X, the carrier of V for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds g1 + f1 = g + f let V be RealNormSpace; ::_thesis: for g, f being PartFunc of X, the carrier of V for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds g1 + f1 = g + f let g, f be PartFunc of X, the carrier of V; ::_thesis: for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds g1 + f1 = g + f let g1, f1 be PartFunc of Y, the carrier of V; ::_thesis: ( g = g1 & f = f1 implies g1 + f1 = g + f ) assume A1: ( g = g1 & f = f1 ) ; ::_thesis: g1 + f1 = g + f A2: dom (g + f) = (dom g) /\ (dom f) by VFUNCT_1:def_1 .= (dom g1) /\ (dom f1) by A1 ; A3: g + f is PartFunc of Y, the carrier of V by A2, RELSET_1:5; for c being Element of Y st c in dom (g + f) holds (g + f) /. c = (g1 /. c) + (f1 /. c) by A1, VFUNCT_1:def_1; hence g1 + f1 = g + f by A3, A2, VFUNCT_1:def_1; ::_thesis: verum end; theorem :: INTEGR18:11 for X, Y being non empty set for V being RealNormSpace for g, f being PartFunc of X, the carrier of V for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds g1 - f1 = g - f proof let X, Y be non empty set ; ::_thesis: for V being RealNormSpace for g, f being PartFunc of X, the carrier of V for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds g1 - f1 = g - f let V be RealNormSpace; ::_thesis: for g, f being PartFunc of X, the carrier of V for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds g1 - f1 = g - f let g, f be PartFunc of X, the carrier of V; ::_thesis: for g1, f1 being PartFunc of Y, the carrier of V st g = g1 & f = f1 holds g1 - f1 = g - f let g1, f1 be PartFunc of Y, the carrier of V; ::_thesis: ( g = g1 & f = f1 implies g1 - f1 = g - f ) assume A1: ( g = g1 & f = f1 ) ; ::_thesis: g1 - f1 = g - f A2: dom (g - f) = (dom g) /\ (dom f) by VFUNCT_1:def_2 .= (dom g1) /\ (dom f1) by A1 ; A3: g - f is PartFunc of Y, the carrier of V by A2, RELSET_1:5; for c being Element of Y st c in dom (g - f) holds (g - f) /. c = (g1 /. c) - (f1 /. c) by A1, VFUNCT_1:def_2; hence g1 - f1 = g - f by A3, A2, VFUNCT_1:def_2; ::_thesis: verum end; theorem Th12: :: INTEGR18:12 for r being Real for X, Y being non empty set for V being RealNormSpace for g being PartFunc of X, the carrier of V for g1 being PartFunc of Y, the carrier of V st g = g1 holds r (#) g1 = r (#) g proof let r be Real; ::_thesis: for X, Y being non empty set for V being RealNormSpace for g being PartFunc of X, the carrier of V for g1 being PartFunc of Y, the carrier of V st g = g1 holds r (#) g1 = r (#) g let X, Y be non empty set ; ::_thesis: for V being RealNormSpace for g being PartFunc of X, the carrier of V for g1 being PartFunc of Y, the carrier of V st g = g1 holds r (#) g1 = r (#) g let V be RealNormSpace; ::_thesis: for g being PartFunc of X, the carrier of V for g1 being PartFunc of Y, the carrier of V st g = g1 holds r (#) g1 = r (#) g let g be PartFunc of X, the carrier of V; ::_thesis: for g1 being PartFunc of Y, the carrier of V st g = g1 holds r (#) g1 = r (#) g let g1 be PartFunc of Y, the carrier of V; ::_thesis: ( g = g1 implies r (#) g1 = r (#) g ) assume A1: g = g1 ; ::_thesis: r (#) g1 = r (#) g A2: dom (r (#) g) = dom g by VFUNCT_1:def_4 .= dom g1 by A1 ; A3: r (#) g is PartFunc of Y, the carrier of V by A2, RELSET_1:5; for c being Element of Y st c in dom (r (#) g) holds (r (#) g) /. c = r * (g1 /. c) by A1, VFUNCT_1:def_4; hence r (#) g1 = r (#) g by A3, A2, VFUNCT_1:def_4; ::_thesis: verum end; begin theorem Th13: :: INTEGR18:13 for X being RealNormSpace for r being Real for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) proof let X be RealNormSpace; ::_thesis: for r being Real for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A 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, the carrier of X st A c= dom f & f is_integrable_on A 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, the carrier of X st A c= dom f & f is_integrable_on A holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) let f be PartFunc of REAL, the carrier of X; ::_thesis: ( A c= dom f & f is_integrable_on A implies ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) ) assume A1: ( A c= dom f & f is_integrable_on A ) ; ::_thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) A2: A c= dom (r (#) f) by A1, VFUNCT_1:def_4; consider g being Function of A, the carrier of X such that A3: ( g = f | A & g is integrable ) by A1, Def7; A4: (r (#) f) | A = r (#) (f | A) by VFUNCT_1:31 .= r (#) g by A3, Th12 ; r (#) g is total by VFUNCT_1:34; then reconsider gg = r (#) g as Function of A, the carrier of X ; ( gg is integrable & integral gg = r * (integral g) ) by A3, Th4; hence r (#) f is_integrable_on A by A4, Th8; ::_thesis: integral ((r (#) f),A) = r * (integral (f,A)) thus integral ((r (#) f),A) = integral gg by A4, A2, Def8 .= r * (integral g) by A3, Th4 .= r * (integral (f,A)) by A3, A1, Def8 ; ::_thesis: verum end; theorem Th14: :: INTEGR18:14 for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds ( f1 + f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) ) proof let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds ( f1 + f2 is_integrable_on 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, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds ( f1 + f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) ) let f1, f2 be PartFunc of REAL, the carrier of X; ::_thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 implies ( f1 + f2 is_integrable_on 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 ) ; ::_thesis: ( f1 + f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) ) A c= (dom f1) /\ (dom f2) by A2, XBOOLE_1:19; then A3: A c= dom (f1 + f2) by VFUNCT_1:def_1; consider g1 being Function of A, the carrier of X such that A4: ( g1 = f1 | A & g1 is integrable ) by A1, Def7; consider g2 being Function of A, the carrier of X such that A5: ( g2 = f2 | A & g2 is integrable ) by A1, Def7; (f1 + f2) | A = (f1 | A) + (f2 | A) by VFUNCT_1:27; then A6: (f1 + f2) | A = g1 + g2 by A4, A5, Th10; g1 + g2 is total by VFUNCT_1:32; then reconsider g = g1 + g2 as Function of A, the carrier of X ; g is integrable by Th6, A4, A5; hence f1 + f2 is_integrable_on A by A6, Th8; ::_thesis: integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) thus integral ((f1 + f2),A) = integral g by Def8, A6, A3 .= (integral g1) + (integral g2) by Th6, A4, A5 .= (integral (f1,A)) + (integral g2) by A2, A4, Def8 .= (integral (f1,A)) + (integral (f2,A)) by A2, A5, Def8 ; ::_thesis: verum end; theorem :: INTEGR18:15 for X being RealNormSpace for A being non empty closed_interval Subset of REAL for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds ( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) proof let X be RealNormSpace; ::_thesis: for A being non empty closed_interval Subset of REAL for f1, f2 being PartFunc of REAL, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds ( f1 - f2 is_integrable_on 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, the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds ( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) let f1, f2 be PartFunc of REAL, the carrier of X; ::_thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 implies ( f1 - f2 is_integrable_on 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 ) ; ::_thesis: ( f1 - f2 is_integrable_on A & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) A3: f1 - f2 = f1 + (- f2) by VFUNCT_1:25; A4: dom (- f2) = dom f2 by VFUNCT_1:def_5; A5: - f2 = (- 1) (#) f2 by VFUNCT_1:23; then A6: - f2 is_integrable_on A by A1, A2, Th13; hence f1 - f2 is_integrable_on A by A1, A2, A3, A4, Th14; ::_thesis: integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) thus integral ((f1 - f2),A) = integral ((f1 + (- f2)),A) by VFUNCT_1:25 .= (integral (f1,A)) + (integral ((- f2),A)) by A1, A2, A4, A6, Th14 .= (integral (f1,A)) + ((- 1) * (integral (f2,A))) by A1, A2, A5, Th13 .= (integral (f1,A)) + (- (integral (f2,A))) by RLVECT_1:16 .= (integral (f1,A)) - (integral (f2,A)) by RLVECT_1:def_11 ; ::_thesis: verum end; definition let X be RealNormSpace; let f be PartFunc of REAL, the carrier of X; let a, b be real number ; func integral (f,a,b) -> Element of X equals :Def9: :: INTEGR18:def 9 integral (f,['a,b']) if a <= b otherwise - (integral (f,['b,a'])); correctness coherence ( ( a <= b implies integral (f,['a,b']) is Element of X ) & ( not a <= b implies - (integral (f,['b,a'])) is Element of X ) ); consistency for b1 being Element of X holds verum; ; end; :: deftheorem Def9 defines integral INTEGR18:def_9_:_ for X being RealNormSpace for f being PartFunc of REAL, the carrier of X for a, b being real number holds ( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) & ( not a <= b implies integral (f,a,b) = - (integral (f,['b,a'])) ) ); theorem Th16: :: INTEGR18:16 for X being RealNormSpace for f being PartFunc of REAL, the carrier of X 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 X be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of X 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, the carrier of X; ::_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) ) consider a1, b1 being Real such that A1: a1 <= b1 and A2: A = [.a1,b1.] by MEASURE5:14; assume A = [.a,b.] ; ::_thesis: integral (f,A) = integral (f,a,b) then A3: ( a1 = a & b1 = b ) by A2, INTEGRA1:5; then integral (f,a,b) = integral (f,['a,b']) by A1, Def9; hence integral (f,A) = integral (f,a,b) by A1, A2, A3, INTEGRA5:def_3; ::_thesis: verum end; theorem Th17: :: INTEGR18:17 for X being RealNormSpace for f being PartFunc of REAL, the carrier of X for A being non empty closed_interval Subset of REAL st vol A = 0 & A c= dom f holds ( f is_integrable_on A & integral (f,A) = 0. X ) proof let X be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of X for A being non empty closed_interval Subset of REAL st vol A = 0 & A c= dom f holds ( f is_integrable_on A & integral (f,A) = 0. X ) let f be PartFunc of REAL, the carrier of X; ::_thesis: for A being non empty closed_interval Subset of REAL st vol A = 0 & A c= dom f holds ( f is_integrable_on A & integral (f,A) = 0. X ) let A be non empty closed_interval Subset of REAL; ::_thesis: ( vol A = 0 & A c= dom f implies ( f is_integrable_on A & integral (f,A) = 0. X ) ) assume A1: ( vol A = 0 & A c= dom f ) ; ::_thesis: ( f is_integrable_on A & integral (f,A) = 0. X ) f is Function of (dom f),(rng f) by FUNCT_2:1; then f is Function of (dom f), the carrier of X by FUNCT_2:2; then reconsider g = f | A as Function of A, the carrier of X by A1, FUNCT_2:32; A2: for T being DivSequence of A for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = 0. X ) proof let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = 0. X ) let S be middle_volume_Sequence of g,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = 0. X ) ) assume ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = 0. X ) A3: for i being Element of NAT holds middle_sum (g,(S . i)) = 0. X proof let i be Element of NAT ; ::_thesis: middle_sum (g,(S . i)) = 0. X A4: len (S . i) = len (S . i) ; now__::_thesis:_for_k_being_Element_of_NAT_ for_v_being_Element_of_X_st_k_in_dom_(S_._i)_&_v_=_(S_._i)_._k_holds_ (S_._i)_._k_=_-_v let k be Element of NAT ; ::_thesis: for v being Element of X st k in dom (S . i) & v = (S . i) . k holds (S . i) . k = - v let v be Element of X; ::_thesis: ( k in dom (S . i) & v = (S . i) . k implies (S . i) . k = - v ) assume A5: ( k in dom (S . i) & v = (S . i) . k ) ; ::_thesis: (S . i) . k = - v then k in Seg (len (S . i)) by FINSEQ_1:def_3; then k in Seg (len (T . i)) by Def1; then A6: k in dom (T . i) by FINSEQ_1:def_3; then consider c being VECTOR of X such that A7: ( c in rng (g | (divset ((T . i),k))) & (S . i) . k = (vol (divset ((T . i),k))) * c ) by Def1; ( 0 <= vol (divset ((T . i),k)) & vol (divset ((T . i),k)) <= 0 ) by A1, A6, INTEGRA1:8, INTEGRA1:9, INTEGRA2:38; then A8: vol (divset ((T . i),k)) = 0 ; (S . i) . k = 0. X by A8, A7, RLVECT_1:10; hence (S . i) . k = - v by A5, RLVECT_1:12; ::_thesis: verum end; then Sum (S . i) = - (Sum (S . i)) by A4, RLVECT_1:40; hence middle_sum (g,(S . i)) = 0. X by RLVECT_1:19; ::_thesis: verum end; A9: for i being Element of NAT holds (middle_sum (g,S)) . i = 0. X proof let i be Element of NAT ; ::_thesis: (middle_sum (g,S)) . i = 0. X thus (middle_sum (g,S)) . i = middle_sum (g,(S . i)) by Def4 .= 0. X by A3 ; ::_thesis: verum end; A10: for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r proof let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r ) assume A11: 0 < r ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r take m = 0 ; ::_thesis: for n being Element of NAT st m <= n holds ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r let n be Element of NAT ; ::_thesis: ( m <= n implies ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r ) assume m <= n ; ::_thesis: ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r ||.(((middle_sum (g,S)) . n) - (0. X)).|| = ||.((0. X) - (0. X)).|| by A9 .= 0 by NORMSP_1:6 ; hence ||.(((middle_sum (g,S)) . n) - (0. X)).|| < r by A11; ::_thesis: verum end; hence middle_sum (g,S) is convergent by NORMSP_1:def_6; ::_thesis: lim (middle_sum (g,S)) = 0. X hence lim (middle_sum (g,S)) = 0. X by A10, NORMSP_1:def_7; ::_thesis: verum end; then A12: g is integrable by Def5; hence f is_integrable_on A by Def7; ::_thesis: integral (f,A) = 0. X integral g = 0. X by A12, A2, Def6; hence integral (f,A) = 0. X by Def8, A1; ::_thesis: verum end; theorem :: INTEGR18:18 for X being RealNormSpace for f being PartFunc of REAL, the carrier of X for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] & A c= dom f holds - (integral (f,A)) = integral (f,a,b) proof let X be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of X for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] & A c= dom f holds - (integral (f,A)) = integral (f,a,b) let f be PartFunc of REAL, the carrier of X; ::_thesis: for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] & A c= dom f 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.] & A c= dom f holds - (integral (f,A)) = integral (f,a,b) let a, b be Real; ::_thesis: ( A = [.b,a.] & A c= dom f implies - (integral (f,A)) = integral (f,a,b) ) consider a1, b1 being Real such that A1: a1 <= b1 and A2: A = [.a1,b1.] by MEASURE5:14; assume A3: ( A = [.b,a.] & A c= dom f ) ; ::_thesis: - (integral (f,A)) = integral (f,a,b) then A4: ( a1 = b & b1 = a ) by A2, INTEGRA1:5; now__::_thesis:_-_(integral_(f,A))_=_integral_(f,a,b) percases ( b < a or b = a ) by A1, A4, XXREAL_0:1; supposeA5: b < a ; ::_thesis: - (integral (f,A)) = integral (f,a,b) then integral (f,a,b) = - (integral (f,['b,a'])) by Def9; hence - (integral (f,A)) = integral (f,a,b) by A3, A5, INTEGRA5:def_3; ::_thesis: verum end; supposeA6: b = a ; ::_thesis: - (integral (f,A)) = integral (f,a,b) A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then ( lower_bound A = b & upper_bound A = a ) by A3, INTEGRA1:5; then A7: vol A = (upper_bound A) - (upper_bound A) by A6 .= 0 ; A8: integral (f,a,b) = integral (f,A) by A3, A6, Th16; A9: - (integral (f,a,b)) = - (integral (f,A)) by A3, A6, Th16; integral (f,a,b) = 0. X by A7, A3, Th17, A8; hence - (integral (f,A)) = integral (f,a,b) by A9, RLVECT_1:12; ::_thesis: verum end; end; end; hence - (integral (f,A)) = integral (f,a,b) ; ::_thesis: verum end;