:: Riemann Integral of Functions from $\mathbbbR$ into Real Normed Space
:: by Keiichi Miyajima , Takahiro Kato and Yasunari Shidama
::
:: Received May 20, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies INTEGRA1, INTEGRA2, FINSEQ_1, NORMSP_1, SEQ_2, TARSKI, STRUCT_0,
ORDINAL2, INTEGRA5, XBOOLE_0, SUBSET_1, NUMBERS, ARYTM_1, NAT_1,
MEASURE7, CARD_3, RELAT_1, FUNCT_1, REAL_1, XXREAL_0, XXREAL_1, VALUED_1,
PARTFUN1, RLVECT_1, FUNCT_3, INTEGR15, PRE_TOPC, ARYTM_3, CARD_1,
SUPINF_2, SEQ_4, MEASURE5;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1,
FUNCT_2, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, FINSEQ_1,
FINSEQ_2, SEQ_2, SEQ_4, RCOMP_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3,
INTEGRA5, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1,
BINOM;
constructors REAL_1, SEQ_4, VFUNCT_1, RELSET_1, INTEGRA2, INTEGRA5, INTEGRA3,
SEQ_2, BINOM, COMSEQ_2;
registrations NUMBERS, XREAL_0, STRUCT_0, RELSET_1, INTEGRA1, FUNCT_2,
XXREAL_0, ORDINAL1, MEASURE5, FINSEQ_1, MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, INTEGRA1;
expansions XBOOLE_0;
theorems XBOOLE_1, INTEGRA1, INTEGRA2, INTEGRA4, RELSET_1, BINOM, XXREAL_0,
RELAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, PARTFUN1, INTEGRA5, NORMSP_1,
VFUNCT_1, RLVECT_1, RLVECT_2, FINSEQ_3, MEASURE5, ORDINAL1;
schemes FUNCT_2, FINSEQ_1;
begin :: Preliminaries
reserve X for RealNormSpace;
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:
len it = len D & for i be Nat st i in dom D holds
ex c be Point of X st c in rng (f|divset(D,i)) &
it.i= (vol divset(D,i)) * c;
correctness
proof
defpred P1[Nat, set] means ex c be 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 P1[k,x]
proof
let k be Nat;
assume k in Seg len D; 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
rng (f|divset(D,k)) is non empty by RELAT_1:42; then
consider c be object such that
A4: c in rng (f|divset(D,k));
reconsider c as Point of X by A4;
(vol divset(D,k)) * c is Element of the carrier of X;
hence thesis by A4;
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 P1[k,p.k]
from FINSEQ_1:sch 5(A2);
len p = len D by A5,FINSEQ_1:def 3;
hence thesis by A5,A1;
end;
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 D be Division of A;
let F be middle_volume of f,D;
func middle_sum(f,F) -> Point of X equals
Sum(F);
coherence;
end;
definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL,
f be Function of A,the carrier of X,
T be DivSequence of A;
mode middle_volume_Sequence of f,T -> sequence of (the carrier of X)*
means :Def3:
for k be Element of NAT holds it.k is middle_volume of f,T.k;
correctness
proof
defpred P[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 P[x, y]
proof
let x be Element of NAT;
set y = the middle_volume of f,T.x;
reconsider y as Element of (the carrier of X)* by FINSEQ_1:def 11;
y is middle_volume of f,T.x;
hence thesis;
end;
ex f being sequence of (the carrier of X)*
st for x being Element of NAT holds P[x, f.x] from FUNCT_2:sch 3(A1);
hence thesis;
end;
end;
definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL,
f be Function of A,the carrier of X,
T be DivSequence of A,
S be middle_volume_Sequence of f,T,
k be Nat;
redefine func S.k -> middle_volume of f,T.k; :: redefines . (FUNCT_1, definition)
coherence
proof
k in NAT by ORDINAL1:def 12;
hence thesis by Def3;
end;
end;
definition
let X be RealNormSpace;
let A be non empty closed_interval Subset of REAL,
f be Function of A,the carrier of X,
T be DivSequence of A,
S be middle_volume_Sequence of f,T;
func middle_sum(f,S) -> sequence of X means :Def4:
for i be Nat holds it.i = middle_sum(f,S.i);
existence
proof
deffunc H1(Nat) = middle_sum(f,S.$1);
consider IT being sequence of the carrier of X such that
A1: for i being Element of NAT holds IT.i = H1(i) from FUNCT_2:sch 4;
take IT;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let F1, F2 be sequence of X;
assume that
A2: for i being Nat holds F1.i = middle_sum(f,S.i) and
A3: for i being Nat holds F2.i = middle_sum(f,S.i);
for i being Element of NAT holds F1.i = F2.i
proof
let i be Element of NAT;
F1.i = middle_sum(f,S.i) by A2
.= F2.i by A3;
hence F1.i = F2.i;
end;
hence F1 = F2 by FUNCT_2:63;
end;
end;
begin :: Definition of Riemann Integral on Functions from $\mathbbbR$ into Real Normed Space
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;
attr f is integrable means
ex I be Point of X st for T being DivSequence of A,
S be 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;
theorem Th1:
for X be RealNormSpace,
R1, R2, R3 be FinSequence of X
st len R1 = len R2 & R3 = R1 + R2 holds Sum(R3) = Sum(R1) + Sum(R2)
proof
let X be RealNormSpace,
R1, R2, R3 be FinSequence of X;
assume A1: len R1 = len R2 & R3 = R1 + R2; then
dom R1 = dom R2 by FINSEQ_3:29;
hence Sum(R3) = Sum(R1) + Sum(R2) by A1,BINOM:7;
end;
theorem
for X be RealNormSpace,
R1, R2, R3 be FinSequence of X
st len R1 = len R2 & R3 = R1 - R2 holds Sum(R3) = Sum(R1) - Sum(R2)
proof
let X be RealNormSpace,
R1, R2, R3 be FinSequence of X;
assume A1: len R1 = len R2 & R3 = R1 - 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 be Nat st k in dom R1 holds R3.k = R1/.k - R2/.k
proof
let k be Nat;
assume A6: k in dom R1;
thus R3.k = R3/.k by A6,A3,PARTFUN1:def 6
.= R1/.k - R2/.k by A1,A6,A3,VFUNCT_1:def 2;
end;
thus thesis by A1,A4,A5,RLVECT_2:5;
end;
theorem Th3:
for X be RealNormSpace,
R1, R2 be FinSequence of X,
a be Real st R2 = a(#)R1 holds Sum(R2) = a * Sum(R1)
proof
let X be RealNormSpace,
R1, R2 be FinSequence of X,
a be Real;
assume A1: R2 = a(#)R1;
dom R2 = dom R1 by A1,VFUNCT_1:def 4; then
A2: len R2 = len R1 by FINSEQ_3:29;
A3: for k be Nat st k in dom R1 holds R2.k = a * R1/.k
proof
let k be Nat;
assume k in dom R1; 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;
end;
thus thesis by A2,A3,RLVECT_2:3;
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:
for T being DivSequence of A,
S be 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 by A1;
uniqueness
proof
let I1, I2 be Point of X;
assume
A2: for T being DivSequence of A,
S be 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;
assume
A3: for T being DivSequence of A,
S be 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;
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,S)) by A2,A4
.= I2 by A3,A4;
end;
end;
theorem Th4:
for X be RealNormSpace,
A be non empty closed_interval Subset of REAL,
r be Real,
f, h be 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,
A be non empty closed_interval Subset of REAL,
r be Real,
f, h be Function of A,the carrier of X;
assume A1: h = r(#)f & f is integrable;
A2: dom h = A & dom f = A by FUNCT_2:def 1;
A3: now let T be DivSequence of A, S be middle_volume_Sequence of h,T;
assume A4: delta(T) is convergent & lim delta(T) = 0;
defpred P[Element of NAT, set] means ex p being FinSequence of REAL st
p = $2 & len p = len (T.$1) & for i be Nat st i in dom (T.$1) holds
(p.i) in dom (h|divset((T.$1),i)) & ex z be 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 P[k, p]
proof
let k being Element of NAT;
defpred P1[ Nat, set] means $2 in dom (h|divset((T.k),$1)) &
ex c be 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 P1[i,x]
proof
let i be Nat;
assume i in Seg len (T.k); then
i in dom (T.k) by FINSEQ_1:def 3; then
consider c be 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 be object 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 as Element of REAL;
take x;
thus thesis by A8,A9;
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
P1[i,p.i] from FINSEQ_1:sch 5(A7);
take p;
len p = len (T.k) by A10,FINSEQ_1:def 3;
hence thesis by A10,A6,FINSEQ_1:def 11;
end;
consider F being sequence of (REAL)* such that
A11: for x being Element of NAT holds P[x, F.x] from FUNCT_2:sch 3(A5);
defpred P1[Element of NAT,set] means ex q be middle_volume of f,T.$1
st q = $2 & for i be Nat st i in dom (T.$1) holds ex z be 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 P1[k, y]
proof
let k being Element of NAT;
defpred P11[ Nat, set] means ex c be 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 P11[i,x]
proof
let i be Nat;
assume i in Seg len (T.k); 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 be Nat st i in dom (T.k) holds
p.i in dom (h|divset((T.k),i)) & ex z be 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 thesis by A16,A18;
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
P11[i,q.i] from FINSEQ_1:sch 5(A14);
A20: len q = len (T.k) by A19,FINSEQ_1:def 3;
now let i be Nat;
assume i in dom (T.k); then
i in Seg len (T.k) by FINSEQ_1:def 3; then
consider c be 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 be 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;
end;
then reconsider 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 thesis by A13,A19;
end;
consider Sf being sequence of (the carrier of X)* such that
A22: for x being Element of NAT holds P1[x, Sf.x] from FUNCT_2:sch 3(A12);
now let k be Element of NAT;
ex q be middle_volume of f,T.k st q = Sf.k &
for i be Nat st i in dom (T.k) holds ex z be 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;
end;
then reconsider Sf as middle_volume_Sequence of f,T by Def3;
A23: middle_sum(f,Sf) is convergent by A1,A4;
A24: r * middle_sum(f,Sf) = middle_sum(h,S)
proof
now let n be Nat;
A25: n in NAT by ORDINAL1:def 12;
consider p being FinSequence of REAL such that
A26: p = F.n & len p = len (T.n) & for i be Nat st i in dom (T.n) holds
(p.i) in dom (h|divset((T.n),i)) & ex z be Point of X st
z = (h|divset((T.n),i)).(p.i) &
(S.n).i = (vol divset((T.n),i)) * z by A11,A25;
consider q be middle_volume of f,T.n such that
A27: q = Sf.n & for i be Nat st i in dom (T.n) holds ex z be 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,A25;
len (Sf.n) = len (T.n) & len (S.n) = len (T.n) by Def1; then
A28: dom (Sf.n) = dom (T.n) & dom (S.n) = dom (T.n) by FINSEQ_3:29;
now let x be Element of NAT;
assume A29: x in dom (S.n);
reconsider i = x as Nat;
consider t be Point of X such that
A30: t = (h|divset((T.n),i)).((F.n).i) &
(S.n).i = (vol divset((T.n),i)) * t by A29,A28,A26;
consider z be Point of X such that
A31: (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 A27,A29,A28;
A32: (F.n).i in divset((T.n),i) by A31,RELAT_1:57;
(F.n).i in A by A31; then
A33: (F.n).i in dom h by FUNCT_2:def 1;
A34: (F.n).i in dom f by A31,RELAT_1:57;
A35: f/.((F.n).i) = f.((F.n).i) by A34,PARTFUN1:def 6
.= z by A31,A32,FUNCT_1:49;
A36: t = (h|divset((T.n),i)).((F.n).i) by A30
.= h.((F.n).i) by A32,FUNCT_1:49
.= h/.((F.n).i) by A33,PARTFUN1:def 6
.= r * (f/.((F.n).i) ) by A33,A1,VFUNCT_1:def 4
.= r * z by A35;
A37: (vol divset((T.n),i)) * z = (Sf.n).x by A31,A27
.= (Sf.n)/.x by A29,A28,PARTFUN1:def 6;
thus (S.n)/.x = (S.n).x by A29,PARTFUN1:def 6
.= (vol divset((T.n),i)) * t by A30
.= (vol divset((T.n),i)) * (r * z) by A36
.= ((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 A37;
end; then
A38: r(#)(Sf.n) = S.n by A28,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 A38,Th3
.= middle_sum(h,S.n)
.= middle_sum(h,S).n by Def4;
end;
hence thesis by NORMSP_1:def 5;
end;
A39: 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;
thus lim (middle_sum(h,S)) = r * integral(f) by A24,A39;
end;
hence h is integrable;
hence integral(h) = r * integral(f) by Def6,A3;
end;
reconsider jj=1 as Real;
theorem Th5:
for X be RealNormSpace,
A be non empty closed_interval Subset of REAL,
f, h be 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,
A be non empty closed_interval Subset of REAL,
f, h be Function of A,the carrier of X;
assume A1: h = -f & f is integrable; then
A2: h = (-jj)(#)f by VFUNCT_1:23;
hence h is integrable by A1,Th4;
integral(h) = (-jj)*integral(f) by A1,A2,Th4;
hence integral(h) = -integral(f) by RLVECT_1:16;
end;
theorem Th6:
for X be RealNormSpace,
A be non empty closed_interval Subset of REAL,
f, g, h be 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,
A be non empty closed_interval Subset of REAL,
f, g, h be Function of A,the carrier of X;
assume A1: h = f + g & f is integrable & g is integrable;
A2: dom h = A & dom f = A & dom g = A by FUNCT_2:def 1;
A3: now let T be DivSequence of A, S be middle_volume_Sequence of h,T;
assume A4: delta(T) is convergent & lim delta(T)=0;
defpred P[Element of NAT, set] means ex p being FinSequence of REAL st
p = $2 & len p = len (T.$1) & for i be Nat st i in dom (T.$1) holds
(p.i) in dom (h|divset((T.$1),i)) & ex z be 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 P[k, p]
proof
let k being Element of NAT;
defpred P1[ Nat, set] means $2 in dom (h|divset((T.k),$1)) &
ex c be 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 P1[i,x]
proof
let i be Nat;
assume i in Seg len (T.k); then
i in dom (T.k) by FINSEQ_1:def 3; then
consider c be 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 be object 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 as Element of REAL;
take x;
thus thesis by A8,A9;
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 P1[i,p.i] from FINSEQ_1:sch 5(A7);
take p;
len p = len (T.k) by A10,FINSEQ_1:def 3;
hence thesis by A10,A6,FINSEQ_1:def 11;
end;
consider F being sequence of (REAL)* such that
A11: for x being Element of NAT holds P[x, F.x] from FUNCT_2:sch 3(A5);
defpred P1[Element of NAT,set] means ex q be middle_volume of f,T.$1
st q = $2 & for i be Nat st i in dom (T.$1) holds ex z be 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 P1[k, y]
proof
let k being Element of NAT;
defpred P11[ Nat, set] means ex c be 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 P11[i,x]
proof
let i be Nat;
assume i in Seg len (T.k); 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 be Nat st i in dom (T.k) holds
p.i in dom (h|divset((T.k),i)) & ex z be 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 thesis by A16,A18;
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
P11[i,q.i] from FINSEQ_1:sch 5(A14);
A20: len q = len (T.k) by A19,FINSEQ_1:def 3;
now let i be Nat;
assume i in dom (T.k); then
i in Seg len (T.k) by FINSEQ_1:def 3; then
consider c be 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 be 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;
end;
then reconsider 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 thesis by A13,A19;
end;
consider Sf being sequence of (the carrier of X)* such that
A22: for x being Element of NAT holds P1[x, Sf.x] from FUNCT_2:sch 3(A12);
now let k be Element of NAT;
ex q be middle_volume of f,T.k st q = Sf.k &
for i be Nat st i in dom (T.k) holds ex z be 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;
end;
then reconsider Sf as middle_volume_Sequence of f,T by Def3;
defpred Q1[Element of NAT,set] means ex q be middle_volume of g,T.$1
st q = $2 & for i be Nat st i in dom (T.$1) holds ex z be 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 Q1[k, y]
proof
let k being Element of NAT;
defpred Q11[Nat, set] means ex c be 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 Q11[i,x]
proof
let i be Nat;
assume i in Seg len (T.k); 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 be Nat st i in dom (T.k) holds
p.i in dom (h|divset((T.k),i)) & ex z be 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 thesis by A27,A29;
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 Q11[i,q.i] from FINSEQ_1:sch 5(A25);
A31: len q = len (T.k) by A30,FINSEQ_1:def 3;
now let i be Nat;
assume i in dom (T.k); then
i in Seg len (T.k) by FINSEQ_1:def 3; then
consider c be 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 be 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;
end;
then reconsider 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 thesis by A24,A30;
end;
consider Sg being sequence of (the carrier of X)* such that
A33: for x being Element of NAT holds Q1[x, Sg.x] from FUNCT_2:sch 3(A23);
now let k be Element of NAT;
ex q be middle_volume of g,T.k st q = Sg.k & for i be Nat st
i in dom (T.k) holds ex z be 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;
end;
then reconsider Sg as middle_volume_Sequence of g,T by Def3;
A34: middle_sum(f,Sf) is convergent &
lim (middle_sum(f,Sf)) = integral(f) by Def6,A1,A4;
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 let n be Nat;
A37: n in NAT by ORDINAL1:def 12;
consider p being FinSequence of REAL such that
A38: p = F.n & len p = len (T.n) & for i be Nat st i in dom (T.n) holds
(p.i) in dom (h|divset((T.n),i)) & ex z be Point of X st
z = (h|divset((T.n),i)).(p.i) &
(S.n).i = (vol divset((T.n),i)) * z by A11,A37;
consider q be middle_volume of f,T.n such that
A39: q = Sf.n & for i be Nat st i in dom (T.n) holds ex z be 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,A37;
consider r be middle_volume of g,T.n such that
A40: r = Sg.n & for i be Nat st i in dom (T.n) holds ex z be 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,A37;
A41: len (Sf.n) = len (T.n) & len (Sg.n) = len (T.n) &
len (S.n) = len (T.n) by Def1;
A42: dom (Sf.n) = dom (T.n) & dom (Sg.n) = dom (T.n) &
dom (S.n) = dom (T.n) by A41,FINSEQ_3:29;
now let i be Nat;
assume 1 <= i & i <= len (S.n); then
i in Seg (len (S.n)) by FINSEQ_1:1; then
A43: i in dom (S.n) by FINSEQ_1:def 3;
consider t be Point of X such that
A44: t = (h|divset((T.n),i)).((F.n).i) &
(S.n).i = (vol divset((T.n),i)) * t by A43,A42,A38;
consider z be Point of X such that
A45: (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 A39,A43,A42;
consider w be Point of X such that
A46: (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 A40,A43,A42;
A47: (F.n).i in divset((T.n),i) by A46,RELAT_1:57;
A48: (F.n).i in dom g by A46,RELAT_1:57;
A49: (F.n).i in A by A46; then
A50: (F.n).i in dom h by FUNCT_2:def 1;
A51: (F.n).i in dom f by A49,FUNCT_2:def 1;
A52: f/.((F.n).i) = f.((F.n).i) by A51,PARTFUN1:def 6
.= z by A45,A47,FUNCT_1:49;
A53: g/.((F.n).i) = g.((F.n).i) by A48,PARTFUN1:def 6
.= w by A46,A47,FUNCT_1:49;
A54: t = (h|divset((T.n),i)).((F.n).i) by A44
.= h.((F.n).i) by A47,FUNCT_1:49
.= h/.((F.n).i) by A50,PARTFUN1:def 6
.= f/.((F.n).i) + g/.((F.n).i) by A50,A1,VFUNCT_1:def 1
.= z + w by A52,A53;
A55: (vol divset((T.n),i)) * z = (Sf.n).i by A45,A39
.= (Sf.n)/.i by A43,A42,PARTFUN1:def 6;
A56: (vol divset((T.n),i)) * w = (Sg.n).i by A46,A40
.= (Sg.n)/.i by A43,A42,PARTFUN1:def 6;
thus (S.n)/.i = (S.n).i by A43,PARTFUN1:def 6
.= (vol divset((T.n),i)) * t by A44
.= (vol divset((T.n),i)) * z + (vol divset((T.n),i)) * w
by A54,RLVECT_1:def 5
.= (Sf.n)/.i + (Sg.n)/.i by A55,A56;
end; then
A57: Sf.n + Sg.n = S.n by A42,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 A57,A41,Th1
.= middle_sum(h,S.n)
.= middle_sum(h,S).n by Def4;
end;
hence thesis by NORMSP_1:def 2;
end;
hence middle_sum(h,S) is convergent by A34,A35,NORMSP_1:19;
thus lim (middle_sum(h,S)) = integral(f) + integral(g)
by A34,A35,A36,NORMSP_1:25;
end;
hence h is integrable;
hence integral(h) = integral(f) + integral(g) by Def6,A3;
end;
theorem
for X be RealNormSpace,
A be non empty closed_interval Subset of REAL,
f, g, h be 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,
A be non empty closed_interval Subset of REAL,
f, g, h be Function of A,the carrier of X;
assume A1: h = f - g & f is integrable & g is integrable; 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;
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;
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;
pred f is_integrable_on A means
ex g be Function of A,the carrier of X st g = f|A & g is integrable;
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;
assume A1: A c= dom f;
func integral(f,A) -> Element of X means :Def8:
ex g be Function of A,the carrier of X st g = f|A & it = integral(g);
correctness
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 thesis;
end;
end;
theorem
for A be non empty closed_interval Subset of REAL,
f be PartFunc of REAL,the carrier of X,
g be Function of A,the carrier of X
st f|A = g holds f is_integrable_on A iff g is integrable;
theorem
for A be non empty closed_interval Subset of REAL,
f be PartFunc of REAL,the carrier of X,
g be 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:
for X, Y be non empty set,
V be RealNormSpace,
g, f be PartFunc of X,the carrier of V,
g1, f1 be 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,
V be RealNormSpace,
g, f be PartFunc of X,the carrier of V,
g1, f1 be PartFunc of Y,the carrier of V;
assume A1: g = g1 & f = f1;
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 be Element of Y st c in dom (g + f) holds
(g + f)/.c = g1/.c + f1/.c by A1,VFUNCT_1:def 1;
hence thesis by A3,A2,VFUNCT_1:def 1;
end;
theorem
for X, Y be non empty set,
V be RealNormSpace,
g, f be PartFunc of X,the carrier of V,
g1, f1 be 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,
V be RealNormSpace,
g, f be PartFunc of X,the carrier of V,
g1, f1 be PartFunc of Y,the carrier of V;
assume A1: g = g1 & f = f1;
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 be Element of Y st c in dom (g - f) holds
(g - f)/.c = g1/.c - f1/.c by A1,VFUNCT_1:def 2;
hence thesis by A3,A2,VFUNCT_1:def 2;
end;
theorem Th12:
for r be Real,
X, Y be non empty set,
V be RealNormSpace,
g be PartFunc of X,the carrier of V,
g1 be PartFunc of Y,the carrier of V
st g = g1 holds r(#)g1 = r(#)g
proof
let r be Real,
X, Y be non empty set,
V be RealNormSpace,
g be PartFunc of X,the carrier of V,
g1 be PartFunc of Y,the carrier of V;
assume A1: g = g1;
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 be Element of Y st c in dom (r(#)g) holds
(r(#)g)/.c = r * (g1/.c) by A1,VFUNCT_1:def 4;
hence thesis by A3,A2,VFUNCT_1:def 4;
end;
begin :: Linearity of the Integration Operator
theorem Th13:
for r be Real
for A be non empty closed_interval Subset of REAL
for f be 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 r be Real;
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 & f is_integrable_on A;
A2: A c= dom(r(#)f) by A1,VFUNCT_1:def 4;
consider g be Function of A,the carrier of X such that
A3: g = f|A & g is integrable by A1;
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;
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;
end;
theorem Th14:
for A be non empty closed_interval Subset of REAL,
f1, f2 be 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 A be non empty closed_interval Subset of REAL;
let f1, f2 be PartFunc of REAL,the carrier of X;
assume that
A1: f1 is_integrable_on A &
f2 is_integrable_on A and
A2: A c= dom f1 & A c= dom f2;
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 be Function of A,the carrier of X such that
A4: g1 = f1|A & g1 is integrable by A1;
consider g2 be Function of A,the carrier of X such that
A5: g2 = f2|A & g2 is integrable by A1;
(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;
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;
end;
theorem
for A be non empty closed_interval Subset of REAL,
f1, f2 be 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 A be non empty closed_interval Subset of REAL;
let f1, f2 be PartFunc of REAL,the carrier of X;
assume that
A1: f1 is_integrable_on A &
f2 is_integrable_on A and
A2: A c= dom f1 & A c= dom f2;
A3: f1 - f2 = f1 + -f2 by VFUNCT_1:25;
A4: dom (-f2) = dom f2 by VFUNCT_1:def 5;
A5: -f2 = (-jj)(#)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;
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) + (-jj) * 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;
end;
definition
let X be RealNormSpace;
let f be PartFunc of REAL,the carrier of X;
let a, b be Real;
func integral(f,a,b) -> Element of X equals :Def9:
integral(f,[' a,b ']) if a <= b otherwise -integral(f,[' b,a ']);
correctness;
end;
theorem Th16:
for f being PartFunc of REAL,the carrier of X,
A being non empty closed_interval Subset of REAL,
a, b be Real
st A = [.a,b.] holds integral(f,A) = integral(f,a,b)
proof
let f be PartFunc of REAL,the carrier of X;
let A be non empty closed_interval Subset of REAL;
let a, b be Real;
consider a1, b1 being Real such that
A1: a1 <= b1 and
A2: A = [.a1,b1.] by MEASURE5:14;
assume A = [.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 thesis by A1,A2,A3,INTEGRA5:def 3;
end;
theorem Th17:
for f being PartFunc of REAL,the carrier of X,
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 f being PartFunc of REAL,the carrier of X,
A being non empty closed_interval Subset of REAL;
assume A1: vol(A) = 0 & A c= dom f;
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,
S be 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 being DivSequence of A,
S be middle_volume_Sequence of g,T;
assume delta(T) is convergent & lim delta(T) = 0;
A3: for i be Nat holds middle_sum(g,S.i) = 0.X
proof
let i be Nat;
A4: len (S.i) = len (S.i);
now let k be Nat, v be Element of X;
assume A5: k in dom (S.i) & v = (S.i).k; 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 be 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,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;
end;
then Sum((S.i)) = -Sum((S.i)) by A4,RLVECT_1:40;
hence thesis by RLVECT_1:19;
end;
A9: for i be Nat holds (middle_sum(g,S)).i = 0.X
proof
let i be Nat;
thus (middle_sum(g,S)).i = middle_sum(g,S.i) by Def4
.= 0.X by A3;
end;
A10: for r be Real st 0 < r
ex m be Nat st for n be Nat
st m <= n holds ||.((middle_sum(g,S)).n) - 0.X.|| < r
proof
let r be Real;
assume A11: 0 < r;
take m = 0;
let n be Nat;
assume m <= n;
||.((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;
end;
hence (middle_sum(g,S)) is convergent by NORMSP_1:def 6;
hence lim (middle_sum(g,S)) = 0.X by A10,NORMSP_1:def 7;
end; then
A12: g is integrable;
hence f is_integrable_on A;
integral(g) = 0.X by A12,A2,Def6;
hence integral(f,A) = 0.X by Def8,A1;
end;
theorem
for f being PartFunc of REAL,the carrier of X,
A being non empty closed_interval Subset of REAL,
a, b be Real
st A = [.b,a.] & A c= dom f holds -integral(f,A) = integral(f,a,b)
proof
let f be PartFunc of REAL,the carrier of X;
let A be non empty closed_interval Subset of REAL;
let a, b be Real;
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; then
A4: a1 = b & b1 = a by A2,INTEGRA1:5;
now
per cases by A1,A4,XXREAL_0:1;
suppose
A5: b < a; then
integral(f,a,b) = -integral(f,[' b,a ']) by Def9;
hence thesis by A3,A5,INTEGRA5:def 3;
end;
suppose
A6: b = a;
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 thesis by A9,RLVECT_1:12;
end;
end;
hence thesis;
end;