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

definition

let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let D be Division of A;

mode middle_volume of f,D -> FinSequence of REAL means :Def1: :: INTEGR15:def 1
( len it = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & it . i = r * (vol (divset (D,i))) ) ) );

correctness
existence
ex 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 Def1 defines middle_volume INTEGR15:def 1 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for 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))) ) ) ) );

Lm1: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume (f,D)) . i <= F . i

proof end;

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

proof end;

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

proof end;

Lm4: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume (f,D)) . i

proof end;

definition

let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let D be Division of A;
let F be middle_volume of f,D;

func middle_sum (f,F) -> Real equals :: INTEGR15:def 2
Sum F;

correctness
coherence
Sum F is Real;
;

end;

:: deftheorem defines middle_sum INTEGR15:def 2 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;

theorem Th1: :: INTEGR15:1

for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D st f | A is bounded_below holds
lower_sum (f,D) <= middle_sum (f,F)

proof end;

theorem Th2: :: INTEGR15:2

for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D st f | A is bounded_above holds
middle_sum (f,F) <= upper_sum (f,D)

proof end;

theorem Th3: :: INTEGR15:3

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

proof end;

theorem Th4: :: INTEGR15:4

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

proof end;

definition

let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let T be DivSequence of A;

mode middle_volume_Sequence of f,T -> sequence of (REAL *) means :Def3: :: INTEGR15:def 3
for k being Element of NAT holds it . k is middle_volume of f,T . k;

correctness
existence
ex b₁ being sequence of (REAL *) st
for k being Element of NAT holds b₁ . k is middle_volume of f,T . k;

proof end;

end;

:: deftheorem Def3 defines middle_volume_Sequence INTEGR15:def 3 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for b₄ being sequence of (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 non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT ;
:: original: .
redefine func S . k -> middle_volume of f,T . k;
coherence
S . k is middle_volume of f,T . k by Def3;

end;

definition

let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;

func middle_sum (f,S) -> Real_Sequence means :Def4: :: INTEGR15:def 4
for i being Element of NAT holds it . i = middle_sum (f,(S . i));

existence
ex 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 Def4 defines middle_sum INTEGR15:def 4 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for 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 Th5: :: INTEGR15:5

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

proof end;

theorem Th6: :: INTEGR15:6

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

proof end;

theorem Th7: :: INTEGR15:7

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

proof end;

theorem Th8: :: INTEGR15:8

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

proof end;

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

proof end;

theorem Th9: :: INTEGR15:9

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

proof end;

theorem Th10: :: INTEGR15:10

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

proof end;

definition

let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
let D be Division of A;

mode middle_volume of f,D -> FinSequence of REAL n means :Def5: :: INTEGR15:def 5
( len it = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset (D,i))) & it . i = (vol (divset (D,i))) * r ) ) );

correctness
existence
ex 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 Def5 defines middle_volume INTEGR15:def 5 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for D being Division of A
for 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 non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
let D be Division of A;
let F be middle_volume of f,D;

func middle_sum (f,F) -> Element of REAL n means :Def6: :: INTEGR15:def 6
for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & it . i = Sum Fi );

existence
ex 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 Def6 defines middle_sum INTEGR15:def 6 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for D being Division of A
for F being middle_volume of f,D
for 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 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: :: INTEGR15:def 7
for k being Element of NAT holds it . k is middle_volume of f,T . k;

correctness
existence
ex b₁ being sequence of ((REAL n) *) st
for k being Element of NAT holds b₁ . k is middle_volume of f,T . k;

proof end;

end;

:: deftheorem Def7 defines middle_volume_Sequence INTEGR15:def 7 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for b₅ being sequence of ((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 non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT ;
:: original: .
redefine func S . k -> middle_volume of f,T . k;
coherence
S . k is middle_volume of f,T . k by Def7;

end;

definition

let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;

func middle_sum (f,S) -> sequence of (REAL-NS n) means :Def8: :: INTEGR15:def 8
for i being Element of NAT holds it . i = middle_sum (f,(S . i));

existence
ex 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 Def8 defines middle_sum INTEGR15:def 8 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for 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 Nat;
let Z be set ;
let f, g be PartFunc of Z,(REAL n);

func f + g -> PartFunc of Z,(REAL n) equals :: INTEGR15:def 9
f <++> g;

coherence
f <++> g is PartFunc of Z,(REAL n)

proof end;

func f - g -> PartFunc of Z,(REAL n) equals :: INTEGR15:def 10
f <--> g;

coherence
f <--> g is PartFunc of Z,(REAL n)

proof end;

end;

:: deftheorem defines + INTEGR15:def 9 :
for n being Nat
for Z being set
for f, g being PartFunc of Z,(REAL n) holds f + g = f <++> g;

:: deftheorem defines - INTEGR15:def 10 :
for n being Nat
for Z being set
for f, g being PartFunc of Z,(REAL n) holds f - g = f <--> g;

definition

let n be Nat;
let r be Real;
let Z be set ;
let f be PartFunc of Z,(REAL n);

func r (#) f -> PartFunc of Z,(REAL n) equals :: INTEGR15:def 11
f [#] r;

coherence
f [#] r is PartFunc of Z,(REAL n)

proof end;

end;

:: deftheorem defines (#) INTEGR15:def 11 :
for n being Nat
for r being Real
for Z being set
for f being PartFunc of Z,(REAL n) holds r (#) f = f [#] r;

definition

let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);

attr f is bounded means :: INTEGR15:def 12
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is bounded ;

end;

:: deftheorem defines bounded INTEGR15:def 12 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n) holds
( f is bounded iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is bounded );

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

proof 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 :: INTEGR15:def 13
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is integrable ;

end;

:: deftheorem defines integrable INTEGR15:def 13 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n) holds
( f is integrable iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is integrable );

definition

let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);

func integral f -> Element of REAL n means :Def14: :: INTEGR15:def 14
( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds
it . i = integral ((proj (i,n)) * f) ) );

existence
ex 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 Def14 defines integral INTEGR15:def 14 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for 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 Th11: :: INTEGR15:11

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

proof end;

theorem :: INTEGR15:12

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

proof end;

definition

let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);

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

end;

:: deftheorem defines bounded INTEGR15:def 15 :
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is bounded iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is bounded );

definition

let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,(REAL n);

pred f is_integrable_on A means :: 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 defines is_integrable_on INTEGR15:def 16 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n) holds
( f is_integrable_on A iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on A );

definition

let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,(REAL n);

func integral (f,A) -> Element of REAL n means :Def17: :: INTEGR15:def 17
( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds
it . i = integral (((proj (i,n)) * f),A) ) );

existence
ex 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 Def17 defines integral INTEGR15:def 17 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for 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 non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
( f is_integrable_on A iff g is integrable )

proof end;

theorem :: INTEGR15:14

for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
integral (f,A) = integral g

proof 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: :: 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 Def18 defines integral INTEGR15:def 18 :
for a, b being Real
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 Th15: :: INTEGR15:15

for Z being set
for n, i being Element of NAT
for f1, f2 being PartFunc of Z,(REAL n) holds
( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) )

proof end;

theorem Th16: :: INTEGR15:16

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

proof end;

theorem :: INTEGR15:17

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

proof end;

theorem :: INTEGR15:18

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

proof end;

theorem :: INTEGR15:19

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

proof end;

theorem :: INTEGR15:20

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

proof end;

theorem :: INTEGR15:21

for n being Nat
for Z, x being set
for f, g being PartFunc of Z,(REAL n) st x in dom (f + g) holds
(f + g) /. x = (f /. x) + (g /. x)

proof end;

theorem :: INTEGR15:22

for n being Nat
for Z, x being set
for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds
(f - g) /. x = (f /. x) - (g /. x)

proof end;

theorem :: INTEGR15:23

for n being Nat
for Z, x being set
for f being PartFunc of Z,(REAL n)
for r being Real st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)

proof end;