:: Riemann Integral of Functions $\mathbbbR$ into $\mathbbbR^n$
:: by Keiichi Miyajima and Yasunari Shidama
::
:: Received May 5, 2009
:: Copyright (c) 2009-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 NUMBERS, INTEGRA1, SUBSET_1, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1,
MEASURE7, XBOOLE_0, XXREAL_2, XXREAL_0, SEQ_4, CARD_1, REAL_1, ARYTM_3,
ARYTM_1, CARD_3, FINSEQ_2, INTEGRA2, SEQ_1, SEQ_2, ORDINAL2, COMPLEX1,
XXREAL_1, FUNCT_3, REAL_NS1, STRUCT_0, PARTFUN1, VALUED_1, TARSKI,
PRE_TOPC, INTEGRA5, REALSET1, INTEGR15, VALUED_2, MEASURE5, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, XCMPLX_0,
COMPLEX1, XXREAL_2, NAT_1, FUNCT_1, FUNCT_2, STRUCT_0, REAL_1, RCOMP_1,
VALUED_1, RELSET_1, PARTFUN1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, FINSEQ_1,
FINSEQ_2, FINSEQOP, VALUED_2, RVSUM_1, PRE_TOPC, XXREAL_0, EUCLID,
PDIFF_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA5, NORMSP_0,
NORMSP_1, REAL_NS1;
constructors REAL_1, FINSEQOP, MONOID_0, SEQ_4, PSCOMP_1, NAT_D, VFUNCT_1,
PDIFF_1, BINOP_2, INTEGRA2, INTEGRA5, RELSET_1, SEQ_2, INTEGRA3,
VALUED_2, COMSEQ_2;
registrations NUMBERS, XREAL_0, SEQ_2, INTEGRA1, FUNCT_2, NAT_1, MEMBERED,
XXREAL_0, ORDINAL1, VALUED_0, VALUED_1, REAL_NS1, RELSET_1, EUCLID,
VALUED_2, CARD_1, MEASURE5, FINSEQ_1, FINSEQ_2, RELAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities XBOOLE_0, EUCLID, INTEGRA1, INTEGRA5;
expansions XBOOLE_0, INTEGRA5;
theorems XBOOLE_0, XBOOLE_1, XREAL_0, INTEGRA1, INTEGRA2, INTEGRA4, XXREAL_2,
XXREAL_0, RELAT_1, XCMPLX_1, PREPOWER, ORDINAL1, XREAL_1, RCOMP_1, SEQ_4,
SEQ_2, FINSEQ_1, FINSEQ_2, RVSUM_1, FUNCT_1, FUNCT_2, PARTFUN1, REAL_NS1,
INTEGRA5, PDIFF_1, INTEGRA6, VALUED_1, VALUED_2, RELSET_1, CARD_1,
TARSKI;
schemes SEQ_1, FUNCT_2, FINSEQ_1;
begin :: Preliminaries
reserve Z for set;
definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let D be Division of A;
mode middle_volume of f,D -> FinSequence of REAL means
:Def1:
len it = len D
& for i be Nat st i in dom D holds ex r be Element of REAL st r in rng (f|
divset(D,i)) & it.i=r*vol divset(D,i);
correctness
proof
defpred P1[ Nat, Real] means ex r be Element of REAL st r in
rng (f|divset(D,$1)) & $2=r*vol divset(D,$1);
A1: Seg len D = dom D by FINSEQ_1:def 3;
A2: for k being Nat st k in Seg len D holds ex x being Element of REAL st
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 r be object such that
A4: r in rng (f|divset(D,k));
reconsider r as Element of REAL by A4;
r*vol divset(D,k) is Element of REAL by XREAL_0:def 1;
hence thesis by A4;
end;
consider p being FinSequence of REAL such that
A5: dom p = Seg len D & for k being Nat st k in Seg len D holds 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;
Lm1: for A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, F be middle_volume of f,D, i be Nat st f|A is bounded_below & i
in dom D holds (lower_volume (f,D)).i <= F.i
proof
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, F be middle_volume of f,D, i be Nat;
assume that
A1: f|A is bounded_below and
A2: i in dom D;
A3: (lower_volume (f,D)).i = (lower_bound rng (f|divset(D,i)))*vol divset(D,i
) by A2,INTEGRA1:def 7;
consider r be Element of REAL such that
A4: r in rng (f|divset(D,i)) and
A5: F.i=r*vol divset(D,i) by A2,Def1;
rng f is bounded_below by A1,INTEGRA1:11;
then rng(f|divset(D,i)) is bounded_below by RELAT_1:70,XXREAL_2:44;
then
0 <= vol(divset (D,i)) & lower_bound (rng (f | (divset (D,i)))) <= r by A4,
INTEGRA1:9,SEQ_4:def 2;
hence (lower_volume (f,D)).i <= F.i by A5,A3,XREAL_1:64;
end;
Lm2: for A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, e be Real st f|A is bounded_below & 0 < e holds ex F be
middle_volume of f,D st for i be Nat st i in dom D holds (lower_volume (f,D)).i
<=F.i & F.i < (lower_volume (f,D)).i + e
proof
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, e be Real;
assume that
A1: f|A is bounded_below and
A2: 0 < e;
defpred P1[Nat, Real] means ex r be Element of REAL st r in rng (
f|divset(D,$1)) & $2=r*vol divset(D,$1) & (lower_volume (f,D)).$1 <= $2 & $2 <
(lower_volume (f,D)).$1 + e;
A3: for k being Nat st k in Seg len D holds ex x being Element of REAL st P1
[k,x]
proof
let k be Nat;
assume k in Seg len D;
then
A4: k in dom D by FINSEQ_1:def 3;
dom f = A by FUNCT_2:def 1;
then dom (f|divset(D,k)) = divset(D,k) by A4,INTEGRA1:8,RELAT_1:62;
then
A5: rng(f|divset(D,k)) is non empty by RELAT_1:42;
rng f is bounded_below by A1,INTEGRA1:11;
then
A6: rng(f|divset(D,k)) is bounded_below by RELAT_1:70,XXREAL_2:44;
per cases;
suppose
A7: vol divset(D,k) = 0;
consider r be object such that
A8: r in rng (f|divset(D,k)) by A5;
reconsider r as Element of REAL by A8;
reconsider x=r*vol divset(D,k) as Element of REAL by XREAL_0:def 1;
A9: (lower_volume (f,D)).k = (lower_bound rng (f|divset(D,k)))*vol
divset(D,k) by A4,INTEGRA1:def 7
.= 0 by A7;
then x < (lower_volume (f,D)).k + e by A2,A7;
hence ex x being Element of REAL st P1[k,x] by A7,A8,A9;
end;
suppose
A10: vol divset(D,k) <> 0;
set l=lower_bound rng (f|divset(D,k));
set e1=e/(vol divset(D,k));
A11: 0 < vol divset(D,k) by A10,INTEGRA1:9;
then 0 < e1 by A2,XREAL_1:139;
then consider r being Real such that
A12: r in rng (f|divset(D,k)) and
A13: r < l + e1 by A6,A5,SEQ_4:def 2;
A14: (lower_volume (f,D)).k = (lower_bound rng (f|divset(D,k)))*vol
divset(D,k) by A4,INTEGRA1:def 7;
reconsider x=r*vol divset(D,k) as Element of REAL by XREAL_0:def 1;
x < (l + e1)* (vol divset(D,k)) by A11,A13,XREAL_1:68;
then x < (lower_volume (f,D)).k + e1* (vol divset(D,k)) by A14;
then
A15: x < (lower_volume (f,D)).k + e by A10,XCMPLX_1:87;
l <= r by A6,A12,SEQ_4:def 2;
then (lower_volume (f,D)).k <= x by A11,A14,XREAL_1:64;
hence ex x being Element of REAL st P1[k,x] by A12,A15;
end;
end;
consider p being FinSequence of REAL such that
A16: dom p = Seg len D & for k being Nat st k in Seg len D holds P1[k,p
. k] from FINSEQ_1:sch 5(A3);
A17: now
let i be Nat;
assume i in dom D;
then i in Seg len D by FINSEQ_1:def 3;
then consider r be Element of REAL such that
A18: r in rng (f|divset(D,i)) & p.i=r*vol divset(D,i) and
(lower_volume (f,D)).i <= p.i and
p.i < (lower_volume (f,D)).i + e by A16;
take r;
thus r in rng (f|divset(D,i)) & p.i=r*vol divset(D,i) by A18;
end;
len p = len D by A16,FINSEQ_1:def 3;
then reconsider p as middle_volume of f,D by A17,Def1;
now
let i be Nat;
assume i in dom D;
then i in Seg len D by FINSEQ_1:def 3;
then ex r be Element of REAL st r in rng (f|divset(D,i)) & p.i =r*vol
divset(D,i) & (lower_volume (f,D)).i <= p.i & p.i < (lower_volume (f,D )).i + e
by A16;
hence (lower_volume (f,D)).i <= p.i & p.i < (lower_volume (f,D)).i + e;
end;
hence thesis;
end;
Lm3: for A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, e be Real st f|A is bounded_above & 0 < e holds ex F be
middle_volume of f,D st for i be Nat st i in dom D holds F.i <= (upper_volume (
f,D)).i & (upper_volume (f,D)).i - e < F.i
proof
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, e be Real;
assume that
A1: f|A is bounded_above and
A2: 0 < e;
defpred P1[ Nat, Real] means ex r be Element of REAL st r in rng
(f|divset(D,$1)) & $2=r*vol divset(D,$1) & $2 <= (upper_volume (f,D)).$1 & (
upper_volume (f,D)).$1 - e < $2;
A3: for k being Nat st k in Seg len D holds ex x being Element of REAL st P1
[k,x]
proof
let k being Nat;
assume k in Seg len D;
then
A4: k in dom D by FINSEQ_1:def 3;
dom f = A by FUNCT_2:def 1;
then dom (f|divset(D,k)) = divset(D,k) by A4,INTEGRA1:8,RELAT_1:62;
then
A5: rng(f|divset(D,k)) is non empty by RELAT_1:42;
rng f is bounded_above by A1,INTEGRA1:13;
then
A6: rng(f|divset(D,k)) is bounded_above by RELAT_1:70,XXREAL_2:43;
per cases;
suppose
A7: vol divset(D,k) = 0;
consider r be object such that
A8: r in rng (f|divset(D,k)) by A5;
reconsider r as Element of REAL by A8;
reconsider x=r*vol divset(D,k) as Element of REAL by XREAL_0:def 1;
A9: (upper_volume (f,D)).k = (upper_bound rng (f|divset(D,k)))*vol
divset(D,k) by A4,INTEGRA1:def 6
.= 0 by A7;
then (upper_volume (f,D)).k - e < x by A2,A7;
hence ex x being Element of REAL st P1[k,x] by A7,A8,A9;
end;
suppose
A10: vol divset(D,k) <> 0;
set l=upper_bound rng (f|divset(D,k));
set e1=e/(vol divset(D,k));
A11: 0 < vol divset(D,k) by A10,INTEGRA1:9;
then 0 < e1 by A2,XREAL_1:139;
then consider r being Real such that
A12: r in rng (f|divset(D,k)) and
A13: l - e1 < r by A6,A5,SEQ_4:def 1;
A14: (upper_volume (f,D)).k = (upper_bound rng (f|divset(D,k)))*vol
divset(D,k) by A4,INTEGRA1:def 6;
reconsider x=r*vol divset(D,k) as Element of REAL by XREAL_0:def 1;
(l - e1)* (vol divset(D,k)) < x by A11,A13,XREAL_1:68;
then (upper_volume (f,D)).k - e1* (vol divset(D,k)) < x by A14;
then
A15: (upper_volume (f,D)).k - e < x by A10,XCMPLX_1:87;
r <= l by A6,A12,SEQ_4:def 1;
then x <=(upper_volume (f,D)).k by A11,A14,XREAL_1:64;
hence ex x being Element of REAL st P1[k,x] by A12,A15;
end;
end;
consider p being FinSequence of REAL such that
A16: dom p = Seg len D & for k being Nat st k in Seg len D holds P1[k,p
. k] from FINSEQ_1:sch 5(A3);
A17: now
let i be Nat;
assume i in dom D;
then i in Seg len D by FINSEQ_1:def 3;
then consider r be Element of REAL such that
A18: r in rng (f|divset(D,i)) & p.i=r*vol divset(D,i) and
p.i <= (upper_volume (f,D)).i and
(upper_volume (f,D)).i - e < p.i by A16;
take r;
thus r in rng (f|divset(D,i)) & p.i=r*vol divset(D,i) by A18;
end;
len p = len D by A16,FINSEQ_1:def 3;
then reconsider p as middle_volume of f,D by A17,Def1;
now
let i be Nat;
assume i in dom D;
then i in Seg len D by FINSEQ_1:def 3;
then ex r be Element of REAL st r in rng (f|divset(D,i)) & p.i =r*vol
divset(D,i) & p.i<=(upper_volume (f,D)).i & (upper_volume (f,D)).i - e < p.i
by A16;
hence p.i<=(upper_volume (f,D)).i & (upper_volume (f,D)).i - e < p.i;
end;
hence thesis;
end;
Lm4: for A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, F be middle_volume of f,D, i be Nat st f|A is bounded_above & i
in dom D holds F.i <=(upper_volume (f,D)).i
proof
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, F be middle_volume of f,D, i be Nat;
assume that
A1: f|A is bounded_above and
A2: i in dom D;
A3: (upper_volume (f,D)).i = (upper_bound rng (f|divset(D,i)))*vol divset(D,i
) by A2,INTEGRA1:def 6;
consider r be Element of REAL such that
A4: r in rng (f|divset(D,i)) and
A5: F.i=r*vol divset(D,i) by A2,Def1;
rng f is bounded_above by A1,INTEGRA1:13;
then rng(f|divset(D,i)) is bounded_above by RELAT_1:70,XXREAL_2:43;
then
0 <= vol(divset (D,i)) & r <= upper_bound (rng (f | (divset (D,i)))) by A4,
INTEGRA1:9,SEQ_4:def 1;
hence F.i <= (upper_volume (f,D)).i by A5,A3,XREAL_1:64;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let D be Division of A;
let F be middle_volume of f,D;
func middle_sum(f,F) -> Real equals
Sum(F);
correctness;
end;
theorem Th1:
for A be non empty closed_interval Subset of REAL, f be Function of A,REAL,
D be Division of A, F be middle_volume of f,D st f|A is bounded_below holds
lower_sum (f,D) <= middle_sum(f,F)
proof
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, F be middle_volume of f,D;
len lower_volume (f,D) = len D by INTEGRA1:def 7;
then reconsider
p = lower_volume (f,D) as Element of (len D)-tuples_on REAL by FINSEQ_2:92;
len F = len D by Def1;
then reconsider q =F as Element of (len D)-tuples_on REAL by FINSEQ_2:92;
assume
A1: f|A is bounded_below;
now
let i be Nat;
assume i in Seg len D;
then i in dom D by FINSEQ_1:def 3;
hence p.i <= q.i by A1,Lm1;
end;
hence thesis by RVSUM_1:82;
end;
theorem Th2:
for A be non empty closed_interval Subset of REAL, f be Function of A,REAL,
D be Division of A, F be middle_volume of f,D st f|A is bounded_above holds
middle_sum(f,F) <= upper_sum (f,D)
proof
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, F be middle_volume of f,D;
len upper_volume (f,D) = len D by INTEGRA1:def 6;
then reconsider
p = upper_volume (f,D) as Element of (len D)-tuples_on REAL by FINSEQ_2:92;
len F = len D by Def1;
then reconsider q =F as Element of (len D)-tuples_on REAL by FINSEQ_2:92;
assume
A1: f|A is bounded_above;
now
let i be Nat;
assume i in Seg (len D);
then i in dom D by FINSEQ_1:def 3;
hence q.i <= p.i by A1,Lm4;
end;
hence thesis by RVSUM_1:82;
end;
theorem Th3:
for A be non empty closed_interval Subset of REAL, f be Function of A,REAL,
D be Division of A, e be Real st f|A is bounded_below & 0 < e holds ex F be
middle_volume of f,D st middle_sum(f,F) <= lower_sum (f,D) + e
proof
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, e be Real;
len lower_volume (f,D) = len D by INTEGRA1:def 7;
then reconsider
p = lower_volume (f,D) as Element of (len D)-tuples_on REAL by FINSEQ_2:92;
reconsider e1= e/(len D) as Element of REAL by XREAL_0:def 1;
assume f|A is bounded_below & 0 < e;
then consider F be middle_volume of f,D such that
A1: for i be Nat st i in dom D holds (lower_volume (f,D)).i <=F.i & F.i
< (lower_volume (f,D)).i + e1 by Lm2,XREAL_1:139;
set s= (len D) |-> e1;
reconsider t =p + s as Element of (len D)-tuples_on REAL;
take F;
len F = len D by Def1;
then reconsider q =F as Element of (len D)-tuples_on REAL by FINSEQ_2:92;
now
let i be Nat;
assume
A2: i in Seg (len D);
then i in dom D by FINSEQ_1:def 3;
then q.i <= p.i + e1 by A1;
then q.i <= p.i + s.i by A2,FINSEQ_2:57;
hence q.i <= t.i by RVSUM_1:11;
end;
then Sum(q) <= Sum(t) by RVSUM_1:82;
then Sum(q) <= Sum(p)+Sum(s) by RVSUM_1:89;
then Sum(q) <= Sum(p)+ (len D)*e1 by RVSUM_1:80;
hence thesis by XCMPLX_1:87;
end;
theorem Th4:
for A be non empty closed_interval Subset of REAL, f be Function of A,REAL,
D be Division of A, e be Real st f|A is bounded_above & 0 < e holds ex F be
middle_volume of f,D st upper_sum (f,D) - e <= middle_sum(f,F)
proof
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, D be
Division of A, e be Real;
len upper_volume (f,D) = len D by INTEGRA1:def 6;
then reconsider
p = upper_volume (f,D) as Element of (len D)-tuples_on REAL by FINSEQ_2:92;
reconsider e1= e/(len D) as Element of REAL by XREAL_0:def 1;
assume f|A is bounded_above & 0 < e;
then consider F be middle_volume of f,D such that
A1: for i be Nat st i in dom D holds F.i <= (upper_volume (f,D)).i & (
upper_volume (f,D)).i - e1 < F.i by Lm3,XREAL_1:139;
set s= (len D) |-> e1;
reconsider t =p - s as Element of (len D)-tuples_on REAL;
take F;
len F = len D by Def1;
then reconsider q =F as Element of (len D)-tuples_on REAL by FINSEQ_2:92;
now
let i be Nat;
assume
A2: i in Seg (len D);
then i in dom D by FINSEQ_1:def 3;
then p.i - e1 <= q.i by A1;
then p.i - s.i <= q.i by A2,FINSEQ_2:57;
hence t.i <= q.i by RVSUM_1:27;
end;
then Sum(t) <= Sum(q) by RVSUM_1:82;
then Sum(p)-Sum(s) <= Sum(q) by RVSUM_1:90;
then Sum(p)- (len D)*e1 <= Sum(q) by RVSUM_1:80;
hence thesis by XCMPLX_1:87;
end;
definition
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, T be
DivSequence of A;
mode middle_volume_Sequence of f,T -> sequence of (REAL)* 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 (REAL)* st P[x, y]
proof
let x being Element of NAT;
set y = the middle_volume of f,T.x;
reconsider y as Element of (REAL)* by FINSEQ_1:def 11;
y is middle_volume of f,T.x;
hence thesis;
end;
ex f being sequence of REAL* st for x being Element of NAT holds
P[x, f.x] from FUNCT_2:sch 3(A1);
hence thesis;
end;
end;
definition
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, T be
DivSequence of A, S be middle_volume_Sequence of f,T, k be Element of NAT;
redefine func S.k -> middle_volume of f,T.k; :: redefines . (FUNCT_1, definition)
coherence by Def3;
end;
definition
let A be non empty closed_interval Subset of REAL,
f be Function of A,REAL, T be
DivSequence of A, S be middle_volume_Sequence of f,T;
func middle_sum(f,S) -> Real_Sequence means
:Def4:
for i be Element of NAT holds it.i = middle_sum(f,S.i);
existence
proof
deffunc H1(Nat) = middle_sum(f,S.In($1,NAT));
consider IT being Real_Sequence such that
A1: for i being Nat holds IT . i
= H1(i) from SEQ_1:sch 1;
take IT;
let i be Element of NAT;
IT.i = H1(i) by A1;
hence thesis;
end;
uniqueness
proof
let F1, F2 be Real_Sequence;
assume that
A2: for i being Element of NAT holds F1.i = middle_sum(f,S.i) and
A3: for i being Element of NAT holds F2.i = middle_sum(f,S.i);
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;
theorem Th5:
for A be non empty closed_interval Subset of REAL, f being Function of A,
REAL, T being DivSequence of A, S be middle_volume_Sequence of f,T, i be
Element of NAT st f|A is bounded_below holds (lower_sum(f,T)).i <= (middle_sum(
f,S)).i
proof
let A be non empty closed_interval Subset of REAL,
f being Function of A,REAL, T being
DivSequence of A, S be middle_volume_Sequence of f,T, i be Element of NAT;
assume
A1: f|A is bounded_below;
(middle_sum(f,S)).i= middle_sum(f,S.i) & (lower_sum(f,T)).i = lower_sum(
f,T. i) by Def4,INTEGRA2:def 3;
hence thesis by A1,Th1;
end;
theorem Th6:
for A be non empty closed_interval Subset of REAL, f being Function of A,
REAL, T being DivSequence of A, S be middle_volume_Sequence of f,T, i be
Element of NAT st f|A is bounded_above holds (middle_sum(f,S)).i <= (upper_sum(
f,T)).i
proof
let A be non empty closed_interval Subset of REAL,
f being Function of A,REAL, T being
DivSequence of A, S be middle_volume_Sequence of f,T, i be Element of NAT;
assume
A1: f|A is bounded_above;
(middle_sum(f,S)).i= middle_sum(f,S.i) & (upper_sum(f,T)).i = upper_sum(
f,T. i) by Def4,INTEGRA2:def 2;
hence thesis by A1,Th2;
end;
theorem Th7:
for A be non empty closed_interval Subset of REAL, f being Function of A,
REAL, T being DivSequence of A, e be Element of REAL st 0 < e & f|A is
bounded_below holds ex S be middle_volume_Sequence of f,T st for i be Element
of NAT holds (middle_sum(f,S)).i <= (lower_sum(f,T)).i + e
proof
let A be non empty closed_interval Subset of REAL,
f being Function of A,REAL, T being
DivSequence of A, e be Element of REAL;
defpred P[Element of NAT,set ] means $2 is middle_volume of f,T.$1 & ex z be
middle_volume of f,T.$1 st z=$2 & middle_sum(f,z) <= lower_sum(f,T.$1) + e;
assume
A1: 0 < e & f|A is bounded_below;
A2: for x being Element of NAT ex y being Element of (REAL)* st P[x, y]
proof
let x be Element of NAT;
consider z be middle_volume of f,T.x such that
A3: middle_sum(f,z) <= lower_sum (f,T.x) + e by A1,Th3;
reconsider y=z as Element of (REAL)* by FINSEQ_1:def 11;
take y;
thus thesis by A3;
end;
consider F being sequence of (REAL)* such that
A4: for x being Element of NAT holds P[x, F.x] from FUNCT_2:sch 3(A2);
reconsider F as middle_volume_Sequence of f,T by A4,Def3;
now
let x being Element of NAT;
ex z be middle_volume of f,T.x st z=F.x & middle_sum(f,z) <= lower_sum
(f,T.x) + e by A4;
then (middle_sum(f,F)).x <= lower_sum(f,T.x) + e by Def4;
hence (middle_sum(f,F)).x <= (lower_sum(f,T)).x + e by INTEGRA2:def 3;
end;
hence thesis;
end;
theorem Th8:
for A be non empty closed_interval Subset of REAL, f being Function of A,
REAL, T being DivSequence of A, e be Element of REAL st 0 < e & f|A is
bounded_above holds ex S be middle_volume_Sequence of f,T st for i be Element
of NAT holds (upper_sum(f,T)).i - e <= (middle_sum(f,S)).i
proof
let A be non empty closed_interval Subset of REAL,
f being Function of A,REAL, T being
DivSequence of A, e be Element of REAL;
defpred P[Element of NAT,set ] means $2 is middle_volume of f,T.$1 & ex z be
middle_volume of f,T.$1 st z=$2 & upper_sum(f,T.$1) -e <= middle_sum(f,z);
assume
A1: 0 < e & f|A is bounded_above;
A2: for x being Element of NAT ex y being Element of (REAL)* st P[x, y]
proof
let x being Element of NAT;
consider z be middle_volume of f,T.x such that
A3: upper_sum (f,T.x) - e <= middle_sum(f,z) by A1,Th4;
reconsider y=z as Element of (REAL)* by FINSEQ_1:def 11;
take y;
thus thesis by A3;
end;
consider F being sequence of (REAL)* such that
A4: for x being Element of NAT holds P[x, F.x] from FUNCT_2:sch 3(A2);
reconsider F as middle_volume_Sequence of f,T by A4,Def3;
now
let x being Element of NAT;
ex z be middle_volume of f,T.x st z=F.x & upper_sum (f,T.x) - e <=
middle_sum(f,z) by A4;
then upper_sum(f,T.x) - e <= (middle_sum(f,F)).x by Def4;
hence (upper_sum(f,T)).x - e <=(middle_sum(f,F)).x by INTEGRA2:def 2;
end;
hence thesis;
end;
Lm5: for p,q,r be Real_Sequence st p is convergent & r is convergent & lim p =
lim r & (for i be Element of NAT holds p.i <= q.i) & (for i be Element of NAT
holds q.i <= r.i) holds q is convergent & lim p = lim q & lim r = lim q
proof
let p,q,r be Real_Sequence;
assume that
A1: p is convergent and
A2: r is convergent and
A3: lim p = lim r and
A4: for i be Element of NAT holds p.i <= q.i and
A5: for i be Element of NAT holds q.i <= r.i;
A6: now
let e be Real;
assume
A7: 0<e;
then consider n1 be Nat such that
A8: for m be Nat st n1<=m holds |.p.m-lim p.|<e by A1,SEQ_2:def 7;
consider n2 be Nat such that
A9: for m be Nat st n2<=m holds |.r.m-lim r.|<e by A2,A7,
SEQ_2:def 7;
reconsider n=max(n1,n2) as Nat by TARSKI:1;
take n;
thus for m be Nat st n<=m holds |.q.m-lim p.|<e
proof
let m be Nat;
assume
A10: n<=m;
A11: m in NAT by ORDINAL1:def 12;
n1 <=n by XXREAL_0:25;
then n1 <= m by A10,XXREAL_0:2;
then |.p.m-lim p.|<e by A8;
then p.m in ].lim p - e,lim p + e.[ by RCOMP_1:1;
then p.m in {z where z is Real: lim p - e<z & z<lim p + e } by
RCOMP_1:def 2;
then
A12: ex z be Real st z=p.m & lim p - e < z & z < lim p + e;
p.m <= q.m by A4,A11;
then
A13: lim p - e < q.m by A12,XXREAL_0:2;
n2 <=n by XXREAL_0:25;
then n2 <= m by A10,XXREAL_0:2;
then |.r.m-lim r.|<e by A9;
then r.m in ].lim r - e,lim r + e.[ by RCOMP_1:1;
then r.m in {z where z is Real: lim r - e<z & z<lim r + e } by
RCOMP_1:def 2;
then
A14: ex z be Real st z=r.m & lim r - e < z & z < lim r + e;
q.m <= r.m by A5,A11;
then q.m < lim p + e by A3,A14,XXREAL_0:2;
then q.m in {z where z is Real: lim p - e<z & z<lim p + e }
by A13;
then q.m in ].lim p - e,lim p + e.[ by RCOMP_1:def 2;
hence |.q.m-lim p.|<e by RCOMP_1:1;
end;
end;
hence q is convergent by SEQ_2:def 6;
hence lim q = lim p & lim q = lim r by A3,A6,SEQ_2:def 7;
end;
theorem Th9:
for A be non empty closed_interval Subset of REAL, f being Function of A,
REAL, T being DivSequence of A, S be middle_volume_Sequence of f,T st f is
bounded & f is integrable & delta(T) is convergent & lim delta(T)=0 holds
middle_sum(f,S) is convergent & lim (middle_sum(f,S))=integral(f)
proof
let A be non empty closed_interval Subset of REAL,
f being Function of A,REAL, T being
DivSequence of A, S be middle_volume_Sequence of f,T;
assume that
A1: f is bounded and
A2: f is integrable and
A3: delta(T) is convergent & lim delta(T)=0;
f|A is bounded_below by A1;
then
A5: for i be Element of NAT holds (lower_sum(f,T)).i <= (middle_sum(f,S)).i
by Th5;
A6: f|A= f;
then
A7: lower_sum(f,T) is convergent & upper_sum(f,T) is convergent by A1,A3,
INTEGRA4:8,9;
f|A is bounded_above by A1;
then
A8: for i be Element of NAT holds (middle_sum(f,S)).i <= (upper_sum(f,T)).i
by Th6;
A9: lim upper_sum(f,T)-lim lower_sum(f,T)=0 by A1,A2,A3,A6,INTEGRA4:12;
then lim lower_sum(f,T) = integral(f) by A1,A3,A6,INTEGRA4:9;
hence thesis by A7,A9,A5,A8,Lm5;
end;
theorem Th10:
for A be non empty closed_interval Subset of REAL, f being Function of A,
REAL st f is bounded holds f is integrable iff ex I be Real 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
proof
let A be non empty closed_interval Subset of REAL,
f being Function of A,REAL;
assume
A1: f is bounded;
hereby
assume
A2: f is integrable;
reconsider I=integral(f) as Real;
take I;
thus 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 by A1,A2,Th9;
end;
A3: f|A is bounded by A1;
now
given I be Real such that
A4: 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;
A5: for T being DivSequence of A st delta(T) is convergent & lim delta(T)
=0 holds lim upper_sum(f,T)= I
proof
let T being DivSequence of A;
set S = the middle_volume_Sequence of f,T;
A6: now
let i be Nat;
A7: i in NAT by ORDINAL1:def 12;
(middle_sum(f,S)).i <=(upper_sum(f,T)).i by A3,Th6,A7;
then
(middle_sum(f,S)).i - (middle_sum(f,S)).i <= (upper_sum(f,T)).i -
(middle_sum(f,S)).i by XREAL_1:9;
hence 0 <= ( upper_sum(f,T) - middle_sum(f,S)).i by VALUED_1:15,A7;
end;
assume
A8: delta(T) is convergent & lim delta(T)=0;
then
A9: upper_sum(f,T) is convergent by A3,INTEGRA4:9;
A10: now
let e1 be Real;
reconsider e=e1 as Element of REAL by XREAL_0:def 1;
assume 0 < e1;
then consider S be middle_volume_Sequence of f,T such that
A11: for i be Element of NAT holds (upper_sum(f,T)).i - e <=(
middle_sum(f,S)).i by A3,Th8;
A12: now
let i be Nat;
A13: i in NAT by ORDINAL1:def 12;
(upper_sum(f,T)).i - e <=(middle_sum(f,S)).i by A11,A13;
then (upper_sum(f,T)).i - e + e <=(middle_sum(f,S)).i + e by
XREAL_1:6;
then
(upper_sum(f,T)).i - (middle_sum(f,S)).i <= (middle_sum(f,S)).i
+ e - (middle_sum(f,S)).i by XREAL_1:9;
hence (upper_sum(f,T) - middle_sum(f,S) ).i <= e by VALUED_1:15,A13;
end;
A14: middle_sum(f,S) is convergent by A4,A8;
then
A15: upper_sum(f,T) - middle_sum(f,S) is convergent by A9;
lim (upper_sum(f,T) - middle_sum(f,S)) =lim (upper_sum(f,T))- lim
(middle_sum(f,S)) by A9,A14,SEQ_2:12
.=lim(upper_sum(f,T)) - I by A4,A8;
hence lim(upper_sum(f,T)) - I <= e1 by A12,A15,PREPOWER:2;
end;
A16: middle_sum(f,S) is convergent by A4,A8;
then
A17: upper_sum(f,T) - middle_sum(f,S) is convergent by A9;
lim (upper_sum(f,T) - middle_sum(f,S) ) = lim(upper_sum(f,T)) - lim
(middle_sum(f,S)) by A9,A16,SEQ_2:12
.= lim(upper_sum(f,T)) - I by A4,A8;
then 0 <= lim(upper_sum(f,T)) - I by A6,A17,SEQ_2:17;
then lim(upper_sum(f,T)) - I = 0 by A10,XREAL_1:5;
hence thesis;
end;
A18: for T being DivSequence of A st delta(T) is convergent & lim delta(T)=0
holds I = lim lower_sum(f,T)
proof
let T being DivSequence of A;
set S = the middle_volume_Sequence of f,T;
A19: now
let i be Nat;
A20: i in NAT by ORDINAL1:def 12;
(lower_sum(f,T)).i <= (middle_sum(f,S)).i by A3,Th5,A20;
then (lower_sum(f,T)).i - (lower_sum(f,T)).i <= (middle_sum(f,S)).i -
(lower_sum(f,T)).i by XREAL_1:9;
hence 0 <= (middle_sum(f,S) - lower_sum(f,T)).i by VALUED_1:15,A20;
end;
assume
A21: delta(T) is convergent & lim delta(T)=0;
then
A22: lower_sum(f,T) is convergent by A3,INTEGRA4:8;
A23: now
let e1 be Real;
reconsider e=e1 as Element of REAL by XREAL_0:def 1;
assume 0 < e1;
then consider S be middle_volume_Sequence of f,T such that
A24: for i be Element of NAT holds (middle_sum(f,S)).i <= (
lower_sum(f,T)).i + e by A3,Th7;
A25: now
let i be Nat;
A26: i in NAT by ORDINAL1:def 12;
(middle_sum(f,S)).i <= (lower_sum(f,T)).i + e by A24,A26;
then (middle_sum(f,S)).i - (lower_sum(f,T)).i <= (lower_sum(f,T)).i
+ e - (lower_sum(f,T)).i by XREAL_1:9;
hence (middle_sum(f,S) - lower_sum(f,T)).i <= e by VALUED_1:15,A26;
end;
A27: middle_sum(f,S) is convergent by A4,A21;
then
A28: middle_sum(f,S) - lower_sum(f,T) is convergent by A22;
lim (middle_sum(f,S) - lower_sum(f,T)) = lim (middle_sum(f,S))-
lim(lower_sum(f,T)) by A22,A27,SEQ_2:12
.= I -lim(lower_sum(f,T)) by A4,A21;
hence I -lim(lower_sum(f,T)) <= e1 by A25,A28,PREPOWER:2;
end;
A29: middle_sum(f,S) is convergent by A4,A21;
then
A30: middle_sum(f,S) - lower_sum(f,T) is convergent by A22;
lim (middle_sum(f,S) - lower_sum(f,T)) = lim (middle_sum(f,S))- lim
(lower_sum(f,T)) by A22,A29,SEQ_2:12
.= I -lim(lower_sum(f,T)) by A4,A21;
then 0 <= I -lim(lower_sum(f,T)) by A19,A30,SEQ_2:17;
then I-lim(lower_sum(f,T)) =0 by A23,XREAL_1:5;
hence thesis;
end;
now
let T being DivSequence of A;
assume
A31: delta(T) is convergent & lim delta(T)=0;
hence lim upper_sum(f,T)-lim lower_sum(f,T) =lim upper_sum(f,T)-I by A18
.=I-I by A5,A31
.=0;
end;
hence f is integrable by A3,INTEGRA4:12;
end;
hence thesis;
end;
definition
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL n;
let D be Division of A;
mode middle_volume of f,D -> FinSequence of (REAL n) means
:Def5:
len it =
len D & for i be Nat st i in dom D holds ex r be Element of (REAL n) st r in
rng (f|divset(D,i)) & it.i=vol divset(D,i)*r;
correctness
proof
defpred P1[ Nat, set ] means ex r be Element of (REAL n) st r in rng (f|
divset(D,$1)) & $2=vol divset(D,$1)*r;
A1: Seg len D = dom D by FINSEQ_1:def 3;
A2: for k being Nat st k in Seg len D holds ex x being Element of (REAL n)
st P1[k,x]
proof
let k being 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 r be object such that
A4: r in rng (f|divset(D,k));
reconsider r as Element of (REAL n) by A4;
(vol divset(D,k))*r is Element of (REAL n);
hence thesis by A4;
end;
consider p being FinSequence of (REAL n) such that
A5: dom p = Seg len D & for k being Nat st k in Seg len D holds 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 n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL n;
let D be Division of A;
let F be middle_volume of f,D;
func middle_sum(f,F) -> Element of (REAL n) means
:Def6:
for i be Element of
NAT st i in Seg n holds ex Fi be FinSequence of REAL st Fi=proj(i,n)*F & it.i =
Sum(Fi);
existence
proof
defpred P[Nat, Real] means ex i be Element of NAT, Fi be
FinSequence of REAL st $1 = i & Fi=proj(i,n)*F & $2 = Sum(Fi);
A1: for i be Nat st i in Seg n ex x being Element of REAL st P[i,x]
proof
let i be Nat;
assume i in Seg n;
then reconsider ii = i as Element of NAT;
reconsider Fi = proj(ii,n)*F as FinSequence of REAL;
reconsider x = Sum(Fi) as Element of REAL by XREAL_0:def 1;
take x;
thus ex ii be Element of NAT, Fi be FinSequence of REAL st i = ii & Fi=
proj(ii,n)*F & x = Sum(Fi);
end;
consider p being FinSequence of REAL such that
A2: dom p = Seg n & for i be Nat st i in Seg n holds P[i,p.i] from
FINSEQ_1:sch 5(A1);
take p;
A3: for i be Element of NAT st i in Seg n holds ex Fi be FinSequence of
REAL st Fi=proj(i,n)*F & p.i = Sum(Fi)
proof
let i be Element of NAT;
reconsider k=i as Nat;
assume i in Seg n;
then P[k,p.k] by A2;
hence thesis;
end;
len p = n by A2,FINSEQ_1:def 3;
hence thesis by A3,FINSEQ_2:92;
end;
uniqueness
proof
let x1, x2 be Element of REAL n such that
A4: (for i be Element of NAT st i in Seg n holds ex Fi1 be FinSequence
of REAL st Fi1=proj(i,n)*F & x1.i = Sum(Fi1))& for i be Element of NAT st i in
Seg n holds ex Fi2 be FinSequence of REAL st Fi2=proj(i,n)*F & x2.i = Sum(Fi2);
A5: for k0 be Nat st k0 in dom x1 holds x1.k0 = x2.k0
proof
let k0 be Nat;
assume
A6: k0 in dom x1;
then reconsider k=k0 as Element of NAT;
len x1= n by CARD_1:def 7;
then k0 in Seg n by A6,FINSEQ_1:def 3;
then
(ex Fi1 be FinSequence of REAL st Fi1=proj(k,n)*F & x1.k = Sum(Fi1)
)& ex Fi2 be FinSequence of REAL st Fi2=proj(k,n)*F & x2.k = Sum(Fi2) by A4;
hence thesis;
end;
A7: len x2= n by CARD_1:def 7;
len x1= n by CARD_1:def 7;
then dom x1 =Seg n by FINSEQ_1:def 3
.=dom x2 by A7,FINSEQ_1:def 3;
hence thesis by A5,FINSEQ_1:13;
end;
end;
definition
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL n;
let T be DivSequence of A;
mode middle_volume_Sequence of f,T -> sequence of (REAL n)* means
:Def7
:
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 (REAL n)* st P[x, y]
proof
let x being Element of NAT;
set y = the middle_volume of f,T.x;
reconsider y as Element of (REAL n)* by FINSEQ_1:def 11;
y is middle_volume of f,T.x;
hence thesis;
end;
ex f being sequence of (REAL n)* st for x being Element of NAT
holds P[x, f.x] from FUNCT_2:sch 3(A1);
hence thesis;
end;
end;
definition
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL n;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT;
redefine func S.k -> middle_volume of f,T.k; :: redefines . (FUNCT_1, definition)
coherence by Def7;
end;
definition
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL n;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
func middle_sum(f,S) -> sequence of (REAL-NS n) means
:Def8:
for i be Element of NAT holds it.i = middle_sum(f,S.i);
existence
proof
deffunc H1( Element of NAT ) = middle_sum(f,S.$1);
A1: (REAL n) = the carrier of (REAL-NS n) by REAL_NS1:def 4;
ex IT being sequence of (REAL n) st for i being Element of NAT holds IT
.i =H1(i) from FUNCT_2:sch 4;
hence thesis by A1;
end;
uniqueness
proof
let F1, F2 be sequence of (REAL-NS n);
assume that
A2: for i being Element of NAT holds F1.i = middle_sum(f,S.i) and
A3: for i being Element of NAT holds F2.i = middle_sum(f,S.i);
for i being Element of NAT holds F1.i = F2.i
proof
let i be Element of NAT;
thus F1.i = middle_sum(f,S.i) by A2
.= F2.i by A3;
end;
hence F1 = F2 by FUNCT_2:63;
end;
end;
definition
let n be Nat;
let Z be set;
let f,g be PartFunc of Z,REAL n;
func f+g -> PartFunc of Z, REAL n equals
f <++> g;
coherence
proof
set F = f<++>g;
rng F c= REAL n
proof
let y be object;
assume y in rng F;
then consider x being object such that
A1: x in dom F and
A2: F.x = y by FUNCT_1:def 3;
dom F = dom f /\ dom g by VALUED_2:def 45;
then x in dom f & x in dom g by A1,XBOOLE_0:def 4;
then
A3: f.x = f/.x & g.x = g/.x by PARTFUN1:def 6;
f/.x + g/.x in REAL n;
hence thesis by A2,A3,A1,VALUED_2:def 45;
end;
hence thesis by RELSET_1:6;
end;
func f-g -> PartFunc of Z, REAL n equals
f <--> g;
coherence
proof
set F = f<-->g;
rng F c= REAL n
proof
let y be object;
assume y in rng F;
then consider x being object such that
A4: x in dom F and
A5: F.x = y by FUNCT_1:def 3;
dom F = dom f /\ dom g by VALUED_2:def 46;
then x in dom f & x in dom g by A4,XBOOLE_0:def 4;
then
A6: f.x = f/.x & g.x = g/.x by PARTFUN1:def 6;
f/.x - g/.x in REAL n;
hence thesis by A5,A6,A4,VALUED_2:def 46;
end;
hence thesis by RELSET_1:6;
end;
end;
definition
let n be Nat;
let r be Real;
let Z be set;
let f be PartFunc of Z,REAL n;
func r(#)f -> PartFunc of Z, REAL n equals
f [#] r;
coherence
proof
set F = f[#]r;
rng F c= REAL n
proof
let y be object;
assume y in rng F;
then consider x being object such that
A1: x in dom F and
A2: F.x = y by FUNCT_1:def 3;
dom F = dom f by VALUED_2:def 39;
then
A3: f.x = f/.x by A1,PARTFUN1:def 6;
r * f/.x in REAL n;
hence thesis by A2,A3,A1,VALUED_2:def 39;
end;
hence thesis by RELSET_1:6;
end;
end;
begin :: Definition of Riemann Integral on Functions REAL to REAL n
definition
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL n;
attr f is bounded means
for i be Element of NAT st i in Seg n holds (proj(i,n)*f) is bounded;
end;
Lm6: for n,i be Element of NAT, f be PartFunc of REAL,REAL n, i be Element of
NAT, A be Subset of REAL holds proj(i,n)*(f|A) = (proj(i,n)*f)|A
proof
let n,i be Element of NAT, f be PartFunc of REAL,REAL n, i be Element of NAT
, A be Subset of REAL;
A1: dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then
A2: rng f c= dom(proj(i,n));
A3: rng (f|A) c= dom (proj(i,n)) by A1;
A4: now
let c be object;
assume
A5: c in dom ((proj(i,n)*f)|A);
then
A6: c in dom (proj(i,n)*f) /\ A by RELAT_1:61;
then
A7: c in A by XBOOLE_0:def 4;
A8: c in dom (proj(i,n)*f) by A6,XBOOLE_0:def 4;
then c in dom f by A2,RELAT_1:27;
then c in dom f /\ A by A7,XBOOLE_0:def 4;
then
A9: c in dom (f|A) by RELAT_1:61;
then c in dom (proj(i,n)*(f|A)) by A3,RELAT_1:27;
then (proj(i,n)*(f|A)).c = (proj(i,n)).((f|A).c) by FUNCT_1:12
.= (proj(i,n)).(f.c) by A9,FUNCT_1:47
.= (proj(i,n)*f).c by A8,FUNCT_1:12;
hence ((proj(i,n)*f)|A).c = (proj(i,n)*(f|A)).c by A5,FUNCT_1:47;
end;
dom ((proj(i,n)*f)|A) = dom (proj(i,n)*f) /\ A by RELAT_1:61
.= dom f /\ A by A2,RELAT_1:27
.= dom (f|A) by RELAT_1:61
.= dom (proj(i,n)*(f|A)) by A3,RELAT_1:27;
hence thesis by A4,FUNCT_1:2;
end;
definition
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL n;
attr f is integrable means
for i be Element of NAT st i in Seg n holds (proj(i,n)*f) is integrable;
end;
definition
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL n;
func integral(f) -> Element of REAL n means
:Def14:
dom it = Seg n & for i
be Element of NAT st i in Seg n holds it.i = integral((proj(i,n)*f));
existence
proof
defpred P[Nat, Real] means ex i be Element of NAT st $1 = i &
$2 = integral( (proj(i,n)*f) );
A1: for i be Nat st i in Seg n ex x being Element of REAL st P[i,x]
proof
let i be Nat;
assume i in Seg n;
then reconsider ii = i as Element of NAT;
reconsider x = integral( (proj(ii,n)*f)) as Element of REAL
by XREAL_0:def 1;
take x;
thus thesis;
end;
consider p being FinSequence of REAL such that
A2: dom p = Seg n & for i be Nat st i in Seg n holds P[i,p.i] from
FINSEQ_1:sch 5(A1);
take p;
A3: for i be Element of NAT st i in Seg n holds p.i = integral( (proj(i,n) *f))
proof
let i be Element of NAT;
assume i in Seg n;
then P[i,p.i] by A2;
hence thesis;
end;
len p = n by A2,FINSEQ_1:def 3;
hence thesis by A2,A3,FINSEQ_2:92;
end;
uniqueness
proof
let x1, x2 be Element of REAL n such that
A4: dom x1 = Seg n and
A5: for i be Element of NAT st i in Seg n holds x1.i = integral( (
proj( i,n)*f) ) and
A6: dom x2 = Seg n and
A7: for i be Element of NAT st i in Seg n holds x2.i = integral( (
proj( i,n)*f) );
now
let k be Nat;
assume
A8: k in dom x1;
then reconsider i=k as Element of NAT;
x1.i = integral( (proj(i,n)*f)) by A4,A5,A8
.= x2.i by A4,A7,A8;
hence x1.k = x2.k;
end;
hence thesis by A4,A6,FINSEQ_1:13;
end;
end;
theorem Th11:
for n be Element of NAT, A be non empty closed_interval Subset of REAL, f
being Function of A,REAL n, T being DivSequence of A, S be
middle_volume_Sequence of f,T st f is bounded & f is integrable & delta(T) is
convergent & lim delta(T)=0 holds middle_sum(f,S) is convergent & lim (
middle_sum(f,S))=integral(f)
proof
let n be Element of NAT, A be non empty closed_interval Subset of REAL,
f being
Function of A,REAL n, T being DivSequence of A, S be middle_volume_Sequence of
f,T;
assume that
A1: f is bounded & f is integrable and
A2: delta(T) is convergent & lim delta(T)=0;
set seq=middle_sum(f,S);
set xs=integral(f);
(REAL n) = the carrier of (REAL-NS n) by REAL_NS1:def 4;
then reconsider xseq=seq as sequence of REAL n;
A3: for i be Nat st i in Seg n ex rseqi be Real_Sequence st
for k be Nat holds rseqi.k = (xseq.k).i &
rseqi is convergent & xs.i = lim rseqi
proof
let i be Nat;
reconsider pjinf= (proj(i,n)*f) as Function of A,REAL;
defpred P[Element of NAT,set] means $2= proj(i,n)*(S.$1);
A4: for x being Element of NAT ex y being Element of (REAL)* st P[x, y]
proof
let x being Element of NAT;
proj(i,n)*(S.x) is Element of REAL* by FINSEQ_1:def 11;
hence thesis;
end;
consider F being sequence of (REAL)* such that
A5: for x being Element of NAT holds P[x, F.x] from FUNCT_2:sch 3(A4);
A6: for x being Element of NAT holds proj(i,n)*(S.x) is FinSequence of REAL
& dom(proj(i,n)*(S.x)) =Seg len(S.x) & rng(proj(i,n)*(S.x)) c= REAL
proof
let x being Element of NAT;
dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then rng (S.x) c= dom(proj(i,n));
then dom(proj(i,n)*(S.x)) = dom (S.x) by RELAT_1:27
.= Seg len(S.x) by FINSEQ_1:def 3;
hence thesis;
end;
for k be Element of NAT holds F.k is middle_volume of pjinf,T.k
proof
let k be Element of NAT;
reconsider Tk=T.k as FinSequence;
reconsider Fk=F.k as FinSequence of REAL;
A7: F.k= proj(i,n)*(S.k) by A5;
then
A8: dom (Fk) =Seg len(S.k) by A6
.=Seg len(Tk) by Def5;
then
A9: dom (Fk) = dom (Tk) by FINSEQ_1:def 3;
A10: now
let j be Nat;
dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then
A11: rng (f) c= dom(proj(i,n));
assume
A12: j in dom (Tk);
then consider r be Element of (REAL n) such that
A13: r in rng (f|divset((T.k),j)) and
A14: (S.k).j=vol divset((T.k),j)*r by Def5;
reconsider v=proj(i,n).r as Element of REAL;
take v;
consider t be object such that
A15: t in dom (f|divset((T.k),j)) and
A16: r=(f|divset((T.k),j)).t by A13,FUNCT_1:def 3;
t in dom(f) /\ divset((T.k),j) by A15,RELAT_1:61;
then t in dom(f) by XBOOLE_0:def 4;
then
A17: t in dom (proj(i,n)*f) by A11,RELAT_1:27;
A18: dom (f|divset((T.k),j)) =dom (f) /\ divset((T.k),j) by RELAT_1:61
.=dom (pjinf) /\ divset((T.k),j) by A11,RELAT_1:27
.=dom (pjinf|divset((T.k),j)) by RELAT_1:61;
proj(i,n).r = proj(i,n).(f.t) by A15,A16,FUNCT_1:47
.= (proj(i,n)*f).t by A17,FUNCT_1:12
.= (pjinf|divset((T.k),j)).t by A15,A18,FUNCT_1:47;
hence v in rng (pjinf|divset((T.k),j)) by A15,A18,FUNCT_1:3;
thus (Fk).j = proj(i,n).((S.k).j) by A7,A9,A12,FUNCT_1:12
.= (vol divset((T.k),j)*r).i by A14,PDIFF_1:def 1
.= vol divset((T.k),j) * (r.i) by RVSUM_1:44
.= v*vol divset((T.k),j) by PDIFF_1:def 1;
end;
len (Fk) = len(Tk) by A8,FINSEQ_1:def 3;
hence thesis by A10,Def1;
end;
then reconsider pjis = F as middle_volume_Sequence of pjinf,T by Def3;
reconsider rseqi = middle_sum(pjinf,pjis) as Real_Sequence;
assume
A19: i in Seg n;
A20: for k be Nat holds rseqi.k = (xseq.k).i
proof
let k be Nat;
reconsider k as Element of NAT by ORDINAL1:def 12;
A21: ex Fi be FinSequence of REAL st Fi=proj(i,n)*(S.k) &
(middle_sum(f,S.k)).i = Sum(Fi) by A19,Def6;
rseqi.k = middle_sum(pjinf,pjis.k) by Def4
.= (middle_sum(f,S.k)).i by A5,A21
.= (xseq.k).i by Def8;
hence thesis;
end;
take rseqi;
A22: (proj(i,n)*f) is bounded & pjinf is integrable by A1,A19;
then lim (middle_sum(pjinf,pjis))=integral(pjinf) by A2,Th9;
hence thesis by A2,A19,A22,A20,Def14,Th9;
end;
reconsider x=xs as Point of REAL-NS n by REAL_NS1:def 4;
xs = x;
hence thesis by A3,REAL_NS1:11;
end;
theorem
for n be Element of NAT, A be non empty closed_interval Subset of REAL,
f being
Function of A,REAL n st f is bounded holds f is integrable iff ex I be Element
of REAL n 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
proof
let n be Element of NAT, A be non empty closed_interval Subset of REAL,
f being
Function of A,REAL n;
assume
A1: f is bounded;
hereby
reconsider I=integral(f) as Element of REAL n;
assume
A2: f is integrable;
take I;
thus 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 by A1,A2,Th11;
end;
now
assume ex I be Element of REAL n 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;
then consider I be Element of REAL n such that
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))=I;
now
let i be Element of NAT;
reconsider Ii=I.i as Element of REAL by XREAL_0:def 1;
assume
A4: i in Seg n;
A5: now
set x=I;
let T being DivSequence of A, Si be middle_volume_Sequence of (proj(i,
n)*f) ,T;
defpred P[Element of NAT,set] means ex H be FinSequence,z be
FinSequence st H=T.$1 & z = $2 & len z = len H & for j be Element of NAT st j
in dom H holds ex rji be Element of REAL n, tji be Element of REAL st tji in
dom ( f|divset((T.$1),j) ) & (Si.$1).j = vol divset((T.$1),j)* (((proj(i,n)*f)|
divset((T.$1),j)).tji) & rji=(f|divset((T.$1),j)).tji & z.j =(vol divset((T.$1)
,j))* rji;
reconsider xs=x as Element of REAL n;
A6: for k being Element of NAT ex y being Element of (REAL n)* st P[k, y]
proof
let k being Element of NAT;
reconsider Tk=T.k as FinSequence;
defpred P1[Nat, set] means ex j be Element of NAT st $1 = j & ex rji
be Element of (REAL n), tji be Element of REAL st tji in dom ( f|divset((T.k),j
) ) & ((Si.k)).j = vol divset((T.k),j)* (((proj(i,n)*f)|divset((T.k),j)).tji) &
rji=(f|divset((T.k),j)).tji & $2=vol divset((T.k),j)*rji;
A7: for j be Nat st j in Seg len Tk ex x being Element of (REAL n)
st P1[j,x]
proof
dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then
A8: rng (f) c= dom(proj(i,n));
let j0 be Nat;
assume
A9: j0 in Seg len Tk;
then reconsider j = j0 as Element of NAT;
j in dom (Tk) by A9,FINSEQ_1:def 3;
then consider r be Element of REAL such that
A10: r in rng ((proj(i,n)*f)|divset((T.k),j)) and
A11: (Si.k).j=r * vol divset((T.k),j) by Def1;
consider tji be object such that
A12: tji in dom ((proj(i,n)*f)|divset((T.k),j)) and
A13: r=((proj(i,n)*f)|divset((T.k),j)).tji by A10,FUNCT_1:def 3;
tji in dom((proj(i,n)*f)) /\ divset((T.k),j) by A12,RELAT_1:61;
then reconsider tji as Element of REAL;
A14: dom (f|divset((T.k),j)) = dom (f) /\ divset((T.k),j) by RELAT_1:61
.= dom ((proj(i,n)*f)) /\ divset((T.k),j) by A8,RELAT_1:27
.= dom ((proj(i,n)*f)|divset((T.k),j)) by RELAT_1:61;
then
(f|divset((T.k),j)).tji in rng (f|divset((T.k),j)) by A12,FUNCT_1:3;
then reconsider rji=(f|divset((T.k),j)).tji as Element of REAL n;
reconsider x=vol divset((T.k),j)*rji as Element of REAL n;
take x;
thus P1[j0,x] by A11,A12,A13,A14;
end;
consider p being FinSequence of (REAL n ) such that
A15: dom p = Seg len Tk & for j be Nat st j in Seg len Tk holds
P1[j,p.j] from FINSEQ_1:sch 5(A7);
reconsider x=p as Element of (REAL n)* by FINSEQ_1:def 11;
take x;
A16: now
let jj0 be Element of NAT;
reconsider j0=jj0 as Nat;
A17: dom Tk = Seg len Tk by FINSEQ_1:def 3;
assume jj0 in dom Tk;
then P1[j0,p.j0] by A15,A17;
hence
ex rji be Element of REAL n, tji be Element of REAL st tji in
dom ( f|divset((T.k),jj0) ) & (Si.k).jj0 = vol divset((T.k),jj0)* (((proj(i,n)*
f)|divset((T.k),jj0)).tji) & rji=(f|divset((T.k),jj0)).tji & p.jj0 =(vol divset
((T.k),jj0))* rji;
end;
len p = len Tk by A15,FINSEQ_1:def 3;
hence P[k,x] by A16;
end;
consider S being sequence of (REAL n)* such that
A18: for x being Element of NAT holds P[x, S.x] from FUNCT_2:sch
3(A6);
for k be Element of NAT holds S.k is middle_volume of f,T.k
proof
let k be Element of NAT;
consider H be FinSequence,z be FinSequence such that
A19: H=T.k & z = S.k & len H = len z and
A20: for j be Element of NAT st j in dom H holds ex rji be
Element of REAL n, tji be Element of REAL st tji in dom ( f|divset((T.k),j) ) &
(Si.k).j = vol divset((T.k),j)* (((proj(i,n)*f)|divset((T.k),j)).tji) & rji=(f|
divset((T.k ),j)).tji & z.j =(vol divset((T.k),j))* rji by A18;
A21: now
let x be Nat;
assume
A22: x in dom H;
then reconsider j=x as Element of NAT;
consider rji be Element of REAL n, tji be Element of REAL such
that
A23: tji in dom ( f|divset((T.k),j) ) and
(Si.k).j = vol divset((T.k),j)* (((proj(i,n)*f)|divset((T.k),j
)). tji) and
A24: rji=(f|divset((T.k),j)).tji and
A25: z.j =(vol divset((T.k),j))* rji by A20,A22;
take rji;
thus rji in rng (f|divset((T.k),x)) by A23,A24,FUNCT_1:3;
thus z.x =(vol divset((T.k),x))* rji by A25;
end;
thus thesis by A19,A21,Def5;
end;
then reconsider S as middle_volume_Sequence of f,T by Def7;
set seq=middle_sum(f,S);
(REAL n) = the carrier of (REAL-NS n) by REAL_NS1:def 4;
then reconsider xseq=seq as sequence of REAL n;
assume delta(T) is convergent & lim delta(T)=0;
then seq is convergent & lim seq = x by A3;
then consider rseqi be Real_Sequence such that
A26: for k be Nat holds rseqi.k = (xseq.k).i & rseqi is
convergent & xs.i = lim rseqi by A4,REAL_NS1:11;
for k be Element of NAT holds rseqi.k = (middle_sum((proj(i,n)*f)
,Si)).k
proof
let k be Element of NAT;
consider H be FinSequence,z be FinSequence such that
A27: H=T.k and
A28: z = S.k and
A29: len H = len z and
A30: for j be Element of NAT st j in dom H holds ex rji be
Element of REAL n, tji be Element of REAL st tji in dom ( f|divset((T.k),j) ) &
(Si.k).j = vol divset((T.k),j)* (((proj(i,n)*f)|divset((T.k),j)).tji) & rji=(f|
divset((T.k ),j)).tji & z.j =(vol divset((T.k),j))* rji by A18;
dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then rng (S.k) c= dom(proj(i,n));
then
A31: dom(proj(i,n)*(S.k)) =dom (S.k) by RELAT_1:27
.=Seg len(H) by A28,A29,FINSEQ_1:def 3
.=Seg len(Si.k) by A27,Def1
.=dom (Si.k) by FINSEQ_1:def 3;
A32: for j be Nat st j in dom(proj(i,n)*(S.k)) holds (proj(i,n)*(S.k)
).j = (Si.k).j
proof
let j0 be Nat;
reconsider j=j0 as Element of NAT by ORDINAL1:def 12;
dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then
A33: rng (f) c= dom(proj(i,n));
assume
A34: j0 in dom(proj(i,n)*(S.k));
then j0 in Seg len(Si.k) by A31,FINSEQ_1:def 3;
then j0 in Seg len(H) by A27,Def1;
then j in dom H by FINSEQ_1:def 3;
then consider
rji be Element of REAL n, tji be Element of REAL such
that
A35: tji in dom ( f|divset((T.k),j) ) and
A36: (Si.k).j = vol divset((T.k),j)* (((proj(i,n)*f)|divset((T
.k),j)). tji) and
A37: rji=(f|divset((T.k),j)).tji and
A38: z.j =(vol divset((T.k),j))* rji by A30;
A39: dom (f|divset((T.k),j)) =dom (f) /\ divset((T.k),j) by RELAT_1:61
.=dom ((proj(i,n)*f)) /\ divset((T.k),j) by A33,RELAT_1:27
.= dom ((proj(i,n)*f)|divset((T.k),j)) by RELAT_1:61;
then tji in dom((proj(i,n)*f)) /\ divset((T.k),j) by A35,RELAT_1:61
;
then
A40: tji in dom((proj(i,n)*f)) by XBOOLE_0:def 4;
A41: ((proj(i,n)*f)|divset((T.k),j)).tji =(proj(i,n)*f).tji by A35,A39,
FUNCT_1:47
.= proj(i,n).(f.tji) by A40,FUNCT_1:12
.= proj(i,n).rji by A35,A37,FUNCT_1:47;
(proj(i,n)*(S.k)).j = proj(i,n).((S.k).j) by A34,FUNCT_1:12
.= (vol divset((T.k),j)*rji).i by A28,A38,PDIFF_1:def 1
.= vol divset((T.k),j) * (rji.i) by RVSUM_1:44
.= (Si.k).j by A36,A41,PDIFF_1:def 1;
hence thesis;
end;
consider Fi be FinSequence of REAL such that
A42: Fi=proj(i,n)*(S.k) and
A43: (middle_sum(f,S.k)).i = Sum(Fi) by A4,Def6;
thus rseqi.k = (xseq.k).i by A26
.=Sum(Fi) by A43,Def8
.=(middle_sum((proj(i,n)*f),Si.k)) by A31,A32,A42,FINSEQ_1:13
.=(middle_sum((proj(i,n)*f),Si)).k by Def4;
end;
hence middle_sum((proj(i,n)*f),Si) is convergent & lim (middle_sum((
proj(i,n)*f),Si))=Ii by A26,FUNCT_2:63;
end;
proj(i,n)*f is bounded by A1,A4;
hence (proj(i,n)*f) is integrable by A5,Th10;
end;
hence f is integrable;
end;
hence thesis;
end;
definition
let n be Element of NAT;
let f be PartFunc of REAL,REAL n;
attr f is bounded means
for i be Element of NAT st i in Seg n holds (proj(i,n)*f) is bounded;
end;
definition
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL n;
pred f is_integrable_on A means
for i be Element of NAT st i in Seg n holds (proj(i,n)*f) is_integrable_on A;
end;
definition
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL n;
func integral(f,A) -> Element of REAL n means
:Def17:
dom it = Seg n & for i
be Element of NAT st i in Seg n holds it.i = integral( (proj(i,n)*f), A);
existence
proof
defpred P[Nat, Real] means ex i be Element of NAT st $1 = i &
$2 = integral((proj(i,n)*f), A);
A1: for i be Nat st i in Seg n ex x being Element of REAL st P[i,x]
proof
let i be Nat;
assume i in Seg n;
then reconsider ii = i as Element of NAT;
reconsider x = integral( (proj(ii,n)*f), A) as Element of REAL
by XREAL_0:def 1;
take x;
thus thesis;
end;
consider p being FinSequence of REAL such that
A2: dom p = Seg n & for i be Nat st i in Seg n holds P[i,p.i] from
FINSEQ_1:sch 5(A1);
take p;
A3: for i be Element of NAT st i in Seg n holds p.i = integral( (proj(i,n)
*f), A)
proof
let i be Element of NAT;
assume i in Seg n;
then P[i,p.i] by A2;
hence thesis;
end;
len p = n by A2,FINSEQ_1:def 3;
hence thesis by A2,A3,FINSEQ_2:92;
end;
uniqueness
proof
let x1, x2 be Element of REAL n such that
A4: dom x1 = Seg n and
A5: for i be Element of NAT st i in Seg n holds x1.i = integral( (
proj( i,n)*f), A) and
A6: dom x2 = Seg n and
A7: for i be Element of NAT st i in Seg n holds x2.i = integral( (
proj( i,n)*f), A);
for k be Nat st k in dom x1 holds x1.k = x2.k
proof
let k be Nat;
assume
A8: k in dom x1;
then reconsider k as Element of NAT;
x2.k = integral( (proj(k,n)*f), A) by A4,A7,A8;
hence thesis by A4,A5,A8;
end;
hence thesis by A4,A6,FINSEQ_1:13;
end;
end;
theorem
for n be Element of NAT, A be non empty closed_interval Subset of REAL, f be
PartFunc of REAL,REAL n, g be Function of A,REAL n st f|A = g holds f
is_integrable_on A iff g is integrable
proof
let n be Element of NAT, A be non empty closed_interval Subset of REAL,
f be PartFunc
of REAL,REAL n, g be Function of A,REAL n;
assume
A1: f|A = g;
thus f is_integrable_on A implies g is integrable
proof
assume
A2: f is_integrable_on A;
for i be Element of NAT st i in Seg n holds (proj(i,n)*g) is integrable
proof
let i be Element of NAT;
dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then rng f c= dom(proj(i,n));
then
A3: dom(proj(i,n)*f) = dom f by RELAT_1:27;
A = dom g by FUNCT_2:def 1
.= dom f /\ A by A1,RELAT_1:61;
then (proj(i,n)*f)||A is total by A3,INTEGRA5:6,XBOOLE_1:17;
then reconsider F = (proj(i,n)*f)|A as Function of A,REAL;
assume i in Seg n;
then (proj(i,n)*f) is_integrable_on A by A2;
then F is integrable;
hence thesis by A1,Lm6;
end;
hence thesis;
end;
assume
A4: g is integrable;
for i be Element of NAT st i in Seg n holds (proj(i,n)*f) is_integrable_on A
proof
let i be Element of NAT;
assume
A5: i in Seg n;
proj(i,n)*g = (proj(i,n)*f)|A by A1,Lm6;
then (proj(i,n)*f)||A is integrable by A4,A5;
hence thesis;
end;
hence thesis;
end;
theorem
for n be Element of NAT, A be non empty closed_interval Subset of REAL, f be
PartFunc of REAL,REAL n, g be Function of A,REAL n st f|A = g holds
integral(f,A) = integral(g)
proof
let n be Element of NAT, A be non empty closed_interval Subset of REAL,
f be PartFunc
of REAL,REAL n, g be Function of A,REAL n;
assume
A1: f|A = g;
A2: now
let k be Nat;
assume
A3: k in dom (integral(f,A));
then reconsider i=k as Element of NAT;
dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then rng f c= dom(proj(i,n));
then
A4: dom(proj(i,n)*f) = dom f by RELAT_1:27;
A = dom g by FUNCT_2:def 1
.= dom f /\ A by A1,RELAT_1:61;
then (proj(i,n)*f)||A is total by A4,INTEGRA5:6,XBOOLE_1:17;
then reconsider F = (proj(i,n)*f)|A as Function of A,REAL;
A5: F = proj(i,n)*g by A1,Lm6;
A6: i in Seg n by A3,Def17;
then integral(f,A).i = integral((proj(i,n)*f), A) by Def17
.= integral((proj(i,n)*f)||A );
hence integral(f,A).k = (integral(g)).k by A6,A5,Def14;
end;
dom (integral(f,A)) = Seg n by Def17
.= dom (integral(g)) by Def14;
hence thesis by A2,FINSEQ_1:13;
end;
definition
let a,b be Real;
let n be Element of NAT;
let f be PartFunc of REAL, REAL n;
func integral(f,a,b) -> Element of REAL n means
:Def18:
dom it = Seg n & for
i be Element of NAT st i in Seg n holds it.i = integral( (proj(i,n)*f) ,a,b);
existence
proof
defpred P[Nat, Real] means ex i be Element of NAT st $1 = i &
$2 = integral((proj(i,n)*f), a,b);
A1: for i be Nat st i in Seg n ex x being Element of REAL st P[i,x]
proof
let i be Nat;
assume i in Seg n;
then reconsider ii = i as Element of NAT;
reconsider x = integral((proj(ii,n)*f), a,b) as Element of REAL
by XREAL_0:def 1;
take x;
thus thesis;
end;
consider p being FinSequence of REAL such that
A2: dom p = Seg n & for i be Nat st i in Seg n holds P[i,p.i] from
FINSEQ_1:sch 5(A1);
take p;
A3: for i be Element of NAT st i in Seg n holds p.i = integral( (proj(i,n)
*f), a,b)
proof
let i be Element of NAT;
assume i in Seg n;
then P[i,p.i] by A2;
hence thesis;
end;
len p = n by A2,FINSEQ_1:def 3;
hence thesis by A2,A3,FINSEQ_2:92;
end;
uniqueness
proof
let x1, x2 be Element of REAL n such that
A4: dom x1 = Seg n and
A5: for i be Element of NAT st i in Seg n holds x1.i = integral( (
proj( i,n)*f), a,b) and
A6: dom x2 = Seg n and
A7: for i be Element of NAT st i in Seg n holds x2.i = integral( (
proj( i,n)*f), a,b);
for k be Nat st k in dom x1 holds x1.k = x2.k
proof
let k be Nat;
assume
A8: k in dom x1;
then reconsider k as Element of NAT;
x2.k = integral( (proj(k,n)*f), a,b) by A4,A7,A8;
hence thesis by A4,A5,A8;
end;
hence thesis by A4,A6,FINSEQ_1:13;
end;
end;
begin :: Linearity of the Integration Operator
theorem Th15:
for n, i be Element of NAT, f1,f2 be PartFunc of Z, REAL n holds
proj(i,n)*(f1+f2) = proj(i,n)*f1 + proj(i,n)*f2 &
proj(i,n)*(f1-f2) = proj(i,n)*f1 - proj(i,n)*f2
proof
let n,i be Element of NAT;
let f1,f2 be PartFunc of Z, REAL n;
A1: dom(proj(i,n))= REAL n by FUNCT_2:def 1;
then rng f1 c= dom(proj(i,n));
then
A2: dom(proj(i,n)*f1) = dom f1 by RELAT_1:27;
A3: rng (f1+f2) c= dom(proj(i,n)) by A1;
then
A4: dom(proj(i,n)*(f1+f2)) = dom(f1+f2) by RELAT_1:27;
rng f2 c= dom(proj(i,n)) by A1;
then
A5: dom(proj(i,n)*f2) = dom f2 by RELAT_1:27;
A6: dom(f1+f2) = dom f1 /\ dom f2 by VALUED_2:def 45;
A7: for z being Element of Z st z in dom(proj(i,n)*(f1+f2)) holds (proj(
i,n)*(f1+f2)).z = (proj(i,n)*f1+proj(i,n)*f2).z
proof
let z be Element of Z;
reconsider f1z = f1/.z as Element of n-tuples_on REAL;
reconsider f2z = f2/.z as Element of n-tuples_on REAL;
assume
A8: z in dom(proj(i,n)*(f1+f2));
then
A9: z in dom(f1+f2) by A3,RELAT_1:27;
then
A10: z in dom f1 /\ dom f2 by VALUED_2:def 45;
then z in dom f1 by XBOOLE_0:def 4;
then
A11: f1.z = f1z by PARTFUN1:def 6;
z in dom f2 by A10,XBOOLE_0:def 4;
then
A12: f2.z = f2z by PARTFUN1:def 6;
proj(i,n).((f1+f2).z)=proj(i,n).(f1.z+f2.z) by A9,VALUED_2:def 45;
then proj(i,n).((f1+f2).z)= (f1/.z+f2/.z).i by A11,A12,PDIFF_1:def 1;
then
A13: proj(i,n).((f1+f2).z)= f1z.i + f2z.i by RVSUM_1:11;
A14: z in dom(proj(i,n)*f1) /\ dom(proj(i,n)*f2)
by A2,A5,A4,A8,VALUED_2:def 45;
then z in dom(proj(i,n)*f1) by XBOOLE_0:def 4;
then (proj(i,n)*f1).z = proj(i,n).(f1.z) by FUNCT_1:12;
then
A15: (proj(i,n)*f1).z = f1z.i by A11,PDIFF_1:def 1;
z in dom(proj(i,n)*f2) by A14,XBOOLE_0:def 4;
then (proj(i,n)*f2).z = proj(i,n).(f2.z) by FUNCT_1:12;
then
A16: (proj(i,n)*f2).z = f2z.i by A12,PDIFF_1:def 1;
z in dom(proj(i,n)*f1+proj(i,n)*f2) by A6,A2,A5,A4,A8,VALUED_1:def 1;
then (proj(i,n)*f1+proj(i,n)*f2).z = f1z.i + f2z.i by A15,A16,
VALUED_1:def 1;
hence thesis by A8,A13,FUNCT_1:12;
end;
dom(proj(i,n)*(f1+f2)) = dom(proj(i,n)*f1+proj(i,n)*f2) by A6,A2,A5,A4,
VALUED_1:def 1;
hence proj(i,n)*(f1+f2) = proj(i,n)*f1 + proj(i,n)*f2 by A7,PARTFUN1:5;
A17: rng (f1-f2) c= dom(proj(i,n)) by A1;
then
A18: dom(proj(i,n)*(f1-f2)) = dom(f1-f2) by RELAT_1:27;
A19: dom(f1-f2) = dom f1 /\ dom f2 by VALUED_2:def 46;
then
A20: dom(proj(i,n)*(f1-f2)) = dom(proj(i,n)*f1-proj(i,n)*f2) by A2,A5,A18,
VALUED_1:12;
for z being Element of Z st z in dom(proj(i,n)*(f1-f2)) holds (proj(
i,n)*(f1-f2)).z = (proj(i,n)*f1-proj(i,n)*f2).z
proof
let z being Element of Z;
reconsider f1z = f1/.z as Element of n-tuples_on REAL;
reconsider f2z = f2/.z as Element of n-tuples_on REAL;
assume
A21: z in dom(proj(i,n)*(f1-f2));
then
A22: z in dom(f1-f2) by A17,RELAT_1:27;
then
A23: z in dom f1 /\ dom f2 by VALUED_2:def 46;
then z in dom f1 by XBOOLE_0:def 4;
then
A24: f1.z = f1z by PARTFUN1:def 6;
z in dom f2 by A23,XBOOLE_0:def 4;
then
A25: f2.z = f2z by PARTFUN1:def 6;
z in dom(proj(i,n)*f2) by A5,A19,A18,A21,XBOOLE_0:def 4;
then (proj(i,n)*f2).z = proj(i,n).(f2.z) by FUNCT_1:12;
then
A26: (proj(i,n)*f2).z = f2z.i by A25,PDIFF_1:def 1;
proj(i,n).((f1-f2).z)=proj(i,n).(f1.z-f2.z) by A22,VALUED_2:def 46;
then proj(i,n).((f1-f2).z)= (f1/.z-f2/.z).i by A24,A25,PDIFF_1:def 1;
then
A27: proj(i,n).((f1-f2).z)= f1z.i - f2z.i by RVSUM_1:27;
z in dom(proj(i,n)*f1) by A2,A19,A18,A21,XBOOLE_0:def 4;
then (proj(i,n)*f1).z = proj(i,n).(f1.z) by FUNCT_1:12;
then
A28: (proj(i,n)*f1).z = f1z.i by A24,PDIFF_1:def 1;
(proj(i,n)*f1-proj(i,n)*f2).z = (proj(i,n)*f1).z - (proj(i,n)*f2).z
by A20,A21,VALUED_1:13;
hence thesis by A21,A27,A28,A26,FUNCT_1:12;
end;
hence thesis by A20,PARTFUN1:5;
end;
theorem Th16:
for n,i be Element of NAT, r be Real, f be PartFunc of Z, REAL n
holds proj(i,n)*(r(#)f) = r(#)(proj(i,n)*f)
proof
let n,i be Element of NAT;
let r be Real;
let f be PartFunc of Z, REAL n;
A1: dom (r(#)f) = dom f by VALUED_2:def 39;
A2: dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then
A3: rng (r(#)f) c= dom(proj(i,n));
rng f c= dom(proj(i,n)) by A2;
then
A4: dom(proj(i,n)*f) = dom f by RELAT_1:27;
then dom(r(#)(proj(i,n)*f)) = dom f by VALUED_1:def 5;
then
A5: dom((proj(i,n))*(r(#)f)) = dom(r(#)(proj(i,n)*f)) by A1,A3,RELAT_1:27;
for z being Element of Z st z in dom (r(#)(proj(i,n)*f)) holds (proj(
i,n)*(r(#)f)).z = (r(#)(proj(i,n)*f)).z
proof
let z be Element of Z;
reconsider fz = f/.z as Element of n-tuples_on REAL;
reconsider rfz = (r(#)f)/.z as Element of n-tuples_on REAL;
assume
A6: z in dom (r(#)(proj(i,n)*f));
then
A7: z in dom (proj(i,n)*f) by VALUED_1:def 5;
then
A8: f.z = fz by A4,PARTFUN1:def 6;
(r(#)(proj(i,n)*f)).z = r * (proj(i,n)*f).z by A6,VALUED_1:def 5
.= r * ((proj(i,n)).(fz)) by A7,A8,FUNCT_1:12;
then
A9: (r(#)(proj(i,n)*f)).z = r * fz.i by PDIFF_1:def 1;
A10: ((r(#)f).z) = rfz by A1,A4,A7,PARTFUN1:def 6;
thus (proj(i,n)*(r(#)f)).z = (proj(i,n)).((r(#)f).z) by A5,A6,FUNCT_1:12
.= (rfz).i by A10,PDIFF_1:def 1
.= (r (#) fz).i by A1,A4,A7,A8,A10,VALUED_2:def 39
.= (r(#)(proj(i,n)*f)).z by A9,RVSUM_1:44;
end;
hence thesis by A5,PARTFUN1:5;
end;
theorem
for n be Element of NAT for A be non empty closed_interval Subset of REAL
for f1
,f2 be PartFunc of REAL, REAL n st f1 is_integrable_on A & f2 is_integrable_on
A & A c= dom f1 & A c= dom f2 & (f1|A) is bounded & (f2|A) is bounded holds f1+
f2 is_integrable_on A & f1-f2 is_integrable_on A & integral(f1+f2,A)=integral(
f1,A)+integral(f2,A) & integral(f1-f2,A)=integral(f1,A)-integral(f2,A)
proof
let n be Element of NAT;
let A be non empty closed_interval Subset of REAL;
let f1,f2 be PartFunc of REAL, REAL n;
assume that
A1: f1 is_integrable_on A & f2 is_integrable_on A and
A2: A c= dom f1 & A c= dom f2 and
A3: f1|A is bounded and
A4: f2|A is bounded;
A5: for i be Element of NAT st i in Seg n holds A c= dom (proj(i,n)*f1) & A
c= dom (proj(i,n)*f2)
proof
let i be Element of NAT;
assume i in Seg n;
dom proj(i,n) = REAL n by FUNCT_2:def 1;
then rng f1 c= dom proj(i,n) & rng f2 c= dom proj(i,n);
hence thesis by A2,RELAT_1:27;
end;
A6: for i be Element of NAT st i in Seg n holds proj(i,n)*f1 + proj(i,n)*f2
is_integrable_on A & integral(proj(i,n)*f1+proj(i,n)*f2,A) = integral(proj(i,n)
*f1,A) + integral(proj(i,n)*f2,A) & proj(i,n)*f1 - proj(i,n)*f2
is_integrable_on A & integral(proj(i,n)*f1-proj(i,n)*f2,A) = integral(proj(i,n)
*f1,A) - integral(proj(i,n)*f2,A)
proof
let i be Element of NAT;
assume
A7: i in Seg n;
then
A8: A c= dom (proj(i,n)*f1) & A c= dom (proj(i,n)*f2) by A5;
proj(i,n)*(f2|A) is bounded by A4,A7;
then
A9: (proj(i,n)*f2)|A is bounded by Lm6;
proj(i,n)*(f1|A) is bounded by A3,A7;
then
A10: (proj(i,n)*f1)|A is bounded by Lm6;
A11: proj(i,n)*f1 is_integrable_on A & proj(i,n)*f2 is_integrable_on A by A1,A7
;
hence proj(i,n)*f1 + proj(i,n)*f2 is_integrable_on A & integral(proj(i,n)*
f1+proj(i,n)*f2,A) = integral(proj(i,n)*f1,A) + integral(proj(i,n)*f2,A) by A8
,A10,A9,INTEGRA6:11;
thus proj(i,n)*f1 - proj(i,n)*f2 is_integrable_on A & integral(proj(i,n)*
f1-proj(i,n)*f2,A) = integral(proj(i,n)*f1,A) - integral(proj(i,n)*f2,A) by A8
,A10,A9,A11,INTEGRA6:11;
end;
A12: for i be Element of NAT st i in Seg n holds proj(i,n)*(f1+f2)
is_integrable_on A & proj(i,n)*(f1-f2) is_integrable_on A
proof
let i be Element of NAT;
assume i in Seg n;
then
(proj(i,n)*f1+proj(i,n)*f2) is_integrable_on A & (proj(i,n)*f1-proj(i
,n)*f2) is_integrable_on A by A6;
hence thesis by Th15;
end;
then for i be Element of NAT st i in Seg n holds proj(i,n)*(f1+f2)
is_integrable_on A;
hence f1+f2 is_integrable_on A;
A13: for i be Element of NAT st i in Seg n holds integral(f1,A).i + integral
(f2,A).i =integral((proj(i,n)*f1),A) + integral((proj(i,n)*f2),A) & integral(f1
,A).i - integral(f2,A).i =integral((proj(i,n)*f1),A) - integral((proj(i,n)*f2),
A)
proof
let i be Element of NAT;
assume
A14: i in Seg n;
then integral(f1,A).i = integral((proj(i,n)*f1),A) by Def17;
hence thesis by A14,Def17;
end;
A15: for i be Element of NAT st i in Seg n holds integral(f1,A).i + integral
(f2,A).i = integral(proj(i,n)*f1+proj(i,n)*f2,A) & integral(f1,A).i - integral(
f2,A).i = integral(proj(i,n)*f1-proj(i,n)*f2,A)
proof
let i be Element of NAT;
assume
A16: i in Seg n;
then integral(f1,A).i + integral(f2,A).i =integral((proj(i,n)*f1),A) +
integral(( proj(i,n)*f2),A) & integral(f1,A).i - integral(f2,A).i =integral((
proj(i,n)*f1 ),A) - integral((proj(i,n)*f2),A) by A13;
hence thesis by A6,A16;
end;
A17: for i be Element of NAT st i in Seg n holds integral(f1,A).i + integral
(f2,A).i = integral(proj(i,n)*(f1+f2),A) & integral(f1,A).i - integral(f2,A).i
= integral(proj(i,n)*(f1-f2),A)
proof
let i be Element of NAT;
assume i in Seg n;
then
integral(f1,A).i + integral(f2,A).i = integral(proj(i,n)*f1+proj(i,n)
* f2,A) & integral(f1,A).i - integral(f2,A).i = integral(proj(i,n)*f1-proj(i,n)
* f2,A) by A15;
hence thesis by Th15;
end;
A18: for i be Element of NAT st i in Seg n holds integral(f1+f2,A).i =
integral(f1,A).i + integral(f2,A).i & integral(f1-f2,A).i = integral(f1,A).i -
integral(f2,A).i
proof
let i be Element of NAT;
assume
A19: i in Seg n;
then
integral(f1,A).i + integral(f2,A).i = integral(proj(i,n)*(f1+f2),A) &
integral(f1,A).i - integral(f2,A).i = integral(proj(i,n)*(f1-f2),A) by A17;
hence thesis by A19,Def17;
end;
for i be Element of NAT st i in Seg n holds proj(i,n)*(f1-f2)
is_integrable_on A by A12;
hence f1-f2 is_integrable_on A;
A20: dom(integral(f1+f2,A)) = Seg n by FINSEQ_1:89;
A21: for i be Element of NAT st i in dom (integral(f1+f2,A)) holds (integral
(f1+f2,A)).i = (integral(f1,A) + integral(f2,A)).i
proof
let i be Element of NAT;
assume i in dom (integral(f1+f2,A));
then
integral(f1+f2,A).i = integral(f1,A).i + integral(f2,A).i by A18,A20;
hence thesis by RVSUM_1:11;
end;
dom(integral(f1,A) + integral(f2,A)) = Seg n by FINSEQ_1:89;
hence integral(f1+f2,A) = integral(f1,A)+integral(f2,A) by A21,FINSEQ_1:89
,PARTFUN1:5;
A22: dom(integral(f1-f2,A)) = Seg n by FINSEQ_1:89;
A23: for i be Element of NAT st i in dom (integral(f1-f2,A)) holds (integral
(f1-f2,A)).i = (integral(f1,A) - integral(f2,A)).i
proof
let i be Element of NAT;
assume i in dom (integral(f1-f2,A));
then
integral(f1-f2,A).i = integral(f1,A).i - integral(f2,A).i by A18,A22;
hence thesis by RVSUM_1:27;
end;
dom(integral(f1,A) - integral(f2,A)) = Seg n by FINSEQ_1:89;
hence thesis by A23,FINSEQ_1:89,PARTFUN1:5;
end;
theorem
for n be Element of NAT for r be Real
for A be non empty closed_interval Subset
of REAL for f be PartFunc of REAL, REAL n st A c= dom f & f is_integrable_on A
& f|A is bounded holds r(#)f is_integrable_on A & integral( (r(#)f) ,A) = r*
integral(f,A)
proof
let n be Element of NAT;
let r be Real;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL, REAL n;
assume that
A1: A c= dom f and
A2: f is_integrable_on A and
A3: f|A is bounded;
A4: now
let i be Element of NAT;
dom proj(i,n) = REAL n by FUNCT_2:def 1;
then rng f c= dom proj(i,n);
hence A c= dom (proj(i,n)*f) by A1,RELAT_1:27;
end;
A5: for i be Element of NAT st i in Seg n holds integral(r(#)(proj(i,n)*f),
A)=r*integral((proj(i,n)*f), A)
proof
let i be Element of NAT;
assume
A6: i in Seg n;
(proj(i,n)*f)|A = proj(i,n)*(f|A) by Lm6;
then
A7: (proj(i,n)*f)|A is bounded by A3,A6;
A8: A c= dom (proj(i,n)*f) by A4;
(proj(i,n)*f) is_integrable_on A by A2,A6;
hence thesis by A7,A8,INTEGRA6:9;
end;
A9: for i be Element of NAT st i in Seg n holds (r*integral(f,A)).i = r*
integral((proj(i,n)*f ),A)
proof
let i be Element of NAT;
assume i in Seg n;
then r*integral(f,A).i = r*integral((proj(i,n)*f ),A) by Def17;
hence thesis by RVSUM_1:45;
end;
A10: for i be Element of NAT st i in Seg n holds integral((r(#)f), A).i = (r*
integral(f,A)).i
proof
let i be Element of NAT;
A11: integral(r(#)(proj(i,n)*f),A)=integral((proj(i,n)*(r(#)f)),A) by Th16;
assume
A12: i in Seg n;
then
integral((r(#)f),A).i = integral((proj(i,n)*(r(#)f)),A) & (r*integral
(f,A)).i = r*integral((proj(i,n)*f ),A) by A9,Def17;
hence thesis by A5,A12,A11;
end;
for i be Element of NAT st i in Seg n holds (proj(i,n)*(r(#)f) )
is_integrable_on A
proof
let i be Element of NAT;
assume
A13: i in Seg n;
(proj(i,n)*f)|A = proj(i,n)*(f|A) by Lm6;
then
A14: (proj(i,n)*f)|A is bounded by A3,A13;
A15: A c= dom (proj(i,n)*f) by A4;
(proj(i,n)*f ) is_integrable_on A by A2,A13;
then r(#)(proj(i,n)*f ) is_integrable_on A by A14,A15,INTEGRA6:9;
hence thesis by Th16;
end;
hence r(#)f is_integrable_on A;
A16: dom(integral((r(#)f),A)) = Seg n by FINSEQ_1:89;
then dom(integral((r(#)f),A)) = dom(r*integral(f,A)) by FINSEQ_1:89;
hence thesis by A10,A16,PARTFUN1:5;
end;
theorem
for n be Element of NAT for f being PartFunc of REAL,REAL n, 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 n be Element of NAT;
let f being PartFunc of REAL,REAL n,
A being non empty closed_interval Subset of REAL,
a,b be Real;
assume
A1: A=[.a,b.];
A2: now
let i be Nat;
assume
A3: i in dom (integral(f,A));
then reconsider k=i as Element of NAT;
dom (integral(f,A)) = Seg n by Def17;
then integral(f,A).k = integral((proj(k,n)*f),A) & integral(f,a,b).k =
integral(( proj(k,n)*f), a,b) by A3,Def17,Def18;
hence integral(f,A).i = integral(f,a,b).i by A1,INTEGRA5:19;
end;
dom (integral(f,A)) = Seg n by Def17
.= dom (integral(f,a,b)) by Def18;
hence integral(f,A)=integral(f,a,b) by A2,FINSEQ_1:13;
end;
theorem
for n be Element of NAT for f being PartFunc of REAL,REAL n, A being
non empty closed_interval Subset of REAL, a,b be Real st A=[.b,a.]
holds -integral(f,A) = integral(f,a,b)
proof
let n be Element of NAT;
let f being PartFunc of REAL,REAL n,
A being non empty closed_interval Subset of REAL,
a,b be Real;
assume
A1: A=[.b,a.];
A2: now
let i be Nat;
assume
A3: i in dom (-integral(f,A));
then reconsider k=i as Element of NAT;
A4: dom (integral(f,A))= Seg n by Def17;
A5: k in dom (integral(f,A)) by A3,VALUED_1:8;
then
A6: integral(f,a,b).k = integral((proj(k,n)*f), a,b) by A4,Def18;
(-integral(f,A)).k =-((integral(f,A)).k) by VALUED_1:8
.=-integral((proj(k,n)*f),A) by A5,A4,Def17;
hence (-integral(f,A)).i = integral(f,a,b).i by A1,A6,INTEGRA5:20;
end;
reconsider jj=1 as Real;
dom (-integral(f,A)) = dom ((-jj)(#)integral(f,A)) by VALUED_1:def 6
.= dom (integral(f,A)) by VALUED_1:def 5
.= Seg n by Def17
.= dom (integral(f,a,b)) by Def18;
hence thesis by A2,FINSEQ_1:13;
end;
theorem
for n being Nat, Z,x being set, f,g being PartFunc of Z,REAL n
st x in dom (f+g) holds (f+g)/.x = (f/.x) + (g/.x)
proof
let n be Nat;
let Z,x be set;
let f,g be PartFunc of Z,REAL n;
assume
A1: x in dom (f+g);
dom(f+g) = dom f /\ dom g by VALUED_2:def 45;
then x in dom f & x in dom g by A1,XBOOLE_0:def 4;
then
A2: f.x = f/.x & g.x = g/.x by PARTFUN1:def 6;
thus (f+g)/.x = (f+g).x by A1,PARTFUN1:def 6
.= (f/.x) + (g/.x) by A1,A2,VALUED_2:def 45;
end;
theorem
for n being Nat, Z,x being set, f,g being PartFunc of Z,REAL n
st x in dom (f-g) holds (f-g)/.x = (f/.x) - (g/.x)
proof
let n be Nat;
let Z,x be set;
let f,g be PartFunc of Z,REAL n;
assume
A1: x in dom (f-g);
dom(f-g) = dom f /\ dom g by VALUED_2:def 46;
then x in dom f & x in dom g by A1,XBOOLE_0:def 4;
then
A2: f.x = f/.x & g.x = g/.x by PARTFUN1:def 6;
thus (f-g)/.x = (f-g).x by A1,PARTFUN1:def 6
.= (f/.x) - (g/.x) by A1,A2,VALUED_2:def 46;
end;
theorem
for n being Nat, Z,x being set, f being PartFunc of Z,REAL n
for r being Real
st x in dom (r(#)f) holds (r(#)f)/.x = r* (f/.x)
proof
let n be Nat;
let Z,x be set;
let f be PartFunc of Z,REAL n;
let r be Real;
assume
A1: x in dom (r(#)f);
dom (r(#)f) = dom f by VALUED_2:def 39;
then
A2: f.x = f/.x by A1,PARTFUN1:def 6;
thus (r(#)f)/.x = (r(#)f).x by A1,PARTFUN1:def 6
.= r * (f/.x) by A1,A2,VALUED_2:def 39;
end;