:: Several Integrability Formulas of Some Functions, Orthogonal Polynomialsand Norm Functions
:: by Bo Li , Yanping Zhuang , Bing Xie and Pan Wang
::
:: Received October 14, 2008
:: Copyright (c) 2008 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;