:: Integrability Formulas -- Part {III}
::  by Bo Li and Na Ma
::
:: Received February 4, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RELAT_1, FUNCT_1, ARYTM_1, SIN_COS, VALUED_1, NAT_1, INTEGRA1,
      FDIFF_1, SQUARE_1, ARYTM_3, ORDINAL2, PREPOWER, REAL_1, PARTFUN1,
      TAYLOR_1, CARD_1, ORDINAL4, RCOMP_1, INTEGRA5, XXREAL_0, SIN_COS4,
      SUBSET_1, XBOOLE_0, TARSKI, NUMBERS, XXREAL_2, SEQ_4, MEASURE5;
 notations TARSKI, XBOOLE_0, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS, VALUED_1,
      XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1,
      PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, FCONT_1, SQUARE_1, INTEGRA5,
      PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2, FDIFF_9, SIN_COS4, SEQ_4;
 constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER,
      INTEGRA5, SEQ_4, PARTFUN2, RFUNCT_1, FDIFF_9, SIN_COS4, RELSET_1,
      INTEGRA1, COMSEQ_2, BINOP_2;
 registrations NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1, RCOMP_1, RELSET_1,
      MEASURE5, XREAL_0, SQUARE_1, PREPOWER;
 requirements NUMERALS, SUBSET, ARITHM;


begin :: Differentiation Formulas

 reserve a,x for Real;
 reserve n for Nat;
 reserve A for non empty closed_interval Subset of REAL;
 reserve f,f1 for PartFunc of REAL,REAL;
 reserve Z for open Subset of REAL;

theorem :: INTEGR14:1
  Z c= dom (sec*((id Z)^)) implies (-sec*((id Z)^)) is_differentiable_on Z &
  for x st x in Z holds
  ((-sec*((id Z)^))`|Z).x = sin.(1/x)/(x^2*(cos.(1/x))^2);

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

theorem :: INTEGR14:2
  Z c= dom (cosec*exp_R) implies -cosec*exp_R is_differentiable_on Z &
  for x st x in Z holds ((-cosec*exp_R)`|Z).x
  = exp_R.x*cos.(exp_R.x)/(sin.(exp_R.x))^2;

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

theorem :: INTEGR14:3
  Z c= dom (cosec*ln) implies -cosec*ln is_differentiable_on Z &
  for x st x in Z holds ((-cosec*ln)`|Z).x = cos.(ln.x)/(x*(sin.(ln.x))^2);

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

theorem :: INTEGR14:4
  Z c= dom (exp_R*cosec) implies -exp_R*cosec is_differentiable_on Z
  & for x st x in Z holds
  ((-exp_R*cosec)`|Z).x = exp_R.(cosec.x)*cos.x/(sin.x)^2;

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

theorem :: INTEGR14:5
  Z c= dom (ln*cosec) implies -ln*cosec is_differentiable_on Z
  & for x st x in Z holds ((-ln*cosec)`|Z).x = cot.x;

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

theorem :: INTEGR14:6
  Z c= dom (( #Z n)*cosec) & 1<=n
  implies -( #Z n)*cosec is_differentiable_on Z & for x st x in Z holds
  ((-( #Z n)*cosec)`|Z).x = n*cos.x/(sin.x) #Z (n+1);

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

theorem :: INTEGR14:7
  Z c= dom ((id Z)^(#)sec)
  implies (-(id Z)^(#)sec) is_differentiable_on Z & for x st x in Z holds
  ((-(id Z)^(#)sec)`|Z).x = 1/cos.x/x^2-sin.x/x/(cos.x)^2;

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

theorem :: INTEGR14:8
 Z c= dom ((id Z)^(#)cosec)
 implies (-(id Z)^(#)cosec) is_differentiable_on Z & for x st x in Z holds
 ((-(id Z)^(#)cosec)`|Z).x = 1/sin.x/x^2+cos.x/x/(sin.x)^2;

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

theorem :: INTEGR14:9
  Z c= dom (cosec*sin) implies -cosec*sin is_differentiable_on Z &
  for x st x in Z holds ((-cosec*sin)`|Z).x
  = cos.x*cos.(sin.x)/(sin.(sin.x))^2;

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

theorem :: INTEGR14:10
  Z c= dom (sec*cot) implies -sec*cot is_differentiable_on Z &
  for x st x in Z holds ((-sec*cot)`|Z).x
  = sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2;

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

theorem :: INTEGR14:11
  Z c= dom (cosec*tan) implies -cosec*tan is_differentiable_on Z &
  for x st x in Z holds ((-cosec*tan)`|Z).x
  = cos.(tan.x)/(cos.x)^2/(sin.(tan.x))^2;

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

theorem :: INTEGR14:12
  Z c= dom (cot(#)sec) implies (-cot(#)sec) is_differentiable_on Z &
  for x st x in Z holds
  ((-cot(#)sec)`|Z).x = 1/(sin.x)^2/cos.x-cot.x*sin.x/(cos.x)^2;

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

theorem :: INTEGR14:13
  Z c= dom (cot(#)cosec) implies (-cot(#)cosec) is_differentiable_on Z &
  for x st x in Z holds
  ((-cot(#)cosec)`|Z).x = 1/(sin.x)^2/sin.x+cot.x*cos.x/(sin.x)^2;

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

theorem :: INTEGR14:14
  Z c= dom (cos (#) cot) implies (-cos (#) cot) is_differentiable_on Z &
  for x st x in Z holds((-cos (#) cot)`|Z).x = cos.x+cos.x/(sin.x)^2;

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

theorem :: INTEGR14:15
A c= Z & (for x 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
implies integral(f,A)=(-sec*((id Z)^)).(upper_bound A)-
(-sec*((id Z)^)).(lower_bound A);

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

theorem :: INTEGR14:16
A c= Z & (for x 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
implies integral(f,A)=(cosec*((id Z)^)).(upper_bound A)-
(cosec*((id Z)^)).(lower_bound A);

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

theorem :: INTEGR14:17
A c= Z & (for x 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
implies integral(f,A)=(sec*exp_R).(upper_bound A)-(sec*exp_R).(lower_bound A);

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

theorem :: INTEGR14:18
A c= Z & (for x 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 implies
integral(f,A)=(-cosec*exp_R).(upper_bound A)-(-cosec*exp_R).(lower_bound A);

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

theorem :: INTEGR14:19
A c= Z & (for x 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
implies integral(f,A)=(sec*ln).(upper_bound A)-(sec*ln).(lower_bound A);

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

theorem :: INTEGR14:20
A c= Z & (for x 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
implies integral(f,A)=(-cosec*ln).(upper_bound A)-(-cosec*ln).(lower_bound A);

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

theorem :: INTEGR14:21
A c= Z & f=(exp_R*sec)(#)(sin/cos^2) & Z = dom f & f|A is continuous
implies integral(f,A)=(exp_R*sec).(upper_bound A)-(exp_R*sec).(lower_bound A);

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

theorem :: INTEGR14:22
A c= Z & f=(exp_R*cosec)(#)(cos/sin^2) & Z = dom f & f|A is continuous
implies integral(f,A)=(-exp_R*cosec).(upper_bound A)-
(-exp_R*cosec).(lower_bound A);

::f.x=tan.x

theorem :: INTEGR14:23
A c= Z & Z c= dom (ln*sec) & Z = dom tan & tan|A is continuous
implies integral(tan,A)=(ln*sec).(upper_bound A)-(ln*sec).(lower_bound A);

::f.x=-cot.x

theorem :: INTEGR14:24
A c= Z & Z c= dom (ln*cosec) & Z = dom cot & (-cot)|A is continuous
implies integral((-cot),A)=(ln*cosec).(upper_bound A)-
(ln*cosec).(lower_bound A);

::f.x=cot.x

theorem :: INTEGR14:25
A c= Z & Z c= dom (ln*cosec) & Z = dom cot & cot|A is continuous
implies integral(cot,A)=(-ln*cosec).(upper_bound A)-(-ln*cosec).(lower_bound A)
;

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

theorem :: INTEGR14:26
A c= Z & (for x 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
implies integral(f,A)=(( #Z n)*sec).(upper_bound A)-
(( #Z n)*sec).(lower_bound A);

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

theorem :: INTEGR14:27
A c= Z & (for x 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
implies integral(f,A)=(-( #Z n)*cosec).(upper_bound A)-
(-( #Z n)*cosec).(lower_bound A);

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

theorem :: INTEGR14:28
A c= Z & (for x 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
implies integral(f,A)=(exp_R(#)sec).(upper_bound A)-
(exp_R(#)sec).(lower_bound A);

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

theorem :: INTEGR14:29
A c= Z & (for x 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
implies integral(f,A)=(exp_R(#)cosec).(upper_bound A)-
(exp_R(#)cosec).(lower_bound A);

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

theorem :: INTEGR14:30
A c= Z & (for x 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 st x in Z holds f1.x=a*x & a<>0)
& Z = dom f & f|A is continuous implies
integral(f,A)=((1/a)(#)(sec*f1)-id Z).(upper_bound A)-
((1/a)(#)(sec*f1)-id Z).(lower_bound A);

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

theorem :: INTEGR14:31
A c= Z & (for x 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 st x in Z holds f1.x=a*x & a<>0)
& Z = dom f & f|A is continuous implies
integral(f,A)=((-1/a)(#)(cosec*f1)-id Z).(upper_bound A)
             -((-1/a)(#)(cosec*f1)-id Z).(lower_bound A);

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

theorem :: INTEGR14:32
A c= Z & (for x 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 implies
integral(f,A)=(ln(#)sec).(upper_bound A)-(ln(#)sec).(lower_bound A);

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

theorem :: INTEGR14:33
A c= Z & (for x 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 implies
integral(f,A)=(ln(#)cosec).(upper_bound A)-(ln(#)cosec).(lower_bound A);

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

theorem :: INTEGR14:34
A c= Z & (for x 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 implies
integral(f,A)=(-(id Z)^(#)sec).(upper_bound A)-(-(id Z)^(#)sec).(lower_bound A)
;

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

theorem :: INTEGR14:35
A c= Z & (for x 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 implies
integral(f,A)=(-(id Z)^(#)cosec).(upper_bound A)-
(-(id Z)^(#)cosec).(lower_bound A);

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

theorem :: INTEGR14:36
A c= Z & (for x 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
implies integral(f,A)=(sec*sin).(upper_bound A)-(sec*sin).(lower_bound A);

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

theorem :: INTEGR14:37
A c= Z & (for x 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
implies integral(f,A)=(-sec*cos).(upper_bound A)-(-sec*cos).(lower_bound A);

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

theorem :: INTEGR14:38
A c= Z & (for x 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
implies integral(f,A)=(-cosec*sin).(upper_bound A)-(-cosec*sin).(lower_bound A)
;

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

theorem :: INTEGR14:39
A c= Z & (for x 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
implies integral(f,A)=(cosec*cos).(upper_bound A)-(cosec*cos).(lower_bound A);

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

theorem :: INTEGR14:40
A c= Z & (for x 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
implies integral(f,A)=(sec*tan).(upper_bound A)-(sec*tan).(lower_bound A);

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

theorem :: INTEGR14:41
A c= Z & (for x 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
implies integral(f,A)=(-sec*cot).(upper_bound A)-(-sec*cot).(lower_bound A);

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

theorem :: INTEGR14:42
A c= Z & (for x 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
implies integral(f,A)=(-cosec*tan).(upper_bound A)-(-cosec*tan).(lower_bound A)
;

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

theorem :: INTEGR14:43
A c= Z & (for x 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
implies integral(f,A)=(cosec*cot).(upper_bound A)-(cosec*cot).(lower_bound A);

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

theorem :: INTEGR14:44
A c= Z & (for x 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
implies integral(f,A)=(tan(#)sec).(upper_bound A)-(tan(#)sec).(lower_bound A);

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

theorem :: INTEGR14:45
A c= Z & (for x 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
implies integral(f,A)=(-cot(#)sec).(upper_bound A)-(-cot(#)sec).(lower_bound A)
;

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

theorem :: INTEGR14:46
A c= Z & (for x 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
implies integral(f,A)=(tan(#)cosec).(upper_bound A)-
(tan(#)cosec).(lower_bound A);

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

theorem :: INTEGR14:47
A c= Z & (for x 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
implies integral(f,A)=(-cot(#)cosec).(upper_bound A)-
(-cot(#)cosec).(lower_bound A);

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

theorem :: INTEGR14:48
A c= Z & (for x 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
implies integral(f,A)=(-tan*cot).(upper_bound A)-(-tan*cot).(lower_bound A);

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

theorem :: INTEGR14:49
A c= Z & (for x 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
implies integral(f,A)=(tan*tan).(upper_bound A)-(tan*tan).(lower_bound A);

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

theorem :: INTEGR14:50
A c= Z & (for x 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
implies integral(f,A)=(cot*cot).(upper_bound A)-(cot*cot).(lower_bound A);

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

theorem :: INTEGR14:51
A c= Z & (for x 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
implies integral(f,A)=(-cot*tan).(upper_bound A)-(-cot*tan).(lower_bound A);

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

theorem :: INTEGR14:52
A c= Z & (for x 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
implies integral(f,A)=(tan-cot).(upper_bound A)-(tan-cot).(lower_bound A);

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

theorem :: INTEGR14:53
A c= Z & (for x 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
implies integral(f,A)=(tan+cot).(upper_bound A)-(tan+cot).(lower_bound A);

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

theorem :: INTEGR14:54
A c= Z & (for x st x in Z holds f.x=cos.(sin.x)*cos.x)
 & Z = dom f & f|A is continuous
implies integral(f,A)=(sin*sin).(upper_bound A)-(sin*sin).(lower_bound A);

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

theorem :: INTEGR14:55
A c= Z & (for x st x in Z holds f.x=cos.(cos.x)*sin.x)
 & Z = dom f & f|A is continuous
implies integral(f,A)=(-sin*cos).(upper_bound A)-(-sin*cos).(lower_bound A);

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

theorem :: INTEGR14:56
  A c= Z & (for x st x in Z holds f.x=sin.(sin.x)*cos.x) &
  Z = dom f & f|A is continuous
  implies integral(f,A)=(-cos*sin).(upper_bound A)-(-cos*sin).(lower_bound A);

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

theorem :: INTEGR14:57
A c= Z & (for x st x in Z holds f.x=sin.(cos.x)*sin.x)
 & Z = dom f & f|A is continuous
implies integral(f,A)=(cos*cos).(upper_bound A)-(cos*cos).(lower_bound A);

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

theorem :: INTEGR14:58
A c= Z & (for x 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
implies integral(f,A)=(-cos (#) cot).(upper_bound A)-
(-cos (#) cot).(lower_bound A);

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

theorem :: INTEGR14:59
A c= Z & (for x 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
implies integral(f,A)=(sin (#) tan).(upper_bound A)-
(sin (#) tan).(lower_bound A);