:: Riemann Integral of Functions $\mathbbbR$ into $\mathbbbR^n$
:: by Keiichi Miyajima and Yasunari Shidama
::
:: Received May 5, 2009
:: Copyright (c) 2009 Association of Mizar Users

definition

let A be 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 :defx0: :: INTEGR15:def 1
( len it = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset D,i)) & it . i = r * (vol (divset D,i)) ) ) );
correctness
existence
ex b₁ being FinSequence of REAL st
( len b₁ = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset D,i)) & b₁ . i = r * (vol (divset D,i)) ) ) );

proof end;

end;

:: deftheorem defx0 defines middle_volume INTEGR15:def 1 :

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for b₄ being FinSequence of REAL holds
( b₄ is middle_volume of f,D iff ( len b₄ = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset D,i)) & b₄ . i = r * (vol (divset D,i)) ) ) ) );

PX0101: for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume f,D) . i <= F . i

proof end;

PX0201: for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume f,D) . i <= F . i & F . i < ((lower_volume f,D) . i) + e )

proof end;

PX0202: for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < F . i )

proof end;

PX0102: for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume f,D) . i

proof end;

definition

let A be closed-interval Subset of REAL ;
let f be Function of A,REAL ;
let D be Division of A;
let F be middle_volume of f,D;
func middle_sum f,F -> Real equals :: INTEGR15:def 2
Sum F;
correctness
coherence
Sum F is Real;
;

end;

:: deftheorem defines middle_sum INTEGR15:def 2 :

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D holds middle_sum f,F = Sum F;

theorem PX0103: :: INTEGR15:1

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D st f | A is bounded_below holds
lower_sum f,D <= middle_sum f,F

proof end;

theorem PX0104: :: INTEGR15:2

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D st f | A is bounded_above holds
middle_sum f,F <= upper_sum f,D

proof end;

theorem PX0203: :: INTEGR15:3

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st middle_sum f,F <= (lower_sum f,D) + e

proof end;

theorem PX0204: :: INTEGR15:4

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum f,D) - e <= middle_sum f,F

proof end;

definition

let A be closed-interval Subset of REAL ;
let f be Function of A,REAL ;
let T be DivSequence of A;
mode middle_volume_Sequence of f,T -> Function of NAT ,(REAL * ) means :defx2: :: INTEGR15:def 3
for k being Element of NAT holds it . k is middle_volume of f,T . k;
correctness
existence
ex b₁ being Function of NAT ,(REAL * ) st
for k being Element of NAT holds b₁ . k is middle_volume of f,T . k;

proof end;

end;

:: deftheorem defx2 defines middle_volume_Sequence INTEGR15:def 3 :

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for b₄ being Function of NAT ,(REAL * ) holds
( b₄ is middle_volume_Sequence of f,T iff for k being Element of NAT holds b₄ . k is middle_volume of f,T . k );

definition

let A be closed-interval Subset of REAL ;
let f be Function of A,REAL ;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT ;
:: original: .
redefine func S . k -> middle_volume of f,T . k;
coherence
S . k is middle_volume of f,T . k by defx2;

end;

definition

let A be closed-interval Subset of REAL ;
let f be Function of A,REAL ;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
func middle_sum f,S -> Real_Sequence means :defx3: :: INTEGR15:def 4
for i being Element of NAT holds it . i = middle_sum f,(S . i);
existence
ex b₁ being Real_Sequence st
for i being Element of NAT holds b₁ . i = middle_sum f,(S . i)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Element of NAT holds b₁ . i = middle_sum f,(S . i) ) & ( for i being Element of NAT holds b₂ . i = middle_sum f,(S . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defx3 defines middle_sum INTEGR15:def 4 :

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b₅ being Real_Sequence holds
( b₅ = middle_sum f,S iff for i being Element of NAT holds b₅ . i = middle_sum f,(S . i) );

theorem PX011: :: INTEGR15:5

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_below holds
(lower_sum f,T) . i <= (middle_sum f,S) . i

proof end;

theorem PX012: :: INTEGR15:6

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_above holds
(middle_sum f,S) . i <= (upper_sum f,T) . i

proof end;

theorem PX02: :: INTEGR15:7

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_below holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum f,S) . i <= ((lower_sum f,T) . i) + e

proof end;

theorem PX03: :: INTEGR15:8

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_above holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum f,T) . i) - e <= (middle_sum f,S) . i

proof end;

PX041: for p, q, r being Real_Sequence st p is convergent & r is convergent & lim p = lim r & ( for i being Element of NAT holds p . i <= q . i ) & ( for i being Element of NAT holds q . i <= r . i ) holds
( q is convergent & lim p = lim q & lim r = lim q )

proof end;

theorem PX04: :: INTEGR15:9

for A being closed-interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )

proof end;

theorem PX05: :: INTEGR15:10

for A being closed-interval Subset of REAL
for f being Function of A,REAL st f is bounded holds
( f is integrable iff ex I being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = I ) )

proof end;

definition

let n be Element of NAT ;
let A be 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 :defxn0: :: INTEGR15:def 5
( len it = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset D,i)) & it . i = (vol (divset D,i)) * r ) ) );
correctness
existence
ex b₁ being FinSequence of REAL n st
( len b₁ = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset D,i)) & b₁ . i = (vol (divset D,i)) * r ) ) );

proof end;

end;

:: deftheorem defxn0 defines middle_volume INTEGR15:def 5 :

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,(REAL n)
for D being Division of A
for b₅ being FinSequence of REAL n holds
( b₅ is middle_volume of f,D iff ( len b₅ = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset D,i)) & b₅ . i = (vol (divset D,i)) * r ) ) ) );

definition

let n be Element of NAT ;
let A be 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 :defxn1: :: INTEGR15:def 6
for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj i,n) * F & it . i = Sum Fi );
existence
ex b₁ being Element of REAL n st
for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj i,n) * F & b₁ . i = Sum Fi )

proof end;

uniqueness
for b₁, b₂ being Element of REAL n st ( for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj i,n) * F & b₁ . i = Sum Fi ) ) & ( for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj i,n) * F & b₂ . i = Sum Fi ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defxn1 defines middle_sum INTEGR15:def 6 :

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,(REAL n)
for D being Division of A
for F being middle_volume of f,D
for b₆ being Element of REAL n holds
( b₆ = middle_sum f,F iff for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj i,n) * F & b₆ . i = Sum Fi ) );

definition

let n be Element of NAT ;
let A be closed-interval Subset of REAL ;
let f be Function of A,(REAL n);
let T be DivSequence of A;
mode middle_volume_Sequence of f,T -> Function of NAT ,((REAL n) * ) means :defxn2: :: INTEGR15:def 7
for k being Element of NAT holds it . k is middle_volume of f,T . k;
correctness
existence
ex b₁ being Function of NAT ,((REAL n) * ) st
for k being Element of NAT holds b₁ . k is middle_volume of f,T . k;

proof end;

end;

:: deftheorem defxn2 defines middle_volume_Sequence INTEGR15:def 7 :

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for b₅ being Function of NAT ,((REAL n) * ) holds
( b₅ is middle_volume_Sequence of f,T iff for k being Element of NAT holds b₅ . k is middle_volume of f,T . k );

definition

let n be Element of NAT ;
let A be closed-interval Subset of REAL ;
let f be Function of A,(REAL n);
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT ;
:: original: .
redefine func S . k -> middle_volume of f,T . k;
coherence
S . k is middle_volume of f,T . k by defxn2;

end;

definition

let n be Element of NAT ;
let A be 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 :defxn3: :: INTEGR15:def 8
for i being Element of NAT holds it . i = middle_sum f,(S . i);
existence
ex b₁ being sequence of (REAL-NS n) st
for i being Element of NAT holds b₁ . i = middle_sum f,(S . i)

proof end;

uniqueness
for b₁, b₂ being sequence of (REAL-NS n) st ( for i being Element of NAT holds b₁ . i = middle_sum f,(S . i) ) & ( for i being Element of NAT holds b₂ . i = middle_sum f,(S . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defxn3 defines middle_sum INTEGR15:def 8 :

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b₆ being sequence of (REAL-NS n) holds
( b₆ = middle_sum f,S iff for i being Element of NAT holds b₆ . i = middle_sum f,(S . i) );

definition

let n be Element of NAT ;
let Z be non empty set ;
let f, g be PartFunc of Z,(REAL n);
deffunc H₁( Element of Z) -> Element of REAL n = (f /. $1) + (g /. $1);
deffunc H₂( Element of Z) -> Element of REAL n = (f /. $1) - (g /. $1);
defpred S₁[ set ] means $1 in (dom f) /\ (dom g);
set X = (dom f) /\ (dom g);
func f + g -> PartFunc of Z,(REAL n) means :Def1: :: INTEGR15:def 9
( dom it = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom it holds
it /. c = (f /. c) + (g /. c) ) );
existence
ex b₁ being PartFunc of Z,(REAL n) st
( dom b₁ = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b₁ holds
b₁ /. c = (f /. c) + (g /. c) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of Z,(REAL n) st dom b₁ = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b₁ holds
b₁ /. c = (f /. c) + (g /. c) ) & dom b₂ = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b₂ holds
b₂ /. c = (f /. c) + (g /. c) ) holds
b₁ = b₂

proof end;

func f - g -> PartFunc of Z,(REAL n) means :Def2: :: INTEGR15:def 10
( dom it = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom it holds
it /. c = (f /. c) - (g /. c) ) );
existence
ex b₁ being PartFunc of Z,(REAL n) st
( dom b₁ = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b₁ holds
b₁ /. c = (f /. c) - (g /. c) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of Z,(REAL n) st dom b₁ = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b₁ holds
b₁ /. c = (f /. c) - (g /. c) ) & dom b₂ = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b₂ holds
b₂ /. c = (f /. c) - (g /. c) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines + INTEGR15:def 9 :

for n being Element of NAT
for Z being non empty set
for f, g, b₅ being PartFunc of Z,(REAL n) holds
( b₅ = f + g iff ( dom b₅ = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b₅ holds
b₅ /. c = (f /. c) + (g /. c) ) ) );

:: deftheorem Def2 defines - INTEGR15:def 10 :

for n being Element of NAT
for Z being non empty set
for f, g, b₅ being PartFunc of Z,(REAL n) holds
( b₅ = f - g iff ( dom b₅ = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom b₅ holds
b₅ /. c = (f /. c) - (g /. c) ) ) );

definition

let n be Element of NAT ;
let r be real number ;
let Z be non empty set ;
let f be PartFunc of Z,(REAL n);
deffunc H₁( Element of Z) -> Element of REAL n = r * (f /. $1);
defpred S₁[ set ] means $1 in dom f;
set X = dom f;
func r (#) f -> PartFunc of Z,(REAL n) means :Def3: :: INTEGR15:def 11
( dom it = dom f & ( for c being Element of Z st c in dom it holds
it /. c = r * (f /. c) ) );
existence
ex b₁ being PartFunc of Z,(REAL n) st
( dom b₁ = dom f & ( for c being Element of Z st c in dom b₁ holds
b₁ /. c = r * (f /. c) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of Z,(REAL n) st dom b₁ = dom f & ( for c being Element of Z st c in dom b₁ holds
b₁ /. c = r * (f /. c) ) & dom b₂ = dom f & ( for c being Element of Z st c in dom b₂ holds
b₂ /. c = r * (f /. c) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines (#) INTEGR15:def 11 :

for n being Element of NAT
for r being real number
for Z being non empty set
for f, b₅ being PartFunc of Z,(REAL n) holds
( b₅ = r (#) f iff ( dom b₅ = dom f & ( for c being Element of Z st c in dom b₅ holds
b₅ /. c = r * (f /. c) ) ) );

definition

let n be Element of NAT ;
let A be closed-interval Subset of REAL ;
let f be Function of A,(REAL n);
attr f is bounded means :Defboundn: :: INTEGR15:def 12
for i being Element of NAT st i in Seg n holds
(proj i,n) * f is bounded ;

end;

:: deftheorem Defboundn defines bounded INTEGR15:def 12 :

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,(REAL n) holds
( f is bounded iff for i being Element of NAT st i in Seg n holds
(proj i,n) * f is bounded );

LMDEF: for n, i being Element of NAT
for f being PartFunc of REAL ,(REAL n)
for i being Element of NAT
for A being Subset of REAL st i in Seg n holds
(proj i,n) * (f | A) = ((proj i,n) * f) | A

proof end;

definition

let n be Element of NAT ;
let A be closed-interval Subset of REAL ;
let f be Function of A,(REAL n);
attr f is integrable means :Intablen: :: INTEGR15:def 13
for i being Element of NAT st i in Seg n holds
(proj i,n) * f is integrable ;

end;

:: deftheorem Intablen defines integrable INTEGR15:def 13 :

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,(REAL n) holds
( f is integrable iff for i being Element of NAT st i in Seg n holds
(proj i,n) * f is integrable );

definition

let n be Element of NAT ;
let A be closed-interval Subset of REAL ;
let f be Function of A,(REAL n);
func integral f -> Element of REAL n means :DefintNn: :: INTEGR15:def 14
( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds
it . i = integral ((proj i,n) * f) ) );
existence
ex b₁ being Element of REAL n st
( dom b₁ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₁ . i = integral ((proj i,n) * f) ) )

proof end;

uniqueness
for b₁, b₂ being Element of REAL n st dom b₁ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₁ . i = integral ((proj i,n) * f) ) & dom b₂ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₂ . i = integral ((proj i,n) * f) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefintNn defines integral INTEGR15:def 14 :

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,(REAL n)
for b₄ being Element of REAL n holds
( b₄ = integral f iff ( dom b₄ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₄ . i = integral ((proj i,n) * f) ) ) );

theorem PX04n: :: INTEGR15:11

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )

proof end;

theorem :: INTEGR15:12

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,(REAL n) st f is bounded holds
( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = I ) )

proof end;

definition

let n be Element of NAT ;
let f be PartFunc of REAL ,(REAL n);
attr f is bounded means :Defbounded: :: INTEGR15:def 15
for i being Element of NAT st i in Seg n holds
(proj i,n) * f is bounded ;

end;

:: deftheorem Defbounded defines bounded INTEGR15:def 15 :

for n being Element of NAT
for f being PartFunc of REAL ,(REAL n) holds
( f is bounded iff for i being Element of NAT st i in Seg n holds
(proj i,n) * f is bounded );

definition

let n be Element of NAT ;
let A be closed-interval Subset of REAL ;
let f be PartFunc of REAL ,(REAL n);
pred f is_integrable_on A means :Defintable: :: INTEGR15:def 16
for i being Element of NAT st i in Seg n holds
(proj i,n) * f is_integrable_on A;

end;

:: deftheorem Defintable defines is_integrable_on INTEGR15:def 16 :

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,(REAL n) holds
( f is_integrable_on A iff for i being Element of NAT st i in Seg n holds
(proj i,n) * f is_integrable_on A );

definition

let n be Element of NAT ;
let A be closed-interval Subset of REAL ;
let f be PartFunc of REAL ,(REAL n);
func integral f,A -> Element of REAL n means :DefintN: :: INTEGR15:def 17
( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds
it . i = integral ((proj i,n) * f),A ) );
existence
ex b₁ being Element of REAL n st
( dom b₁ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₁ . i = integral ((proj i,n) * f),A ) )

proof end;

uniqueness
for b₁, b₂ being Element of REAL n st dom b₁ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₁ . i = integral ((proj i,n) * f),A ) & dom b₂ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₂ . i = integral ((proj i,n) * f),A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefintN defines integral INTEGR15:def 17 :

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,(REAL n)
for b₄ being Element of REAL n holds
( b₄ = integral f,A iff ( dom b₄ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₄ . i = integral ((proj i,n) * f),A ) ) );

theorem :: INTEGR15:13

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
( f is_integrable_on A iff g is integrable )

proof end;

theorem :: INTEGR15:14

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
integral f,A = integral g

proof end;

definition

let a, b be real number ;
let n be Element of NAT ;
let f be PartFunc of REAL ,(REAL n);
func integral f,a,b -> Element of REAL n means :Defintn: :: INTEGR15:def 18
( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds
it . i = integral ((proj i,n) * f),a,b ) );
existence
ex b₁ being Element of REAL n st
( dom b₁ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₁ . i = integral ((proj i,n) * f),a,b ) )

proof end;

uniqueness
for b₁, b₂ being Element of REAL n st dom b₁ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₁ . i = integral ((proj i,n) * f),a,b ) & dom b₂ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₂ . i = integral ((proj i,n) * f),a,b ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Defintn defines integral INTEGR15:def 18 :

for a, b being real number
for n being Element of NAT
for f being PartFunc of REAL ,(REAL n)
for b₅ being Element of REAL n holds
( b₅ = integral f,a,b iff ( dom b₅ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₅ . i = integral ((proj i,n) * f),a,b ) ) );

theorem Th31: :: INTEGR15:15

for n being Element of NAT
for f1, f2 being PartFunc of REAL ,(REAL n)
for i being Element of NAT st i in Seg 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 end;

theorem Th32: :: INTEGR15:16

for n being Element of NAT
for r being Real
for f being PartFunc of REAL ,(REAL n)
for i being Element of NAT st i in Seg n holds
(proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)

proof end;

theorem :: INTEGR15:17

for n being Element of NAT
for A being closed-interval Subset of REAL
for f1, f2 being PartFunc of REAL ,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds
( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) & integral (f1 - f2),A = (integral f1,A) - (integral f2,A) )

proof end;

theorem :: INTEGR15:18

for n being Element of NAT
for r being Real
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )

proof end;

theorem :: INTEGR15:19

for n being Element of NAT
for f being PartFunc of REAL ,(REAL n)
for A being closed-interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral f,A = integral f,a,b

proof end;

theorem :: INTEGR15:20

for n being Element of NAT
for f being PartFunc of REAL ,(REAL n)
for A being closed-interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral f,A) = integral f,a,b

proof end;