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


begin

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 b1 being FinSequence of REAL st
( len b1 = 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))) & b1 . 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 b4 being FinSequence of REAL holds
( b4 is middle_volume of f,D iff ( len b4 = 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))) & b4 . 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 -> Function of NAT,(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 b1 being Function of NAT,(REAL *) st
for k being Element of NAT holds b1 . 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 b4 being Function of NAT,(REAL *) holds
( b4 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b4 . 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 b1 being Real_Sequence st
for i being Element of NAT holds b1 . i = middle_sum (f,(S . i))
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds
b1 = b2
proof 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 b5 being Real_Sequence holds
( b5 = middle_sum (f,S) iff for i being Element of NAT holds b5 . 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 b1 being FinSequence of REAL n st
( len b1 = 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))) & b1 . 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 b5 being FinSequence of REAL n holds
( b5 is middle_volume of f,D iff ( len b5 = 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))) & b5 . 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 b1 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 & b1 . i = Sum Fi )
proof end;
uniqueness
for b1, b2 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 & b1 . 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 & b2 . i = Sum Fi ) ) holds
b1 = b2
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 b6 being Element of REAL n holds
( b6 = 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 & b6 . 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 -> Function of NAT,((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 b1 being Function of NAT,((REAL n) *) st
for k being Element of NAT holds b1 . 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 b5 being Function of NAT,((REAL n) *) holds
( b5 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b5 . k is middle_volume of f,T . k );

definition
let 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 b1 being sequence of (REAL-NS n) st
for i being Element of NAT holds b1 . i = middle_sum (f,(S . i))
proof end;
uniqueness
for b1, b2 being sequence of (REAL-NS n) st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds
b1 = b2
proof 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 b6 being sequence of (REAL-NS n) holds
( b6 = middle_sum (f,S) iff for i being Element of NAT holds b6 . 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 number ;
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 number
for Z being set
for f being PartFunc of Z,(REAL n) holds r (#) f = f [#] r;

begin

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

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

:: deftheorem Def13 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 b1 being Element of REAL n st
( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral ((proj (i,n)) * f) ) )
proof end;
uniqueness
for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral ((proj (i,n)) * f) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds
b2 . i = integral ((proj (i,n)) * f) ) holds
b1 = b2
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 b4 being Element of REAL n holds
( b4 = integral f iff ( dom b4 = Seg n & ( for i being Element of NAT st i in Seg n holds
b4 . 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 :Def15: :: INTEGR15:def 15
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is bounded ;
end;

:: deftheorem Def15 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 :Def16: :: 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 Def16 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 b1 being Element of REAL n st
( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),A) ) )
proof end;
uniqueness
for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),A) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds
b2 . i = integral (((proj (i,n)) * f),A) ) holds
b1 = b2
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 b4 being Element of REAL n holds
( b4 = integral (f,A) iff ( dom b4 = Seg n & ( for i being Element of NAT st i in Seg n holds
b4 . 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 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 :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 b1 being Element of REAL n st
( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),a,b) ) )
proof end;
uniqueness
for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),a,b) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds
b2 . i = integral (((proj (i,n)) * f),a,b) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 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 b5 being Element of REAL n holds
( b5 = integral (f,a,b) iff ( dom b5 = Seg n & ( for i being Element of NAT st i in Seg n holds
b5 . i = integral (((proj (i,n)) * f),a,b) ) ) );

begin

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 number st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)
proof end;