:: by Bo Li and Na Ma

::

:: Received February 4, 2010

:: Copyright (c) 2010-2017 Association of Mizar Users

Lm1: for Z being open Subset of REAL st 0 in Z holds

(id Z) " {0} = {0}

proof end;

theorem Th1: :: INTEGR14:1

for Z being open Subset of REAL st Z c= dom (sec * ((id Z) ^)) holds

( - (sec * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) )

( - (sec * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) )

proof end;

::f.x=-cosec.(exp_R.x)

theorem Th2: :: INTEGR14:2

for Z being open Subset of REAL st Z c= dom (cosec * exp_R) holds

( - (cosec * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) )

( - (cosec * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) )

proof end;

:: f.x = -cosec.(ln.x)

theorem Th3: :: INTEGR14:3

for Z being open Subset of REAL st Z c= dom (cosec * ln) holds

( - (cosec * ln) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) )

( - (cosec * ln) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) )

proof end;

:: f.x = -exp_R.(cosec.x)

theorem Th4: :: INTEGR14:4

for Z being open Subset of REAL st Z c= dom (exp_R * cosec) holds

( - (exp_R * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) )

( - (exp_R * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) )

proof end;

:: f.x = -ln.(cosec.x)

theorem Th5: :: INTEGR14:5

for Z being open Subset of REAL st Z c= dom (ln * cosec) holds

( - (ln * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (ln * cosec)) `| Z) . x = cot . x ) )

( - (ln * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (ln * cosec)) `| Z) . x = cot . x ) )

proof end;

::f.x=-(cosec.x) #Z n

theorem Th6: :: INTEGR14:6

for n being Nat

for Z being open Subset of REAL st Z c= dom ((#Z n) * cosec) & 1 <= n holds

( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) )

for Z being open Subset of REAL st Z c= dom ((#Z n) * cosec) & 1 <= n holds

( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) )

proof end;

::f.x= -1/x*sec.x

theorem Th7: :: INTEGR14:7

for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) sec) holds

( - (((id Z) ^) (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) )

( - (((id Z) ^) (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) )

proof end;

::f.x=-1/x*cosec.x

theorem Th8: :: INTEGR14:8

for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) cosec) holds

( - (((id Z) ^) (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) )

( - (((id Z) ^) (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) )

proof end;

::f.x = -cosec.(sin.x)

theorem Th9: :: INTEGR14:9

for Z being open Subset of REAL st Z c= dom (cosec * sin) holds

( - (cosec * sin) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) )

( - (cosec * sin) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) )

proof end;

::f.x=-sec.(cot.x)

theorem Th10: :: INTEGR14:10

for Z being open Subset of REAL st Z c= dom (sec * cot) holds

( - (sec * cot) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) )

( - (sec * cot) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) )

proof end;

::f.x=-cosec.(tan.x)

theorem Th11: :: INTEGR14:11

for Z being open Subset of REAL st Z c= dom (cosec * tan) holds

( - (cosec * tan) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) )

( - (cosec * tan) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) )

proof end;

::f.x=-cot.x*sec.x

theorem Th12: :: INTEGR14:12

for Z being open Subset of REAL st Z c= dom (cot (#) sec) holds

( - (cot (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) )

( - (cot (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) )

proof end;

::f.x=-cot.x*cosec.x

theorem Th13: :: INTEGR14:13

for Z being open Subset of REAL st Z c= dom (cot (#) cosec) holds

( - (cot (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) )

( - (cot (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) )

proof end;

::f.x=-cos.x * cot.x

theorem Th14: :: INTEGR14:14

for Z being open Subset of REAL st Z c= dom (cos (#) cot) holds

( - (cos (#) cot) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) )

( - (cos (#) cot) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) )

proof end;

::f.x=sin.(1/x)/(x^2*(cos.(1/x))^2)

theorem :: INTEGR14:15

for A being non empty closed_interval Subset of REAL

for f 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 = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) & Z c= dom (sec * ((id Z) ^)) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (sec * ((id Z) ^))) . (upper_bound A)) - ((- (sec * ((id Z) ^))) . (lower_bound A))

for f 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 = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) & Z c= dom (sec * ((id Z) ^)) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (sec * ((id Z) ^))) . (upper_bound A)) - ((- (sec * ((id Z) ^))) . (lower_bound A))

proof end;

::f.x=cos.(1/x)/(x^2*(sin.(1/x))^2)

theorem :: INTEGR14:16

for A being non empty closed_interval Subset of REAL

for f 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 = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) & Z c= dom (cosec * ((id Z) ^)) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cosec * ((id Z) ^)) . (upper_bound A)) - ((cosec * ((id Z) ^)) . (lower_bound A))

for f 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 = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) & Z c= dom (cosec * ((id Z) ^)) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cosec * ((id Z) ^)) . (upper_bound A)) - ((cosec * ((id Z) ^)) . (lower_bound A))

proof end;

::f.x=exp_R.x*sin.(exp_R.x)/(cos.(exp_R.x))^2

theorem :: INTEGR14:17

for A being non empty closed_interval Subset of REAL

for f 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 = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) & Z c= dom (sec * exp_R) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sec * exp_R) . (upper_bound A)) - ((sec * exp_R) . (lower_bound A))

for f 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 = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) & Z c= dom (sec * exp_R) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sec * exp_R) . (upper_bound A)) - ((sec * exp_R) . (lower_bound A))

proof end;

::f.x=exp_R.x*cos.(exp_R.x)/(sin.(exp_R.x))^2

theorem :: INTEGR14:18

for A being non empty closed_interval Subset of REAL

for f 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 = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) & Z c= dom (cosec * exp_R) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cosec * exp_R)) . (upper_bound A)) - ((- (cosec * exp_R)) . (lower_bound A))

for f 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 = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) & Z c= dom (cosec * exp_R) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cosec * exp_R)) . (upper_bound A)) - ((- (cosec * exp_R)) . (lower_bound A))

proof end;

::f.x=sin.(ln.x)/(x*(cos.(ln.x))^2)

theorem :: INTEGR14:19

for A being non empty closed_interval Subset of REAL

for f 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 = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) & Z c= dom (sec * ln) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sec * ln) . (upper_bound A)) - ((sec * ln) . (lower_bound A))

for f 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 = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) & Z c= dom (sec * ln) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sec * ln) . (upper_bound A)) - ((sec * ln) . (lower_bound A))

proof end;

::f.x=cos.(ln.x)/(x*(sin.(ln.x))^2)

theorem :: INTEGR14:20

for A being non empty closed_interval Subset of REAL

for f 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 = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) & Z c= dom (cosec * ln) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cosec * ln)) . (upper_bound A)) - ((- (cosec * ln)) . (lower_bound A))

for f 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 = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) & Z c= dom (cosec * ln) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cosec * ln)) . (upper_bound A)) - ((- (cosec * ln)) . (lower_bound A))

proof end;

::f.x=exp_R.(sec.x)*sin.x/(cos.x)^2

theorem :: INTEGR14:21

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,REAL

for Z being open Subset of REAL st A c= Z & f = (exp_R * sec) (#) (sin / (cos ^2)) & Z = dom f & f | A is continuous holds

integral (f,A) = ((exp_R * sec) . (upper_bound A)) - ((exp_R * sec) . (lower_bound A))

for f being PartFunc of REAL,REAL

for Z being open Subset of REAL st A c= Z & f = (exp_R * sec) (#) (sin / (cos ^2)) & Z = dom f & f | A is continuous holds

integral (f,A) = ((exp_R * sec) . (upper_bound A)) - ((exp_R * sec) . (lower_bound A))

proof end;

::f.x=exp_R.(cosec.x)*cos.x/(sin.x)^2

theorem :: INTEGR14:22

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,REAL

for Z being open Subset of REAL st A c= Z & f = (exp_R * cosec) (#) (cos / (sin ^2)) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (exp_R * cosec)) . (upper_bound A)) - ((- (exp_R * cosec)) . (lower_bound A))

for f being PartFunc of REAL,REAL

for Z being open Subset of REAL st A c= Z & f = (exp_R * cosec) (#) (cos / (sin ^2)) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (exp_R * cosec)) . (upper_bound A)) - ((- (exp_R * cosec)) . (lower_bound A))

proof end;

::f.x=tan.x

theorem :: INTEGR14:23

for A being non empty closed_interval Subset of REAL

for Z being open Subset of REAL st A c= Z & Z c= dom (ln * sec) & Z = dom tan & tan | A is continuous holds

integral (tan,A) = ((ln * sec) . (upper_bound A)) - ((ln * sec) . (lower_bound A))

for Z being open Subset of REAL st A c= Z & Z c= dom (ln * sec) & Z = dom tan & tan | A is continuous holds

integral (tan,A) = ((ln * sec) . (upper_bound A)) - ((ln * sec) . (lower_bound A))

proof end;

::f.x=-cot.x

theorem :: INTEGR14:24

for A being non empty closed_interval Subset of REAL

for Z being open Subset of REAL st A c= Z & Z c= dom (ln * cosec) & Z = dom cot & (- cot) | A is continuous holds

integral ((- cot),A) = ((ln * cosec) . (upper_bound A)) - ((ln * cosec) . (lower_bound A))

for Z being open Subset of REAL st A c= Z & Z c= dom (ln * cosec) & Z = dom cot & (- cot) | A is continuous holds

integral ((- cot),A) = ((ln * cosec) . (upper_bound A)) - ((ln * cosec) . (lower_bound A))

proof end;

::f.x=cot.x

theorem :: INTEGR14:25

for A being non empty closed_interval Subset of REAL

for Z being open Subset of REAL st A c= Z & Z c= dom (ln * cosec) & Z = dom cot & cot | A is continuous holds

integral (cot,A) = ((- (ln * cosec)) . (upper_bound A)) - ((- (ln * cosec)) . (lower_bound A))

for Z being open Subset of REAL st A c= Z & Z c= dom (ln * cosec) & Z = dom cot & cot | A is continuous holds

integral (cot,A) = ((- (ln * cosec)) . (upper_bound A)) - ((- (ln * cosec)) . (lower_bound A))

proof end;

::f.x=n*sin.x/(cos.x) #Z (n+1)

theorem :: INTEGR14:26

for n being Nat

for A being non empty closed_interval Subset of REAL

for f 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 = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * sec) & 1 <= n & Z = dom f & f | A is continuous holds

integral (f,A) = (((#Z n) * sec) . (upper_bound A)) - (((#Z n) * sec) . (lower_bound A))

for A being non empty closed_interval Subset of REAL

for f 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 = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * sec) & 1 <= n & Z = dom f & f | A is continuous holds

integral (f,A) = (((#Z n) * sec) . (upper_bound A)) - (((#Z n) * sec) . (lower_bound A))

proof end;

::f.x=n*cos.x/(sin.x) #Z (n+1)

theorem :: INTEGR14:27

for n being Nat

for A being non empty closed_interval Subset of REAL

for f 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 = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * cosec) & 1 <= n & Z = dom f & f | A is continuous holds

integral (f,A) = ((- ((#Z n) * cosec)) . (upper_bound A)) - ((- ((#Z n) * cosec)) . (lower_bound A))

for A being non empty closed_interval Subset of REAL

for f 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 = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * cosec) & 1 <= n & Z = dom f & f | A is continuous holds

integral (f,A) = ((- ((#Z n) * cosec)) . (upper_bound A)) - ((- ((#Z n) * cosec)) . (lower_bound A))

proof end;

::f.x=exp_R.x/cos.x+exp_R.x*sin.x/(cos.x)^2

theorem :: INTEGR14:28

for A being non empty closed_interval Subset of REAL

for f 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 = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (exp_R (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((exp_R (#) sec) . (upper_bound A)) - ((exp_R (#) sec) . (lower_bound A))

for f 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 = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (exp_R (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((exp_R (#) sec) . (upper_bound A)) - ((exp_R (#) sec) . (lower_bound A))

proof end;

::f.x=exp_R.x/sin.x-exp_R.x*cos.x/(sin.x)^2

theorem :: INTEGR14:29

for A being non empty closed_interval Subset of REAL

for f 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 = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (exp_R (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((exp_R (#) cosec) . (upper_bound A)) - ((exp_R (#) cosec) . (lower_bound A))

for f 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 = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (exp_R (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((exp_R (#) cosec) . (upper_bound A)) - ((exp_R (#) cosec) . (lower_bound A))

proof end;

::f.x=(sin.(a*x)-(cos.(a*x))^2)/(cos.(a*x))^2

theorem :: INTEGR14:30

for a being Real

for A being non empty closed_interval Subset of REAL

for f, f1 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 = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) & Z c= dom (((1 / a) (#) (sec * f1)) - (id Z)) & ( for x being Real st x in Z holds

( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((((1 / a) (#) (sec * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (sec * f1)) - (id Z)) . (lower_bound A))

for A being non empty closed_interval Subset of REAL

for f, f1 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 = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) & Z c= dom (((1 / a) (#) (sec * f1)) - (id Z)) & ( for x being Real st x in Z holds

( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((((1 / a) (#) (sec * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (sec * f1)) - (id Z)) . (lower_bound A))

proof end;

::f.x=(cos.(a*x)-(sin.(a*x))^2)/(sin.(a*x))^2

theorem :: INTEGR14:31

for a being Real

for A being non empty closed_interval Subset of REAL

for f, f1 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 = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) & Z c= dom (((- (1 / a)) (#) (cosec * f1)) - (id Z)) & ( for x being Real st x in Z holds

( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (lower_bound A))

for A being non empty closed_interval Subset of REAL

for f, f1 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 = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) & Z c= dom (((- (1 / a)) (#) (cosec * f1)) - (id Z)) & ( for x being Real st x in Z holds

( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (lower_bound A))

proof end;

::f.x=1/cos.x/x+ln.x*sin.x/(cos.x)^2

theorem :: INTEGR14:32

for A being non empty closed_interval Subset of REAL

for f 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 = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (ln (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((ln (#) sec) . (upper_bound A)) - ((ln (#) sec) . (lower_bound A))

for f 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 = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (ln (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((ln (#) sec) . (upper_bound A)) - ((ln (#) sec) . (lower_bound A))

proof end;

::f.x=1/sin.x/x-ln.x*cos.x/(sin.x)^2

theorem :: INTEGR14:33

for A being non empty closed_interval Subset of REAL

for f 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 = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (ln (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((ln (#) cosec) . (upper_bound A)) - ((ln (#) cosec) . (lower_bound A))

for f 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 = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (ln (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((ln (#) cosec) . (upper_bound A)) - ((ln (#) cosec) . (lower_bound A))

proof end;

::f.x=1/cos.x/x^2-sin.x/x/(cos.x)^2

theorem :: INTEGR14:34

for A being non empty closed_interval Subset of REAL

for f 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 = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) & Z c= dom (((id Z) ^) (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (((id Z) ^) (#) sec)) . (upper_bound A)) - ((- (((id Z) ^) (#) sec)) . (lower_bound A))

for f 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 = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) & Z c= dom (((id Z) ^) (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (((id Z) ^) (#) sec)) . (upper_bound A)) - ((- (((id Z) ^) (#) sec)) . (lower_bound A))

proof end;

::f.x=1/sin.x/x^2+cos.x/x/(sin.x)^2

theorem :: INTEGR14:35

for A being non empty closed_interval Subset of REAL

for f 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 = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) & Z c= dom (((id Z) ^) (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (((id Z) ^) (#) cosec)) . (upper_bound A)) - ((- (((id Z) ^) (#) cosec)) . (lower_bound A))

for f 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 = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) & Z c= dom (((id Z) ^) (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (((id Z) ^) (#) cosec)) . (upper_bound A)) - ((- (((id Z) ^) (#) cosec)) . (lower_bound A))

proof end;

::f.x=cos.x*sin.(sin.x)/(cos.(sin.x))^2

theorem :: INTEGR14:36

for A being non empty closed_interval Subset of REAL

for f 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 = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) & Z c= dom (sec * sin) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sec * sin) . (upper_bound A)) - ((sec * sin) . (lower_bound A))

for f 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 = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) & Z c= dom (sec * sin) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sec * sin) . (upper_bound A)) - ((sec * sin) . (lower_bound A))

proof end;

::f.x=sin.x*sin.(cos.x)/(cos.(cos.x))^2

theorem :: INTEGR14:37

for A being non empty closed_interval Subset of REAL

for f 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 = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ) & Z c= dom (sec * cos) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (sec * cos)) . (upper_bound A)) - ((- (sec * cos)) . (lower_bound A))

for f 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 = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ) & Z c= dom (sec * cos) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (sec * cos)) . (upper_bound A)) - ((- (sec * cos)) . (lower_bound A))

proof end;

::f.x=cos.x*cos.(sin.x)/(sin.(sin.x))^2

theorem :: INTEGR14:38

for A being non empty closed_interval Subset of REAL

for f 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 = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) & Z c= dom (cosec * sin) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cosec * sin)) . (upper_bound A)) - ((- (cosec * sin)) . (lower_bound A))

for f 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 = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) & Z c= dom (cosec * sin) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cosec * sin)) . (upper_bound A)) - ((- (cosec * sin)) . (lower_bound A))

proof end;

::f.x=sin.x*cos.(cos.x)/(sin.(cos.x))^2

theorem :: INTEGR14:39

for A being non empty closed_interval Subset of REAL

for f 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 = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) & Z c= dom (cosec * cos) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cosec * cos) . (upper_bound A)) - ((cosec * cos) . (lower_bound A))

for f 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 = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) & Z c= dom (cosec * cos) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cosec * cos) . (upper_bound A)) - ((cosec * cos) . (lower_bound A))

proof end;

::f.x=sin.(tan.x)/(cos.x)^2/(cos.(tan.x))^2

theorem :: INTEGR14:40

for A being non empty closed_interval Subset of REAL

for f 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 = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) & Z c= dom (sec * tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sec * tan) . (upper_bound A)) - ((sec * tan) . (lower_bound A))

for f 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 = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) & Z c= dom (sec * tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sec * tan) . (upper_bound A)) - ((sec * tan) . (lower_bound A))

proof end;

::f.x=sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2

theorem :: INTEGR14:41

for A being non empty closed_interval Subset of REAL

for f 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 = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) & Z c= dom (sec * cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (sec * cot)) . (upper_bound A)) - ((- (sec * cot)) . (lower_bound A))

for f 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 = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) & Z c= dom (sec * cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (sec * cot)) . (upper_bound A)) - ((- (sec * cot)) . (lower_bound A))

proof end;

::f.x= cos.(tan.x)/(cos.x)^2/(sin.(tan.x))^2

theorem :: INTEGR14:42

for A being non empty closed_interval Subset of REAL

for f 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 = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) & Z c= dom (cosec * tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cosec * tan)) . (upper_bound A)) - ((- (cosec * tan)) . (lower_bound A))

for f 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 = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) & Z c= dom (cosec * tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cosec * tan)) . (upper_bound A)) - ((- (cosec * tan)) . (lower_bound A))

proof end;

::f.x=cos.(cot.x)/(sin.x)^2/(sin.(cot.x))^2

theorem :: INTEGR14:43

for A being non empty closed_interval Subset of REAL

for f 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 = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) & Z c= dom (cosec * cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cosec * cot) . (upper_bound A)) - ((cosec * cot) . (lower_bound A))

for f 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 = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) & Z c= dom (cosec * cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cosec * cot) . (upper_bound A)) - ((cosec * cot) . (lower_bound A))

proof end;

::f.x=1/(cos.x)^2/cos.x+tan.x*sin.x/(cos.x)^2

theorem :: INTEGR14:44

for A being non empty closed_interval Subset of REAL

for f 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 = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (tan (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan (#) sec) . (upper_bound A)) - ((tan (#) sec) . (lower_bound A))

for f 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 = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (tan (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan (#) sec) . (upper_bound A)) - ((tan (#) sec) . (lower_bound A))

proof end;

::f.x=1/(sin.x)^2/cos.x-cot.x*sin.x/(cos.x)^2

theorem :: INTEGR14:45

for A being non empty closed_interval Subset of REAL

for f 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 = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (cot (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cot (#) sec)) . (upper_bound A)) - ((- (cot (#) sec)) . (lower_bound A))

for f 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 = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (cot (#) sec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cot (#) sec)) . (upper_bound A)) - ((- (cot (#) sec)) . (lower_bound A))

proof end;

::f.x=1/(cos.x)^2/sin.x-tan.x*cos.x/(sin.x)^2

theorem :: INTEGR14:46

for A being non empty closed_interval Subset of REAL

for f 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 = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (tan (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan (#) cosec) . (upper_bound A)) - ((tan (#) cosec) . (lower_bound A))

for f 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 = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (tan (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan (#) cosec) . (upper_bound A)) - ((tan (#) cosec) . (lower_bound A))

proof end;

::f.x=1/(sin.x)^2/sin.x+cot.x*cos.x/(sin.x)^2

theorem :: INTEGR14:47

for A being non empty closed_interval Subset of REAL

for f 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 = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (cot (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cot (#) cosec)) . (upper_bound A)) - ((- (cot (#) cosec)) . (lower_bound A))

for f 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 = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (cot (#) cosec) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cot (#) cosec)) . (upper_bound A)) - ((- (cot (#) cosec)) . (lower_bound A))

proof end;

::f.x=1/(cos.(cot.x))^2*(1/(sin.x)^2)

theorem :: INTEGR14:48

for A being non empty closed_interval Subset of REAL

for f 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 = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (tan * cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (tan * cot)) . (upper_bound A)) - ((- (tan * cot)) . (lower_bound A))

for f 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 = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (tan * cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (tan * cot)) . (upper_bound A)) - ((- (tan * cot)) . (lower_bound A))

proof end;

::f.x=1/(cos.(tan.x))^2 *(1/(cos.x)^2)

theorem :: INTEGR14:49

for A being non empty closed_interval Subset of REAL

for f 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 = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (tan * tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan * tan) . (upper_bound A)) - ((tan * tan) . (lower_bound A))

for f 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 = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (tan * tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan * tan) . (upper_bound A)) - ((tan * tan) . (lower_bound A))

proof end;

::f.x=(1/(sin.(cot.x))^2) *(1/(sin.x)^2)

theorem :: INTEGR14:50

for A being non empty closed_interval Subset of REAL

for f 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 = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (cot * cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cot * cot) . (upper_bound A)) - ((cot * cot) . (lower_bound A))

for f 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 = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (cot * cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cot * cot) . (upper_bound A)) - ((cot * cot) . (lower_bound A))

proof end;

::f.x=(1/(sin.(tan.x))^2)*(1/(cos.x)^2)

theorem :: INTEGR14:51

for A being non empty closed_interval Subset of REAL

for f 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 = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (cot * tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cot * tan)) . (upper_bound A)) - ((- (cot * tan)) . (lower_bound A))

for f 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 = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (cot * tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cot * tan)) . (upper_bound A)) - ((- (cot * tan)) . (lower_bound A))

proof end;

::f.x=1/(cos.x)^2+1/(sin.x)^2

theorem :: INTEGR14:52

for A being non empty closed_interval Subset of REAL

for f 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 = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) & Z c= dom (tan - cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan - cot) . (upper_bound A)) - ((tan - cot) . (lower_bound A))

for f 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 = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) & Z c= dom (tan - cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan - cot) . (upper_bound A)) - ((tan - cot) . (lower_bound A))

proof end;

::f.x=1/(cos.x)^2-1/(sin.x)^2

theorem :: INTEGR14:53

for A being non empty closed_interval Subset of REAL

for f 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 = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) & Z c= dom (tan + cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan + cot) . (upper_bound A)) - ((tan + cot) . (lower_bound A))

for f 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 = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) & Z c= dom (tan + cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((tan + cot) . (upper_bound A)) - ((tan + cot) . (lower_bound A))

proof end;

::f.x=cos.(sin.x)*cos.x

theorem :: INTEGR14:54

for A being non empty closed_interval Subset of REAL

for f 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 = (cos . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sin * sin) . (upper_bound A)) - ((sin * sin) . (lower_bound A))

for f 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 = (cos . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sin * sin) . (upper_bound A)) - ((sin * sin) . (lower_bound A))

proof end;

::f.x=cos.(cos.x)*sin.x

theorem :: INTEGR14:55

for A being non empty closed_interval Subset of REAL

for f 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 = (cos . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (sin * cos)) . (upper_bound A)) - ((- (sin * cos)) . (lower_bound A))

for f 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 = (cos . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (sin * cos)) . (upper_bound A)) - ((- (sin * cos)) . (lower_bound A))

proof end;

::f.x=sin.(sin.x)*cos.x

theorem :: INTEGR14:56

for A being non empty closed_interval Subset of REAL

for f 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 = (sin . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cos * sin)) . (upper_bound A)) - ((- (cos * sin)) . (lower_bound A))

for f 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 = (sin . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cos * sin)) . (upper_bound A)) - ((- (cos * sin)) . (lower_bound A))

proof end;

::f.x=sin.(cos.x)*sin.x

theorem :: INTEGR14:57

for A being non empty closed_interval Subset of REAL

for f 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 = (sin . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cos * cos) . (upper_bound A)) - ((cos * cos) . (lower_bound A))

for f 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 = (sin . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds

integral (f,A) = ((cos * cos) . (upper_bound A)) - ((cos * cos) . (lower_bound A))

proof end;

::f.x=cos.x+cos.x/(sin.x)^2

theorem :: INTEGR14:58

for A being non empty closed_interval Subset of REAL

for f 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 = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) & Z c= dom (cos (#) cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cos (#) cot)) . (upper_bound A)) - ((- (cos (#) cot)) . (lower_bound A))

for f 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 = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) & Z c= dom (cos (#) cot) & Z = dom f & f | A is continuous holds

integral (f,A) = ((- (cos (#) cot)) . (upper_bound A)) - ((- (cos (#) cot)) . (lower_bound A))

proof end;

::f.x=sin.x + sin.x/(cos.x)^2

theorem :: INTEGR14:59

for A being non empty closed_interval Subset of REAL

for f 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 = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) & Z c= dom (sin (#) tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sin (#) tan) . (upper_bound A)) - ((sin (#) tan) . (lower_bound A))

for f 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 = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) & Z c= dom (sin (#) tan) & Z = dom f & f | A is continuous holds

integral (f,A) = ((sin (#) tan) . (upper_bound A)) - ((sin (#) tan) . (lower_bound A))

proof end;