:: Several Integrability Formulas of Some Functions, Orthogonal Polynomials and Norm Functions
:: by Bo Li , Yanping Zhuang , Bing Xie and Pan Wang
::
:: Received October 14, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users


begin

Lm1: dom (- (exp_R * (AffineMap ((- 1),0)))) = [#] REAL
by FUNCT_2:def 1;

theorem :: INTEGRA9:1
( - (exp_R * (AffineMap ((- 1),0))) is_differentiable_on REAL & ( for x being Real holds ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ) )
proof end;

theorem :: INTEGRA9:2
canceled;

theorem :: INTEGRA9:3
canceled;

theorem :: INTEGRA9:4
canceled;

theorem Th5: :: INTEGRA9:5
for r being Real st r <> 0 holds
( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) )
proof end;

theorem :: INTEGRA9:6
for r being Real
for A being closed-interval Subset of REAL st r <> 0 holds
integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A))
proof end;

theorem :: INTEGRA9:7
canceled;

theorem Th8: :: INTEGRA9:8
for n being Element of NAT st n <> 0 holds
( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) )
proof end;

theorem :: INTEGRA9:9
for n being Element of NAT
for A being closed-interval Subset of REAL st n <> 0 holds
integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A))
proof end;

theorem :: INTEGRA9:10
canceled;

theorem :: INTEGRA9:11
canceled;

theorem Th12: :: INTEGRA9:12
for n being Element of NAT st n <> 0 holds
( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) )
proof end;

theorem :: INTEGRA9:13
for n being Element of NAT
for A being closed-interval Subset of REAL st n <> 0 holds
integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A))
proof end;

theorem :: INTEGRA9:14
for A being closed-interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))
proof end;

theorem :: INTEGRA9:15
for A being closed-interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A))
proof end;

theorem Th16: :: INTEGRA9:16
for Z being open Subset of REAL holds
( (id Z) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) ) )
proof end;

Lm2: for x being Real holds
( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) )
proof end;

theorem Th17: :: INTEGRA9:17
for Z being open Subset of REAL holds
( (- sin) + ((id Z) (#) cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) ) )
proof end;

theorem :: INTEGRA9:18
for A being closed-interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A))
proof end;

theorem Th19: :: INTEGRA9:19
for Z being open Subset of REAL holds
( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) )
proof end;

theorem :: INTEGRA9:20
for A being closed-interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:21
for A being closed-interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A))
proof end;

theorem :: INTEGRA9:22
for A being closed-interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A))
proof end;

theorem :: INTEGRA9:23
for A being closed-interval Subset of REAL holds integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A))
proof end;

theorem Th24: :: INTEGRA9:24
for n being Element of NAT holds
( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ) )
proof end;

theorem :: INTEGRA9:25
for n being Element of NAT
for A being closed-interval Subset of REAL holds integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1)))
proof end;

begin

theorem Th26: :: INTEGRA9:26
for f, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds (f - g) || C = (f || C) - (g || C)
proof end;

theorem Th27: :: INTEGRA9:27
for f1, f2, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C
proof end;

theorem Th28: :: INTEGRA9:28
for f1, f2, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds ((f1 - f2) || C) (#) (g || C) = ((f1 (#) g) - (f2 (#) g)) || C
proof end;

theorem :: INTEGRA9:29
for f1, f2, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C)
proof end;

definition
let A be closed-interval Subset of REAL;
let f, g be PartFunc of REAL,REAL;
func |||(f,g,A)||| -> Real equals :: INTEGRA9:def 1
integral ((f (#) g),A);
correctness
coherence
integral ((f (#) g),A) is Real
;
;
end;

:: deftheorem defines |||( INTEGRA9:def 1 :
for A being closed-interval Subset of REAL
for f, g being PartFunc of REAL,REAL holds |||(f,g,A)||| = integral ((f (#) g),A);

theorem :: INTEGRA9:30
for f, g being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL holds |||(f,g,A)||| = |||(g,f,A)||| ;

theorem :: INTEGRA9:31
for f1, f2, g being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable holds
|||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)|||
proof end;

theorem :: INTEGRA9:32
for f1, f2, g being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable holds
|||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)|||
proof end;

theorem :: INTEGRA9:33
for f, g being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds
|||((- f),g,A)||| = - |||(f,g,A)|||
proof end;

theorem :: INTEGRA9:34
for r being Real
for f, g being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds
|||((r (#) f),g,A)||| = r * |||(f,g,A)|||
proof end;

theorem :: INTEGRA9:35
for r, p being Real
for f, g being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds
|||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)|||
proof end;

theorem :: INTEGRA9:36
for f, g, h being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL holds |||((f (#) g),h,A)||| = |||(f,(g (#) h),A)||| by RFUNCT_1:21;

theorem Th37: :: INTEGRA9:37
for f, g being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A holds
|||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)|||
proof end;

begin

definition
let A be closed-interval Subset of REAL;
let f, g be PartFunc of REAL,REAL;
pred f is_orthogonal_with g,A means :Def2: :: INTEGRA9:def 2
|||(f,g,A)||| = 0 ;
end;

:: deftheorem Def2 defines is_orthogonal_with INTEGRA9:def 2 :
for A being closed-interval Subset of REAL
for f, g being PartFunc of REAL,REAL holds
( f is_orthogonal_with g,A iff |||(f,g,A)||| = 0 );

theorem Th38: :: INTEGRA9:38
for f, g being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A holds
|||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)|||
proof end;

theorem :: INTEGRA9:39
for f being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & (f (#) f) || A is integrable & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
|||(f,f,A)||| >= 0 by INTEGRA2:32;

theorem :: INTEGRA9:40
for A being closed-interval Subset of REAL st A = [.0,PI.] holds
sin is_orthogonal_with cos ,A
proof end;

theorem :: INTEGRA9:41
for A being closed-interval Subset of REAL st A = [.0,(PI * 2).] holds
sin is_orthogonal_with cos ,A
proof end;

theorem :: INTEGRA9:42
for n being Element of NAT
for A being closed-interval Subset of REAL st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
sin is_orthogonal_with cos ,A
proof end;

theorem :: INTEGRA9:43
for x being Real
for n being Element of NAT
for A being closed-interval Subset of REAL st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
sin is_orthogonal_with cos ,A
proof end;

theorem :: INTEGRA9:44
for A being closed-interval Subset of REAL st A = [.(- PI),PI.] holds
sin is_orthogonal_with cos ,A
proof end;

theorem :: INTEGRA9:45
for A being closed-interval Subset of REAL st A = [.(- (PI / 2)),(PI / 2).] holds
sin is_orthogonal_with cos ,A
proof end;

theorem :: INTEGRA9:46
for A being closed-interval Subset of REAL st A = [.(- (2 * PI)),(2 * PI).] holds
sin is_orthogonal_with cos ,A
proof end;

theorem :: INTEGRA9:47
for n being Element of NAT
for A being closed-interval Subset of REAL st A = [.(- ((2 * n) * PI)),((2 * n) * PI).] holds
sin is_orthogonal_with cos ,A
proof end;

theorem :: INTEGRA9:48
for x being Real
for n being Element of NAT
for A being closed-interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds
sin is_orthogonal_with cos ,A
proof end;

begin

definition
let A be closed-interval Subset of REAL;
let f be PartFunc of REAL,REAL;
func ||..f,A..|| -> Real equals :: INTEGRA9:def 3
sqrt |||(f,f,A)|||;
correctness
coherence
sqrt |||(f,f,A)||| is Real
;
;
end;

:: deftheorem defines ||.. INTEGRA9:def 3 :
for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL holds ||..f,A..|| = sqrt |||(f,f,A)|||;

theorem :: INTEGRA9:49
for f being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
0 <= ||..f,A..||
proof end;

theorem :: INTEGRA9:50
for f being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL holds ||..(1 (#) f),A..|| = ||..f,A..|| by RFUNCT_1:33;

theorem :: INTEGRA9:51
for f, g being PartFunc of REAL,REAL
for A being closed-interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) & ( for x being Real st x in A holds
((g (#) g) || A) . x >= 0 ) holds
||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2)
proof end;

begin

theorem :: INTEGRA9:52
for a being Real
for A being closed-interval Subset of REAL st not - a in A holds
((AffineMap (1,a)) ^) | A is continuous
proof end;

theorem :: INTEGRA9:53
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
proof end;

theorem :: INTEGRA9:54
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:55
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
proof end;

theorem :: INTEGRA9:56
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
proof end;

theorem :: INTEGRA9:57
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
proof end;

theorem :: INTEGRA9:58
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a - x) ) & f2 | A is continuous holds
integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:59
for a being Real
for A being closed-interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = x / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:60
for a being Real
for A being closed-interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:61
for a being Real
for A being closed-interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:62
for a being Real
for A being closed-interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:63
for b, a being Real
for A being closed-interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:64
for b, a being Real
for A being closed-interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:65
for b, a being Real
for A being closed-interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:66
for b, a being Real
for A being closed-interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:67
for A being closed-interval Subset of REAL
for Z being open Subset of REAL st A c= Z & dom ln = Z & Z = dom ((id Z) ^) & ((id Z) ^) | A is continuous holds
integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A))
proof end;

theorem :: INTEGRA9:68
for n being Element of NAT
for A being closed-interval Subset of REAL
for f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = n / x ) & f2 | A is continuous holds
integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:69
for A being closed-interval Subset of REAL
for f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:70
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:71
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:72
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:73
for a being Real
for A being closed-interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A))
proof end;

theorem :: INTEGRA9:74
for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & dom (((- (id Z)) (#) cos) + sin) = Z & ( for x being Real st x in Z holds
f . x = x * (sin . x) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))
proof end;

theorem :: INTEGRA9:75
for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & dom sec = Z & ( for x being Real st x in Z holds
f . x = (sin . x) / ((cos . x) ^2) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A))
proof end;

theorem Th76: :: INTEGRA9:76
for Z being open Subset of REAL st Z c= dom (- cosec) holds
( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) )
proof end;

theorem :: INTEGRA9:77
for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & dom (- cosec) = Z & ( for x being Real st x in Z holds
f . x = (cos . x) / ((sin . x) ^2) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A))
proof end;