:: Integrability Formulas -- Part {II}
:: by Bo Li , Na Ma and Xiquan Liang
::
:: Copyright (c) 2010-2017 Association of Mizar Users

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

proof end;

Lm2: right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;

:: f.x = 1/(sin.x*cos.x)
theorem :: INTEGR13:1
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 = () ^ & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

:: f.x = -1/(sin.x*cos.x)
theorem :: INTEGR13:2
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 = - (() ^) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=2 * exp_R.x * sin.x
theorem :: INTEGR13:3
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 = 2 (#) () & Z c= dom (exp_R (#) ()) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) ()) . ()) - ((exp_R (#) ()) . ())
proof end;

::f.x=2 * exp_R.x * cos.x
theorem :: INTEGR13:4
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 = 2 (#) () & Z c= dom (exp_R (#) ()) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) ()) . ()) - ((exp_R (#) ()) . ())
proof end;

::f.x=cos.x-sin.x
theorem :: INTEGR13:5
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z & Z = dom () & () | A is continuous holds
integral ((),A) = (() . ()) - (() . ())
proof end;

::f.x=cos.x+sin.x
theorem :: INTEGR13:6
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z & Z = dom () & () | A is continuous holds
integral ((),A) = (() . ()) - (() . ())
proof end;

theorem Th7: :: INTEGR13:7
for Z being open Subset of REAL st Z c= dom ((- (1 / 2)) (#) (() / exp_R)) holds
( (- (1 / 2)) (#) (() / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) (() / exp_R)) `| Z) . x = (sin . x) / () ) )
proof end;

::f.x=sin.x/exp_R.x
theorem :: INTEGR13:8
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 / exp_R & Z c= dom ((- (1 / 2)) (#) (() / exp_R)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((- (1 / 2)) (#) (() / exp_R)) . ()) - (((- (1 / 2)) (#) (() / exp_R)) . ())
proof end;

theorem Th9: :: INTEGR13:9
for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) (() / exp_R)) holds
( (1 / 2) (#) (() / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (() / exp_R)) `| Z) . x = (cos . x) / () ) )
proof end;

::f.x=cos.x/exp_R.x
theorem :: INTEGR13:10
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 / exp_R & Z c= dom ((1 / 2) (#) (() / exp_R)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / 2) (#) (() / exp_R)) . ()) - (((1 / 2) (#) (() / exp_R)) . ())
proof end;

::f.x=exp_R.x*(sin.x+cos.x)
theorem :: INTEGR13:11
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 (#) () & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=exp_R.x*(cos.x-sin.x)
theorem :: INTEGR13:12
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 (#) () & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=-sin.x/cos.x/x^2+1/x/(cos.x)^2
theorem :: INTEGR13:13
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 & f1 = #Z 2 & f = (- (() / f1)) + (((id Z) ^) / ()) & Z c= dom (((id Z) ^) (#) tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) ^) (#) tan) . ()) - ((((id Z) ^) (#) tan) . ())
proof end;

::f.x=-cos.x/sin.x/x^2-1/x/(sin.x)^2
theorem :: INTEGR13:14
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 & f = (- (() / f1)) - (((id Z) ^) / ()) & f1 = #Z 2 & Z c= dom (((id Z) ^) (#) cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) ^) (#) cot) . ()) - ((((id Z) ^) (#) cot) . ())
proof end;

::f.x=sin.x/cos.x/x+ln.x/(cos.x)^2
theorem :: INTEGR13: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 & f = (() / (id Z)) + (ln / ()) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=cos.x/sin.x/x-ln.x/(sin.x)^2
theorem :: INTEGR13: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 & f = (() / (id Z)) - (ln / ()) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=tan.x/x+ln.x/(cos.x)^2
theorem :: INTEGR13: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 & f = (tan / (id Z)) + (ln / ()) & Z c= dom () & Z c= dom tan & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=cot.x/x-ln.x/(sin.x)^2
theorem :: INTEGR13: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 & f = (cot / (id Z)) - (ln / ()) & Z c= dom () & Z c= dom cot & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=arctan.x/x+ln.x/(1+x^2)
theorem :: INTEGR13:19
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
f1 . x = 1 ) & f = (arctan / (id Z)) + (ln / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=arccot.x/x-ln.x/(1+x^2)
theorem :: INTEGR13:20
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
f1 . x = 1 ) & f = (arccot / (id Z)) - (ln / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=exp_R.(tan.x)/(cos.x)^2
theorem :: INTEGR13: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 = () / () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=-exp_R.(cot.x)/(sin.x)^2
theorem :: INTEGR13: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 = - (() / ()) & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

theorem Th23: :: INTEGR13:23
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 . (cot . x)) / ((sin . x) ^2) ) )
proof end;

::f.x=exp_R.(cot.x)/(sin.x)^2
theorem :: INTEGR13:24
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 = () / () & Z = dom f & f | A is continuous holds
integral (f,A) = ((- ()) . ()) - ((- ()) . ())
proof end;

::f.x=1/(x*(cos.(ln.x))^2)
theorem :: INTEGR13:25
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 = ((id Z) (#) (() ^2)) ^ & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x= -1/(x*(sin.(ln.x))^2)
theorem :: INTEGR13:26
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 = - (((id Z) (#) (() ^2)) ^) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

theorem Th27: :: INTEGR13:27
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 / (x * ((sin . (ln . x)) ^2)) ) )
proof end;

::f.x= 1/(x*(sin.(ln.x))^2)
theorem :: INTEGR13: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 & f = ((id Z) (#) (() ^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))^2
theorem :: INTEGR13: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 & f = exp_R / (() ^2) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=-exp_R.x/(sin.(exp_R.x))^2
theorem :: INTEGR13:30
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 / (() ^2)) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

theorem Th31: :: INTEGR13:31
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 . ()) ^2) ) )
proof end;

::f.x=exp_R.x/(sin.(exp_R.x))^2
theorem :: INTEGR13: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 & f = exp_R / (() ^2) & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = ((- ()) . ()) - ((- ()) . ())
proof end;

::f.x=-1/(x^2*(cos.(1/x))^2)
theorem :: INTEGR13: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 / ((x ^2) * ((cos . (1 / x)) ^2))) ) & Z c= dom (tan * ((id Z) ^)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan * ((id Z) ^)) . ()) - ((tan * ((id Z) ^)) . ())
proof end;

theorem Th34: :: INTEGR13:34
for Z being open Subset of REAL st Z c= dom (tan * ((id Z) ^)) holds
( - (tan * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (tan * ((id Z) ^))) `| Z) . x = 1 / ((x ^2) * ((cos . (1 / x)) ^2)) ) )
proof end;

::f.x=1/(x^2*(cos.(1/x))^2)
theorem :: INTEGR13: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 / ((x ^2) * ((cos . (1 / x)) ^2)) ) & Z c= dom (tan * ((id Z) ^)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (tan * ((id Z) ^))) . ()) - ((- (tan * ((id Z) ^))) . ())
proof end;

::f.x=1/(x^2*(sin.(1/x))^2)
theorem :: INTEGR13: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 = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) ) & Z c= dom (cot * ((id Z) ^)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((cot * ((id Z) ^)) . ()) - ((cot * ((id Z) ^)) . ())
proof end;

::f.x=1/((1+x^2)*arctan.x)
theorem :: INTEGR13:37
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
( f1 . x = 1 & arctan . x > 0 ) ) & f = ((f1 + (#Z 2)) (#) arctan) ^ & Z c= ].(- 1),1.[ & Z c= dom () & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=n*(arctan.x) #Z (n-1) / (1+x^2)
theorem :: INTEGR13:38
for n being Element of NAT
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 & f = n (#) (((#Z (n - 1)) * arctan) / (f1 + (#Z 2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z c= dom ((#Z n) * arctan) & Z = dom f & f | A is continuous holds
integral (f,A) = (((#Z n) * arctan) . ()) - (((#Z n) * arctan) . ())
proof end;

::f.x=-n*(arccot.x) #Z (n-1) / (1+x^2)
theorem :: INTEGR13:39
for n being Element of NAT
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
f1 . x = 1 ) & f = - (n (#) (((#Z (n - 1)) * arccot) / (f1 + (#Z 2)))) & Z c= ].(- 1),1.[ & Z c= dom ((#Z n) * arccot) & Z = dom f & f | A is continuous holds
integral (f,A) = (((#Z n) * arccot) . ()) - (((#Z n) * arccot) . ())
proof end;

theorem Th40: :: INTEGR13:40
for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((#Z n) * arccot) & Z c= ].(- 1),1.[ holds
( - ((#Z n) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * arccot)) `| Z) . x = (n * (() #Z (n - 1))) / (1 + (x ^2)) ) )
proof end;

::f.x=n*(arccot.x) #Z (n-1) / (1+x^2)
theorem :: INTEGR13:41
for n being Element of NAT
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
f1 . x = 1 ) & f = n (#) (((#Z (n - 1)) * arccot) / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z c= dom ((#Z n) * arccot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- ((#Z n) * arccot)) . ()) - ((- ((#Z n) * arccot)) . ())
proof end;

::f.x=arctan.x / (1+x^2)
theorem :: INTEGR13:42
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
f1 . x = 1 ) & f = arctan / (f1 + (#Z 2)) & Z c= ].(- 1),1.[ & Z c= dom ((#Z 2) * arctan) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / 2) (#) ((#Z 2) * arctan)) . ()) - (((1 / 2) (#) ((#Z 2) * arctan)) . ())
proof end;

::f.x=-arccot.x / (1+x^2)
theorem :: INTEGR13:43
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
f1 . x = 1 ) & f = - (arccot / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z c= dom ((#Z 2) * arccot) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / 2) (#) ((#Z 2) * arccot)) . ()) - (((1 / 2) (#) ((#Z 2) * arccot)) . ())
proof end;

theorem Th44: :: INTEGR13:44
for Z being open Subset of REAL st Z c= dom ((#Z 2) * arccot) & Z c= ].(- 1),1.[ holds
( - ((1 / 2) (#) ((#Z 2) * arccot)) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = () / (1 + (x ^2)) ) )
proof end;

::f.x=arccot.x / (1+x^2)
theorem :: INTEGR13:45
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
f1 . x = 1 ) & f = arccot / (f1 + (#Z 2)) & Z c= ].(- 1),1.[ & Z c= dom ((#Z 2) * arccot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- ((1 / 2) (#) ((#Z 2) * arccot))) . ()) - ((- ((1 / 2) (#) ((#Z 2) * arccot))) . ())
proof end;

::f.x=arctan.x + x/(1+x^2)
theorem :: INTEGR13:46
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
f1 . x = 1 ) & f = arctan + ((id Z) / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral (f,A) = (((id Z) (#) arctan) . ()) - (((id Z) (#) arctan) . ())
proof end;

::f.x=arccot.x - x/(1+x^2)
theorem :: INTEGR13:47
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
f1 . x = 1 ) & f = arccot - ((id Z) / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral (f,A) = (((id Z) (#) arccot) . ()) - (((id Z) (#) arccot) . ())
proof end;

::f.x=exp_R.(arctan.x)/(1+x^2)
theorem :: INTEGR13:48
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 & Z c= ].(- 1),1.[ & f = () / (f1 + (#Z 2)) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

::f.x=-exp_R.(arccot.x)/(1+x^2)
theorem :: INTEGR13:49
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 & Z c= ].(- 1),1.[ & f = - (() / (f1 + (#Z 2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous holds
integral (f,A) = (() . ()) - (() . ())
proof end;

theorem Th50: :: INTEGR13:50
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( - () is_differentiable_on Z & ( for x being Real st x in Z holds
((- ()) `| Z) . x = (exp_R . ()) / (1 + (x ^2)) ) )
proof end;

::f.x=exp_R.(arccot.x)/(1+x^2)
theorem :: INTEGR13:51
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 & Z c= ].(- 1),1.[ & f = () / (f1 + (#Z 2)) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- ()) . ()) - ((- ()) . ())
proof end;

::f.x=x/(1+x^2)
theorem :: INTEGR13:52
for A being non empty 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 & Z c= dom (ln * (f1 + f2)) & f = (id Z) / (f1 + f2) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / 2) (#) (ln * (f1 + f2))) . ()) - (((1 / 2) (#) (ln * (f1 + f2))) . ())
proof end;

::f.x=x/(a*(1+(x/a)^2))
theorem :: INTEGR13:53
for a being Real
for A being non empty closed_interval Subset of REAL
for f, h, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (ln * (f1 + f2)) & f = (id Z) / (a (#) (f1 + f2)) & ( for x being Real st x in Z holds
( h . x = x / a & f1 . x = 1 ) ) & a <> 0 & f2 = (#Z 2) * h & Z = dom f & f | A is continuous holds
integral (f,A) = (((a / 2) (#) (ln * (f1 + f2))) . ()) - (((a / 2) (#) (ln * (f1 + f2))) . ())
proof end;

theorem Th54: :: INTEGR13:54
for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) arctan) & Z c= ].(- 1),1.[ holds
( - (((id Z) ^) (#) arctan) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) arctan)) `| Z) . x = (() / (x ^2)) - (1 / (x * (1 + (x ^2)))) ) )
proof end;

theorem Th55: :: INTEGR13:55
for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) arccot) & Z c= ].(- 1),1.[ holds
( - (((id Z) ^) (#) arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) arccot)) `| Z) . x = (() / (x ^2)) + (1 / (x * (1 + (x ^2)))) ) )
proof end;

::f.x=arctan.x/(x^2)-1/(x*(1+x^2))
theorem :: INTEGR13:56
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
f1 . x = 1 ) & f = (arctan / (#Z 2)) - (((id Z) (#) (f1 + (#Z 2))) ^) & Z c= dom (((id Z) ^) (#) arctan) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (((id Z) ^) (#) arctan)) . ()) - ((- (((id Z) ^) (#) arctan)) . ())
proof end;

::f.x=arccot.x/(x^2)+1/(x*(1+x^2))
theorem :: INTEGR13:57
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
f1 . x = 1 ) & f = (arccot / (#Z 2)) + (((id Z) (#) (f1 + (#Z 2))) ^) & Z c= dom (((id Z) ^) (#) arccot) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (((id Z) ^) (#) arccot)) . ()) - ((- (((id Z) ^) (#) arccot)) . ())
proof end;