:: INTEGR13 semantic presentation

begin

         Lm1:  for Z being open Subset of REAL st 0 in Z holds
(id Z) " {0} = {0}
proof
let Z be open Subset of REAL; ::_thesis: ( 0 in Z implies (id Z) " {0} = {0} )
assume A1: 0 in Z ; ::_thesis: (id Z) " {0} = {0}
thus  (id Z) " {0} c= {0} :: according to XBOOLE_0:def_10 ::_thesis: {0} c= (id Z) " {0}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (id Z) " {0} or x in {0} )
assume A2: x in (id Z) " {0} ; ::_thesis: x in {0}
then  x in dom (id Z) by FUNCT_1:def_7;
then A3: x in Z ;
 (id Z) . x in {0} by A2, FUNCT_1:def_7;
hence  x in {0} by A3, FUNCT_1:18; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {0} or x in (id Z) " {0} )
assume  x in {0} ; ::_thesis: x in (id Z) " {0}
then A4: x = 0 by TARSKI:def_1;
then  (id Z) . x = 0 by A1, FUNCT_1:18;
then A5: (id Z) . x in {0} by TARSKI:def_1;
 x in dom (id Z) by A1, A4;
hence  x in (id Z) " {0} by A5, FUNCT_1:def_7; ::_thesis: verum
end;

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

Lm3:  ( - 1 is Real & - (1 / 2) is Real & 1 / 2 is Real )
;

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 = (sin (#) cos) ^ & Z c= dom (ln * tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln * tan) . (upper_bound A)) - ((ln * tan) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (sin (#) cos) ^ & Z c= dom (ln * tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln * tan) . (upper_bound A)) - ((ln * tan) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = (sin (#) cos) ^ & Z c= dom (ln * tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln * tan) . (upper_bound A)) - ((ln * tan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = (sin (#) cos) ^ & Z c= dom (ln * tan) & Z = dom f & f | A is continuous implies integral (f,A) = ((ln * tan) . (upper_bound A)) - ((ln * tan) . (lower_bound A)) )
assume A1: ( A c= Z & f = (sin (#) cos) ^ & Z c= dom (ln * tan) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((ln * tan) . (upper_bound A)) - ((ln * tan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: ln * tan is_differentiable_on Z by A1, FDIFF_8:18;
A4: for x being Real st x in Z holds
f . x = 1 / ((sin . x) * (cos . x))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = 1 / ((sin . x) * (cos . x)) )
assume  x in Z ; ::_thesis: f . x = 1 / ((sin . x) * (cos . x))
then ((sin (#) cos) ^) . x = 1 / ((sin (#) cos) . x) by A1, RFUNCT_1:def_2
.= 1 / ((sin . x) * (cos . x)) by VALUED_1:5 ;
hence  f . x = 1 / ((sin . x) * (cos . x)) by A1; ::_thesis: verum
end;
A5: for x being Real st x in dom ((ln * tan) `| Z) holds
((ln * tan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((ln * tan) `| Z) implies ((ln * tan) `| Z) . x = f . x )
assume  x in dom ((ln * tan) `| Z) ; ::_thesis: ((ln * tan) `| Z) . x = f . x
then A6: x in Z by A3, FDIFF_1:def_7;
then ((ln * tan) `| Z) . x = 1 / ((sin . x) * (cos . x)) by A1, FDIFF_8:18
.= f . x by A4, A6 ;
hence  ((ln * tan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((ln * tan) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (ln * tan) `| Z = f by A5, PARTFUN1:5;
hence  integral (f,A) = ((ln * tan) . (upper_bound A)) - ((ln * tan) . (lower_bound A)) by A1, A2, FDIFF_8:18, INTEGRA5:13; ::_thesis: verum
end;

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 = - ((sin (#) cos) ^) & Z c= dom (ln * cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln * cot) . (upper_bound A)) - ((ln * cot) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = - ((sin (#) cos) ^) & Z c= dom (ln * cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln * cot) . (upper_bound A)) - ((ln * cot) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = - ((sin (#) cos) ^) & Z c= dom (ln * cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln * cot) . (upper_bound A)) - ((ln * cot) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = - ((sin (#) cos) ^) & Z c= dom (ln * cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((ln * cot) . (upper_bound A)) - ((ln * cot) . (lower_bound A)) )
assume A1: ( A c= Z & f = - ((sin (#) cos) ^) & Z c= dom (ln * cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((ln * cot) . (upper_bound A)) - ((ln * cot) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: ln * cot is_differentiable_on Z by A1, FDIFF_8:19;
A4: Z = dom ((sin (#) cos) ^) by A1, VALUED_1:8;
A5: for x being Real st x in Z holds
f . x = - (1 / ((sin . x) * (cos . x)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = - (1 / ((sin . x) * (cos . x))) )
assume A6: x in Z ; ::_thesis: f . x = - (1 / ((sin . x) * (cos . x)))
(- ((sin (#) cos) ^)) . x = - (((sin (#) cos) ^) . x) by VALUED_1:8
.= - (1 / ((sin (#) cos) . x)) by A4, A6, RFUNCT_1:def_2
.= - (1 / ((sin . x) * (cos . x))) by VALUED_1:5 ;
hence  f . x = - (1 / ((sin . x) * (cos . x))) by A1; ::_thesis: verum
end;
A7: for x being Real st x in dom ((ln * cot) `| Z) holds
((ln * cot) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((ln * cot) `| Z) implies ((ln * cot) `| Z) . x = f . x )
assume  x in dom ((ln * cot) `| Z) ; ::_thesis: ((ln * cot) `| Z) . x = f . x
then A8: x in Z by A3, FDIFF_1:def_7;
then ((ln * cot) `| Z) . x = - (1 / ((sin . x) * (cos . x))) by A1, FDIFF_8:19
.= f . x by A5, A8 ;
hence  ((ln * cot) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((ln * cot) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (ln * cot) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((ln * cot) . (upper_bound A)) - ((ln * cot) . (lower_bound A)) by A1, A2, FDIFF_8:19, INTEGRA5:13; ::_thesis: verum
end;

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 (#) (exp_R (#) sin) & Z c= dom (exp_R (#) (sin - cos)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) (sin - cos)) . (upper_bound A)) - ((exp_R (#) (sin - cos)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = 2 (#) (exp_R (#) sin) & Z c= dom (exp_R (#) (sin - cos)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) (sin - cos)) . (upper_bound A)) - ((exp_R (#) (sin - cos)) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = 2 (#) (exp_R (#) sin) & Z c= dom (exp_R (#) (sin - cos)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) (sin - cos)) . (upper_bound A)) - ((exp_R (#) (sin - cos)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = 2 (#) (exp_R (#) sin) & Z c= dom (exp_R (#) (sin - cos)) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R (#) (sin - cos)) . (upper_bound A)) - ((exp_R (#) (sin - cos)) . (lower_bound A)) )
assume A1: ( A c= Z & f = 2 (#) (exp_R (#) sin) & Z c= dom (exp_R (#) (sin - cos)) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R (#) (sin - cos)) . (upper_bound A)) - ((exp_R (#) (sin - cos)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: exp_R (#) (sin - cos) is_differentiable_on Z by A1, FDIFF_7:40;
A4: for x being Real st x in Z holds
f . x = (2 * (exp_R . x)) * (sin . x)
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (2 * (exp_R . x)) * (sin . x) )
assume  x in Z ; ::_thesis: f . x = (2 * (exp_R . x)) * (sin . x)
(2 (#) (exp_R (#) sin)) . x = 2 * ((exp_R (#) sin) . x) by VALUED_1:6
.= 2 * ((exp_R . x) * (sin . x)) by VALUED_1:5 ;
hence  f . x = (2 * (exp_R . x)) * (sin . x) by A1; ::_thesis: verum
end;
A5: for x being Real st x in dom ((exp_R (#) (sin - cos)) `| Z) holds
((exp_R (#) (sin - cos)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((exp_R (#) (sin - cos)) `| Z) implies ((exp_R (#) (sin - cos)) `| Z) . x = f . x )
assume  x in dom ((exp_R (#) (sin - cos)) `| Z) ; ::_thesis: ((exp_R (#) (sin - cos)) `| Z) . x = f . x
then A6: x in Z by A3, FDIFF_1:def_7;
then ((exp_R (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) by A1, FDIFF_7:40
.= f . x by A4, A6 ;
hence  ((exp_R (#) (sin - cos)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((exp_R (#) (sin - cos)) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (exp_R (#) (sin - cos)) `| Z = f by A5, PARTFUN1:5;
hence  integral (f,A) = ((exp_R (#) (sin - cos)) . (upper_bound A)) - ((exp_R (#) (sin - cos)) . (lower_bound A)) by A1, A2, FDIFF_7:40, INTEGRA5:13; ::_thesis: verum
end;

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 (#) (exp_R (#) cos) & Z c= dom (exp_R (#) (sin + cos)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) (sin + cos)) . (upper_bound A)) - ((exp_R (#) (sin + cos)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = 2 (#) (exp_R (#) cos) & Z c= dom (exp_R (#) (sin + cos)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) (sin + cos)) . (upper_bound A)) - ((exp_R (#) (sin + cos)) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = 2 (#) (exp_R (#) cos) & Z c= dom (exp_R (#) (sin + cos)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) (sin + cos)) . (upper_bound A)) - ((exp_R (#) (sin + cos)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = 2 (#) (exp_R (#) cos) & Z c= dom (exp_R (#) (sin + cos)) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R (#) (sin + cos)) . (upper_bound A)) - ((exp_R (#) (sin + cos)) . (lower_bound A)) )
assume A1: ( A c= Z & f = 2 (#) (exp_R (#) cos) & Z c= dom (exp_R (#) (sin + cos)) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R (#) (sin + cos)) . (upper_bound A)) - ((exp_R (#) (sin + cos)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: exp_R (#) (sin + cos) is_differentiable_on Z by A1, FDIFF_7:41;
A4: for x being Real st x in Z holds
f . x = (2 * (exp_R . x)) * (cos . x)
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (2 * (exp_R . x)) * (cos . x) )
assume  x in Z ; ::_thesis: f . x = (2 * (exp_R . x)) * (cos . x)
(2 (#) (exp_R (#) cos)) . x = 2 * ((exp_R (#) cos) . x) by VALUED_1:6
.= 2 * ((exp_R . x) * (cos . x)) by VALUED_1:5 ;
hence  f . x = (2 * (exp_R . x)) * (cos . x) by A1; ::_thesis: verum
end;
A5: for x being Real st x in dom ((exp_R (#) (sin + cos)) `| Z) holds
((exp_R (#) (sin + cos)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((exp_R (#) (sin + cos)) `| Z) implies ((exp_R (#) (sin + cos)) `| Z) . x = f . x )
assume  x in dom ((exp_R (#) (sin + cos)) `| Z) ; ::_thesis: ((exp_R (#) (sin + cos)) `| Z) . x = f . x
then A6: x in Z by A3, FDIFF_1:def_7;
then ((exp_R (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) by A1, FDIFF_7:41
.= f . x by A6, A4 ;
hence  ((exp_R (#) (sin + cos)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((exp_R (#) (sin + cos)) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (exp_R (#) (sin + cos)) `| Z = f by A5, PARTFUN1:5;
hence  integral (f,A) = ((exp_R (#) (sin + cos)) . (upper_bound A)) - ((exp_R (#) (sin + cos)) . (lower_bound A)) by A1, A2, FDIFF_7:41, INTEGRA5:13; ::_thesis: verum
end;

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 (cos - sin) & (cos - sin) | A is continuous holds
integral ((cos - sin),A) = ((sin + cos) . (upper_bound A)) - ((sin + cos) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & Z = dom (cos - sin) & (cos - sin) | A is continuous holds
integral ((cos - sin),A) = ((sin + cos) . (upper_bound A)) - ((sin + cos) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & Z = dom (cos - sin) & (cos - sin) | A is continuous implies integral ((cos - sin),A) = ((sin + cos) . (upper_bound A)) - ((sin + cos) . (lower_bound A)) )
assume A1: ( A c= Z & Z = dom (cos - sin) & (cos - sin) | A is continuous ) ; ::_thesis: integral ((cos - sin),A) = ((sin + cos) . (upper_bound A)) - ((sin + cos) . (lower_bound A))
then A2: ( cos - sin is_integrable_on A & (cos - sin) | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom cos) /\ (dom sin) by A1, VALUED_1:12;
then A3: Z c= dom (sin + cos) by VALUED_1:def_1;
then A4: sin + cos is_differentiable_on Z by FDIFF_7:38;
A5: for x being Real st x in dom ((sin + cos) `| Z) holds
((sin + cos) `| Z) . x = (cos - sin) . x
proof
let x be Real; ::_thesis: ( x in dom ((sin + cos) `| Z) implies ((sin + cos) `| Z) . x = (cos - sin) . x )
assume  x in dom ((sin + cos) `| Z) ; ::_thesis: ((sin + cos) `| Z) . x = (cos - sin) . x
then A6: x in Z by A4, FDIFF_1:def_7;
then ((sin + cos) `| Z) . x = (cos . x) - (sin . x) by A3, FDIFF_7:38
.= (cos - sin) . x by A1, A6, VALUED_1:13 ;
hence  ((sin + cos) `| Z) . x = (cos - sin) . x ; ::_thesis: verum
end;
 dom ((sin + cos) `| Z) = dom (cos - sin) by A1, A4, FDIFF_1:def_7;
then  (sin + cos) `| Z = cos - sin by A5, PARTFUN1:5;
hence  integral ((cos - sin),A) = ((sin + cos) . (upper_bound A)) - ((sin + cos) . (lower_bound A)) by A1, A2, A3, FDIFF_7:38, INTEGRA5:13; ::_thesis: verum
end;

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 (cos + sin) & (cos + sin) | A is continuous holds
integral ((cos + sin),A) = ((sin - cos) . (upper_bound A)) - ((sin - cos) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & Z = dom (cos + sin) & (cos + sin) | A is continuous holds
integral ((cos + sin),A) = ((sin - cos) . (upper_bound A)) - ((sin - cos) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & Z = dom (cos + sin) & (cos + sin) | A is continuous implies integral ((cos + sin),A) = ((sin - cos) . (upper_bound A)) - ((sin - cos) . (lower_bound A)) )
assume A1: ( A c= Z & Z = dom (cos + sin) & (cos + sin) | A is continuous ) ; ::_thesis: integral ((cos + sin),A) = ((sin - cos) . (upper_bound A)) - ((sin - cos) . (lower_bound A))
then A2: ( cos + sin is_integrable_on A & (cos + sin) | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom cos) /\ (dom sin) by A1, VALUED_1:def_1;
then A3: Z c= dom (sin - cos) by VALUED_1:12;
then A4: sin - cos is_differentiable_on Z by FDIFF_7:39;
A5: for x being Real st x in dom ((sin - cos) `| Z) holds
((sin - cos) `| Z) . x = (cos + sin) . x
proof
let x be Real; ::_thesis: ( x in dom ((sin - cos) `| Z) implies ((sin - cos) `| Z) . x = (cos + sin) . x )
assume  x in dom ((sin - cos) `| Z) ; ::_thesis: ((sin - cos) `| Z) . x = (cos + sin) . x
then A6: x in Z by A4, FDIFF_1:def_7;
then ((sin - cos) `| Z) . x = (cos . x) + (sin . x) by A3, FDIFF_7:39
.= (cos + sin) . x by A1, A6, VALUED_1:def_1 ;
hence  ((sin - cos) `| Z) . x = (cos + sin) . x ; ::_thesis: verum
end;
 dom ((sin - cos) `| Z) = dom (cos + sin) by A1, A4, FDIFF_1:def_7;
then  (sin - cos) `| Z = cos + sin by A5, PARTFUN1:5;
hence  integral ((cos + sin),A) = ((sin - cos) . (upper_bound A)) - ((sin - cos) . (lower_bound A)) by A1, A2, A3, FDIFF_7:39, INTEGRA5:13; ::_thesis: verum
end;

theorem Th7: :: INTEGR13:7
for Z being open Subset of REAL st Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) holds
( (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) implies ( (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ) ) )
assume A1: Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) ; ::_thesis: ( (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ) )
then A2: Z c= dom ((sin + cos) / exp_R) by VALUED_1:def_5;
then  Z c= (dom (sin + cos)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def_1;
then A3: Z c= dom (sin + cos) by XBOOLE_1:18;
then A4: ( sin + cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + cos) `| Z) . x = (cos . x) - (sin . x) ) ) by FDIFF_7:38;
A5: (sin + cos) / exp_R is_differentiable_on Z by A2, FDIFF_7:42;
then A6: (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z by FDIFF_2:19;
 for x being Real st x in Z holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x)
proof
let x be Real; ::_thesis: ( x in Z implies (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) )
assume A7: x in Z ; ::_thesis: (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x)
A8: exp_R is_differentiable_in x by SIN_COS:65;
A9: sin + cos is_differentiable_in x by A4, A7, FDIFF_1:9;
A10: (sin + cos) . x = (sin . x) + (cos . x) by VALUED_1:1;
A11: exp_R . x <> 0 by SIN_COS:54;
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (- (1 / 2)) * (diff (((sin + cos) / exp_R),x)) by A1, A5, A7, FDIFF_1:20
.= (- (1 / 2)) * ((((diff ((sin + cos),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin + cos) . x))) / ((exp_R . x) ^2)) by A8, A9, A11, FDIFF_2:14
.= (- (1 / 2)) * ((((((sin + cos) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin + cos) . x))) / ((exp_R . x) ^2)) by A4, A7, FDIFF_1:def_7
.= (- (1 / 2)) * (((((cos . x) - (sin . x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin + cos) . x))) / ((exp_R . x) ^2)) by A3, A7, FDIFF_7:38
.= (- (1 / 2)) * (((((cos . x) - (sin . x)) * (exp_R . x)) - ((exp_R . x) * ((sin . x) + (cos . x)))) / ((exp_R . x) ^2)) by A10, SIN_COS:65
.= (- (1 / 2)) * ((- (2 * (sin . x))) * ((exp_R . x) / ((exp_R . x) * (exp_R . x))))
.= (- (1 / 2)) * ((- (2 * (sin . x))) * (((exp_R . x) / (exp_R . x)) / (exp_R . x))) by XCMPLX_1:78
.= (- (1 / 2)) * ((- (2 * (sin . x))) * (1 / (exp_R . x))) by A11, XCMPLX_1:60
.= (sin . x) / (exp_R . x) ;
hence  (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ; ::_thesis: verum
end;
hence  ( (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ) ) by A6; ::_thesis: verum
end;

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)) (#) ((sin + cos) / exp_R)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (upper_bound A)) - (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: 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)) (#) ((sin + cos) / exp_R)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (upper_bound A)) - (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = sin / exp_R & Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (upper_bound A)) - (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = sin / exp_R & Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) & Z = dom f & f | A is continuous implies integral (f,A) = (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (upper_bound A)) - (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (lower_bound A)) )
assume A1: ( A c= Z & f = sin / exp_R & Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (upper_bound A)) - (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z by A1, Th7;
A4: for x being Real st x in Z holds
f . x = (sin . x) / (exp_R . x) by A1, RFUNCT_1:def_1;
A5: for x being Real st x in dom (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) implies (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = f . x )
assume  x in dom (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) ; ::_thesis: (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = f . x
then A6: x in Z by A3, FDIFF_1:def_7;
then (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) by A1, Th7
.= f . x by A6, A4 ;
hence  (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  ((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z = f by A5, PARTFUN1:5;
hence  integral (f,A) = (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (upper_bound A)) - (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (lower_bound A)) by A1, A2, Th7, INTEGRA5:13; ::_thesis: verum
end;

theorem Th9: :: INTEGR13:9
for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((sin - cos) / exp_R)) holds
( (1 / 2) (#) ((sin - cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((1 / 2) (#) ((sin - cos) / exp_R)) implies ( (1 / 2) (#) ((sin - cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x) ) ) )
assume A1: Z c= dom ((1 / 2) (#) ((sin - cos) / exp_R)) ; ::_thesis: ( (1 / 2) (#) ((sin - cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x) ) )
then A2: Z c= dom ((sin - cos) / exp_R) by VALUED_1:def_5;
then  Z c= (dom (sin - cos)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def_1;
then A3: Z c= dom (sin - cos) by XBOOLE_1:18;
then A4: ( sin - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin - cos) `| Z) . x = (cos . x) + (sin . x) ) ) by FDIFF_7:39;
A5: (sin - cos) / exp_R is_differentiable_on Z by A2, FDIFF_7:43;
then A6: (1 / 2) (#) ((sin - cos) / exp_R) is_differentiable_on Z by FDIFF_2:19;
 for x being Real st x in Z holds
(((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x)
proof
let x be Real; ::_thesis: ( x in Z implies (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x) )
assume A7: x in Z ; ::_thesis: (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x)
A8: exp_R is_differentiable_in x by SIN_COS:65;
A9: sin - cos is_differentiable_in x by A4, A7, FDIFF_1:9;
A10: (sin - cos) . x = (sin . x) - (cos . x) by A3, A7, VALUED_1:13;
A11: exp_R . x <> 0 by SIN_COS:54;
(((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (1 / 2) * (diff (((sin - cos) / exp_R),x)) by A1, A5, A7, FDIFF_1:20
.= (1 / 2) * ((((diff ((sin - cos),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin - cos) . x))) / ((exp_R . x) ^2)) by A8, A9, A11, FDIFF_2:14
.= (1 / 2) * ((((((sin - cos) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin - cos) . x))) / ((exp_R . x) ^2)) by A4, A7, FDIFF_1:def_7
.= (1 / 2) * (((((cos . x) + (sin . x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin - cos) . x))) / ((exp_R . x) ^2)) by A3, A7, FDIFF_7:39
.= (1 / 2) * (((((cos . x) + (sin . x)) * (exp_R . x)) - ((exp_R . x) * ((sin . x) - (cos . x)))) / ((exp_R . x) ^2)) by A10, SIN_COS:65
.= (1 / 2) * ((2 * (cos . x)) * ((exp_R . x) / ((exp_R . x) * (exp_R . x))))
.= (1 / 2) * ((2 * (cos . x)) * (((exp_R . x) / (exp_R . x)) / (exp_R . x))) by XCMPLX_1:78
.= (1 / 2) * ((2 * (cos . x)) * (1 / (exp_R . x))) by A11, XCMPLX_1:60
.= (cos . x) / (exp_R . x) ;
hence  (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x) ; ::_thesis: verum
end;
hence  ( (1 / 2) (#) ((sin - cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x) ) ) by A6; ::_thesis: verum
end;

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) (#) ((sin - cos) / exp_R)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / 2) (#) ((sin - cos) / exp_R)) . (upper_bound A)) - (((1 / 2) (#) ((sin - cos) / exp_R)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: 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) (#) ((sin - cos) / exp_R)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / 2) (#) ((sin - cos) / exp_R)) . (upper_bound A)) - (((1 / 2) (#) ((sin - cos) / exp_R)) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = cos / exp_R & Z c= dom ((1 / 2) (#) ((sin - cos) / exp_R)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / 2) (#) ((sin - cos) / exp_R)) . (upper_bound A)) - (((1 / 2) (#) ((sin - cos) / exp_R)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = cos / exp_R & Z c= dom ((1 / 2) (#) ((sin - cos) / exp_R)) & Z = dom f & f | A is continuous implies integral (f,A) = (((1 / 2) (#) ((sin - cos) / exp_R)) . (upper_bound A)) - (((1 / 2) (#) ((sin - cos) / exp_R)) . (lower_bound A)) )
assume A1: ( A c= Z & f = cos / exp_R & Z c= dom ((1 / 2) (#) ((sin - cos) / exp_R)) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = (((1 / 2) (#) ((sin - cos) / exp_R)) . (upper_bound A)) - (((1 / 2) (#) ((sin - cos) / exp_R)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: (1 / 2) (#) ((sin - cos) / exp_R) is_differentiable_on Z by A1, Th9;
A4: for x being Real st x in Z holds
f . x = (cos . x) / (exp_R . x) by A1, RFUNCT_1:def_1;
A5: for x being Real st x in dom (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) holds
(((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) implies (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = f . x )
assume  x in dom (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) ; ::_thesis: (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = f . x
then A6: x in Z by A3, FDIFF_1:def_7;
then (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x) by A1, Th9
.= f . x by A4, A6 ;
hence  (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  ((1 / 2) (#) ((sin - cos) / exp_R)) `| Z = f by A5, PARTFUN1:5;
hence  integral (f,A) = (((1 / 2) (#) ((sin - cos) / exp_R)) . (upper_bound A)) - (((1 / 2) (#) ((sin - cos) / exp_R)) . (lower_bound A)) by A1, A2, Th9, INTEGRA5:13; ::_thesis: verum
end;

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 (#) (sin + cos) & Z c= dom (exp_R (#) sin) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = exp_R (#) (sin + cos) & Z c= dom (exp_R (#) sin) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = exp_R (#) (sin + cos) & Z c= dom (exp_R (#) sin) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = exp_R (#) (sin + cos) & Z c= dom (exp_R (#) sin) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A)) )
assume A1: ( A c= Z & f = exp_R (#) (sin + cos) & Z c= dom (exp_R (#) sin) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: exp_R (#) sin is_differentiable_on Z by A1, FDIFF_7:44;
 dom f = (dom exp_R) /\ (dom (sin + cos)) by A1, VALUED_1:def_4;
then A4: Z c= dom (sin + cos) by A1, XBOOLE_1:18;
A5: for x being Real st x in Z holds
f . x = (exp_R . x) * ((sin . x) + (cos . x))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (exp_R . x) * ((sin . x) + (cos . x)) )
assume A6: x in Z ; ::_thesis: f . x = (exp_R . x) * ((sin . x) + (cos . x))
(exp_R (#) (sin + cos)) . x = (exp_R . x) * ((sin + cos) . x) by VALUED_1:5
.= (exp_R . x) * ((sin . x) + (cos . x)) by A4, A6, VALUED_1:def_1 ;
hence  f . x = (exp_R . x) * ((sin . x) + (cos . x)) by A1; ::_thesis: verum
end;
A7: for x being Real st x in dom ((exp_R (#) sin) `| Z) holds
((exp_R (#) sin) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((exp_R (#) sin) `| Z) implies ((exp_R (#) sin) `| Z) . x = f . x )
assume  x in dom ((exp_R (#) sin) `| Z) ; ::_thesis: ((exp_R (#) sin) `| Z) . x = f . x
then A8: x in Z by A3, FDIFF_1:def_7;
then ((exp_R (#) sin) `| Z) . x = (exp_R . x) * ((sin . x) + (cos . x)) by A1, FDIFF_7:44
.= f . x by A5, A8 ;
hence  ((exp_R (#) sin) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((exp_R (#) sin) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (exp_R (#) sin) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A)) by A1, A2, FDIFF_7:44, INTEGRA5:13; ::_thesis: verum
end;

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 (#) (cos - sin) & Z c= dom (exp_R (#) cos) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = exp_R (#) (cos - sin) & Z c= dom (exp_R (#) cos) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = exp_R (#) (cos - sin) & Z c= dom (exp_R (#) cos) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = exp_R (#) (cos - sin) & Z c= dom (exp_R (#) cos) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A)) )
assume A1: ( A c= Z & f = exp_R (#) (cos - sin) & Z c= dom (exp_R (#) cos) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: exp_R (#) cos is_differentiable_on Z by A1, FDIFF_7:45;
 dom f = (dom exp_R) /\ (dom (cos - sin)) by A1, VALUED_1:def_4;
then A4: Z c= dom (cos - sin) by A1, XBOOLE_1:18;
A5: for x being Real st x in Z holds
f . x = (exp_R . x) * ((cos . x) - (sin . x))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (exp_R . x) * ((cos . x) - (sin . x)) )
assume A6: x in Z ; ::_thesis: f . x = (exp_R . x) * ((cos . x) - (sin . x))
(exp_R (#) (cos - sin)) . x = (exp_R . x) * ((cos - sin) . x) by VALUED_1:5
.= (exp_R . x) * ((cos . x) - (sin . x)) by A4, A6, VALUED_1:13 ;
hence  f . x = (exp_R . x) * ((cos . x) - (sin . x)) by A1; ::_thesis: verum
end;
A7: for x being Real st x in dom ((exp_R (#) cos) `| Z) holds
((exp_R (#) cos) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((exp_R (#) cos) `| Z) implies ((exp_R (#) cos) `| Z) . x = f . x )
assume  x in dom ((exp_R (#) cos) `| Z) ; ::_thesis: ((exp_R (#) cos) `| Z) . x = f . x
then A8: x in Z by A3, FDIFF_1:def_7;
then ((exp_R (#) cos) `| Z) . x = (exp_R . x) * ((cos . x) - (sin . x)) by A1, FDIFF_7:45
.= f . x by A5, A8 ;
hence  ((exp_R (#) cos) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((exp_R (#) cos) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (exp_R (#) cos) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A)) by A1, A2, FDIFF_7:45, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGR13:13
for A being non empty closed_interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f1 = #Z 2 & f = (- ((sin / cos) / f1)) + (((id Z) ^) / (cos ^2)) & Z c= dom (((id Z) ^) (#) tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) ^) (#) tan) . (upper_bound A)) - ((((id Z) ^) (#) tan) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f1 = #Z 2 & f = (- ((sin / cos) / f1)) + (((id Z) ^) / (cos ^2)) & Z c= dom (((id Z) ^) (#) tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) ^) (#) tan) . (upper_bound A)) - ((((id Z) ^) (#) tan) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f1 = #Z 2 & f = (- ((sin / cos) / f1)) + (((id Z) ^) / (cos ^2)) & Z c= dom (((id Z) ^) (#) tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) ^) (#) tan) . (upper_bound A)) - ((((id Z) ^) (#) tan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f1 = #Z 2 & f = (- ((sin / cos) / f1)) + (((id Z) ^) / (cos ^2)) & Z c= dom (((id Z) ^) (#) tan) & Z = dom f & f | A is continuous implies integral (f,A) = ((((id Z) ^) (#) tan) . (upper_bound A)) - ((((id Z) ^) (#) tan) . (lower_bound A)) )
assume A1: ( A c= Z & f1 = #Z 2 & f = (- ((sin / cos) / f1)) + (((id Z) ^) / (cos ^2)) & Z c= dom (((id Z) ^) (#) tan) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((((id Z) ^) (#) tan) . (upper_bound A)) - ((((id Z) ^) (#) tan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
set g = id Z;
 Z c= (dom ((id Z) ^)) /\ (dom tan) by A1, VALUED_1:def_4;
then A3: Z c= dom ((id Z) ^) by XBOOLE_1:18;
A4: not 0 in Z
proof
assume A5: 0 in Z ; ::_thesis: contradiction
dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2
.= (dom (id Z)) \ {0} by Lm1, A5 ;
then  not 0 in {0} by A5, A3, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
then A6: ((id Z) ^) (#) tan is_differentiable_on Z by A1, FDIFF_8:34;
 dom f = (dom (- ((sin / cos) / f1))) /\ (dom (((id Z) ^) / (cos ^2))) by A1, VALUED_1:def_1;
then  ( dom f c= dom (- ((sin / cos) / f1)) & dom f c= dom (((id Z) ^) / (cos ^2)) ) by XBOOLE_1:18;
then A7: ( Z c= dom ((sin / cos) / f1) & Z c= dom (((id Z) ^) / (cos ^2)) ) by A1, VALUED_1:8;
 dom ((sin / cos) / f1) = (dom (sin / cos)) /\ ((dom f1) \ (f1 " {0})) by RFUNCT_1:def_1;
then A8: Z c= dom (sin / cos) by A7, XBOOLE_1:18;
 dom (((id Z) ^) / (cos ^2)) c= (dom ((id Z) ^)) /\ ((dom (cos ^2)) \ ((cos ^2) " {0})) by RFUNCT_1:def_1;
then  ( dom (((id Z) ^) / (cos ^2)) c= dom ((id Z) ^) & dom (((id Z) ^) / (cos ^2)) c= (dom (cos ^2)) \ ((cos ^2) " {0}) ) by XBOOLE_1:18;
then A9: ( Z c= dom ((id Z) ^) & Z c= (dom (cos ^2)) \ ((cos ^2) " {0}) ) by A7, XBOOLE_1:1;
A10: for x being Real st x in Z holds
f . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) )
assume A11: x in Z ; ::_thesis: f . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2))
then ((- ((sin / cos) / f1)) + (((id Z) ^) / (cos ^2))) . x = ((- ((sin / cos) / f1)) . x) + ((((id Z) ^) / (cos ^2)) . x) by A1, VALUED_1:def_1
.= (- (((sin / cos) / f1) . x)) + ((((id Z) ^) / (cos ^2)) . x) by VALUED_1:8
.= (- (((sin / cos) . x) / (f1 . x))) + ((((id Z) ^) / (cos ^2)) . x) by A11, A7, RFUNCT_1:def_1
.= (- (((sin . x) * ((cos . x) ")) / (f1 . x))) + ((((id Z) ^) / (cos ^2)) . x) by A8, A11, RFUNCT_1:def_1
.= (- (((sin . x) / (cos . x)) / (f1 . x))) + ((((id Z) ^) . x) / ((cos ^2) . x)) by A7, A11, RFUNCT_1:def_1
.= (- (((sin . x) / (cos . x)) / (f1 . x))) + ((((id Z) . x) ") / ((cos ^2) . x)) by A9, A11, RFUNCT_1:def_2
.= (- (((sin . x) / (cos . x)) / (f1 . x))) + ((1 / x) / ((cos ^2) . x)) by A11, FUNCT_1:18
.= (- (((sin . x) / (cos . x)) / (f1 . x))) + ((1 / x) / ((cos . x) ^2)) by VALUED_1:11
.= (- (((sin . x) / (cos . x)) / (x #Z 2))) + ((1 / x) / ((cos . x) ^2)) by A1, TAYLOR_1:def_1
.= (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) by FDIFF_7:1 ;
hence  f . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) by A1; ::_thesis: verum
end;
A12: for x being Real st x in dom ((((id Z) ^) (#) tan) `| Z) holds
((((id Z) ^) (#) tan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((((id Z) ^) (#) tan) `| Z) implies ((((id Z) ^) (#) tan) `| Z) . x = f . x )
assume  x in dom ((((id Z) ^) (#) tan) `| Z) ; ::_thesis: ((((id Z) ^) (#) tan) `| Z) . x = f . x
then A13: x in Z by A6, FDIFF_1:def_7;
then ((((id Z) ^) (#) tan) `| Z) . x = (- (((sin . x) / (cos . x)) / (x ^2))) + ((1 / x) / ((cos . x) ^2)) by A4, A1, FDIFF_8:34
.= f . x by A13, A10 ;
hence  ((((id Z) ^) (#) tan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((((id Z) ^) (#) tan) `| Z) = dom f by A1, A6, FDIFF_1:def_7;
then  (((id Z) ^) (#) tan) `| Z = f by A12, PARTFUN1:5;
hence  integral (f,A) = ((((id Z) ^) (#) tan) . (upper_bound A)) - ((((id Z) ^) (#) tan) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13; ::_thesis: verum
end;

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 = (- ((cos / sin) / f1)) - (((id Z) ^) / (sin ^2)) & f1 = #Z 2 & Z c= dom (((id Z) ^) (#) cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) ^) (#) cot) . (upper_bound A)) - ((((id Z) ^) (#) cot) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (- ((cos / sin) / f1)) - (((id Z) ^) / (sin ^2)) & f1 = #Z 2 & Z c= dom (((id Z) ^) (#) cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) ^) (#) cot) . (upper_bound A)) - ((((id Z) ^) (#) cot) . (lower_bound A))
let f, f1 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = (- ((cos / sin) / f1)) - (((id Z) ^) / (sin ^2)) & f1 = #Z 2 & Z c= dom (((id Z) ^) (#) cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) ^) (#) cot) . (upper_bound A)) - ((((id Z) ^) (#) cot) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = (- ((cos / sin) / f1)) - (((id Z) ^) / (sin ^2)) & f1 = #Z 2 & Z c= dom (((id Z) ^) (#) cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((((id Z) ^) (#) cot) . (upper_bound A)) - ((((id Z) ^) (#) cot) . (lower_bound A)) )
assume A1: ( A c= Z & f = (- ((cos / sin) / f1)) - (((id Z) ^) / (sin ^2)) & f1 = #Z 2 & Z c= dom (((id Z) ^) (#) cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((((id Z) ^) (#) cot) . (upper_bound A)) - ((((id Z) ^) (#) cot) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
set g = id Z;
 Z c= dom (((id Z) ^) (#) cot) by A1;
then  Z c= (dom ((id Z) ^)) /\ (dom cot) by VALUED_1:def_4;
then A3: Z c= dom ((id Z) ^) by XBOOLE_1:18;
A4: not 0 in Z
proof
assume A5: 0 in Z ; ::_thesis: contradiction
dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2
.= (dom (id Z)) \ {0} by Lm1, A5 ;
then  not 0 in {0} by A5, A3, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
then A6: ((id Z) ^) (#) cot is_differentiable_on Z by A1, FDIFF_8:35;
 dom f = (dom (- ((cos / sin) / f1))) /\ (dom (((id Z) ^) / (sin ^2))) by A1, VALUED_1:12;
then A7: ( dom f c= dom (- ((cos / sin) / f1)) & dom f c= dom (((id Z) ^) / (sin ^2)) ) by XBOOLE_1:18;
then  dom f c= dom ((cos / sin) / f1) by VALUED_1:8;
then A8: ( Z c= dom ((cos / sin) / f1) & Z c= dom (((id Z) ^) / (sin ^2)) ) by A1, A7;
 dom ((cos / sin) / f1) = (dom (cos / sin)) /\ ((dom f1) \ (f1 " {0})) by RFUNCT_1:def_1;
then A9: Z c= dom (cos / sin) by A8, XBOOLE_1:18;
 dom (((id Z) ^) / (sin ^2)) c= (dom ((id Z) ^)) /\ ((dom (sin ^2)) \ ((sin ^2) " {0})) by RFUNCT_1:def_1;
then  ( dom (((id Z) ^) / (sin ^2)) c= dom ((id Z) ^) & dom (((id Z) ^) / (sin ^2)) c= (dom (sin ^2)) \ ((sin ^2) " {0}) ) by XBOOLE_1:18;
then A10: ( Z c= dom ((id Z) ^) & Z c= (dom (sin ^2)) \ ((sin ^2) " {0}) ) by A8, XBOOLE_1:1;
A11: for x being Real st x in Z holds
f . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) )
assume A12: x in Z ; ::_thesis: f . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2))
then ((- ((cos / sin) / f1)) - (((id Z) ^) / (sin ^2))) . x = ((- ((cos / sin) / f1)) . x) - ((((id Z) ^) / (sin ^2)) . x) by A1, VALUED_1:13
.= (- (((cos / sin) / f1) . x)) - ((((id Z) ^) / (sin ^2)) . x) by VALUED_1:8
.= (- (((cos / sin) . x) / (f1 . x))) - ((((id Z) ^) / (sin ^2)) . x) by A12, A8, RFUNCT_1:def_1
.= (- (((cos . x) / (sin . x)) / (f1 . x))) - ((((id Z) ^) / (sin ^2)) . x) by A9, A12, RFUNCT_1:def_1
.= (- (((cos . x) / (sin . x)) / (f1 . x))) - ((((id Z) ^) . x) / ((sin ^2) . x)) by A8, A12, RFUNCT_1:def_1
.= (- (((cos . x) / (sin . x)) / (f1 . x))) - ((((id Z) . x) ") / ((sin ^2) . x)) by A10, A12, RFUNCT_1:def_2
.= (- (((cos . x) / (sin . x)) / (f1 . x))) - ((1 / x) / ((sin ^2) . x)) by A12, FUNCT_1:18
.= (- (((cos . x) / (sin . x)) / (f1 . x))) - ((1 / x) / ((sin . x) ^2)) by VALUED_1:11
.= (- (((cos . x) / (sin . x)) / (x #Z 2))) - ((1 / x) / ((sin . x) ^2)) by A1, TAYLOR_1:def_1
.= (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) by FDIFF_7:1 ;
hence  f . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) by A1; ::_thesis: verum
end;
A13: for x being Real st x in dom ((((id Z) ^) (#) cot) `| Z) holds
((((id Z) ^) (#) cot) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((((id Z) ^) (#) cot) `| Z) implies ((((id Z) ^) (#) cot) `| Z) . x = f . x )
assume  x in dom ((((id Z) ^) (#) cot) `| Z) ; ::_thesis: ((((id Z) ^) (#) cot) `| Z) . x = f . x
then A14: x in Z by A6, FDIFF_1:def_7;
then ((((id Z) ^) (#) cot) `| Z) . x = (- (((cos . x) / (sin . x)) / (x ^2))) - ((1 / x) / ((sin . x) ^2)) by A1, A4, FDIFF_8:35
.= f . x by A11, A14 ;
hence  ((((id Z) ^) (#) cot) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((((id Z) ^) (#) cot) `| Z) = dom f by A1, A6, FDIFF_1:def_7;
then  (((id Z) ^) (#) cot) `| Z = f by A13, PARTFUN1:5;
hence  integral (f,A) = ((((id Z) ^) (#) cot) . (upper_bound A)) - ((((id Z) ^) (#) cot) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13; ::_thesis: verum
end;

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 = ((sin / cos) / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ((sin / cos) / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ((sin / cos) / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ((sin / cos) / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z = dom f & f | A is continuous implies integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A)) )
assume A1: ( A c= Z & f = ((sin / cos) / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: ln (#) tan is_differentiable_on Z by A1, FDIFF_8:32;
 Z = (dom ((sin / cos) / (id Z))) /\ (dom (ln / (cos ^2))) by A1, VALUED_1:def_1;
then A4: ( Z c= dom ((sin / cos) / (id Z)) & Z c= dom (ln / (cos ^2)) ) by XBOOLE_1:18;
 dom ((sin / cos) / (id Z)) c= (dom (sin / cos)) /\ ((dom (id Z)) \ ((id Z) " {0})) by RFUNCT_1:def_1;
then  dom ((sin / cos) / (id Z)) c= dom (sin / cos) by XBOOLE_1:18;
then A5: Z c= dom (sin / cos) by A4, XBOOLE_1:1;
A6: for x being Real st x in Z holds
f . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) )
assume A7: x in Z ; ::_thesis: f . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2))
then (((sin / cos) / (id Z)) + (ln / (cos ^2))) . x = (((sin / cos) / (id Z)) . x) + ((ln / (cos ^2)) . x) by A1, VALUED_1:def_1
.= (((sin / cos) . x) / ((id Z) . x)) + ((ln / (cos ^2)) . x) by A7, A4, RFUNCT_1:def_1
.= (((sin . x) / (cos . x)) / ((id Z) . x)) + ((ln / (cos ^2)) . x) by A5, A7, RFUNCT_1:def_1
.= (((sin . x) / (cos . x)) / x) + ((ln / (cos ^2)) . x) by A7, FUNCT_1:18
.= (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos ^2) . x)) by A7, A4, RFUNCT_1:def_1
.= (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) by VALUED_1:11 ;
hence  f . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) by A1; ::_thesis: verum
end;
A8: for x being Real st x in dom ((ln (#) tan) `| Z) holds
((ln (#) tan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((ln (#) tan) `| Z) implies ((ln (#) tan) `| Z) . x = f . x )
assume  x in dom ((ln (#) tan) `| Z) ; ::_thesis: ((ln (#) tan) `| Z) . x = f . x
then A9: x in Z by A3, FDIFF_1:def_7;
then ((ln (#) tan) `| Z) . x = (((sin . x) / (cos . x)) / x) + ((ln . x) / ((cos . x) ^2)) by A1, FDIFF_8:32
.= f . x by A9, A6 ;
hence  ((ln (#) tan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((ln (#) tan) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (ln (#) tan) `| Z = f by A8, PARTFUN1:5;
hence  integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A)) by A1, A2, FDIFF_8:32, INTEGRA5:13; ::_thesis: verum
end;

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 = ((cos / sin) / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ((cos / sin) / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ((cos / sin) / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ((cos / sin) / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A)) )
assume A1: ( A c= Z & f = ((cos / sin) / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: ln (#) cot is_differentiable_on Z by A1, FDIFF_8:33;
 Z = (dom ((cos / sin) / (id Z))) /\ (dom (ln / (sin ^2))) by A1, VALUED_1:12;
then A4: ( Z c= dom ((cos / sin) / (id Z)) & Z c= dom (ln / (sin ^2)) ) by XBOOLE_1:18;
 dom ((cos / sin) / (id Z)) c= (dom (cos / sin)) /\ ((dom (id Z)) \ ((id Z) " {0})) by RFUNCT_1:def_1;
then  dom ((cos / sin) / (id Z)) c= dom (cos / sin) by XBOOLE_1:18;
then A5: Z c= dom (cos / sin) by A4, XBOOLE_1:1;
A6: for x being Real st x in Z holds
f . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) )
assume A7: x in Z ; ::_thesis: f . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2))
then (((cos / sin) / (id Z)) - (ln / (sin ^2))) . x = (((cos / sin) / (id Z)) . x) - ((ln / (sin ^2)) . x) by A1, VALUED_1:13
.= (((cos / sin) . x) / ((id Z) . x)) - ((ln / (sin ^2)) . x) by A7, A4, RFUNCT_1:def_1
.= (((cos . x) / (sin . x)) / ((id Z) . x)) - ((ln / (sin ^2)) . x) by A5, A7, RFUNCT_1:def_1
.= (((cos . x) / (sin . x)) / x) - ((ln / (sin ^2)) . x) by A7, FUNCT_1:18
.= (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin ^2) . x)) by A7, A4, RFUNCT_1:def_1
.= (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) by VALUED_1:11 ;
hence  f . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) by A1; ::_thesis: verum
end;
A8: for x being Real st x in dom ((ln (#) cot) `| Z) holds
((ln (#) cot) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((ln (#) cot) `| Z) implies ((ln (#) cot) `| Z) . x = f . x )
assume  x in dom ((ln (#) cot) `| Z) ; ::_thesis: ((ln (#) cot) `| Z) . x = f . x
then A9: x in Z by A3, FDIFF_1:def_7;
then ((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) by A1, FDIFF_8:33
.= f . x by A9, A6 ;
hence  ((ln (#) cot) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((ln (#) cot) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (ln (#) cot) `| Z = f by A8, PARTFUN1:5;
hence  integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A)) by A1, A2, FDIFF_8:33, INTEGRA5:13; ::_thesis: verum
end;

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 / (cos ^2)) & Z c= dom (ln (#) tan) & Z c= dom tan & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (tan / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z c= dom tan & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = (tan / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z c= dom tan & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = (tan / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z c= dom tan & Z = dom f & f | A is continuous implies integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A)) )
assume A1: ( A c= Z & f = (tan / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z c= dom tan & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: ln (#) tan is_differentiable_on Z by A1, FDIFF_8:32;
 Z = (dom (tan / (id Z))) /\ (dom (ln / (cos ^2))) by A1, VALUED_1:def_1;
then A4: ( Z c= dom (tan / (id Z)) & Z c= dom (ln / (cos ^2)) ) by XBOOLE_1:18;
A5: for x being Real st x in Z holds
f . x = ((tan . x) / x) + ((ln . x) / ((cos . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = ((tan . x) / x) + ((ln . x) / ((cos . x) ^2)) )
assume A6: x in Z ; ::_thesis: f . x = ((tan . x) / x) + ((ln . x) / ((cos . x) ^2))
then ((tan / (id Z)) + (ln / (cos ^2))) . x = ((tan / (id Z)) . x) + ((ln / (cos ^2)) . x) by A1, VALUED_1:def_1
.= ((tan . x) / ((id Z) . x)) + ((ln / (cos ^2)) . x) by A6, A4, RFUNCT_1:def_1
.= ((tan . x) / x) + ((ln / (cos ^2)) . x) by A6, FUNCT_1:18
.= ((tan . x) / x) + ((ln . x) / ((cos ^2) . x)) by A6, A4, RFUNCT_1:def_1
.= ((tan . x) / x) + ((ln . x) / ((cos . x) ^2)) by VALUED_1:11 ;
hence  f . x = ((tan . x) / x) + ((ln . x) / ((cos . x) ^2)) by A1; ::_thesis: verum
end;
A7: for x being Real st x in dom ((ln (#) tan) `| Z) holds
((ln (#) tan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((ln (#) tan) `| Z) implies ((ln (#) tan) `| Z) . x = f . x )
assume  x in dom ((ln (#) tan) `| Z) ; ::_thesis: ((ln (#) tan) `| Z) . x = f . x
then A8: x in Z by A3, FDIFF_1:def_7;
then ((ln (#) tan) `| Z) . x = ((tan x) / x) + ((ln . x) / ((cos . x) ^2)) by A1, FDIFF_8:32
.= ((tan . x) / x) + ((ln . x) / ((cos . x) ^2)) by A1, A8, FDIFF_8:1, SIN_COS9:15
.= f . x by A8, A5 ;
hence  ((ln (#) tan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((ln (#) tan) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (ln (#) tan) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A)) by A1, A2, FDIFF_8:32, INTEGRA5:13; ::_thesis: verum
end;

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 / (sin ^2)) & Z c= dom (ln (#) cot) & Z c= dom cot & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (cot / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z c= dom cot & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = (cot / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z c= dom cot & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = (cot / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z c= dom cot & Z = dom f & f | A is continuous implies integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A)) )
assume A1: ( A c= Z & f = (cot / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z c= dom cot & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: ln (#) cot is_differentiable_on Z by A1, FDIFF_8:33;
 Z = (dom (cot / (id Z))) /\ (dom (ln / (sin ^2))) by A1, VALUED_1:12;
then A4: ( Z c= dom (cot / (id Z)) & Z c= dom (ln / (sin ^2)) ) by XBOOLE_1:18;
A5: for x being Real st x in Z holds
f . x = ((cot . x) / x) - ((ln . x) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = ((cot . x) / x) - ((ln . x) / ((sin . x) ^2)) )
assume A6: x in Z ; ::_thesis: f . x = ((cot . x) / x) - ((ln . x) / ((sin . x) ^2))
then ((cot / (id Z)) - (ln / (sin ^2))) . x = ((cot / (id Z)) . x) - ((ln / (sin ^2)) . x) by A1, VALUED_1:13
.= ((cot . x) / ((id Z) . x)) - ((ln / (sin ^2)) . x) by A6, A4, RFUNCT_1:def_1
.= ((cot . x) / x) - ((ln / (sin ^2)) . x) by A6, FUNCT_1:18
.= ((cot . x) / x) - ((ln . x) / ((sin ^2) . x)) by A6, A4, RFUNCT_1:def_1
.= ((cot . x) / x) - ((ln . x) / ((sin . x) ^2)) by VALUED_1:11 ;
hence  f . x = ((cot . x) / x) - ((ln . x) / ((sin . x) ^2)) by A1; ::_thesis: verum
end;
A7: for x being Real st x in dom ((ln (#) cot) `| Z) holds
((ln (#) cot) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((ln (#) cot) `| Z) implies ((ln (#) cot) `| Z) . x = f . x )
assume  x in dom ((ln (#) cot) `| Z) ; ::_thesis: ((ln (#) cot) `| Z) . x = f . x
then A8: x in Z by A3, FDIFF_1:def_7;
then ((ln (#) cot) `| Z) . x = ((cot x) / x) - ((ln . x) / ((sin . x) ^2)) by A1, FDIFF_8:33
.= ((cot . x) / x) - ((ln . x) / ((sin . x) ^2)) by A1, A8, FDIFF_8:2, SIN_COS9:16
.= f . x by A5, A8 ;
hence  ((ln (#) cot) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((ln (#) cot) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (ln (#) cot) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A)) by A1, A2, FDIFF_8:33, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGR13:19
for A being non empty closed_interval Subset of REAL
for f1, 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
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) = ((ln (#) arctan) . (upper_bound A)) - ((ln (#) arctan) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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) = ((ln (#) arctan) . (upper_bound A)) - ((ln (#) arctan) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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) = ((ln (#) arctan) . (upper_bound A)) - ((ln (#) arctan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = ((ln (#) arctan) . (upper_bound A)) - ((ln (#) arctan) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = ((ln (#) arctan) . (upper_bound A)) - ((ln (#) arctan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom (arctan / (id Z))) /\ (dom (ln / (f1 + (#Z 2)))) by A1, VALUED_1:def_1;
then A3: ( Z c= dom (arctan / (id Z)) & Z c= dom (ln / (f1 + (#Z 2))) ) by XBOOLE_1:18;
then  Z c= (dom arctan) /\ ((dom (id Z)) \ ((id Z) " {0})) by RFUNCT_1:def_1;
then A4: Z c= dom arctan by XBOOLE_1:18;
 Z c= (dom ln) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by A3, RFUNCT_1:def_1;
then A5: ( Z c= dom ln & Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) ) by XBOOLE_1:18;
then  Z c= (dom arctan) /\ (dom ln) by A4, XBOOLE_1:19;
then A6: Z c= dom (ln (#) arctan) by VALUED_1:def_4;
then A7: ln (#) arctan is_differentiable_on Z by A1, SIN_COS9:127;
A8: Z c= dom ((f1 + (#Z 2)) ^) by A5, RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A9: Z c= dom (f1 + (#Z 2)) by A8, XBOOLE_1:1;
A10: for x being Real st x in Z holds
f . x = ((arctan . x) / x) + ((ln . x) / (1 + (x ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = ((arctan . x) / x) + ((ln . x) / (1 + (x ^2))) )
assume A11: x in Z ; ::_thesis: f . x = ((arctan . x) / x) + ((ln . x) / (1 + (x ^2)))
then ((arctan / (id Z)) + (ln / (f1 + (#Z 2)))) . x = ((arctan / (id Z)) . x) + ((ln / (f1 + (#Z 2))) . x) by A1, VALUED_1:def_1
.= ((arctan . x) * (((id Z) . x) ")) + ((ln / (f1 + (#Z 2))) . x) by A3, A11, RFUNCT_1:def_1
.= ((arctan . x) * (((id Z) . x) ")) + ((ln . x) * (((f1 + (#Z 2)) . x) ")) by A3, A11, RFUNCT_1:def_1
.= ((arctan . x) / x) + ((ln . x) / ((f1 + (#Z 2)) . x)) by A11, FUNCT_1:18
.= ((arctan . x) / x) + ((ln . x) / ((f1 . x) + ((#Z 2) . x))) by A9, A11, VALUED_1:def_1
.= ((arctan . x) / x) + ((ln . x) / (1 + ((#Z 2) . x))) by A1, A11
.= ((arctan . x) / x) + ((ln . x) / (1 + (x #Z 2))) by TAYLOR_1:def_1
.= ((arctan . x) / x) + ((ln . x) / (1 + (x ^2))) by FDIFF_7:1 ;
hence  f . x = ((arctan . x) / x) + ((ln . x) / (1 + (x ^2))) by A1; ::_thesis: verum
end;
A12: for x being Real st x in dom ((ln (#) arctan) `| Z) holds
((ln (#) arctan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((ln (#) arctan) `| Z) implies ((ln (#) arctan) `| Z) . x = f . x )
assume  x in dom ((ln (#) arctan) `| Z) ; ::_thesis: ((ln (#) arctan) `| Z) . x = f . x
then A13: x in Z by A7, FDIFF_1:def_7;
then ((ln (#) arctan) `| Z) . x = ((arctan . x) / x) + ((ln . x) / (1 + (x ^2))) by A1, A6, SIN_COS9:127
.= f . x by A13, A10 ;
hence  ((ln (#) arctan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((ln (#) arctan) `| Z) = dom f by A1, A7, FDIFF_1:def_7;
then  (ln (#) arctan) `| Z = f by A12, PARTFUN1:5;
hence  integral (f,A) = ((ln (#) arctan) . (upper_bound A)) - ((ln (#) arctan) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13, SIN_COS9:127; ::_thesis: verum
end;

theorem :: INTEGR13:20
for A being non empty closed_interval Subset of REAL
for f1, 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
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) = ((ln (#) arccot) . (upper_bound A)) - ((ln (#) arccot) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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) = ((ln (#) arccot) . (upper_bound A)) - ((ln (#) arccot) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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) = ((ln (#) arccot) . (upper_bound A)) - ((ln (#) arccot) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = ((ln (#) arccot) . (upper_bound A)) - ((ln (#) arccot) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = ((ln (#) arccot) . (upper_bound A)) - ((ln (#) arccot) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom (arccot / (id Z))) /\ (dom (ln / (f1 + (#Z 2)))) by A1, VALUED_1:12;
then A3: ( Z c= dom (arccot / (id Z)) & Z c= dom (ln / (f1 + (#Z 2))) ) by XBOOLE_1:18;
then  Z c= (dom arccot) /\ ((dom (id Z)) \ ((id Z) " {0})) by RFUNCT_1:def_1;
then A4: Z c= dom arccot by XBOOLE_1:18;
 Z c= (dom ln) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by A3, RFUNCT_1:def_1;
then A5: ( Z c= dom ln & Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) ) by XBOOLE_1:18;
then  Z c= (dom arccot) /\ (dom ln) by A4, XBOOLE_1:19;
then A6: Z c= dom (ln (#) arccot) by VALUED_1:def_4;
then A7: ln (#) arccot is_differentiable_on Z by A1, SIN_COS9:128;
A8: Z c= dom ((f1 + (#Z 2)) ^) by A5, RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A9: Z c= dom (f1 + (#Z 2)) by A8, XBOOLE_1:1;
A10: for x being Real st x in Z holds
f . x = ((arccot . x) / x) - ((ln . x) / (1 + (x ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = ((arccot . x) / x) - ((ln . x) / (1 + (x ^2))) )
assume A11: x in Z ; ::_thesis: f . x = ((arccot . x) / x) - ((ln . x) / (1 + (x ^2)))
then ((arccot / (id Z)) - (ln / (f1 + (#Z 2)))) . x = ((arccot / (id Z)) . x) - ((ln / (f1 + (#Z 2))) . x) by A1, VALUED_1:13
.= ((arccot . x) * (((id Z) . x) ")) - ((ln / (f1 + (#Z 2))) . x) by A3, A11, RFUNCT_1:def_1
.= ((arccot . x) * (((id Z) . x) ")) - ((ln . x) * (((f1 + (#Z 2)) . x) ")) by A3, A11, RFUNCT_1:def_1
.= ((arccot . x) / x) - ((ln . x) / ((f1 + (#Z 2)) . x)) by A11, FUNCT_1:18
.= ((arccot . x) / x) - ((ln . x) / ((f1 . x) + ((#Z 2) . x))) by A9, A11, VALUED_1:def_1
.= ((arccot . x) / x) - ((ln . x) / (1 + ((#Z 2) . x))) by A1, A11
.= ((arccot . x) / x) - ((ln . x) / (1 + (x #Z 2))) by TAYLOR_1:def_1
.= ((arccot . x) / x) - ((ln . x) / (1 + (x ^2))) by FDIFF_7:1 ;
hence  f . x = ((arccot . x) / x) - ((ln . x) / (1 + (x ^2))) by A1; ::_thesis: verum
end;
A12: for x being Real st x in dom ((ln (#) arccot) `| Z) holds
((ln (#) arccot) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((ln (#) arccot) `| Z) implies ((ln (#) arccot) `| Z) . x = f . x )
assume  x in dom ((ln (#) arccot) `| Z) ; ::_thesis: ((ln (#) arccot) `| Z) . x = f . x
then A13: x in Z by A7, FDIFF_1:def_7;
then ((ln (#) arccot) `| Z) . x = ((arccot . x) / x) - ((ln . x) / (1 + (x ^2))) by A1, A6, SIN_COS9:128
.= f . x by A10, A13 ;
hence  ((ln (#) arccot) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((ln (#) arccot) `| Z) = dom f by A1, A7, FDIFF_1:def_7;
then  (ln (#) arccot) `| Z = f by A12, PARTFUN1:5;
hence  integral (f,A) = ((ln (#) arccot) . (upper_bound A)) - ((ln (#) arccot) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13, SIN_COS9:128; ::_thesis: verum
end;

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 = (exp_R * tan) / (cos ^2) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R * tan) . (upper_bound A)) - ((exp_R * tan) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (exp_R * tan) / (cos ^2) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R * tan) . (upper_bound A)) - ((exp_R * tan) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = (exp_R * tan) / (cos ^2) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R * tan) . (upper_bound A)) - ((exp_R * tan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = (exp_R * tan) / (cos ^2) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R * tan) . (upper_bound A)) - ((exp_R * tan) . (lower_bound A)) )
assume A1: ( A c= Z & f = (exp_R * tan) / (cos ^2) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R * tan) . (upper_bound A)) - ((exp_R * tan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom (exp_R * tan)) /\ ((dom (cos ^2)) \ ((cos ^2) " {0})) by A1, RFUNCT_1:def_1;
then A3: Z c= dom (exp_R * tan) by XBOOLE_1:18;
then A4: exp_R * tan is_differentiable_on Z by FDIFF_8:16;
A5: for x being Real st x in Z holds
f . x = (exp_R . (tan . x)) / ((cos . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (exp_R . (tan . x)) / ((cos . x) ^2) )
assume A6: x in Z ; ::_thesis: f . x = (exp_R . (tan . x)) / ((cos . x) ^2)
then ((exp_R * tan) / (cos ^2)) . x = ((exp_R * tan) . x) / ((cos ^2) . x) by A1, RFUNCT_1:def_1
.= (exp_R . (tan . x)) / ((cos ^2) . x) by A3, A6, FUNCT_1:12
.= (exp_R . (tan . x)) / ((cos . x) ^2) by VALUED_1:11 ;
hence  f . x = (exp_R . (tan . x)) / ((cos . x) ^2) by A1; ::_thesis: verum
end;
A7: for x being Real st x in dom ((exp_R * tan) `| Z) holds
((exp_R * tan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((exp_R * tan) `| Z) implies ((exp_R * tan) `| Z) . x = f . x )
assume  x in dom ((exp_R * tan) `| Z) ; ::_thesis: ((exp_R * tan) `| Z) . x = f . x
then A8: x in Z by A4, FDIFF_1:def_7;
then ((exp_R * tan) `| Z) . x = (exp_R . (tan . x)) / ((cos . x) ^2) by A3, FDIFF_8:16
.= f . x by A5, A8 ;
hence  ((exp_R * tan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((exp_R * tan) `| Z) = dom f by A1, A4, FDIFF_1:def_7;
then  (exp_R * tan) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((exp_R * tan) . (upper_bound A)) - ((exp_R * tan) . (lower_bound A)) by A1, A2, A3, FDIFF_8:16, INTEGRA5:13; ::_thesis: verum
end;

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 = - ((exp_R * cot) / (sin ^2)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R * cot) . (upper_bound A)) - ((exp_R * cot) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = - ((exp_R * cot) / (sin ^2)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R * cot) . (upper_bound A)) - ((exp_R * cot) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = - ((exp_R * cot) / (sin ^2)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((exp_R * cot) . (upper_bound A)) - ((exp_R * cot) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = - ((exp_R * cot) / (sin ^2)) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R * cot) . (upper_bound A)) - ((exp_R * cot) . (lower_bound A)) )
assume A1: ( A c= Z & f = - ((exp_R * cot) / (sin ^2)) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R * cot) . (upper_bound A)) - ((exp_R * cot) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: Z = dom ((exp_R * cot) / (sin ^2)) by A1, VALUED_1:8;
then  Z c= (dom (exp_R * cot)) /\ ((dom (sin ^2)) \ ((sin ^2) " {0})) by RFUNCT_1:def_1;
then A4: Z c= dom (exp_R * cot) by XBOOLE_1:18;
then A5: exp_R * cot is_differentiable_on Z by FDIFF_8:17;
A6: for x being Real st x in Z holds
f . x = - ((exp_R . (cot . x)) / ((sin . x) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) )
assume A7: x in Z ; ::_thesis: f . x = - ((exp_R . (cot . x)) / ((sin . x) ^2))
(- ((exp_R * cot) / (sin ^2))) . x = - (((exp_R * cot) / (sin ^2)) . x) by VALUED_1:8
.= - (((exp_R * cot) . x) / ((sin ^2) . x)) by A7, A3, RFUNCT_1:def_1
.= - ((exp_R . (cot . x)) / ((sin ^2) . x)) by A4, A7, FUNCT_1:12
.= - ((exp_R . (cot . x)) / ((sin . x) ^2)) by VALUED_1:11 ;
hence  f . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) by A1; ::_thesis: verum
end;
A8: for x being Real st x in dom ((exp_R * cot) `| Z) holds
((exp_R * cot) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((exp_R * cot) `| Z) implies ((exp_R * cot) `| Z) . x = f . x )
assume  x in dom ((exp_R * cot) `| Z) ; ::_thesis: ((exp_R * cot) `| Z) . x = f . x
then A9: x in Z by A5, FDIFF_1:def_7;
then ((exp_R * cot) `| Z) . x = - ((exp_R . (cot . x)) / ((sin . x) ^2)) by A4, FDIFF_8:17
.= f . x by A6, A9 ;
hence  ((exp_R * cot) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((exp_R * cot) `| Z) = dom f by A1, A5, FDIFF_1:def_7;
then  (exp_R * cot) `| Z = f by A8, PARTFUN1:5;
hence  integral (f,A) = ((exp_R * cot) . (upper_bound A)) - ((exp_R * cot) . (lower_bound A)) by A1, A2, A4, FDIFF_8:17, INTEGRA5:13; ::_thesis: verum
end;

theorem Th23: :: INTEGR13:23
for Z being open Subset of REAL st Z c= dom (exp_R * cot) holds
( - (exp_R * cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * cot) implies ( - (exp_R * cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ) ) )
assume A1: Z c= dom (exp_R * cot) ; ::_thesis: ( - (exp_R * cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ) )
then A2: Z c= dom (- (exp_R * cot)) by VALUED_1:8;
A3: for x being Real st x in Z holds
sin . x <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 )
assume  x in Z ; ::_thesis: sin . x <> 0
then  x in dom (cos / sin) by A1, FUNCT_1:11;
hence  sin . x <> 0 by FDIFF_8:2; ::_thesis: verum
end;
A4: exp_R * cot is_differentiable_on Z by A1, FDIFF_8:17;
then A5: (- 1) (#) (exp_R * cot) is_differentiable_on Z by A2, FDIFF_1:20;
 for x being Real st x in Z holds
((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) )
assume A6: x in Z ; ::_thesis: ((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2)
then A7: sin . x <> 0 by A3;
then A8: cot is_differentiable_in x by FDIFF_7:47;
A9: exp_R is_differentiable_in cot . x by SIN_COS:65;
A10: exp_R * cot is_differentiable_in x by A4, A6, FDIFF_1:9;
((- (exp_R * cot)) `| Z) . x = diff ((- (exp_R * cot)),x) by A5, A6, FDIFF_1:def_7
.= (- 1) * (diff ((exp_R * cot),x)) by A10, FDIFF_1:15
.= (- 1) * ((diff (exp_R,(cot . x))) * (diff (cot,x))) by A8, A9, FDIFF_2:13
.= (- 1) * ((diff (exp_R,(cot . x))) * (- (1 / ((sin . x) ^2)))) by A7, FDIFF_7:47
.= (- 1) * ((exp_R . (cot . x)) * (- (1 / ((sin . x) ^2)))) by SIN_COS:65
.= (exp_R . (cot . x)) / ((sin . x) ^2) ;
hence  ((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ; ::_thesis: verum
end;
hence  ( - (exp_R * cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ) ) by A2, A4, Lm3, FDIFF_1:20; ::_thesis: verum
end;

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 = (exp_R * cot) / (sin ^2) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (exp_R * cot)) . (upper_bound A)) - ((- (exp_R * cot)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (exp_R * cot) / (sin ^2) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (exp_R * cot)) . (upper_bound A)) - ((- (exp_R * cot)) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = (exp_R * cot) / (sin ^2) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (exp_R * cot)) . (upper_bound A)) - ((- (exp_R * cot)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = (exp_R * cot) / (sin ^2) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (exp_R * cot)) . (upper_bound A)) - ((- (exp_R * cot)) . (lower_bound A)) )
assume A1: ( A c= Z & f = (exp_R * cot) / (sin ^2) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (exp_R * cot)) . (upper_bound A)) - ((- (exp_R * cot)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom (exp_R * cot)) /\ ((dom (sin ^2)) \ ((sin ^2) " {0})) by A1, RFUNCT_1:def_1;
then A3: Z c= dom (exp_R * cot) by XBOOLE_1:18;
then A4: - (exp_R * cot) is_differentiable_on Z by Th23;
A5: for x being Real st x in Z holds
f . x = (exp_R . (cot . x)) / ((sin . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (exp_R . (cot . x)) / ((sin . x) ^2) )
assume A6: x in Z ; ::_thesis: f . x = (exp_R . (cot . x)) / ((sin . x) ^2)
then ((exp_R * cot) / (sin ^2)) . x = ((exp_R * cot) . x) / ((sin ^2) . x) by A1, RFUNCT_1:def_1
.= (exp_R . (cot . x)) / ((sin ^2) . x) by A3, A6, FUNCT_1:12
.= (exp_R . (cot . x)) / ((sin . x) ^2) by VALUED_1:11 ;
hence  f . x = (exp_R . (cot . x)) / ((sin . x) ^2) by A1; ::_thesis: verum
end;
A7: for x being Real st x in dom ((- (exp_R * cot)) `| Z) holds
((- (exp_R * cot)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- (exp_R * cot)) `| Z) implies ((- (exp_R * cot)) `| Z) . x = f . x )
assume  x in dom ((- (exp_R * cot)) `| Z) ; ::_thesis: ((- (exp_R * cot)) `| Z) . x = f . x
then A8: x in Z by A4, FDIFF_1:def_7;
then ((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) by Th23, A3
.= f . x by A5, A8 ;
hence  ((- (exp_R * cot)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((- (exp_R * cot)) `| Z) = dom f by A1, A4, FDIFF_1:def_7;
then  (- (exp_R * cot)) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((- (exp_R * cot)) . (upper_bound A)) - ((- (exp_R * cot)) . (lower_bound A)) by A1, A2, Th23, A3, INTEGRA5:13; ::_thesis: verum
end;

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) (#) ((cos * ln) ^2)) ^ & Z c= dom (tan * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan * ln) . (upper_bound A)) - ((tan * ln) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ((id Z) (#) ((cos * ln) ^2)) ^ & Z c= dom (tan * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan * ln) . (upper_bound A)) - ((tan * ln) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ((id Z) (#) ((cos * ln) ^2)) ^ & Z c= dom (tan * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan * ln) . (upper_bound A)) - ((tan * ln) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ((id Z) (#) ((cos * ln) ^2)) ^ & Z c= dom (tan * ln) & Z = dom f & f | A is continuous implies integral (f,A) = ((tan * ln) . (upper_bound A)) - ((tan * ln) . (lower_bound A)) )
assume A1: ( A c= Z & f = ((id Z) (#) ((cos * ln) ^2)) ^ & Z c= dom (tan * ln) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((tan * ln) . (upper_bound A)) - ((tan * ln) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: tan * ln is_differentiable_on Z by A1, FDIFF_8:14;
 Z c= dom ((id Z) (#) ((cos * ln) ^2)) by A1, RFUNCT_1:1;
then  Z c= (dom (id Z)) /\ (dom ((cos * ln) ^2)) by VALUED_1:def_4;
then  Z c= dom ((cos * ln) ^2) by XBOOLE_1:18;
then A4: Z c= dom (cos * ln) by VALUED_1:11;
A5: for x being Real st x in Z holds
f . x = 1 / (x * ((cos . (ln . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = 1 / (x * ((cos . (ln . x)) ^2)) )
assume A6: x in Z ; ::_thesis: f . x = 1 / (x * ((cos . (ln . x)) ^2))
then (((id Z) (#) ((cos * ln) ^2)) ^) . x = 1 / (((id Z) (#) ((cos * ln) ^2)) . x) by A1, RFUNCT_1:def_2
.= 1 / (((id Z) . x) * (((cos * ln) ^2) . x)) by VALUED_1:5
.= 1 / (x * (((cos * ln) ^2) . x)) by A6, FUNCT_1:18
.= 1 / (x * (((cos * ln) . x) ^2)) by VALUED_1:11
.= 1 / (x * ((cos . (ln . x)) ^2)) by A4, A6, FUNCT_1:12 ;
hence  f . x = 1 / (x * ((cos . (ln . x)) ^2)) by A1; ::_thesis: verum
end;
A7: for x being Real st x in dom ((tan * ln) `| Z) holds
((tan * ln) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((tan * ln) `| Z) implies ((tan * ln) `| Z) . x = f . x )
assume  x in dom ((tan * ln) `| Z) ; ::_thesis: ((tan * ln) `| Z) . x = f . x
then A8: x in Z by A3, FDIFF_1:def_7;
then ((tan * ln) `| Z) . x = 1 / (x * ((cos . (ln . x)) ^2)) by A1, FDIFF_8:14
.= f . x by A5, A8 ;
hence  ((tan * ln) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((tan * ln) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (tan * ln) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((tan * ln) . (upper_bound A)) - ((tan * ln) . (lower_bound A)) by A1, A2, FDIFF_8:14, INTEGRA5:13; ::_thesis: verum
end;

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) (#) ((sin * ln) ^2)) ^) & Z c= dom (cot * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((cot * ln) . (upper_bound A)) - ((cot * ln) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = - (((id Z) (#) ((sin * ln) ^2)) ^) & Z c= dom (cot * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((cot * ln) . (upper_bound A)) - ((cot * ln) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = - (((id Z) (#) ((sin * ln) ^2)) ^) & Z c= dom (cot * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((cot * ln) . (upper_bound A)) - ((cot * ln) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = - (((id Z) (#) ((sin * ln) ^2)) ^) & Z c= dom (cot * ln) & Z = dom f & f | A is continuous implies integral (f,A) = ((cot * ln) . (upper_bound A)) - ((cot * ln) . (lower_bound A)) )
assume A1: ( A c= Z & f = - (((id Z) (#) ((sin * ln) ^2)) ^) & Z c= dom (cot * ln) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((cot * ln) . (upper_bound A)) - ((cot * ln) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: cot * ln is_differentiable_on Z by A1, FDIFF_8:15;
A4: Z = dom (((id Z) (#) ((sin * ln) ^2)) ^) by A1, VALUED_1:8;
then  Z c= dom ((id Z) (#) ((sin * ln) ^2)) by RFUNCT_1:1;
then  Z c= (dom (id Z)) /\ (dom ((sin * ln) ^2)) by VALUED_1:def_4;
then  Z c= dom ((sin * ln) ^2) by XBOOLE_1:18;
then A5: Z c= dom (sin * ln) by VALUED_1:11;
A6: for x being Real st x in Z holds
f . x = - (1 / (x * ((sin . (ln . x)) ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = - (1 / (x * ((sin . (ln . x)) ^2))) )
assume A7: x in Z ; ::_thesis: f . x = - (1 / (x * ((sin . (ln . x)) ^2)))
(- (((id Z) (#) ((sin * ln) ^2)) ^)) . x = - ((((id Z) (#) ((sin * ln) ^2)) ^) . x) by VALUED_1:8
.= - (1 / (((id Z) (#) ((sin * ln) ^2)) . x)) by A4, A7, RFUNCT_1:def_2
.= - (1 / (((id Z) . x) * (((sin * ln) ^2) . x))) by VALUED_1:5
.= - (1 / (x * (((sin * ln) ^2) . x))) by A7, FUNCT_1:18
.= - (1 / (x * (((sin * ln) . x) ^2))) by VALUED_1:11
.= - (1 / (x * ((sin . (ln . x)) ^2))) by A5, A7, FUNCT_1:12 ;
hence  f . x = - (1 / (x * ((sin . (ln . x)) ^2))) by A1; ::_thesis: verum
end;
A8: for x being Real st x in dom ((cot * ln) `| Z) holds
((cot * ln) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((cot * ln) `| Z) implies ((cot * ln) `| Z) . x = f . x )
assume  x in dom ((cot * ln) `| Z) ; ::_thesis: ((cot * ln) `| Z) . x = f . x
then A9: x in Z by A3, FDIFF_1:def_7;
then ((cot * ln) `| Z) . x = - (1 / (x * ((sin . (ln . x)) ^2))) by A1, FDIFF_8:15
.= f . x by A6, A9 ;
hence  ((cot * ln) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((cot * ln) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (cot * ln) `| Z = f by A8, PARTFUN1:5;
hence  integral (f,A) = ((cot * ln) . (upper_bound A)) - ((cot * ln) . (lower_bound A)) by A1, A2, FDIFF_8:15, INTEGRA5:13; ::_thesis: verum
end;

theorem Th27: :: INTEGR13:27
for Z being open Subset of REAL st Z c= dom (cot * ln) holds
( - (cot * ln) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot * ln) implies ( - (cot * ln) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2)) ) ) )
assume A1: Z c= dom (cot * ln) ; ::_thesis: ( - (cot * ln) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2)) ) )
then A2: Z c= dom (- (cot * ln)) by VALUED_1:8;
 dom (cot * ln) c= dom ln by RELAT_1:25;
then A3: Z c= dom ln by A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
x > 0
proof
let x be Real; ::_thesis: ( x in Z implies x > 0 )
assume  x in Z ; ::_thesis: x > 0
then  x in right_open_halfline 0 by A3, TAYLOR_1:18;
then  ex g being Real st
( x = g & 0 < g ) by Lm2;
hence  x > 0 ; ::_thesis: verum
end;
A5: for x being Real st x in Z holds
sin . (ln . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (ln . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (ln . x) <> 0
then  ln . x in dom (cos / sin) by A1, FUNCT_1:11;
hence  sin . (ln . x) <> 0 by FDIFF_8:2; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
diff (ln,x) = 1 / x
proof
let x be Real; ::_thesis: ( x in Z implies diff (ln,x) = 1 / x )
assume  x in Z ; ::_thesis: diff (ln,x) = 1 / x
then  x > 0 by A4;
then  x in right_open_halfline 0 by Lm2;
hence  diff (ln,x) = 1 / x by TAYLOR_1:18; ::_thesis: verum
end;
A7: cot * ln is_differentiable_on Z by A1, FDIFF_8:15;
then A8: (- 1) (#) (cot * ln) is_differentiable_on Z by A2, FDIFF_1:20;
 for x being Real st x in Z holds
((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2)) )
assume A9: x in Z ; ::_thesis: ((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2))
then A10: ln is_differentiable_in x by A4, TAYLOR_1:18;
A11: ( x > 0 & sin . (ln . x) <> 0 ) by A4, A5, A9;
then A12: cot is_differentiable_in ln . x by FDIFF_7:47;
A13: cot * ln is_differentiable_in x by A7, A9, FDIFF_1:9;
((- (cot * ln)) `| Z) . x = diff ((- (cot * ln)),x) by A8, A9, FDIFF_1:def_7
.= (- 1) * (diff ((cot * ln),x)) by A13, FDIFF_1:15
.= (- 1) * ((diff (cot,(ln . x))) * (diff (ln,x))) by A10, A12, FDIFF_2:13
.= (- 1) * ((- (1 / ((sin . (ln . x)) ^2))) * (diff (ln,x))) by A11, FDIFF_7:47
.= (- 1) * (- ((diff (ln,x)) / ((sin . (ln . x)) ^2)))
.= (- 1) * (- ((1 / x) / ((sin . (ln . x)) ^2))) by A6, A9
.= 1 / (x * ((sin . (ln . x)) ^2)) by XCMPLX_1:78 ;
hence  ((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2)) ; ::_thesis: verum
end;
hence  ( - (cot * ln) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2)) ) ) by A2, A7, Lm3, FDIFF_1:20; ::_thesis: verum
end;

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) (#) ((sin * ln) ^2)) ^ & Z c= dom (cot * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (cot * ln)) . (upper_bound A)) - ((- (cot * ln)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ((id Z) (#) ((sin * ln) ^2)) ^ & Z c= dom (cot * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (cot * ln)) . (upper_bound A)) - ((- (cot * ln)) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ((id Z) (#) ((sin * ln) ^2)) ^ & Z c= dom (cot * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (cot * ln)) . (upper_bound A)) - ((- (cot * ln)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ((id Z) (#) ((sin * ln) ^2)) ^ & Z c= dom (cot * ln) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cot * ln)) . (upper_bound A)) - ((- (cot * ln)) . (lower_bound A)) )
assume A1: ( A c= Z & f = ((id Z) (#) ((sin * ln) ^2)) ^ & Z c= dom (cot * ln) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cot * ln)) . (upper_bound A)) - ((- (cot * ln)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: - (cot * ln) is_differentiable_on Z by A1, Th27;
 Z c= dom ((id Z) (#) ((sin * ln) ^2)) by A1, RFUNCT_1:1;
then  Z c= (dom (id Z)) /\ (dom ((sin * ln) ^2)) by VALUED_1:def_4;
then  Z c= dom ((sin * ln) ^2) by XBOOLE_1:18;
then A4: Z c= dom (sin * ln) by VALUED_1:11;
A5: for x being Real st x in Z holds
f . x = 1 / (x * ((sin . (ln . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = 1 / (x * ((sin . (ln . x)) ^2)) )
assume A6: x in Z ; ::_thesis: f . x = 1 / (x * ((sin . (ln . x)) ^2))
then (((id Z) (#) ((sin * ln) ^2)) ^) . x = 1 / (((id Z) (#) ((sin * ln) ^2)) . x) by A1, RFUNCT_1:def_2
.= 1 / (((id Z) . x) * (((sin * ln) ^2) . x)) by VALUED_1:5
.= 1 / (x * (((sin * ln) ^2) . x)) by A6, FUNCT_1:18
.= 1 / (x * (((sin * ln) . x) ^2)) by VALUED_1:11
.= 1 / (x * ((sin . (ln . x)) ^2)) by A4, A6, FUNCT_1:12 ;
hence  f . x = 1 / (x * ((sin . (ln . x)) ^2)) by A1; ::_thesis: verum
end;
A7: for x being Real st x in dom ((- (cot * ln)) `| Z) holds
((- (cot * ln)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- (cot * ln)) `| Z) implies ((- (cot * ln)) `| Z) . x = f . x )
assume  x in dom ((- (cot * ln)) `| Z) ; ::_thesis: ((- (cot * ln)) `| Z) . x = f . x
then A8: x in Z by A3, FDIFF_1:def_7;
then ((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2)) by A1, Th27
.= f . x by A5, A8 ;
hence  ((- (cot * ln)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((- (cot * ln)) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (- (cot * ln)) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((- (cot * ln)) . (upper_bound A)) - ((- (cot * ln)) . (lower_bound A)) by A1, A2, Th27, INTEGRA5:13; ::_thesis: verum
end;

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 / ((cos * exp_R) ^2) & Z c= dom (tan * exp_R) & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan * exp_R) . (upper_bound A)) - ((tan * exp_R) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = exp_R / ((cos * exp_R) ^2) & Z c= dom (tan * exp_R) & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan * exp_R) . (upper_bound A)) - ((tan * exp_R) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = exp_R / ((cos * exp_R) ^2) & Z c= dom (tan * exp_R) & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan * exp_R) . (upper_bound A)) - ((tan * exp_R) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = exp_R / ((cos * exp_R) ^2) & Z c= dom (tan * exp_R) & Z = dom f & f | A is continuous implies integral (f,A) = ((tan * exp_R) . (upper_bound A)) - ((tan * exp_R) . (lower_bound A)) )
assume A1: ( A c= Z & f = exp_R / ((cos * exp_R) ^2) & Z c= dom (tan * exp_R) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((tan * exp_R) . (upper_bound A)) - ((tan * exp_R) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: tan * exp_R is_differentiable_on Z by A1, FDIFF_8:12;
 Z = (dom exp_R) /\ ((dom ((cos * exp_R) ^2)) \ (((cos * exp_R) ^2) " {0})) by A1, RFUNCT_1:def_1;
then  Z c= (dom ((cos * exp_R) ^2)) \ (((cos * exp_R) ^2) " {0}) by XBOOLE_1:18;
then A4: Z c= dom (((cos * exp_R) ^2) ^) by RFUNCT_1:def_2;
 dom (((cos * exp_R) ^2) ^) c= dom ((cos * exp_R) ^2) by RFUNCT_1:1;
then  Z c= dom ((cos * exp_R) ^2) by A4, XBOOLE_1:1;
then A5: Z c= dom (cos * exp_R) by VALUED_1:11;
A6: for x being Real st x in Z holds
f . x = (exp_R . x) / ((cos . (exp_R . x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) )
assume A7: x in Z ; ::_thesis: f . x = (exp_R . x) / ((cos . (exp_R . x)) ^2)
then (exp_R / ((cos * exp_R) ^2)) . x = (exp_R . x) / (((cos * exp_R) ^2) . x) by A1, RFUNCT_1:def_1
.= (exp_R . x) / (((cos * exp_R) . x) ^2) by VALUED_1:11
.= (exp_R . x) / ((cos . (exp_R . x)) ^2) by A5, A7, FUNCT_1:12 ;
hence  f . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) by A1; ::_thesis: verum
end;
A8: for x being Real st x in dom ((tan * exp_R) `| Z) holds
((tan * exp_R) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((tan * exp_R) `| Z) implies ((tan * exp_R) `| Z) . x = f . x )
assume  x in dom ((tan * exp_R) `| Z) ; ::_thesis: ((tan * exp_R) `| Z) . x = f . x
then A9: x in Z by A3, FDIFF_1:def_7;
then ((tan * exp_R) `| Z) . x = (exp_R . x) / ((cos . (exp_R . x)) ^2) by A1, FDIFF_8:12
.= f . x by A6, A9 ;
hence  ((tan * exp_R) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((tan * exp_R) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (tan * exp_R) `| Z = f by A8, PARTFUN1:5;
hence  integral (f,A) = ((tan * exp_R) . (upper_bound A)) - ((tan * exp_R) . (lower_bound A)) by A1, A2, FDIFF_8:12, INTEGRA5:13; ::_thesis: verum
end;

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 / ((sin * exp_R) ^2)) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous holds
integral (f,A) = ((cot * exp_R) . (upper_bound A)) - ((cot * exp_R) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = - (exp_R / ((sin * exp_R) ^2)) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous holds
integral (f,A) = ((cot * exp_R) . (upper_bound A)) - ((cot * exp_R) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = - (exp_R / ((sin * exp_R) ^2)) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous holds
integral (f,A) = ((cot * exp_R) . (upper_bound A)) - ((cot * exp_R) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = - (exp_R / ((sin * exp_R) ^2)) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous implies integral (f,A) = ((cot * exp_R) . (upper_bound A)) - ((cot * exp_R) . (lower_bound A)) )
assume A1: ( A c= Z & f = - (exp_R / ((sin * exp_R) ^2)) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((cot * exp_R) . (upper_bound A)) - ((cot * exp_R) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: cot * exp_R is_differentiable_on Z by A1, FDIFF_8:13;
A4: Z = dom (exp_R / ((sin * exp_R) ^2)) by A1, VALUED_1:8;
then  Z c= (dom exp_R) /\ ((dom ((sin * exp_R) ^2)) \ (((sin * exp_R) ^2) " {0})) by RFUNCT_1:def_1;
then  Z c= (dom ((sin * exp_R) ^2)) \ (((sin * exp_R) ^2) " {0}) by XBOOLE_1:18;
then A5: Z c= dom (((sin * exp_R) ^2) ^) by RFUNCT_1:def_2;
 dom (((sin * exp_R) ^2) ^) c= dom ((sin * exp_R) ^2) by RFUNCT_1:1;
then  Z c= dom ((sin * exp_R) ^2) by A5, XBOOLE_1:1;
then A6: Z c= dom (sin * exp_R) by VALUED_1:11;
A7: for x being Real st x in Z holds
f . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) )
assume A8: x in Z ; ::_thesis: f . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2))
(- (exp_R / ((sin * exp_R) ^2))) . x = - ((exp_R / ((sin * exp_R) ^2)) . x) by VALUED_1:8
.= - ((exp_R . x) / (((sin * exp_R) ^2) . x)) by A4, A8, RFUNCT_1:def_1
.= - ((exp_R . x) / (((sin * exp_R) . x) ^2)) by VALUED_1:11
.= - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) by A6, A8, FUNCT_1:12 ;
hence  f . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) by A1; ::_thesis: verum
end;
A9: for x being Real st x in dom ((cot * exp_R) `| Z) holds
((cot * exp_R) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((cot * exp_R) `| Z) implies ((cot * exp_R) `| Z) . x = f . x )
assume  x in dom ((cot * exp_R) `| Z) ; ::_thesis: ((cot * exp_R) `| Z) . x = f . x
then A10: x in Z by A3, FDIFF_1:def_7;
then ((cot * exp_R) `| Z) . x = - ((exp_R . x) / ((sin . (exp_R . x)) ^2)) by A1, FDIFF_8:13
.= f . x by A7, A10 ;
hence  ((cot * exp_R) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((cot * exp_R) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (cot * exp_R) `| Z = f by A9, PARTFUN1:5;
hence  integral (f,A) = ((cot * exp_R) . (upper_bound A)) - ((cot * exp_R) . (lower_bound A)) by A1, A2, FDIFF_8:13, INTEGRA5:13; ::_thesis: verum
end;

theorem Th31: :: INTEGR13:31
for Z being open Subset of REAL st Z c= dom (cot * exp_R) holds
( - (cot * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot * exp_R) implies ( - (cot * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ) ) )
assume A1: Z c= dom (cot * exp_R) ; ::_thesis: ( - (cot * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ) )
then A2: Z c= dom (- (cot * exp_R)) by VALUED_1:8;
A3: cot * exp_R is_differentiable_on Z by A1, FDIFF_8:13;
then A4: (- 1) (#) (cot * exp_R) is_differentiable_on Z by A2, FDIFF_1:20;
A5: for x being Real st x in Z holds
sin . (exp_R . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies sin . (exp_R . x) <> 0 )
assume  x in Z ; ::_thesis: sin . (exp_R . x) <> 0
then  exp_R . x in dom (cos / sin) by A1, FUNCT_1:11;
hence  sin . (exp_R . x) <> 0 by FDIFF_8:2; ::_thesis: verum
end;
 for x being Real st x in Z holds
((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) )
assume A6: x in Z ; ::_thesis: ((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2)
A7: exp_R is_differentiable_in x by SIN_COS:65;
A8: sin . (exp_R . x) <> 0 by A5, A6;
then A9: cot is_differentiable_in exp_R . x by FDIFF_7:47;
A10: cot * exp_R is_differentiable_in x by A3, A6, FDIFF_1:9;
((- (cot * exp_R)) `| Z) . x = diff ((- (cot * exp_R)),x) by A4, A6, FDIFF_1:def_7
.= (- 1) * (diff ((cot * exp_R),x)) by A10, FDIFF_1:15
.= (- 1) * ((diff (cot,(exp_R . x))) * (diff (exp_R,x))) by A7, A9, FDIFF_2:13
.= (- 1) * ((- (1 / ((sin . (exp_R . x)) ^2))) * (diff (exp_R,x))) by A8, FDIFF_7:47
.= (- 1) * (- ((diff (exp_R,x)) / ((sin . (exp_R . x)) ^2)))
.= (exp_R . x) / ((sin . (exp_R . x)) ^2) by SIN_COS:65 ;
hence  ((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ; ::_thesis: verum
end;
hence  ( - (cot * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ) ) by A4; ::_thesis: verum
end;

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 / ((sin * exp_R) ^2) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (cot * exp_R)) . (upper_bound A)) - ((- (cot * exp_R)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = exp_R / ((sin * exp_R) ^2) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (cot * exp_R)) . (upper_bound A)) - ((- (cot * exp_R)) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = exp_R / ((sin * exp_R) ^2) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (cot * exp_R)) . (upper_bound A)) - ((- (cot * exp_R)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = exp_R / ((sin * exp_R) ^2) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cot * exp_R)) . (upper_bound A)) - ((- (cot * exp_R)) . (lower_bound A)) )
assume A1: ( A c= Z & f = exp_R / ((sin * exp_R) ^2) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cot * exp_R)) . (upper_bound A)) - ((- (cot * exp_R)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: - (cot * exp_R) is_differentiable_on Z by A1, Th31;
 Z c= (dom exp_R) /\ ((dom ((sin * exp_R) ^2)) \ (((sin * exp_R) ^2) " {0})) by A1, RFUNCT_1:def_1;
then  Z c= (dom ((sin * exp_R) ^2)) \ (((sin * exp_R) ^2) " {0}) by XBOOLE_1:18;
then A4: Z c= dom (((sin * exp_R) ^2) ^) by RFUNCT_1:def_2;
 dom (((sin * exp_R) ^2) ^) c= dom ((sin * exp_R) ^2) by RFUNCT_1:1;
then  Z c= dom ((sin * exp_R) ^2) by A4, XBOOLE_1:1;
then A5: Z c= dom (sin * exp_R) by VALUED_1:11;
A6: for x being Real st x in Z holds
f . x = (exp_R . x) / ((sin . (exp_R . x)) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) )
assume A7: x in Z ; ::_thesis: f . x = (exp_R . x) / ((sin . (exp_R . x)) ^2)
then (exp_R / ((sin * exp_R) ^2)) . x = (exp_R . x) / (((sin * exp_R) ^2) . x) by A1, RFUNCT_1:def_1
.= (exp_R . x) / (((sin * exp_R) . x) ^2) by VALUED_1:11
.= (exp_R . x) / ((sin . (exp_R . x)) ^2) by A5, A7, FUNCT_1:12 ;
hence  f . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) by A1; ::_thesis: verum
end;
A8: for x being Real st x in dom ((- (cot * exp_R)) `| Z) holds
((- (cot * exp_R)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- (cot * exp_R)) `| Z) implies ((- (cot * exp_R)) `| Z) . x = f . x )
assume  x in dom ((- (cot * exp_R)) `| Z) ; ::_thesis: ((- (cot * exp_R)) `| Z) . x = f . x
then A9: x in Z by A3, FDIFF_1:def_7;
then ((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) by A1, Th31
.= f . x by A6, A9 ;
hence  ((- (cot * exp_R)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((- (cot * exp_R)) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (- (cot * exp_R)) `| Z = f by A8, PARTFUN1:5;
hence  integral (f,A) = ((- (cot * exp_R)) . (upper_bound A)) - ((- (cot * exp_R)) . (lower_bound A)) by A1, A2, Th31, INTEGRA5:13; ::_thesis: verum
end;

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) ^)) . (upper_bound A)) - ((tan * ((id Z) ^)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: 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) ^)) . (upper_bound A)) - ((tan * ((id Z) ^)) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: 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) ^)) . (upper_bound A)) - ((tan * ((id Z) ^)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = ((tan * ((id Z) ^)) . (upper_bound A)) - ((tan * ((id Z) ^)) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = ((tan * ((id Z) ^)) . (upper_bound A)) - ((tan * ((id Z) ^)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: Z c= dom ((id Z) ^) by A1, FUNCT_1:101;
A4: not 0 in Z
proof
assume A5: 0 in Z ; ::_thesis: contradiction
dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2
.= (dom (id Z)) \ {0} by Lm1, A5 ;
then  not 0 in {0} by A5, A3, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
then A6: tan * ((id Z) ^) is_differentiable_on Z by A1, FDIFF_8:8;
A7: for x being Real st x in dom ((tan * ((id Z) ^)) `| Z) holds
((tan * ((id Z) ^)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((tan * ((id Z) ^)) `| Z) implies ((tan * ((id Z) ^)) `| Z) . x = f . x )
assume  x in dom ((tan * ((id Z) ^)) `| Z) ; ::_thesis: ((tan * ((id Z) ^)) `| Z) . x = f . x
then A8: x in Z by A6, FDIFF_1:def_7;
then ((tan * ((id Z) ^)) `| Z) . x = - (1 / ((x ^2) * ((cos . (1 / x)) ^2))) by A1, A4, FDIFF_8:8
.= f . x by A1, A8 ;
hence  ((tan * ((id Z) ^)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((tan * ((id Z) ^)) `| Z) = dom f by A1, A6, FDIFF_1:def_7;
then  (tan * ((id Z) ^)) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((tan * ((id Z) ^)) . (upper_bound A)) - ((tan * ((id Z) ^)) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13; ::_thesis: verum
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
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (tan * ((id Z) ^)) implies ( - (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)) ) ) )
set f = id Z;
assume A1: Z c= dom (tan * ((id Z) ^)) ; ::_thesis: ( - (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)) ) )
 dom (tan * ((id Z) ^)) c= dom ((id Z) ^) by RELAT_1:25;
then A2: Z c= dom ((id Z) ^) by A1, XBOOLE_1:1;
A3: not 0 in Z
proof
assume A4: 0 in Z ; ::_thesis: contradiction
dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2
.= (dom (id Z)) \ {0} by Lm1, A4 ;
then  not 0 in {0} by A4, A2, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
A5: Z c= dom (- (tan * ((id Z) ^))) by A1, VALUED_1:8;
A6: tan * ((id Z) ^) is_differentiable_on Z by A1, A3, FDIFF_8:8;
then A7: (- 1) (#) (tan * ((id Z) ^)) is_differentiable_on Z by A5, FDIFF_1:20;
A8: ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) by A3, FDIFF_5:4;
A9: for x being Real st x in Z holds
cos . (((id Z) ^) . x) <> 0
proof
let x be Real; ::_thesis: ( x in Z implies cos . (((id Z) ^) . x) <> 0 )
assume  x in Z ; ::_thesis: cos . (((id Z) ^) . x) <> 0
then  ((id Z) ^) . x in dom (sin / cos) by A1, FUNCT_1:11;
hence  cos . (((id Z) ^) . x) <> 0 by FDIFF_8:1; ::_thesis: verum
end;
 for x being Real st x in Z holds
((- (tan * ((id Z) ^))) `| Z) . x = 1 / ((x ^2) * ((cos . (1 / x)) ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((- (tan * ((id Z) ^))) `| Z) . x = 1 / ((x ^2) * ((cos . (1 / x)) ^2)) )
assume A10: x in Z ; ::_thesis: ((- (tan * ((id Z) ^))) `| Z) . x = 1 / ((x ^2) * ((cos . (1 / x)) ^2))
then A11: (id Z) ^ is_differentiable_in x by A8, FDIFF_1:9;
A12: cos . (((id Z) ^) . x) <> 0 by A9, A10;
then A13: tan is_differentiable_in ((id Z) ^) . x by FDIFF_7:46;
A14: tan * ((id Z) ^) is_differentiable_in x by A6, A10, FDIFF_1:9;
((- (tan * ((id Z) ^))) `| Z) . x = diff ((- (tan * ((id Z) ^))),x) by A7, A10, FDIFF_1:def_7
.= (- 1) * (diff ((tan * ((id Z) ^)),x)) by A14, FDIFF_1:15
.= (- 1) * ((diff (tan,(((id Z) ^) . x))) * (diff (((id Z) ^),x))) by A11, A13, FDIFF_2:13
.= (- 1) * ((1 / ((cos . (((id Z) ^) . x)) ^2)) * (diff (((id Z) ^),x))) by A12, FDIFF_7:46
.= (- 1) * ((diff (((id Z) ^),x)) / ((cos . (((id Z) . x) ")) ^2)) by A2, A10, RFUNCT_1:def_2
.= (- 1) * ((diff (((id Z) ^),x)) / ((cos . (1 * (x "))) ^2)) by A10, FUNCT_1:18
.= (- 1) * (((((id Z) ^) `| Z) . x) / ((cos . (1 * (x "))) ^2)) by A8, A10, FDIFF_1:def_7
.= (- 1) * ((- (1 / (x ^2))) / ((cos . (1 * (x "))) ^2)) by A10, A3, FDIFF_5:4
.= (- 1) * (((- 1) / (x ^2)) / ((cos . (1 / x)) ^2))
.= (- 1) * ((- 1) / ((x ^2) * ((cos . (1 / x)) ^2))) by XCMPLX_1:78
.= 1 / ((x ^2) * ((cos . (1 / x)) ^2)) ;
hence  ((- (tan * ((id Z) ^))) `| Z) . x = 1 / ((x ^2) * ((cos . (1 / x)) ^2)) ; ::_thesis: verum
end;
hence  ( - (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)) ) ) by A7; ::_thesis: verum
end;

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) ^))) . (upper_bound A)) - ((- (tan * ((id Z) ^))) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: 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) ^))) . (upper_bound A)) - ((- (tan * ((id Z) ^))) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: 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) ^))) . (upper_bound A)) - ((- (tan * ((id Z) ^))) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = ((- (tan * ((id Z) ^))) . (upper_bound A)) - ((- (tan * ((id Z) ^))) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = ((- (tan * ((id Z) ^))) . (upper_bound A)) - ((- (tan * ((id Z) ^))) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: - (tan * ((id Z) ^)) is_differentiable_on Z by A1, Th34;
A4: for x being Real st x in dom ((- (tan * ((id Z) ^))) `| Z) holds
((- (tan * ((id Z) ^))) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- (tan * ((id Z) ^))) `| Z) implies ((- (tan * ((id Z) ^))) `| Z) . x = f . x )
assume  x in dom ((- (tan * ((id Z) ^))) `| Z) ; ::_thesis: ((- (tan * ((id Z) ^))) `| Z) . x = f . x
then A5: x in Z by A3, FDIFF_1:def_7;
then ((- (tan * ((id Z) ^))) `| Z) . x = 1 / ((x ^2) * ((cos . (1 / x)) ^2)) by A1, Th34
.= f . x by A1, A5 ;
hence  ((- (tan * ((id Z) ^))) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((- (tan * ((id Z) ^))) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (- (tan * ((id Z) ^))) `| Z = f by A4, PARTFUN1:5;
hence  integral (f,A) = ((- (tan * ((id Z) ^))) . (upper_bound A)) - ((- (tan * ((id Z) ^))) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum
end;

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) ^)) . (upper_bound A)) - ((cot * ((id Z) ^)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: 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) ^)) . (upper_bound A)) - ((cot * ((id Z) ^)) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: 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) ^)) . (upper_bound A)) - ((cot * ((id Z) ^)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = ((cot * ((id Z) ^)) . (upper_bound A)) - ((cot * ((id Z) ^)) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = ((cot * ((id Z) ^)) . (upper_bound A)) - ((cot * ((id Z) ^)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: Z c= dom ((id Z) ^) by A1, FUNCT_1:101;
A4: not 0 in Z
proof
assume A5: 0 in Z ; ::_thesis: contradiction
dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2
.= (dom (id Z)) \ {0} by Lm1, A5 ;
then  not 0 in {0} by A5, A3, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
then A6: cot * ((id Z) ^) is_differentiable_on Z by A1, FDIFF_8:9;
A7: for x being Real st x in dom ((cot * ((id Z) ^)) `| Z) holds
((cot * ((id Z) ^)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((cot * ((id Z) ^)) `| Z) implies ((cot * ((id Z) ^)) `| Z) . x = f . x )
assume  x in dom ((cot * ((id Z) ^)) `| Z) ; ::_thesis: ((cot * ((id Z) ^)) `| Z) . x = f . x
then A8: x in Z by A6, FDIFF_1:def_7;
then ((cot * ((id Z) ^)) `| Z) . x = 1 / ((x ^2) * ((sin . (1 / x)) ^2)) by A1, A4, FDIFF_8:9
.= f . x by A1, A8 ;
hence  ((cot * ((id Z) ^)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((cot * ((id Z) ^)) `| Z) = dom f by A1, A6, FDIFF_1:def_7;
then  (cot * ((id Z) ^)) `| Z = f by A7, PARTFUN1:5;
hence  integral (f,A) = ((cot * ((id Z) ^)) . (upper_bound A)) - ((cot * ((id Z) ^)) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGR13:37
for A being non empty closed_interval Subset of REAL
for f1, 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
( f1 . x = 1 & arctan . x > 0 ) ) & f = ((f1 + (#Z 2)) (#) arctan) ^ & Z c= ].(- 1),1.[ & Z c= dom (ln * arctan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln * arctan) . (upper_bound A)) - ((ln * arctan) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
( f1 . x = 1 & arctan . x > 0 ) ) & f = ((f1 + (#Z 2)) (#) arctan) ^ & Z c= ].(- 1),1.[ & Z c= dom (ln * arctan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln * arctan) . (upper_bound A)) - ((ln * arctan) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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 (ln * arctan) & Z = dom f & f | A is continuous holds
integral (f,A) = ((ln * arctan) . (upper_bound A)) - ((ln * arctan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 (ln * arctan) & Z = dom f & f | A is continuous implies integral (f,A) = ((ln * arctan) . (upper_bound A)) - ((ln * arctan) . (lower_bound A)) )
assume A1: ( 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 (ln * arctan) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((ln * arctan) . (upper_bound A)) - ((ln * arctan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: for x being Real st x in Z holds
arctan . x > 0 by A1;
then A4: ln * arctan is_differentiable_on Z by A1, SIN_COS9:89;
 Z c= dom ((f1 + (#Z 2)) (#) arctan) by A1, RFUNCT_1:1;
then  Z c= (dom (f1 + (#Z 2))) /\ (dom arctan) by VALUED_1:def_4;
then A5: Z c= dom (f1 + (#Z 2)) by XBOOLE_1:18;
A6: for x being Real st x in Z holds
f . x = 1 / ((1 + (x ^2)) * (arctan . x))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = 1 / ((1 + (x ^2)) * (arctan . x)) )
assume A7: x in Z ; ::_thesis: f . x = 1 / ((1 + (x ^2)) * (arctan . x))
then (((f1 + (#Z 2)) (#) arctan) ^) . x = 1 / (((f1 + (#Z 2)) (#) arctan) . x) by A1, RFUNCT_1:def_2
.= 1 / (((f1 + (#Z 2)) . x) * (arctan . x)) by VALUED_1:5
.= 1 / (((f1 . x) + ((#Z 2) . x)) * (arctan . x)) by A5, A7, VALUED_1:def_1
.= 1 / (((f1 . x) + (x #Z 2)) * (arctan . x)) by TAYLOR_1:def_1
.= 1 / ((1 + (x #Z 2)) * (arctan . x)) by A1, A7
.= 1 / ((1 + (x ^2)) * (arctan . x)) by FDIFF_7:1 ;
hence  f . x = 1 / ((1 + (x ^2)) * (arctan . x)) by A1; ::_thesis: verum
end;
A8: for x being Real st x in dom ((ln * arctan) `| Z) holds
((ln * arctan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((ln * arctan) `| Z) implies ((ln * arctan) `| Z) . x = f . x )
assume  x in dom ((ln * arctan) `| Z) ; ::_thesis: ((ln * arctan) `| Z) . x = f . x
then A9: x in Z by A4, FDIFF_1:def_7;
then ((ln * arctan) `| Z) . x = 1 / ((1 + (x ^2)) * (arctan . x)) by A1, A3, SIN_COS9:89
.= f . x by A6, A9 ;
hence  ((ln * arctan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((ln * arctan) `| Z) = dom f by A1, A4, FDIFF_1:def_7;
then  (ln * arctan) `| Z = f by A8, PARTFUN1:5;
hence  integral (f,A) = ((ln * arctan) . (upper_bound A)) - ((ln * arctan) . (lower_bound A)) by A1, A2, A4, INTEGRA5:13; ::_thesis: verum
end;

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) . (upper_bound A)) - (((#Z n) * arctan) . (lower_bound A))
proof
let n be Element of NAT ; ::_thesis: 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) . (upper_bound A)) - (((#Z n) * arctan) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: 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) . (upper_bound A)) - (((#Z n) * arctan) . (lower_bound A))
let f, f1 be PartFunc of REAL,REAL; ::_thesis: 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) . (upper_bound A)) - (((#Z n) * arctan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = (((#Z n) * arctan) . (upper_bound A)) - (((#Z n) * arctan) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = (((#Z n) * arctan) . (upper_bound A)) - (((#Z n) * arctan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: (#Z n) * arctan is_differentiable_on Z by A1, SIN_COS9:91;
A4: Z = dom (((#Z (n - 1)) * arctan) / (f1 + (#Z 2))) by A1, VALUED_1:def_5;
then  Z c= (dom ((#Z (n - 1)) * arctan)) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by RFUNCT_1:def_1;
then A5: ( Z c= dom ((#Z (n - 1)) * arctan) & Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) ) by XBOOLE_1:18;
then A6: Z c= dom ((f1 + (#Z 2)) ^) by RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A7: Z c= dom (f1 + (#Z 2)) by A6, XBOOLE_1:1;
A8: for x being Real st x in Z holds
f . x = (n * ((arctan . x) #Z (n - 1))) / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (n * ((arctan . x) #Z (n - 1))) / (1 + (x ^2)) )
assume A9: x in Z ; ::_thesis: f . x = (n * ((arctan . x) #Z (n - 1))) / (1 + (x ^2))
(n (#) (((#Z (n - 1)) * arctan) / (f1 + (#Z 2)))) . x = n * ((((#Z (n - 1)) * arctan) / (f1 + (#Z 2))) . x) by VALUED_1:6
.= n * ((((#Z (n - 1)) * arctan) . x) * (((f1 + (#Z 2)) . x) ")) by A4, A9, RFUNCT_1:def_1
.= (n * (((#Z (n - 1)) * arctan) . x)) / ((f1 + (#Z 2)) . x)
.= (n * ((#Z (n - 1)) . (arctan . x))) / ((f1 + (#Z 2)) . x) by A5, A9, FUNCT_1:12
.= (n * ((arctan . x) #Z (n - 1))) / ((f1 + (#Z 2)) . x) by TAYLOR_1:def_1
.= (n * ((arctan . x) #Z (n - 1))) / ((f1 . x) + ((#Z 2) . x)) by A7, A9, VALUED_1:def_1
.= (n * ((arctan . x) #Z (n - 1))) / (1 + ((#Z 2) . x)) by A1, A9
.= (n * ((arctan . x) #Z (n - 1))) / (1 + (x #Z 2)) by TAYLOR_1:def_1
.= (n * ((arctan . x) #Z (n - 1))) / (1 + (x ^2)) by FDIFF_7:1 ;
hence  f . x = (n * ((arctan . x) #Z (n - 1))) / (1 + (x ^2)) by A1; ::_thesis: verum
end;
A10: for x being Real st x in dom (((#Z n) * arctan) `| Z) holds
(((#Z n) * arctan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((#Z n) * arctan) `| Z) implies (((#Z n) * arctan) `| Z) . x = f . x )
assume  x in dom (((#Z n) * arctan) `| Z) ; ::_thesis: (((#Z n) * arctan) `| Z) . x = f . x
then A11: x in Z by A3, FDIFF_1:def_7;
then (((#Z n) * arctan) `| Z) . x = (n * ((arctan . x) #Z (n - 1))) / (1 + (x ^2)) by A1, SIN_COS9:91
.= f . x by A8, A11 ;
hence  (((#Z n) * arctan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((#Z n) * arctan) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  ((#Z n) * arctan) `| Z = f by A10, PARTFUN1:5;
hence  integral (f,A) = (((#Z n) * arctan) . (upper_bound A)) - (((#Z n) * arctan) . (lower_bound A)) by A1, A2, INTEGRA5:13, SIN_COS9:91; ::_thesis: verum
end;

theorem :: INTEGR13:39
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f1, 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
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) . (upper_bound A)) - (((#Z n) * arccot) . (lower_bound A))
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f1, 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
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) . (upper_bound A)) - (((#Z n) * arccot) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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) . (upper_bound A)) - (((#Z n) * arccot) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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) . (upper_bound A)) - (((#Z n) * arccot) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = (((#Z n) * arccot) . (upper_bound A)) - (((#Z n) * arccot) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = (((#Z n) * arccot) . (upper_bound A)) - (((#Z n) * arccot) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: (#Z n) * arccot is_differentiable_on Z by A1, SIN_COS9:92;
 Z = dom (n (#) (((#Z (n - 1)) * arccot) / (f1 + (#Z 2)))) by A1, VALUED_1:8;
then A4: Z = dom (((#Z (n - 1)) * arccot) / (f1 + (#Z 2))) by VALUED_1:def_5;
then  Z c= (dom ((#Z (n - 1)) * arccot)) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by RFUNCT_1:def_1;
then A5: ( Z c= dom ((#Z (n - 1)) * arccot) & Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) ) by XBOOLE_1:18;
then A6: Z c= dom ((f1 + (#Z 2)) ^) by RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A7: Z c= dom (f1 + (#Z 2)) by A6, XBOOLE_1:1;
A8: for x being Real st x in Z holds
f . x = - ((n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = - ((n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2))) )
assume A9: x in Z ; ::_thesis: f . x = - ((n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)))
(- (n (#) (((#Z (n - 1)) * arccot) / (f1 + (#Z 2))))) . x = - ((n (#) (((#Z (n - 1)) * arccot) / (f1 + (#Z 2)))) . x) by VALUED_1:8
.= - (n * ((((#Z (n - 1)) * arccot) / (f1 + (#Z 2))) . x)) by VALUED_1:6
.= - (n * ((((#Z (n - 1)) * arccot) . x) * (((f1 + (#Z 2)) . x) "))) by A4, A9, RFUNCT_1:def_1
.= - ((n * (((#Z (n - 1)) * arccot) . x)) / ((f1 + (#Z 2)) . x))
.= - ((n * ((#Z (n - 1)) . (arccot . x))) / ((f1 + (#Z 2)) . x)) by A5, A9, FUNCT_1:12
.= - ((n * ((arccot . x) #Z (n - 1))) / ((f1 + (#Z 2)) . x)) by TAYLOR_1:def_1
.= - ((n * ((arccot . x) #Z (n - 1))) / ((f1 . x) + ((#Z 2) . x))) by A7, A9, VALUED_1:def_1
.= - ((n * ((arccot . x) #Z (n - 1))) / (1 + ((#Z 2) . x))) by A1, A9
.= - ((n * ((arccot . x) #Z (n - 1))) / (1 + (x #Z 2))) by TAYLOR_1:def_1
.= - ((n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2))) by FDIFF_7:1 ;
hence  f . x = - ((n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2))) by A1; ::_thesis: verum
end;
A10: for x being Real st x in dom (((#Z n) * arccot) `| Z) holds
(((#Z n) * arccot) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((#Z n) * arccot) `| Z) implies (((#Z n) * arccot) `| Z) . x = f . x )
assume  x in dom (((#Z n) * arccot) `| Z) ; ::_thesis: (((#Z n) * arccot) `| Z) . x = f . x
then A11: x in Z by A3, FDIFF_1:def_7;
then (((#Z n) * arccot) `| Z) . x = - ((n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2))) by A1, SIN_COS9:92
.= f . x by A11, A8 ;
hence  (((#Z n) * arccot) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((#Z n) * arccot) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  ((#Z n) * arccot) `| Z = f by A10, PARTFUN1:5;
hence  integral (f,A) = (((#Z n) * arccot) . (upper_bound A)) - (((#Z n) * arccot) . (lower_bound A)) by A1, A2, INTEGRA5:13, SIN_COS9:92; ::_thesis: verum
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 * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) ) )
proof
let n be Element of NAT ; ::_thesis: 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 * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) ) )
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z n) * arccot) & Z c= ].(- 1),1.[ implies ( - ((#Z n) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * arccot)) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) ) ) )
assume A1: ( Z c= dom ((#Z n) * arccot) & Z c= ].(- 1),1.[ ) ; ::_thesis: ( - ((#Z n) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * arccot)) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) ) )
then A2: Z c= dom (- ((#Z n) * arccot)) by VALUED_1:8;
A3: (#Z n) * arccot is_differentiable_on Z by A1, SIN_COS9:92;
then A4: (- 1) (#) ((#Z n) * arccot) is_differentiable_on Z by A2, FDIFF_1:20;
 for x being Real st x in Z holds
((- ((#Z n) * arccot)) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((- ((#Z n) * arccot)) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) )
assume A5: x in Z ; ::_thesis: ((- ((#Z n) * arccot)) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2))
then A6: ( - 1 < x & x < 1 ) by A1, XXREAL_1:4;
 arccot is_differentiable_on Z by A1, SIN_COS9:82;
then A7: arccot is_differentiable_in x by A5, FDIFF_1:9;
A8: (#Z n) * arccot is_differentiable_in x by A3, A5, FDIFF_1:9;
((- ((#Z n) * arccot)) `| Z) . x = diff ((- ((#Z n) * arccot)),x) by A4, A5, FDIFF_1:def_7
.= (- 1) * (diff (((#Z n) * arccot),x)) by A8, FDIFF_1:15
.= (- 1) * ((n * ((arccot . x) #Z (n - 1))) * (diff (arccot,x))) by A7, TAYLOR_1:3
.= (- 1) * ((n * ((arccot . x) #Z (n - 1))) * (- (1 / (1 + (x ^2))))) by A6, SIN_COS9:76
.= (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) ;
hence  ((- ((#Z n) * arccot)) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) ; ::_thesis: verum
end;
hence  ( - ((#Z n) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * arccot)) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) ) ) by A2, A3, Lm3, FDIFF_1:20; ::_thesis: verum
end;

theorem :: INTEGR13:41
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f1, 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
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)) . (upper_bound A)) - ((- ((#Z n) * arccot)) . (lower_bound A))
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f1, 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
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)) . (upper_bound A)) - ((- ((#Z n) * arccot)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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)) . (upper_bound A)) - ((- ((#Z n) * arccot)) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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)) . (upper_bound A)) - ((- ((#Z n) * arccot)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = ((- ((#Z n) * arccot)) . (upper_bound A)) - ((- ((#Z n) * arccot)) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = ((- ((#Z n) * arccot)) . (upper_bound A)) - ((- ((#Z n) * arccot)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: - ((#Z n) * arccot) is_differentiable_on Z by A1, Th40;
A4: Z = dom (((#Z (n - 1)) * arccot) / (f1 + (#Z 2))) by A1, VALUED_1:def_5;
then  Z c= (dom ((#Z (n - 1)) * arccot)) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by RFUNCT_1:def_1;
then A5: ( Z c= dom ((#Z (n - 1)) * arccot) & Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) ) by XBOOLE_1:18;
then A6: Z c= dom ((f1 + (#Z 2)) ^) by RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A7: Z c= dom (f1 + (#Z 2)) by A6, XBOOLE_1:1;
A8: for x being Real st x in Z holds
f . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) )
assume A9: x in Z ; ::_thesis: f . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2))
(n (#) (((#Z (n - 1)) * arccot) / (f1 + (#Z 2)))) . x = n * ((((#Z (n - 1)) * arccot) / (f1 + (#Z 2))) . x) by VALUED_1:6
.= n * ((((#Z (n - 1)) * arccot) . x) * (((f1 + (#Z 2)) . x) ")) by A4, A9, RFUNCT_1:def_1
.= (n * (((#Z (n - 1)) * arccot) . x)) / ((f1 + (#Z 2)) . x)
.= (n * ((#Z (n - 1)) . (arccot . x))) / ((f1 + (#Z 2)) . x) by A5, A9, FUNCT_1:12
.= (n * ((arccot . x) #Z (n - 1))) / ((f1 + (#Z 2)) . x) by TAYLOR_1:def_1
.= (n * ((arccot . x) #Z (n - 1))) / ((f1 . x) + ((#Z 2) . x)) by A7, A9, VALUED_1:def_1
.= (n * ((arccot . x) #Z (n - 1))) / (1 + ((#Z 2) . x)) by A1, A9
.= (n * ((arccot . x) #Z (n - 1))) / (1 + (x #Z 2)) by TAYLOR_1:def_1
.= (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) by FDIFF_7:1 ;
hence  f . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) by A1; ::_thesis: verum
end;
A10: for x being Real st x in dom ((- ((#Z n) * arccot)) `| Z) holds
((- ((#Z n) * arccot)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- ((#Z n) * arccot)) `| Z) implies ((- ((#Z n) * arccot)) `| Z) . x = f . x )
assume  x in dom ((- ((#Z n) * arccot)) `| Z) ; ::_thesis: ((- ((#Z n) * arccot)) `| Z) . x = f . x
then A11: x in Z by A3, FDIFF_1:def_7;
then ((- ((#Z n) * arccot)) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) by A1, Th40
.= f . x by A11, A8 ;
hence  ((- ((#Z n) * arccot)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((- ((#Z n) * arccot)) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (- ((#Z n) * arccot)) `| Z = f by A10, PARTFUN1:5;
hence  integral (f,A) = ((- ((#Z n) * arccot)) . (upper_bound A)) - ((- ((#Z n) * arccot)) . (lower_bound A)) by A1, A2, Th40, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGR13:42
for A being non empty closed_interval Subset of REAL
for f1, 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
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)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arctan)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arctan)) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arctan)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = (((1 / 2) (#) ((#Z 2) * arctan)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arctan)) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = (((1 / 2) (#) ((#Z 2) * arctan)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arctan)) . (lower_bound A))
then A2: Z c= dom ((1 / 2) (#) ((#Z 2) * arctan)) by VALUED_1:def_5;
A3: ( f is_integrable_on A & f | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A4: (1 / 2) (#) ((#Z 2) * arctan) is_differentiable_on Z by A1, A2, SIN_COS9:93;
 Z c= (dom arctan) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by A1, RFUNCT_1:def_1;
then  Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) by XBOOLE_1:18;
then A5: Z c= dom ((f1 + (#Z 2)) ^) by RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A6: Z c= dom (f1 + (#Z 2)) by A5, XBOOLE_1:1;
A7: for x being Real st x in Z holds
f . x = (arctan . x) / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (arctan . x) / (1 + (x ^2)) )
assume A8: x in Z ; ::_thesis: f . x = (arctan . x) / (1 + (x ^2))
then (arctan / (f1 + (#Z 2))) . x = (arctan . x) / ((f1 + (#Z 2)) . x) by A1, RFUNCT_1:def_1
.= (arctan . x) / ((f1 . x) + ((#Z 2) . x)) by A6, A8, VALUED_1:def_1
.= (arctan . x) / ((f1 . x) + (x #Z 2)) by TAYLOR_1:def_1
.= (arctan . x) / (1 + (x #Z 2)) by A1, A8
.= (arctan . x) / (1 + (x ^2)) by FDIFF_7:1 ;
hence  f . x = (arctan . x) / (1 + (x ^2)) by A1; ::_thesis: verum
end;
A9: for x being Real st x in dom (((1 / 2) (#) ((#Z 2) * arctan)) `| Z) holds
(((1 / 2) (#) ((#Z 2) * arctan)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((1 / 2) (#) ((#Z 2) * arctan)) `| Z) implies (((1 / 2) (#) ((#Z 2) * arctan)) `| Z) . x = f . x )
assume  x in dom (((1 / 2) (#) ((#Z 2) * arctan)) `| Z) ; ::_thesis: (((1 / 2) (#) ((#Z 2) * arctan)) `| Z) . x = f . x
then A10: x in Z by A4, FDIFF_1:def_7;
then (((1 / 2) (#) ((#Z 2) * arctan)) `| Z) . x = (arctan . x) / (1 + (x ^2)) by A1, A2, SIN_COS9:93
.= f . x by A7, A10 ;
hence  (((1 / 2) (#) ((#Z 2) * arctan)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((1 / 2) (#) ((#Z 2) * arctan)) `| Z) = dom f by A1, A4, FDIFF_1:def_7;
then  ((1 / 2) (#) ((#Z 2) * arctan)) `| Z = f by A9, PARTFUN1:5;
hence  integral (f,A) = (((1 / 2) (#) ((#Z 2) * arctan)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arctan)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13, SIN_COS9:93; ::_thesis: verum
end;

theorem :: INTEGR13:43
for A being non empty closed_interval Subset of REAL
for f1, 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
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)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccot)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccot)) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccot)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = (((1 / 2) (#) ((#Z 2) * arccot)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccot)) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = (((1 / 2) (#) ((#Z 2) * arccot)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccot)) . (lower_bound A))
then A2: Z c= dom ((1 / 2) (#) ((#Z 2) * arccot)) by VALUED_1:def_5;
A3: ( f is_integrable_on A & f | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A4: (1 / 2) (#) ((#Z 2) * arccot) is_differentiable_on Z by A1, A2, SIN_COS9:94;
A5: Z = dom (arccot / (f1 + (#Z 2))) by A1, VALUED_1:8;
then  Z c= (dom arccot) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by RFUNCT_1:def_1;
then  Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) by XBOOLE_1:18;
then A6: Z c= dom ((f1 + (#Z 2)) ^) by RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A7: Z c= dom (f1 + (#Z 2)) by A6, XBOOLE_1:1;
A8: for x being Real st x in Z holds
f . x = - ((arccot . x) / (1 + (x ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = - ((arccot . x) / (1 + (x ^2))) )
assume A9: x in Z ; ::_thesis: f . x = - ((arccot . x) / (1 + (x ^2)))
(- (arccot / (f1 + (#Z 2)))) . x = - ((arccot / (f1 + (#Z 2))) . x) by VALUED_1:8
.= - ((arccot . x) / ((f1 + (#Z 2)) . x)) by A5, A9, RFUNCT_1:def_1
.= - ((arccot . x) / ((f1 . x) + ((#Z 2) . x))) by A7, A9, VALUED_1:def_1
.= - ((arccot . x) / ((f1 . x) + (x #Z 2))) by TAYLOR_1:def_1
.= - ((arccot . x) / (1 + (x #Z 2))) by A1, A9
.= - ((arccot . x) / (1 + (x ^2))) by FDIFF_7:1 ;
hence  f . x = - ((arccot . x) / (1 + (x ^2))) by A1; ::_thesis: verum
end;
A10: for x being Real st x in dom (((1 / 2) (#) ((#Z 2) * arccot)) `| Z) holds
(((1 / 2) (#) ((#Z 2) * arccot)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((1 / 2) (#) ((#Z 2) * arccot)) `| Z) implies (((1 / 2) (#) ((#Z 2) * arccot)) `| Z) . x = f . x )
assume  x in dom (((1 / 2) (#) ((#Z 2) * arccot)) `| Z) ; ::_thesis: (((1 / 2) (#) ((#Z 2) * arccot)) `| Z) . x = f . x
then A11: x in Z by A4, FDIFF_1:def_7;
then (((1 / 2) (#) ((#Z 2) * arccot)) `| Z) . x = - ((arccot . x) / (1 + (x ^2))) by A1, A2, SIN_COS9:94
.= f . x by A8, A11 ;
hence  (((1 / 2) (#) ((#Z 2) * arccot)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((1 / 2) (#) ((#Z 2) * arccot)) `| Z) = dom f by A1, A4, FDIFF_1:def_7;
then  ((1 / 2) (#) ((#Z 2) * arccot)) `| Z = f by A10, PARTFUN1:5;
hence  integral (f,A) = (((1 / 2) (#) ((#Z 2) * arccot)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccot)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13, SIN_COS9:94; ::_thesis: verum
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 = (arccot . x) / (1 + (x ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z 2) * arccot) & Z c= ].(- 1),1.[ implies ( - ((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 = (arccot . x) / (1 + (x ^2)) ) ) )
assume A1: ( Z c= dom ((#Z 2) * arccot) & Z c= ].(- 1),1.[ ) ; ::_thesis: ( - ((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 = (arccot . x) / (1 + (x ^2)) ) )
then A2: Z c= dom ((1 / 2) (#) ((#Z 2) * arccot)) by VALUED_1:def_5;
then A3: Z c= dom (- ((1 / 2) (#) ((#Z 2) * arccot))) by VALUED_1:8;
A4: (1 / 2) (#) ((#Z 2) * arccot) is_differentiable_on Z by A2, A1, SIN_COS9:94;
then A5: (- 1) (#) ((1 / 2) (#) ((#Z 2) * arccot)) is_differentiable_on Z by A3, FDIFF_1:20;
A6: ( (#Z 2) * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z 2) * arccot) `| Z) . x = - ((2 * ((arccot . x) #Z (2 - 1))) / (1 + (x ^2))) ) ) by A1, SIN_COS9:92;
 for x being Real st x in Z holds
((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = (arccot . x) / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = (arccot . x) / (1 + (x ^2)) )
assume A7: x in Z ; ::_thesis: ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = (arccot . x) / (1 + (x ^2))
then A8: (1 / 2) (#) ((#Z 2) * arccot) is_differentiable_in x by A4, FDIFF_1:9;
A9: (#Z 2) * arccot is_differentiable_in x by A6, A7, FDIFF_1:9;
((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = diff ((- ((1 / 2) (#) ((#Z 2) * arccot))),x) by A5, A7, FDIFF_1:def_7
.= (- 1) * (diff (((1 / 2) (#) ((#Z 2) * arccot)),x)) by A8, FDIFF_1:15
.= (- 1) * ((1 / 2) * (diff (((#Z 2) * arccot),x))) by A9, FDIFF_1:15
.= (- 1) * ((1 / 2) * ((((#Z 2) * arccot) `| Z) . x)) by A6, A7, FDIFF_1:def_7
.= (- 1) * ((1 / 2) * (- ((2 * ((arccot . x) #Z (2 - 1))) / (1 + (x ^2))))) by A1, A7, SIN_COS9:92
.= (- 1) * (- ((1 / 2) * ((2 * ((arccot . x) #Z 1)) / (1 + (x ^2)))))
.= (- 1) * (- ((1 / 2) * ((2 * (arccot . x)) / (1 + (x ^2))))) by PREPOWER:35
.= (arccot . x) / (1 + (x ^2)) ;
hence  ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = (arccot . x) / (1 + (x ^2)) ; ::_thesis: verum
end;
hence  ( - ((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 = (arccot . x) / (1 + (x ^2)) ) ) by A3, A4, Lm3, FDIFF_1:20; ::_thesis: verum
end;

theorem :: INTEGR13:45
for A being non empty closed_interval Subset of REAL
for f1, 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
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))) . (upper_bound A)) - ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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))) . (upper_bound A)) - ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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))) . (upper_bound A)) - ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (upper_bound A)) - ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (upper_bound A)) - ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: - ((1 / 2) (#) ((#Z 2) * arccot)) is_differentiable_on Z by A1, Th44;
 Z c= (dom arccot) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by A1, RFUNCT_1:def_1;
then  Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) by XBOOLE_1:18;
then A4: Z c= dom ((f1 + (#Z 2)) ^) by RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A5: Z c= dom (f1 + (#Z 2)) by A4, XBOOLE_1:1;
A6: for x being Real st x in Z holds
f . x = (arccot . x) / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (arccot . x) / (1 + (x ^2)) )
assume A7: x in Z ; ::_thesis: f . x = (arccot . x) / (1 + (x ^2))
then (arccot / (f1 + (#Z 2))) . x = (arccot . x) / ((f1 + (#Z 2)) . x) by A1, RFUNCT_1:def_1
.= (arccot . x) / ((f1 . x) + ((#Z 2) . x)) by A5, A7, VALUED_1:def_1
.= (arccot . x) / ((f1 . x) + (x #Z 2)) by TAYLOR_1:def_1
.= (arccot . x) / (1 + (x #Z 2)) by A1, A7
.= (arccot . x) / (1 + (x ^2)) by FDIFF_7:1 ;
hence  f . x = (arccot . x) / (1 + (x ^2)) by A1; ::_thesis: verum
end;
A8: for x being Real st x in dom ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) holds
((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) implies ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = f . x )
assume  x in dom ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) ; ::_thesis: ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = f . x
then A9: x in Z by A3, FDIFF_1:def_7;
then ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = (arccot . x) / (1 + (x ^2)) by A1, Th44
.= f . x by A6, A9 ;
hence  ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z = f by A8, PARTFUN1:5;
hence  integral (f,A) = ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (upper_bound A)) - ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (lower_bound A)) by A1, A2, Th44, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGR13:46
for A being non empty closed_interval Subset of REAL
for f1, 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
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) . (upper_bound A)) - (((id Z) (#) arctan) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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) . (upper_bound A)) - (((id Z) (#) arctan) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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) . (upper_bound A)) - (((id Z) (#) arctan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = (((id Z) (#) arctan) . (upper_bound A)) - (((id Z) (#) arctan) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = (((id Z) (#) arctan) . (upper_bound A)) - (((id Z) (#) arctan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom arctan) /\ (dom ((id Z) / (f1 + (#Z 2)))) by A1, VALUED_1:def_1;
then A3: ( Z c= dom arctan & Z c= dom ((id Z) / (f1 + (#Z 2))) ) by XBOOLE_1:18;
then  Z c= (dom (id Z)) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by RFUNCT_1:def_1;
then A4: Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) by XBOOLE_1:18;
A5: (id Z) (#) arctan is_differentiable_on Z by A1, SIN_COS9:95;
A6: Z c= dom ((f1 + (#Z 2)) ^) by A4, RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A7: Z c= dom (f1 + (#Z 2)) by A6, XBOOLE_1:1;
A8: for x being Real st x in Z holds
f . x = (arctan . x) + (x / (1 + (x ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (arctan . x) + (x / (1 + (x ^2))) )
assume A9: x in Z ; ::_thesis: f . x = (arctan . x) + (x / (1 + (x ^2)))
then (arctan + ((id Z) / (f1 + (#Z 2)))) . x = (arctan . x) + (((id Z) / (f1 + (#Z 2))) . x) by A1, VALUED_1:def_1
.= (arctan . x) + (((id Z) . x) / ((f1 + (#Z 2)) . x)) by A3, A9, RFUNCT_1:def_1
.= (arctan . x) + (x / ((f1 + (#Z 2)) . x)) by A9, FUNCT_1:18
.= (arctan . x) + (x / ((f1 . x) + ((#Z 2) . x))) by A7, A9, VALUED_1:def_1
.= (arctan . x) + (x / (1 + ((#Z 2) . x))) by A1, A9
.= (arctan . x) + (x / (1 + (x #Z 2))) by TAYLOR_1:def_1
.= (arctan . x) + (x / (1 + (x ^2))) by FDIFF_7:1 ;
hence  f . x = (arctan . x) + (x / (1 + (x ^2))) by A1; ::_thesis: verum
end;
A10: for x being Real st x in dom (((id Z) (#) arctan) `| Z) holds
(((id Z) (#) arctan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((id Z) (#) arctan) `| Z) implies (((id Z) (#) arctan) `| Z) . x = f . x )
assume  x in dom (((id Z) (#) arctan) `| Z) ; ::_thesis: (((id Z) (#) arctan) `| Z) . x = f . x
then A11: x in Z by A5, FDIFF_1:def_7;
then (((id Z) (#) arctan) `| Z) . x = (arctan . x) + (x / (1 + (x ^2))) by A1, SIN_COS9:95
.= f . x by A8, A11 ;
hence  (((id Z) (#) arctan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((id Z) (#) arctan) `| Z) = dom f by A1, A5, FDIFF_1:def_7;
then  ((id Z) (#) arctan) `| Z = f by A10, PARTFUN1:5;
hence  integral (f,A) = (((id Z) (#) arctan) . (upper_bound A)) - (((id Z) (#) arctan) . (lower_bound A)) by A1, A2, INTEGRA5:13, SIN_COS9:95; ::_thesis: verum
end;

theorem :: INTEGR13:47
for A being non empty closed_interval Subset of REAL
for f1, 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
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) . (upper_bound A)) - (((id Z) (#) arccot) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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) . (upper_bound A)) - (((id Z) (#) arccot) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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) . (upper_bound A)) - (((id Z) (#) arccot) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = (((id Z) (#) arccot) . (upper_bound A)) - (((id Z) (#) arccot) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = (((id Z) (#) arccot) . (upper_bound A)) - (((id Z) (#) arccot) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom arccot) /\ (dom ((id Z) / (f1 + (#Z 2)))) by A1, VALUED_1:12;
then A3: ( Z c= dom arccot & Z c= dom ((id Z) / (f1 + (#Z 2))) ) by XBOOLE_1:18;
then  Z c= (dom (id Z)) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by RFUNCT_1:def_1;
then A4: Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) by XBOOLE_1:18;
A5: (id Z) (#) arccot is_differentiable_on Z by A1, SIN_COS9:96;
A6: Z c= dom ((f1 + (#Z 2)) ^) by A4, RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A7: Z c= dom (f1 + (#Z 2)) by A6, XBOOLE_1:1;
A8: for x being Real st x in Z holds
f . x = (arccot . x) - (x / (1 + (x ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (arccot . x) - (x / (1 + (x ^2))) )
assume A9: x in Z ; ::_thesis: f . x = (arccot . x) - (x / (1 + (x ^2)))
then (arccot - ((id Z) / (f1 + (#Z 2)))) . x = (arccot . x) - (((id Z) / (f1 + (#Z 2))) . x) by A1, VALUED_1:13
.= (arccot . x) - (((id Z) . x) / ((f1 + (#Z 2)) . x)) by A3, A9, RFUNCT_1:def_1
.= (arccot . x) - (x / ((f1 + (#Z 2)) . x)) by A9, FUNCT_1:18
.= (arccot . x) - (x / ((f1 . x) + ((#Z 2) . x))) by A7, A9, VALUED_1:def_1
.= (arccot . x) - (x / (1 + ((#Z 2) . x))) by A1, A9
.= (arccot . x) - (x / (1 + (x #Z 2))) by TAYLOR_1:def_1
.= (arccot . x) - (x / (1 + (x ^2))) by FDIFF_7:1 ;
hence  f . x = (arccot . x) - (x / (1 + (x ^2))) by A1; ::_thesis: verum
end;
A10: for x being Real st x in dom (((id Z) (#) arccot) `| Z) holds
(((id Z) (#) arccot) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((id Z) (#) arccot) `| Z) implies (((id Z) (#) arccot) `| Z) . x = f . x )
assume  x in dom (((id Z) (#) arccot) `| Z) ; ::_thesis: (((id Z) (#) arccot) `| Z) . x = f . x
then A11: x in Z by A5, FDIFF_1:def_7;
then (((id Z) (#) arccot) `| Z) . x = (arccot . x) - (x / (1 + (x ^2))) by A1, SIN_COS9:96
.= f . x by A11, A8 ;
hence  (((id Z) (#) arccot) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((id Z) (#) arccot) `| Z) = dom f by A1, A5, FDIFF_1:def_7;
then  ((id Z) (#) arccot) `| Z = f by A10, PARTFUN1:5;
hence  integral (f,A) = (((id Z) (#) arccot) . (upper_bound A)) - (((id Z) (#) arccot) . (lower_bound A)) by A1, A2, INTEGRA5:13, SIN_COS9:96; ::_thesis: verum
end;

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 = (exp_R * arctan) / (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) = ((exp_R * arctan) . (upper_bound A)) - ((exp_R * arctan) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arctan) / (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) = ((exp_R * arctan) . (upper_bound A)) - ((exp_R * arctan) . (lower_bound A))
let f, f1 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arctan) / (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) = ((exp_R * arctan) . (upper_bound A)) - ((exp_R * arctan) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arctan) / (f1 + (#Z 2)) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R * arctan) . (upper_bound A)) - ((exp_R * arctan) . (lower_bound A)) )
assume A1: ( A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arctan) / (f1 + (#Z 2)) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R * arctan) . (upper_bound A)) - ((exp_R * arctan) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom (exp_R * arctan)) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by A1, RFUNCT_1:def_1;
then A3: ( Z c= dom (exp_R * arctan) & Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) ) by XBOOLE_1:18;
then A4: Z c= dom ((f1 + (#Z 2)) ^) by RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A5: Z c= dom (f1 + (#Z 2)) by A4, XBOOLE_1:1;
A6: exp_R * arctan is_differentiable_on Z by A1, A3, SIN_COS9:119;
A7: for x being Real st x in Z holds
f . x = (exp_R . (arctan . x)) / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (exp_R . (arctan . x)) / (1 + (x ^2)) )
assume A8: x in Z ; ::_thesis: f . x = (exp_R . (arctan . x)) / (1 + (x ^2))
then ((exp_R * arctan) / (f1 + (#Z 2))) . x = ((exp_R * arctan) . x) / ((f1 + (#Z 2)) . x) by A1, RFUNCT_1:def_1
.= (exp_R . (arctan . x)) / ((f1 + (#Z 2)) . x) by A3, A8, FUNCT_1:12
.= (exp_R . (arctan . x)) / ((f1 . x) + ((#Z 2) . x)) by A5, A8, VALUED_1:def_1
.= (exp_R . (arctan . x)) / (1 + ((#Z 2) . x)) by A1, A8
.= (exp_R . (arctan . x)) / (1 + (x #Z 2)) by TAYLOR_1:def_1
.= (exp_R . (arctan . x)) / (1 + (x ^2)) by FDIFF_7:1 ;
hence  f . x = (exp_R . (arctan . x)) / (1 + (x ^2)) by A1; ::_thesis: verum
end;
A9: for x being Real st x in dom ((exp_R * arctan) `| Z) holds
((exp_R * arctan) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((exp_R * arctan) `| Z) implies ((exp_R * arctan) `| Z) . x = f . x )
assume  x in dom ((exp_R * arctan) `| Z) ; ::_thesis: ((exp_R * arctan) `| Z) . x = f . x
then A10: x in Z by A6, FDIFF_1:def_7;
then ((exp_R * arctan) `| Z) . x = (exp_R . (arctan . x)) / (1 + (x ^2)) by A1, A3, SIN_COS9:119
.= f . x by A10, A7 ;
hence  ((exp_R * arctan) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((exp_R * arctan) `| Z) = dom f by A1, A6, FDIFF_1:def_7;
then  (exp_R * arctan) `| Z = f by A9, PARTFUN1:5;
hence  integral (f,A) = ((exp_R * arctan) . (upper_bound A)) - ((exp_R * arctan) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13, SIN_COS9:119; ::_thesis: verum
end;

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 = - ((exp_R * arccot) / (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) = ((exp_R * arccot) . (upper_bound A)) - ((exp_R * arccot) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & f = - ((exp_R * arccot) / (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) = ((exp_R * arccot) . (upper_bound A)) - ((exp_R * arccot) . (lower_bound A))
let f, f1 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & f = - ((exp_R * arccot) / (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) = ((exp_R * arccot) . (upper_bound A)) - ((exp_R * arccot) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & Z c= ].(- 1),1.[ & f = - ((exp_R * arccot) / (f1 + (#Z 2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R * arccot) . (upper_bound A)) - ((exp_R * arccot) . (lower_bound A)) )
assume A1: ( A c= Z & Z c= ].(- 1),1.[ & f = - ((exp_R * arccot) / (f1 + (#Z 2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R * arccot) . (upper_bound A)) - ((exp_R * arccot) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: Z = dom ((exp_R * arccot) / (f1 + (#Z 2))) by A1, VALUED_1:8;
then  Z = (dom (exp_R * arccot)) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by RFUNCT_1:def_1;
then A4: ( Z c= dom (exp_R * arccot) & Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) ) by XBOOLE_1:18;
then A5: Z c= dom ((f1 + (#Z 2)) ^) by RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A6: Z c= dom (f1 + (#Z 2)) by A5, XBOOLE_1:1;
A7: exp_R * arccot is_differentiable_on Z by A1, A4, SIN_COS9:120;
A8: for x being Real st x in Z holds
f . x = - ((exp_R . (arccot . x)) / (1 + (x ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = - ((exp_R . (arccot . x)) / (1 + (x ^2))) )
assume A9: x in Z ; ::_thesis: f . x = - ((exp_R . (arccot . x)) / (1 + (x ^2)))
(- ((exp_R * arccot) / (f1 + (#Z 2)))) . x = - (((exp_R * arccot) / (f1 + (#Z 2))) . x) by VALUED_1:8
.= - (((exp_R * arccot) . x) / ((f1 + (#Z 2)) . x)) by A9, A3, RFUNCT_1:def_1
.= - ((exp_R . (arccot . x)) / ((f1 + (#Z 2)) . x)) by A4, A9, FUNCT_1:12
.= - ((exp_R . (arccot . x)) / ((f1 . x) + ((#Z 2) . x))) by A6, A9, VALUED_1:def_1
.= - ((exp_R . (arccot . x)) / (1 + ((#Z 2) . x))) by A1, A9
.= - ((exp_R . (arccot . x)) / (1 + (x #Z 2))) by TAYLOR_1:def_1
.= - ((exp_R . (arccot . x)) / (1 + (x ^2))) by FDIFF_7:1 ;
hence  f . x = - ((exp_R . (arccot . x)) / (1 + (x ^2))) by A1; ::_thesis: verum
end;
A10: for x being Real st x in dom ((exp_R * arccot) `| Z) holds
((exp_R * arccot) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((exp_R * arccot) `| Z) implies ((exp_R * arccot) `| Z) . x = f . x )
assume  x in dom ((exp_R * arccot) `| Z) ; ::_thesis: ((exp_R * arccot) `| Z) . x = f . x
then A11: x in Z by A7, FDIFF_1:def_7;
then ((exp_R * arccot) `| Z) . x = - ((exp_R . (arccot . x)) / (1 + (x ^2))) by A1, A4, SIN_COS9:120
.= f . x by A11, A8 ;
hence  ((exp_R * arccot) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((exp_R * arccot) `| Z) = dom f by A1, A7, FDIFF_1:def_7;
then  (exp_R * arccot) `| Z = f by A10, PARTFUN1:5;
hence  integral (f,A) = ((exp_R * arccot) . (upper_bound A)) - ((exp_R * arccot) . (lower_bound A)) by A1, A2, A4, INTEGRA5:13, SIN_COS9:120; ::_thesis: verum
end;

theorem Th50: :: INTEGR13:50
for Z being open Subset of REAL st Z c= dom (exp_R * arccot) & Z c= ].(- 1),1.[ holds
( - (exp_R * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * arccot) & Z c= ].(- 1),1.[ implies ( - (exp_R * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) ) ) )
assume A1: ( Z c= dom (exp_R * arccot) & Z c= ].(- 1),1.[ ) ; ::_thesis: ( - (exp_R * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) ) )
then A2: Z c= dom (- (exp_R * arccot)) by VALUED_1:8;
A3: exp_R * arccot is_differentiable_on Z by A1, SIN_COS9:120;
then A4: (- 1) (#) (exp_R * arccot) is_differentiable_on Z by A2, FDIFF_1:20;
 for x being Real st x in Z holds
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies ((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) )
assume A5: x in Z ; ::_thesis: ((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2))
A6: arccot is_differentiable_on Z by A1, SIN_COS9:82;
then A7: arccot is_differentiable_in x by A5, FDIFF_1:9;
A8: exp_R is_differentiable_in arccot . x by SIN_COS:65;
A9: exp_R * arccot is_differentiable_in x by A3, A5, FDIFF_1:9;
((- (exp_R * arccot)) `| Z) . x = diff ((- (exp_R * arccot)),x) by A4, A5, FDIFF_1:def_7
.= (- 1) * (diff ((exp_R * arccot),x)) by A9, FDIFF_1:15
.= (- 1) * ((diff (exp_R,(arccot . x))) * (diff (arccot,x))) by A7, A8, FDIFF_2:13
.= (- 1) * ((diff (exp_R,(arccot . x))) * ((arccot `| Z) . x)) by A5, A6, FDIFF_1:def_7
.= (- 1) * ((diff (exp_R,(arccot . x))) * (- (1 / (1 + (x ^2))))) by A5, A1, SIN_COS9:82
.= (- 1) * (- ((diff (exp_R,(arccot . x))) * (1 / (1 + (x ^2)))))
.= (exp_R . (arccot . x)) / (1 + (x ^2)) by SIN_COS:65 ;
hence  ((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) ; ::_thesis: verum
end;
hence  ( - (exp_R * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) ) ) by A2, A3, Lm3, FDIFF_1:20; ::_thesis: verum
end;

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 = (exp_R * arccot) / (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) = ((- (exp_R * arccot)) . (upper_bound A)) - ((- (exp_R * arccot)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arccot) / (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) = ((- (exp_R * arccot)) . (upper_bound A)) - ((- (exp_R * arccot)) . (lower_bound A))
let f, f1 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arccot) / (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) = ((- (exp_R * arccot)) . (upper_bound A)) - ((- (exp_R * arccot)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arccot) / (f1 + (#Z 2)) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (exp_R * arccot)) . (upper_bound A)) - ((- (exp_R * arccot)) . (lower_bound A)) )
assume A1: ( A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arccot) / (f1 + (#Z 2)) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (exp_R * arccot)) . (upper_bound A)) - ((- (exp_R * arccot)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
 Z = (dom (exp_R * arccot)) /\ ((dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0})) by A1, RFUNCT_1:def_1;
then A3: ( Z c= dom (exp_R * arccot) & Z c= (dom (f1 + (#Z 2))) \ ((f1 + (#Z 2)) " {0}) ) by XBOOLE_1:18;
then A4: Z c= dom ((f1 + (#Z 2)) ^) by RFUNCT_1:def_2;
 dom ((f1 + (#Z 2)) ^) c= dom (f1 + (#Z 2)) by RFUNCT_1:1;
then A5: Z c= dom (f1 + (#Z 2)) by A4, XBOOLE_1:1;
A6: - (exp_R * arccot) is_differentiable_on Z by A1, A3, Th50;
A7: for x being Real st x in Z holds
f . x = (exp_R . (arccot . x)) / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = (exp_R . (arccot . x)) / (1 + (x ^2)) )
assume A8: x in Z ; ::_thesis: f . x = (exp_R . (arccot . x)) / (1 + (x ^2))
then ((exp_R * arccot) / (f1 + (#Z 2))) . x = ((exp_R * arccot) . x) / ((f1 + (#Z 2)) . x) by A1, RFUNCT_1:def_1
.= (exp_R . (arccot . x)) / ((f1 + (#Z 2)) . x) by A3, A8, FUNCT_1:12
.= (exp_R . (arccot . x)) / ((f1 . x) + ((#Z 2) . x)) by A5, A8, VALUED_1:def_1
.= (exp_R . (arccot . x)) / (1 + ((#Z 2) . x)) by A1, A8
.= (exp_R . (arccot . x)) / (1 + (x #Z 2)) by TAYLOR_1:def_1
.= (exp_R . (arccot . x)) / (1 + (x ^2)) by FDIFF_7:1 ;
hence  f . x = (exp_R . (arccot . x)) / (1 + (x ^2)) by A1; ::_thesis: verum
end;
A9: for x being Real st x in dom ((- (exp_R * arccot)) `| Z) holds
((- (exp_R * arccot)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- (exp_R * arccot)) `| Z) implies ((- (exp_R * arccot)) `| Z) . x = f . x )
assume  x in dom ((- (exp_R * arccot)) `| Z) ; ::_thesis: ((- (exp_R * arccot)) `| Z) . x = f . x
then A10: x in Z by A6, FDIFF_1:def_7;
then ((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) by A1, A3, Th50
.= f . x by A7, A10 ;
hence  ((- (exp_R * arccot)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((- (exp_R * arccot)) `| Z) = dom f by A1, A6, FDIFF_1:def_7;
then  (- (exp_R * arccot)) `| Z = f by A9, PARTFUN1:5;
hence  integral (f,A) = ((- (exp_R * arccot)) . (upper_bound A)) - ((- (exp_R * arccot)) . (lower_bound A)) by A1, A2, A3, Th50, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGR13:52
for A being non empty closed_interval Subset of REAL
for f1, f2, f 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))) . (upper_bound A)) - (((1 / 2) (#) (ln * (f1 + f2))) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, f2, f 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))) . (upper_bound A)) - (((1 / 2) (#) (ln * (f1 + f2))) . (lower_bound A))
let f1, f2, f be PartFunc of REAL,REAL; ::_thesis: 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))) . (upper_bound A)) - (((1 / 2) (#) (ln * (f1 + f2))) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = (((1 / 2) (#) (ln * (f1 + f2))) . (upper_bound A)) - (((1 / 2) (#) (ln * (f1 + f2))) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = (((1 / 2) (#) (ln * (f1 + f2))) . (upper_bound A)) - (((1 / 2) (#) (ln * (f1 + f2))) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: Z c= dom ((1 / 2) (#) (ln * (f1 + f2))) by A1, VALUED_1:def_5;
 Z c= (dom (id Z)) /\ ((dom (f1 + f2)) \ ((f1 + f2) " {0})) by A1, RFUNCT_1:def_1;
then  Z c= (dom (f1 + f2)) \ ((f1 + f2) " {0}) by XBOOLE_1:18;
then A4: Z c= dom ((f1 + f2) ^) by RFUNCT_1:def_2;
 dom ((f1 + f2) ^) c= dom (f1 + f2) by RFUNCT_1:1;
then A5: Z c= dom (f1 + f2) by A4, XBOOLE_1:1;
A6: (1 / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z by A1, A3, SIN_COS9:102;
A7: for x being Real st x in Z holds
f . x = x / (1 + (x ^2))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = x / (1 + (x ^2)) )
assume A8: x in Z ; ::_thesis: f . x = x / (1 + (x ^2))
then ((id Z) / (f1 + f2)) . x = ((id Z) . x) / ((f1 + f2) . x) by A1, RFUNCT_1:def_1
.= x / ((f1 + f2) . x) by A8, FUNCT_1:18
.= x / ((f1 . x) + (f2 . x)) by A5, A8, VALUED_1:def_1
.= x / (1 + ((#Z 2) . x)) by A1, A8
.= x / (1 + (x #Z 2)) by TAYLOR_1:def_1
.= x / (1 + (x ^2)) by FDIFF_7:1 ;
hence  f . x = x / (1 + (x ^2)) by A1; ::_thesis: verum
end;
A9: for x being Real st x in dom (((1 / 2) (#) (ln * (f1 + f2))) `| Z) holds
(((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((1 / 2) (#) (ln * (f1 + f2))) `| Z) implies (((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = f . x )
assume  x in dom (((1 / 2) (#) (ln * (f1 + f2))) `| Z) ; ::_thesis: (((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = f . x
then A10: x in Z by A6, FDIFF_1:def_7;
then (((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (1 + (x ^2)) by A1, A3, SIN_COS9:102
.= f . x by A10, A7 ;
hence  (((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((1 / 2) (#) (ln * (f1 + f2))) `| Z) = dom f by A1, A6, FDIFF_1:def_7;
then  ((1 / 2) (#) (ln * (f1 + f2))) `| Z = f by A9, PARTFUN1:5;
hence  integral (f,A) = (((1 / 2) (#) (ln * (f1 + f2))) . (upper_bound A)) - (((1 / 2) (#) (ln * (f1 + f2))) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGR13:53
for a being Real
for A being non empty closed_interval Subset of REAL
for f1, f2, f, h 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))) . (upper_bound A)) - (((a / 2) (#) (ln * (f1 + f2))) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f1, f2, f, h 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))) . (upper_bound A)) - (((a / 2) (#) (ln * (f1 + f2))) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, f2, f, h 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))) . (upper_bound A)) - (((a / 2) (#) (ln * (f1 + f2))) . (lower_bound A))
let f1, f2, f, h be PartFunc of REAL,REAL; ::_thesis: 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))) . (upper_bound A)) - (((a / 2) (#) (ln * (f1 + f2))) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = (((a / 2) (#) (ln * (f1 + f2))) . (upper_bound A)) - (((a / 2) (#) (ln * (f1 + f2))) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = (((a / 2) (#) (ln * (f1 + f2))) . (upper_bound A)) - (((a / 2) (#) (ln * (f1 + f2))) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: Z c= dom ((a / 2) (#) (ln * (f1 + f2))) by A1, VALUED_1:def_5;
A4: for x being Real st x in Z holds
f1 . x = 1 by A1;
A5: for x being Real st x in Z holds
h . x = x / a by A1;
then A6: (a / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z by A1, A3, A4, SIN_COS9:108;
A7: for x being Real st x in Z holds
f . x = x / (a * (1 + ((x / a) ^2)))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = x / (a * (1 + ((x / a) ^2))) )
assume A8: x in Z ; ::_thesis: f . x = x / (a * (1 + ((x / a) ^2)))
then A9: x in dom (f1 + f2) by A1, FUNCT_1:11;
 dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1;
then  dom (f1 + f2) c= dom f2 by XBOOLE_1:18;
then A10: x in dom f2 by A9;
((id Z) / (a (#) (f1 + f2))) . x = ((id Z) . x) / ((a (#) (f1 + f2)) . x) by A1, A8, RFUNCT_1:def_1
.= x / ((a (#) (f1 + f2)) . x) by A8, FUNCT_1:18
.= x / (a * ((f1 + f2) . x)) by VALUED_1:6
.= x / (a * ((f1 . x) + (f2 . x))) by A9, VALUED_1:def_1
.= x / (a * (1 + (f2 . x))) by A4, A8
.= x / (a * (1 + ((#Z 2) . (h . x)))) by A1, A10, FUNCT_1:12
.= x / (a * (1 + ((h . x) #Z 2))) by TAYLOR_1:def_1
.= x / (a * (1 + ((h . x) ^2))) by FDIFF_7:1
.= x / (a * (1 + ((x / a) ^2))) by A5, A8 ;
hence  f . x = x / (a * (1 + ((x / a) ^2))) by A1; ::_thesis: verum
end;
A11: for x being Real st x in dom (((a / 2) (#) (ln * (f1 + f2))) `| Z) holds
(((a / 2) (#) (ln * (f1 + f2))) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (((a / 2) (#) (ln * (f1 + f2))) `| Z) implies (((a / 2) (#) (ln * (f1 + f2))) `| Z) . x = f . x )
assume  x in dom (((a / 2) (#) (ln * (f1 + f2))) `| Z) ; ::_thesis: (((a / 2) (#) (ln * (f1 + f2))) `| Z) . x = f . x
then A12: x in Z by A6, FDIFF_1:def_7;
then (((a / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (a * (1 + ((x / a) ^2))) by A1, A3, A4, A5, SIN_COS9:108
.= f . x by A7, A12 ;
hence  (((a / 2) (#) (ln * (f1 + f2))) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom (((a / 2) (#) (ln * (f1 + f2))) `| Z) = dom f by A1, A6, FDIFF_1:def_7;
then  ((a / 2) (#) (ln * (f1 + f2))) `| Z = f by A11, PARTFUN1:5;
hence  integral (f,A) = (((a / 2) (#) (ln * (f1 + f2))) . (upper_bound A)) - (((a / 2) (#) (ln * (f1 + f2))) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13; ::_thesis: verum
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 = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (((id Z) ^) (#) arctan) & Z c= ].(- 1),1.[ implies ( - (((id Z) ^) (#) arctan) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) arctan)) `| Z) . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) ) ) )
set f = id Z;
assume that
A1: Z c= dom (((id Z) ^) (#) arctan) and
A2: Z c= ].(- 1),1.[ ; ::_thesis: ( - (((id Z) ^) (#) arctan) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) arctan)) `| Z) . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) ) )
A3: Z c= dom (- (((id Z) ^) (#) arctan)) by A1, VALUED_1:8;
A4: for x being Real st x in Z holds
(id Z) . x = x by FUNCT_1:18;
 Z c= (dom ((id Z) ^)) /\ (dom arctan) by A1, VALUED_1:def_4;
then A5: Z c= dom ((id Z) ^) by XBOOLE_1:18;
A6: not 0 in Z
proof
assume A7: 0 in Z ; ::_thesis: contradiction
dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2
.= (dom (id Z)) \ {0} by Lm1, A7 ;
then  not 0 in {0} by A7, A5, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
then A8: ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) by FDIFF_5:4;
A9: arctan is_differentiable_on Z by A2, SIN_COS9:81;
A10: ((id Z) ^) (#) arctan is_differentiable_on Z by A1, A2, A6, SIN_COS9:129;
then A11: (- 1) (#) (((id Z) ^) (#) arctan) is_differentiable_on Z by A3, FDIFF_1:20;
 for x being Real st x in Z holds
((- (((id Z) ^) (#) arctan)) `| Z) . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((- (((id Z) ^) (#) arctan)) `| Z) . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) )
assume A12: x in Z ; ::_thesis: ((- (((id Z) ^) (#) arctan)) `| Z) . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2))))
then A13: ((id Z) ^) (#) arctan is_differentiable_in x by A10, FDIFF_1:9;
A14: (id Z) ^ is_differentiable_in x by A8, A12, FDIFF_1:9;
A15: arctan is_differentiable_in x by A9, A12, FDIFF_1:9;
((- (((id Z) ^) (#) arctan)) `| Z) . x = diff ((- (((id Z) ^) (#) arctan)),x) by A11, A12, FDIFF_1:def_7
.= (- 1) * (diff ((((id Z) ^) (#) arctan),x)) by A13, FDIFF_1:15
.= (- 1) * (((arctan . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (arctan,x)))) by A14, A15, FDIFF_1:16
.= (- 1) * (((arctan . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (arctan,x)))) by A8, A12, FDIFF_1:def_7
.= (- 1) * (((arctan . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (arctan,x)))) by A6, A12, FDIFF_5:4
.= (- 1) * ((- ((arctan . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * ((arctan `| Z) . x))) by A9, A12, FDIFF_1:def_7
.= (- 1) * ((- (((arctan . x) * 1) / (x ^2))) + ((((id Z) ^) . x) * (1 / (1 + (x ^2))))) by A2, A12, SIN_COS9:81
.= (- 1) * ((- ((arctan . x) / (x ^2))) + ((((id Z) . x) ") * (1 / (1 + (x ^2))))) by A5, A12, RFUNCT_1:def_2
.= (- 1) * ((- ((arctan . x) / (x ^2))) + ((1 / x) * (1 / (1 + (x ^2))))) by A4, A12
.= (- 1) * ((- ((arctan . x) / (x ^2))) + ((1 * 1) / (x * (1 + (x ^2))))) by XCMPLX_1:76
.= ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) ;
hence  ((- (((id Z) ^) (#) arctan)) `| Z) . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) ; ::_thesis: verum
end;
hence  ( - (((id Z) ^) (#) arctan) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) arctan)) `| Z) . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) ) ) by A3, A10, Lm3, FDIFF_1:20; ::_thesis: verum
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 = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (((id Z) ^) (#) arccot) & Z c= ].(- 1),1.[ implies ( - (((id Z) ^) (#) arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) arccot)) `| Z) . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) ) ) )
set f = id Z;
assume that
A1: Z c= dom (((id Z) ^) (#) arccot) and
A2: Z c= ].(- 1),1.[ ; ::_thesis: ( - (((id Z) ^) (#) arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) arccot)) `| Z) . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) ) )
A3: Z c= dom (- (((id Z) ^) (#) arccot)) by A1, VALUED_1:8;
A4: for x being Real st x in Z holds
(id Z) . x = x by FUNCT_1:18;
 Z c= (dom ((id Z) ^)) /\ (dom arccot) by A1, VALUED_1:def_4;
then A5: Z c= dom ((id Z) ^) by XBOOLE_1:18;
A6: not 0 in Z
proof
assume A7: 0 in Z ; ::_thesis: contradiction
dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2
.= (dom (id Z)) \ {0} by Lm1, A7 ;
then  not 0 in {0} by A7, A5, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
then A8: ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) by FDIFF_5:4;
A9: arccot is_differentiable_on Z by A2, SIN_COS9:82;
A10: ((id Z) ^) (#) arccot is_differentiable_on Z by A6, A1, A2, SIN_COS9:130;
then A11: (- 1) (#) (((id Z) ^) (#) arccot) is_differentiable_on Z by A3, FDIFF_1:20;
 for x being Real st x in Z holds
((- (((id Z) ^) (#) arccot)) `| Z) . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies ((- (((id Z) ^) (#) arccot)) `| Z) . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) )
assume A12: x in Z ; ::_thesis: ((- (((id Z) ^) (#) arccot)) `| Z) . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2))))
then A13: ((id Z) ^) (#) arccot is_differentiable_in x by A10, FDIFF_1:9;
A14: (id Z) ^ is_differentiable_in x by A8, A12, FDIFF_1:9;
A15: arccot is_differentiable_in x by A9, A12, FDIFF_1:9;
((- (((id Z) ^) (#) arccot)) `| Z) . x = diff ((- (((id Z) ^) (#) arccot)),x) by A11, A12, FDIFF_1:def_7
.= (- 1) * (diff ((((id Z) ^) (#) arccot),x)) by A13, FDIFF_1:15
.= (- 1) * (((arccot . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (arccot,x)))) by A14, A15, FDIFF_1:16
.= (- 1) * (((arccot . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (arccot,x)))) by A8, A12, FDIFF_1:def_7
.= (- 1) * (((arccot . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (arccot,x)))) by A12, A6, FDIFF_5:4
.= (- 1) * ((- ((arccot . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * ((arccot `| Z) . x))) by A9, A12, FDIFF_1:def_7
.= (- 1) * ((- ((arccot . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * (- (1 / (1 + (x ^2)))))) by A2, A12, SIN_COS9:82
.= (- 1) * ((- (((arccot . x) * 1) / (x ^2))) - ((((id Z) ^) . x) * (1 / (1 + (x ^2)))))
.= (- 1) * ((- ((arccot . x) / (x ^2))) - ((((id Z) . x) ") * (1 / (1 + (x ^2))))) by A5, A12, RFUNCT_1:def_2
.= (- 1) * ((- ((arccot . x) / (x ^2))) - ((1 / x) * (1 / (1 + (x ^2))))) by A4, A12
.= (- 1) * ((- ((arccot . x) / (x ^2))) - ((1 * 1) / (x * (1 + (x ^2))))) by XCMPLX_1:76
.= ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) ;
hence  ((- (((id Z) ^) (#) arccot)) `| Z) . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) ; ::_thesis: verum
end;
hence  ( - (((id Z) ^) (#) arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) arccot)) `| Z) . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) ) ) by A11; ::_thesis: verum
end;

theorem :: INTEGR13:56
for A being non empty closed_interval Subset of REAL
for f1, 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
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)) . (upper_bound A)) - ((- (((id Z) ^) (#) arctan)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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)) . (upper_bound A)) - ((- (((id Z) ^) (#) arctan)) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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)) . (upper_bound A)) - ((- (((id Z) ^) (#) arctan)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = ((- (((id Z) ^) (#) arctan)) . (upper_bound A)) - ((- (((id Z) ^) (#) arctan)) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = ((- (((id Z) ^) (#) arctan)) . (upper_bound A)) - ((- (((id Z) ^) (#) arctan)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: - (((id Z) ^) (#) arctan) is_differentiable_on Z by A1, Th54;
A4: Z = (dom (arctan / (#Z 2))) /\ (dom (((id Z) (#) (f1 + (#Z 2))) ^)) by A1, VALUED_1:12;
then A5: Z c= dom (arctan / (#Z 2)) by XBOOLE_1:18;
A6: Z c= dom (((id Z) (#) (f1 + (#Z 2))) ^) by A4, XBOOLE_1:18;
 dom (((id Z) (#) (f1 + (#Z 2))) ^) c= dom ((id Z) (#) (f1 + (#Z 2))) by RFUNCT_1:1;
then  Z c= dom ((id Z) (#) (f1 + (#Z 2))) by A6, XBOOLE_1:1;
then  Z c= (dom (id Z)) /\ (dom (f1 + (#Z 2))) by VALUED_1:def_4;
then A7: Z c= dom (f1 + (#Z 2)) by XBOOLE_1:18;
A8: for x being Real st x in Z holds
f . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) )
assume A9: x in Z ; ::_thesis: f . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2))))
then A10: x in dom (((id Z) (#) (f1 + (#Z 2))) ^) by A6;
((arctan / (#Z 2)) - (((id Z) (#) (f1 + (#Z 2))) ^)) . x = ((arctan / (#Z 2)) . x) - ((((id Z) (#) (f1 + (#Z 2))) ^) . x) by A1, A9, VALUED_1:13
.= ((arctan / (#Z 2)) . x) - (1 / (((id Z) (#) (f1 + (#Z 2))) . x)) by A10, RFUNCT_1:def_2
.= ((arctan / (#Z 2)) . x) - (1 / (((id Z) . x) * ((f1 + (#Z 2)) . x))) by VALUED_1:5
.= ((arctan / (#Z 2)) . x) - (1 / (((id Z) . x) * ((f1 . x) + ((#Z 2) . x)))) by A7, A9, VALUED_1:def_1
.= ((arctan / (#Z 2)) . x) - (1 / (x * ((f1 . x) + ((#Z 2) . x)))) by A9, FUNCT_1:18
.= ((arctan / (#Z 2)) . x) - (1 / (x * (1 + ((#Z 2) . x)))) by A1, A9
.= ((arctan . x) / ((#Z 2) . x)) - (1 / (x * (1 + ((#Z 2) . x)))) by A9, A5, RFUNCT_1:def_1
.= ((arctan . x) / (x #Z 2)) - (1 / (x * (1 + ((#Z 2) . x)))) by TAYLOR_1:def_1
.= ((arctan . x) / (x #Z 2)) - (1 / (x * (1 + (x #Z 2)))) by TAYLOR_1:def_1
.= ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x #Z 2)))) by FDIFF_7:1
.= ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) by FDIFF_7:1 ;
hence  f . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) by A1; ::_thesis: verum
end;
A11: for x being Real st x in dom ((- (((id Z) ^) (#) arctan)) `| Z) holds
((- (((id Z) ^) (#) arctan)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- (((id Z) ^) (#) arctan)) `| Z) implies ((- (((id Z) ^) (#) arctan)) `| Z) . x = f . x )
assume  x in dom ((- (((id Z) ^) (#) arctan)) `| Z) ; ::_thesis: ((- (((id Z) ^) (#) arctan)) `| Z) . x = f . x
then A12: x in Z by A3, FDIFF_1:def_7;
then ((- (((id Z) ^) (#) arctan)) `| Z) . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) by A1, Th54
.= f . x by A8, A12 ;
hence  ((- (((id Z) ^) (#) arctan)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((- (((id Z) ^) (#) arctan)) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (- (((id Z) ^) (#) arctan)) `| Z = f by A11, PARTFUN1:5;
hence  integral (f,A) = ((- (((id Z) ^) (#) arctan)) . (upper_bound A)) - ((- (((id Z) ^) (#) arctan)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGR13:57
for A being non empty closed_interval Subset of REAL
for f1, 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
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)) . (upper_bound A)) - ((- (((id Z) ^) (#) arccot)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, 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
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)) . (upper_bound A)) - ((- (((id Z) ^) (#) arccot)) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; ::_thesis: 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)) . (upper_bound A)) - ((- (((id Z) ^) (#) arccot)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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 implies integral (f,A) = ((- (((id Z) ^) (#) arccot)) . (upper_bound A)) - ((- (((id Z) ^) (#) arccot)) . (lower_bound A)) )
assume A1: ( 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 ) ; ::_thesis: integral (f,A) = ((- (((id Z) ^) (#) arccot)) . (upper_bound A)) - ((- (((id Z) ^) (#) arccot)) . (lower_bound A))
then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11;
A3: - (((id Z) ^) (#) arccot) is_differentiable_on Z by A1, Th55;
A4: Z = (dom (arccot / (#Z 2))) /\ (dom (((id Z) (#) (f1 + (#Z 2))) ^)) by A1, VALUED_1:def_1;
then A5: Z c= dom (arccot / (#Z 2)) by XBOOLE_1:18;
A6: Z c= dom (((id Z) (#) (f1 + (#Z 2))) ^) by A4, XBOOLE_1:18;
 dom (((id Z) (#) (f1 + (#Z 2))) ^) c= dom ((id Z) (#) (f1 + (#Z 2))) by RFUNCT_1:1;
then  Z c= dom ((id Z) (#) (f1 + (#Z 2))) by A6, XBOOLE_1:1;
then  Z c= (dom (id Z)) /\ (dom (f1 + (#Z 2))) by VALUED_1:def_4;
then A7: Z c= dom (f1 + (#Z 2)) by XBOOLE_1:18;
A8: for x being Real st x in Z holds
f . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2))))
proof
let x be Real; ::_thesis: ( x in Z implies f . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) )
assume A9: x in Z ; ::_thesis: f . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2))))
then A10: x in dom (((id Z) (#) (f1 + (#Z 2))) ^) by A6;
((arccot / (#Z 2)) + (((id Z) (#) (f1 + (#Z 2))) ^)) . x = ((arccot / (#Z 2)) . x) + ((((id Z) (#) (f1 + (#Z 2))) ^) . x) by A1, A9, VALUED_1:def_1
.= ((arccot / (#Z 2)) . x) + (1 / (((id Z) (#) (f1 + (#Z 2))) . x)) by A10, RFUNCT_1:def_2
.= ((arccot / (#Z 2)) . x) + (1 / (((id Z) . x) * ((f1 + (#Z 2)) . x))) by VALUED_1:5
.= ((arccot / (#Z 2)) . x) + (1 / (((id Z) . x) * ((f1 . x) + ((#Z 2) . x)))) by A7, A9, VALUED_1:def_1
.= ((arccot / (#Z 2)) . x) + (1 / (x * ((f1 . x) + ((#Z 2) . x)))) by A9, FUNCT_1:18
.= ((arccot / (#Z 2)) . x) + (1 / (x * (1 + ((#Z 2) . x)))) by A1, A9
.= ((arccot . x) / ((#Z 2) . x)) + (1 / (x * (1 + ((#Z 2) . x)))) by A9, A5, RFUNCT_1:def_1
.= ((arccot . x) / (x #Z 2)) + (1 / (x * (1 + ((#Z 2) . x)))) by TAYLOR_1:def_1
.= ((arccot . x) / (x #Z 2)) + (1 / (x * (1 + (x #Z 2)))) by TAYLOR_1:def_1
.= ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x #Z 2)))) by FDIFF_7:1
.= ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) by FDIFF_7:1 ;
hence  f . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) by A1; ::_thesis: verum
end;
A11: for x being Real st x in dom ((- (((id Z) ^) (#) arccot)) `| Z) holds
((- (((id Z) ^) (#) arccot)) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- (((id Z) ^) (#) arccot)) `| Z) implies ((- (((id Z) ^) (#) arccot)) `| Z) . x = f . x )
assume  x in dom ((- (((id Z) ^) (#) arccot)) `| Z) ; ::_thesis: ((- (((id Z) ^) (#) arccot)) `| Z) . x = f . x
then A12: x in Z by A3, FDIFF_1:def_7;
then ((- (((id Z) ^) (#) arccot)) `| Z) . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) by A1, Th55
.= f . x by A12, A8 ;
hence  ((- (((id Z) ^) (#) arccot)) `| Z) . x = f . x ; ::_thesis: verum
end;
 dom ((- (((id Z) ^) (#) arccot)) `| Z) = dom f by A1, A3, FDIFF_1:def_7;
then  (- (((id Z) ^) (#) arccot)) `| Z = f by A11, PARTFUN1:5;
hence  integral (f,A) = ((- (((id Z) ^) (#) arccot)) . (upper_bound A)) - ((- (((id Z) ^) (#) arccot)) . (lower_bound A)) by A1, A2, Th55, INTEGRA5:13; ::_thesis: verum
end;