:: Integrability Formulas -- Part {III}
:: by Bo Li and Na Ma
::
:: Copyright (c) 2010-2018 Association of Mizar Users

Lm1: for Z being open Subset of REAL st 0 in Z holds
(id Z) " =

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)) ) )
proof end;

::f.x=-cosec.(exp_R.x)
theorem Th2: :: INTEGR14:2
for Z being open Subset of REAL st Z c= dom () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | Z) . x = (() * (cos . ())) / ((sin . ()) ^2) ) )
proof end;

:: f.x = -cosec.(ln.x)
theorem Th3: :: INTEGR14:3
for Z being open Subset of REAL st Z c= dom () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | 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 () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | Z) . x = ((exp_R . ()) * (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 () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | 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)) ) )
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)) ) )
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)) ) )
proof end;

::f.x = -cosec.(sin.x)
theorem Th9: :: INTEGR14:9
for Z being open Subset of REAL st Z c= dom () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | 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 () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | 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 () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | 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 () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | 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 () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | 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 () holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) | 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) ^))) . ()) - ((- (sec * ((id Z) ^))) . ())
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) ^)) . ()) - ((cosec * ((id Z) ^)) . ())
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 = (() * (sin . ())) / ((cos . ()) ^2) ) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,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 = (() * (cos . ())) / ((sin . ()) ^2) ) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 = () (#) (sin / ()) & Z = dom f & f | A is continuous holds
integral (f,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 = () (#) (cos / ()) & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom tan & tan | A is continuous holds
integral (tan,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 () & Z = dom cot & () | A is continuous holds
integral ((),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 () & Z = dom cot & cot | A is continuous holds
integral (cot,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) . ()) - (((#Z n) * sec) . ())
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)) . ()) - ((- ((#Z n) * cosec)) . ())
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 = (() / (cos . x)) + ((() * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,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 = (() / (sin . x)) - ((() * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,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)) . ()) - ((((1 / a) (#) (sec * f1)) - (id Z)) . ())
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)) . ()) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . ())
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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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)) . ()) - ((- (((id Z) ^) (#) sec)) . ())
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)) . ()) - ((- (((id Z) ^) (#) cosec)) . ())
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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,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) = (() . ()) - (() . ())
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) = ((- ()) . ()) - ((- ()) . ())
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) = ((- ()) . ()) - ((- ()) . ())
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) = (() . ()) - (() . ())
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 () & Z = dom f & f | A is continuous holds
integral (f,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 () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;