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

environ

 vocabularies RELAT_1, FUNCT_1, ARYTM_1, SIN_COS, INTEGRA1, FDIFF_1, XBOOLE_0,
      SQUARE_1, ARYTM_3, ORDINAL2, RCOMP_1, PREPOWER, LIMFUNC1, PARTFUN1,
      TAYLOR_1, SIN_COS9, SUBSET_1, TARSKI, NUMBERS, REAL_1, CARD_1, INTEGRA5,
      XXREAL_2, ORDINAL4, VALUED_1, XXREAL_1, XXREAL_0, SEQ_4;
 notations TARSKI, XBOOLE_0, SEQ_1, SIN_COS, SUBSET_1, NUMBERS, VALUED_1,
      NAT_1, XXREAL_0, REAL_1, RELAT_1, RELSET_1, PARTFUN1, PARTFUN2, RCOMP_1,
      RFUNCT_1, MEASURE6, INTEGRA1, FCONT_1, SQUARE_1, INTEGRA5, PREPOWER,
      TAYLOR_1, FDIFF_1, SEQ_2, SIN_COS4, SIN_COS9, BINOP_2, LIMFUNC1, XREAL_0,
      INT_1, SEQ_4;
 constructors SIN_COS, TAYLOR_1, SEQ_1, REAL_1, FDIFF_1, FCONT_1, MEASURE6,
      BINOP_2, SQUARE_1, PREPOWER, INTEGRA5, JORDAN16, SIN_COS2, SEQ_4, SEQ_2,
      SIN_COS9, PARTFUN1, PARTFUN2, FUNCT_1, RCOMP_1, RELAT_1, SIN_COS6,
      RFUNCT_1, VALUED_1, FDIFF_9, SIN_COS4, LIMFUNC1, NAT_1, POWER, RELSET_1;
 registrations VALUED_1, NAT_1, XBOOLE_0, NUMBERS, MEMBERED, VALUED_0,
      INTEGRA1, INT_1, RELAT_1, ORDINAL1, FUNCT_2, RCOMP_1, FCONT_1, TOPREALB,
      RELSET_1, RFUNCT_1, XREAL_0, NEWTON, SQUARE_1, FUNCT_1, XXREAL_0, SEQM_3,
      SIN_COS9, FINSET_1, TAYLOR_1, FCONT_3;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions SIN_COS, VALUED_1, SUBSET_1, SQUARE_1, SIN_COS4, SIN_COS6, TARSKI,
      FCONT_1, FDIFF_9, XBOOLE_0, SIN_COS9, RCOMP_1, LIMFUNC1, NAT_1, XCMPLX_0,
      FDIFF_1;
 theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, XCMPLX_1, INTEGRA5, SIN_COS,
      TAYLOR_1, VALUED_1, XREAL_0, XBOOLE_0, XXREAL_1, XBOOLE_1, FDIFF_5,
      FDIFF_7, FDIFF_8, SIN_COS9, PREPOWER, TARSKI, RELAT_1, FDIFF_2;

begin

 reserve a,x for Real;
 reserve n for Element of NAT;
 reserve A for closed-interval Subset of REAL;
 reserve f,h,f1,f2 for PartFunc of REAL,REAL;
 reserve Z for open Subset of REAL;

Lm1:
  0 in Z implies (id Z)"{0} = {0}
  proof
    assume A1: 0 in Z;
    thus (id Z)"{0} c= {0}
    proof
      let x be set; assume
A2:   x in (id Z)"{0};
      then x in dom id Z by FUNCT_1:def 13; then
A3:   x in Z by FUNCT_1:34;
      (id Z).x in {0} by A2,FUNCT_1:def 13;
      hence thesis by A3,FUNCT_1:35;
    end;
    let x be set; assume x in {0}; then
A4: x = 0 by TARSKI:def 1; then
    (id Z).x = 0 by A1,FUNCT_1:35; then
A5: (id Z).x in {0} by TARSKI:def 1;
    x in dom id Z by A1,A4,FUNCT_1:34;
    hence thesis by A5,FUNCT_1:def 13;
  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 by XREAL_0:def 1;

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

theorem
 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)
proof
  assume
A1: A c= Z & f=(sin(#)cos)^
    & Z c= dom (ln*tan) & Z = dom f & f|A is continuous;then
A2: f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3: (ln*tan) is_differentiable_on Z by A1,FDIFF_8:18;
A4:for x st x in Z holds f.x=1/(sin.x*cos.x)
   proof
   let x;
   assume x in Z;
   then ((sin(#)cos)^).x =1/((sin(#)cos).x) by RFUNCT_1:def 8,A1
        .=1/(sin.x*cos.x) by VALUED_1:5;
    hence thesis by A1;
    end;
A5: for x st x in dom ((ln*tan)`|Z) holds ((ln*tan)`|Z).x = f.x
    proof
      let x;
      assume x in dom ((ln*tan)`|Z);then
A6:   x in Z by A3,FDIFF_1:def 8; then
      ((ln*tan)`|Z).x = 1/(sin.x*cos.x) by A1,FDIFF_8:18
        .=f.x by A4,A6;
      hence thesis;
    end;
   dom ((ln*tan)`|Z) = dom f by A1,A3,FDIFF_1:def 8;then
   ((ln*tan)`|Z)=f by A5,PARTFUN1:34;
   hence thesis by A1,A2,FDIFF_8:18,INTEGRA5:13;
end;

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

theorem
 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)
proof
   assume
A1:A c= Z & f=-(sin(#)cos)^
   & Z c= dom (ln*cot) & Z = dom f & f|A is continuous;then
A2: f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 st x in Z holds f.x=-1/(sin.x*cos.x)
   proof
   let x;
   assume
A6:x in Z;
   (-(sin(#)cos)^).x=-(((sin(#)cos)^).x) by VALUED_1:8
                   .=-1/((sin(#)cos).x) by RFUNCT_1:def 8,A4,A6
                   .=-1/(sin.x*cos.x) by VALUED_1:5;
    hence thesis by A1;
    end;
A7: for x st x in dom ((ln*cot)`|Z) holds ((ln*cot)`|Z).x = f.x
    proof
      let x;
      assume x in dom ((ln*cot)`|Z);then
A8:   x in Z by A3,FDIFF_1:def 8; then
      ((ln*cot)`|Z).x = -1/(sin.x*cos.x) by A1,FDIFF_8:19
        .=f.x by A5,A8;
      hence thesis;
    end;
    dom ((ln*cot)`|Z) = dom f by A1,A3,FDIFF_1:def 8;then
    ((ln*cot)`|Z)=f by A7,PARTFUN1:34;
    hence thesis by A1,A2,FDIFF_8:19,INTEGRA5:13;
end;

::f.x=2 * exp_R.x * sin.x

theorem
 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)
proof
  assume
A1:A c= Z & f=2(#)(exp_R(#)sin)
   & Z c= dom (exp_R(#)(sin-cos)) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:exp_R(#)(sin-cos) is_differentiable_on Z by A1,FDIFF_7:40;
A4:for x st x in Z holds f.x=2 * exp_R.x * sin.x
   proof
   let x;
   assume x in Z;
   (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 thesis by A1;
   end;
A5:for x st x in dom ((exp_R(#)(sin-cos))`|Z) holds
   ((exp_R(#)(sin-cos))`|Z).x=f.x
   proof
   let x;
   assume x in dom ((exp_R(#)(sin-cos))`|Z);then
A6:x in Z by A3,FDIFF_1:def 8;then
   ((exp_R(#)(sin-cos))`|Z).x=2 * exp_R.x * sin.x by A1,FDIFF_7:40
   .=f.x by A4,A6;
   hence thesis;
   end;
   dom ((exp_R(#)(sin-cos))`|Z)=dom f by A1,A3,FDIFF_1:def 8;
   then ((exp_R(#)(sin-cos))`|Z)= f by A5,PARTFUN1:34;
   hence thesis by A1,A2,FDIFF_7:40,INTEGRA5:13;
end;

::f.x=2 * exp_R.x * cos.x

theorem
 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)
proof
  assume
A1:A c= Z & f=2(#)(exp_R(#)cos)
   & Z c= dom (exp_R(#)(sin+cos)) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:exp_R(#)(sin+cos) is_differentiable_on Z by A1,FDIFF_7:41;
A4:for x st x in Z holds f.x=2 * exp_R.x * cos.x
   proof
   let x;
   assume x in Z;
   (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 thesis by A1;
   end;
A5:for x st x in dom ((exp_R(#)(sin+cos))`|Z) holds
   ((exp_R(#)(sin+cos))`|Z).x=f.x
   proof
   let x;
   assume x in dom ((exp_R(#)(sin+cos))`|Z);then
A6:x in Z by A3,FDIFF_1:def 8;then
   ((exp_R(#)(sin+cos))`|Z).x=2 * exp_R.x * cos.x by A1,FDIFF_7:41
   .=f.x by A6,A4;
   hence thesis;
   end;
   dom ((exp_R(#)(sin+cos))`|Z)=dom f by A1,A3,FDIFF_1:def 8;
   then ((exp_R(#)(sin+cos))`|Z)= f by A5,PARTFUN1:34;
   hence thesis by A1,A2,FDIFF_7:41,INTEGRA5:13;
end;

::f.x=cos.x-sin.x

theorem
 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)
proof
  assume
A1:A c= Z & Z = dom (cos-sin) & (cos-sin)|A is continuous;then
A2:cos-sin is_integrable_on A & (cos-sin)|A is bounded by INTEGRA5:10,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 st x in dom ((sin+cos)`|Z) holds ((sin+cos)`|Z).x=(cos-sin).x
   proof
   let x;
   assume x in dom((sin+cos)`|Z);then
A6:x in Z by A4,FDIFF_1:def 8;
  then ((sin+cos)`|Z).x=cos.x-sin.x by A3,FDIFF_7:38
                 .=(cos-sin).x by A1,A6,VALUED_1:13;
   hence thesis;
   end;
  dom((sin+cos)`|Z)=dom (cos-sin) by A1,A4,FDIFF_1:def 8;
  then((sin+cos)`|Z)=(cos-sin) by A5,PARTFUN1:34;
  hence thesis by A1,A2,A3,FDIFF_7:38,INTEGRA5:13;
end;

::f.x=cos.x+sin.x

theorem
 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)
proof
  assume
A1:A c= Z & Z = dom (cos+sin) & (cos+sin)|A is continuous;then
A2:cos+sin is_integrable_on A & (cos+sin)|A is bounded by INTEGRA5:10,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 st x in dom ((sin-cos)`|Z) holds ((sin-cos)`|Z).x=(cos+sin).x
   proof
   let x;
   assume x in dom((sin-cos)`|Z);then
A6:x in Z by A4,FDIFF_1:def 8;
  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 thesis;
   end;
  dom((sin-cos)`|Z)=dom (cos+sin) by A1,A4,FDIFF_1:def 8;
  then((sin-cos)`|Z)= (cos+sin) by A5,PARTFUN1:34;
  hence thesis by A1,A2,A3,FDIFF_7:39,INTEGRA5:13;
end;

theorem Th7:
  Z c= dom ((-1/2)(#)((sin+cos)/exp_R)) implies
  (-1/2)(#)((sin+cos)/exp_R) is_differentiable_on Z &
  for x st x in Z holds (((-1/2)(#)((sin+cos)/exp_R))`|Z).x = sin.x/exp_R.x
proof
   assume
A1:Z c= dom ((-1/2)(#)((sin+cos)/exp_R));
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 4;
then A3:Z c= dom (sin+cos) by XBOOLE_1:18; then
A4:sin+cos is_differentiable_on Z &
  for x 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,Lm3;
 for x st x in Z holds ((((-1/2)(#)((sin+cos)/exp_R)))`|Z).x =sin.x/exp_R.x
  proof
    let x;
    assume
A7: x in Z;
A8: exp_R is_differentiable_in x by SIN_COS:70;
A9:sin+cos is_differentiable_in x by A4,A7,FDIFF_1:16;
A10:(sin+cos).x=sin.x+cos.x by VALUED_1:1;
A11:exp_R.x <>0 by SIN_COS:59;
    (((-1/2)(#)((sin+cos)/exp_R))`|Z).x=(-1/2)*(diff((sin+cos)/exp_R,x))
     by A1,A5,A7,FDIFF_1:28,Lm3
 .=(-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 8
 .=(-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:70
 .=(-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:79
 .=(-1/2)*((-2*sin.x)*(1/exp_R.x)) by A11,XCMPLX_1:60
 .=sin.x/exp_R.x;
 hence thesis;
 end;
 hence thesis by A6;
end;

::f.x=sin.x/exp_R.x

theorem
 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)
proof
  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;
  then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(-1/2)(#)((sin+cos)/exp_R) is_differentiable_on Z by A1,Th7;
A4:for x st x in Z holds f.x=sin.x/exp_R.x by RFUNCT_1:def 4,A1;
A5:for x 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;
  assume x in dom (((-1/2)(#)((sin+cos)/exp_R))`|Z);then
A6:x in Z by A3,FDIFF_1:def 8;then
   (((-1/2)(#)((sin+cos)/exp_R))`|Z).x=sin.x/exp_R.x by A1,Th7
   .=f.x by A6,A4;
   hence thesis;
   end;
  dom (((-1/2)(#)((sin+cos)/exp_R))`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then (((-1/2)(#)((sin+cos)/exp_R))`|Z)= f by A5,PARTFUN1:34;
  hence thesis by A1,A2,Th7,INTEGRA5:13;
end;

theorem Th9:
  Z c= dom ((1/2)(#)((sin-cos)/exp_R)) implies
(1/2)(#)((sin-cos)/exp_R) is_differentiable_on Z &
  for x st x in Z holds (((1/2)(#)((sin-cos)/exp_R))`|Z).x =cos.x/exp_R.x
proof
   assume
A1:Z c= dom ((1/2)(#)((sin-cos)/exp_R));
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 4;
then A3:Z c= dom (sin-cos) by XBOOLE_1:18; then
A4:sin-cos is_differentiable_on Z &
  for x 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,Lm3;
 for x st x in Z holds (((1/2)(#)((sin-cos)/exp_R))`|Z).x =cos.x/exp_R.x
   proof
     let x;
     assume
A7:x in Z;
A8:exp_R is_differentiable_in x by SIN_COS:70;
A9:sin-cos is_differentiable_in x by A4,A7,FDIFF_1:16;
A10:(sin-cos).x=sin.x-cos.x by A3,A7,VALUED_1:13;
A11:exp_R.x <>0 by SIN_COS:59;
   (((1/2)(#)((sin-cos)/exp_R))`|Z).x=(1/2)*(diff((sin-cos)/exp_R,x))
    by Lm3,A1,A5,A7,FDIFF_1:28
 .=(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 8
 .=(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:70
 .=(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:79
 .=(1/2)*((2*cos.x)*(1/exp_R.x)) by A11,XCMPLX_1:60
 .=cos.x/exp_R.x;
   hence thesis;
  end;
 hence thesis by A6;
end;

::f.x=cos.x/exp_R.x

theorem
 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)
proof
  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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(1/2)(#)((sin-cos)/exp_R) is_differentiable_on Z by A1,Th9;
A4:for x st x in Z holds f.x=cos.x/exp_R.x by RFUNCT_1:def 4,A1;
A5:for x 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;
  assume x in dom (((1/2)(#)((sin-cos)/exp_R))`|Z);then
A6:x in Z by A3,FDIFF_1:def 8;then
   (((1/2)(#)((sin-cos)/exp_R))`|Z).x=cos.x/exp_R.x by A1,Th9
   .=f.x by A4,A6;
   hence thesis;
   end;
  dom (((1/2)(#)((sin-cos)/exp_R))`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then (((1/2)(#)((sin-cos)/exp_R))`|Z)= f by A5,PARTFUN1:34;
  hence thesis by A1,A2,Th9,INTEGRA5:13;
end;

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

theorem
 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)
proof
   assume
A1:A c= Z & f=exp_R(#)(sin+cos)
   & Z c= dom (exp_R(#)sin) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 st x in Z holds f.x=exp_R.x*(sin.x+cos.x)
    proof
    let x;
    assume
A6:x in Z;
    (exp_R(#)(sin+cos)).x=exp_R.x*((sin+cos).x) by VALUED_1:5
                               .=exp_R.x*(sin.x+cos.x) by VALUED_1:def 1,A4,A6;
    hence thesis by A1;
    end;
A7:for x st x in dom ((exp_R(#)sin)`|Z) holds ((exp_R(#)sin)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((exp_R(#)sin)`|Z);then
A8:x in Z by A3,FDIFF_1:def 8;then
   ((exp_R(#)sin)`|Z).x=exp_R.x*(sin.x+cos.x) by A1,FDIFF_7:44
   .=f.x by A5,A8;
   hence thesis;
   end;
  dom ((exp_R(#)sin)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((exp_R(#)sin)`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_7:44,INTEGRA5:13;
end;

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

theorem
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)
proof
   assume
A1:A c= Z & f=exp_R(#)(cos-sin)
   & Z c= dom (exp_R(#)cos) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 st x in Z holds f.x=exp_R.x*(cos.x-sin.x)
    proof
    let x;
    assume
A6:x in Z;
    (exp_R(#)(cos-sin)).x=exp_R.x*((cos-sin).x) by VALUED_1:5
                               .=exp_R.x*(cos.x-sin.x) by VALUED_1:13,A4,A6;
    hence thesis by A1;
    end;
A7:for x st x in dom ((exp_R(#)cos)`|Z) holds ((exp_R(#)cos)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((exp_R(#)cos)`|Z);then
A8:x in Z by A3,FDIFF_1:def 8;then
   ((exp_R(#)cos)`|Z).x=exp_R.x*(cos.x-sin.x) by A1,FDIFF_7:45
   .=f.x by A5,A8;
   hence thesis;
   end;
  dom ((exp_R(#)cos)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((exp_R(#)cos)`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_7:45,INTEGRA5:13;
end;

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

theorem
 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)
proof
  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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
     set g = id Z;
Z c= dom (g^) /\ dom tan by A1,VALUED_1:def 4;
then A3:Z c= dom (g^) by XBOOLE_1:18;
A4:not 0 in Z
     proof
     assume A5: 0 in Z;
     dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 8
       .= dom id Z \ {0} by Lm1,A5; then
     not 0 in {0} by XBOOLE_0:def 5,A5,A3;
     hence thesis by TARSKI:def 1;
   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 VALUED_1:def 1,A1;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 VALUED_1:8,A1;
   dom (sin/cos/f1) = dom (sin/cos) /\ (dom f1 \ f1"{0}) by RFUNCT_1:def 4;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 4;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 st x in Z holds f.x=-sin.x/cos.x/x^2+1/x/(cos.x)^2
     proof
      let x;
      assume
A11:x in Z;then
     (-sin/cos/f1 + (id Z)^/cos^2).x
     =(-sin/cos/f1).x+((id Z)^/cos^2).x by VALUED_1:def 1,A1
    .=-(sin/cos/f1).x+((id Z)^/cos^2).x by VALUED_1:8
    .=-((sin/cos).x/f1.x)+((id Z)^/cos^2).x by RFUNCT_1:def 4,A11,A7
    .=-((sin.x*(cos.x)")/f1.x)+((id Z)^/cos^2).x by A8,RFUNCT_1:def 4,A11
    .=-sin.x/cos.x/f1.x+((id Z)^).x/(cos^2).x by A7,RFUNCT_1:def 4,A11
    .=-sin.x/cos.x/f1.x+(((id Z).x)")/(cos^2).x by RFUNCT_1:def 8,A9,A11
    .=-sin.x/cos.x/f1.x+1/x/(cos^2).x by FUNCT_1:35,A11
    .=-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 TAYLOR_1:def 1,A1
    .=-sin.x/cos.x/x^2+1/x/(cos.x)^2 by FDIFF_7:1;
    hence thesis by A1;
     end;
A12:for x st x in dom(((id Z)^(#)tan)`|Z) holds (((id Z)^(#)tan)`|Z).x=f.x
   proof
   let x;
   assume x in dom(((id Z)^(#)tan)`|Z);then
A13:x in Z by A6,FDIFF_1:def 8;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 thesis;
  end;
  dom(((id Z)^(#)tan)`|Z)=dom f by A1,A6,FDIFF_1:def 8;
  then(((id Z)^(#)tan)`|Z)= f by A12,PARTFUN1:34;
  hence thesis by A1,A2,A6,INTEGRA5:13;
end;

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

theorem
 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)
proof
  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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
   set g = id Z;
Z c= dom (g^(#)cot) by A1;
    then Z c= dom (g^) /\ dom cot by VALUED_1:def 4;then
A3:Z c= dom (g^) by XBOOLE_1:18;
A4:not 0 in Z
   proof
     assume A5: 0 in Z;
     dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 8
                  .= dom id Z \ {0} by Lm1,A5; then
     not 0 in {0} by XBOOLE_0:def 5,A5,A3;
     hence thesis by TARSKI:def 1;
   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 VALUED_1:12,A1;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 4;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 4;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 st x in Z holds f.x=-cos.x/sin.x/x^2-1/x/(sin.x)^2
     proof
      let x;
      assume
A12:x in Z;then
     (-cos/sin/f1 - (id Z)^/sin^2).x
     =(-cos/sin/f1).x-((id Z)^/sin^2).x by VALUED_1:13,A1
    .=-(cos/sin/f1).x-((id Z)^/sin^2).x by VALUED_1:8
    .=-((cos/sin).x/f1.x)-((id Z)^/sin^2).x by RFUNCT_1:def 4,A12,A8
    .=-cos.x/sin.x/f1.x-((id Z)^/sin^2).x by A9,RFUNCT_1:def 4,A12
    .=-cos.x/sin.x/f1.x-((id Z)^).x/(sin^2).x by A8,RFUNCT_1:def 4,A12
    .=-cos.x/sin.x/f1.x-(((id Z).x)")/(sin^2).x by RFUNCT_1:def 8,A10,A12
    .=-cos.x/sin.x/f1.x-1/x/(sin^2).x by FUNCT_1:35,A12
    .=-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 TAYLOR_1:def 1,A1
    .=-cos.x/sin.x/x^2-1/x/(sin.x)^2 by FDIFF_7:1;
    hence thesis by A1;
     end;
A13:for x st x in dom(((id Z)^(#)cot)`|Z) holds (((id Z)^(#)cot)`|Z).x=f.x
   proof
   let x;
   assume x in dom(((id Z)^(#)cot)`|Z);then
A14:x in Z by A6,FDIFF_1:def 8;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 thesis;
  end;
  dom(((id Z)^(#)cot)`|Z)=dom f by A1,A6,FDIFF_1:def 8;
  then(((id Z)^(#)cot)`|Z)= f by A13,PARTFUN1:34;
  hence thesis by A1,A2,A6,INTEGRA5:13;
end;

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

theorem
 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)
proof
  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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(ln(#)tan) is_differentiable_on Z by A1,FDIFF_8:32;
   Z = dom (sin/cos/(id Z)) /\ dom (ln/cos^2) by VALUED_1:def 1,A1; 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 4;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 st x in Z holds f.x=sin.x/cos.x/x+ln.x/(cos.x)^2
   proof
   let x;
   assume
A7:x in Z;then
   (sin/cos/(id Z)+ln/cos^2).x=(sin/cos/(id Z)).x+(ln/cos^2).x
    by VALUED_1:def 1,A1
   .=(sin/cos).x/(id Z).x+(ln/cos^2).x by RFUNCT_1:def 4,A7,A4
   .=sin.x/cos.x/(id Z).x+(ln/cos^2).x by A5,RFUNCT_1:def 4,A7
   .=sin.x/cos.x/x+(ln/cos^2).x by FUNCT_1:35,A7
   .=sin.x/cos.x/x+ln.x/(cos^2).x by RFUNCT_1:def 4,A7,A4
   .=sin.x/cos.x/x+ln.x/(cos.x)^2 by VALUED_1:11;
    hence thesis by A1;
    end;
A8:for x st x in dom ((ln(#)tan)`|Z) holds ((ln(#)tan)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((ln(#)tan)`|Z);then
A9:x in Z by A3,FDIFF_1:def 8;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 thesis;
  end;
  dom ((ln(#)tan)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((ln(#)tan)`|Z)= f by A8,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_8:32,INTEGRA5:13;
end;

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

theorem
 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)
proof
  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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(ln(#)cot) is_differentiable_on Z by A1,FDIFF_8:33;
   Z = dom (cos/sin/(id Z)) /\ dom (ln/sin^2) by VALUED_1:12,A1;
   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 4;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 st x in Z holds f.x=cos.x/sin.x/x-ln.x/(sin.x)^2
   proof
   let x;
   assume
A7:x in Z;then
   (cos/sin/(id Z)-ln/sin^2).x=(cos/sin/(id Z)).x-(ln/sin^2).x
    by VALUED_1:13,A1
   .=(cos/sin).x/(id Z).x-(ln/sin^2).x by RFUNCT_1:def 4,A7,A4
   .=cos.x/sin.x/(id Z).x-(ln/sin^2).x by A5,RFUNCT_1:def 4,A7
   .=cos.x/sin.x/x-(ln/sin^2).x by FUNCT_1:35,A7
   .=cos.x/sin.x/x-ln.x/(sin^2).x by RFUNCT_1:def 4,A7,A4
   .=cos.x/sin.x/x-ln.x/(sin.x)^2 by VALUED_1:11;
    hence thesis by A1;
    end;
A8:for x st x in dom ((ln(#)cot)`|Z) holds ((ln(#)cot)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((ln(#)cot)`|Z);then
A9:x in Z by A3,FDIFF_1:def 8;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 thesis;
  end;
  dom ((ln(#)cot)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((ln(#)cot)`|Z)= f by A8,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_8:33,INTEGRA5:13;
end;

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

theorem
 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)
proof
  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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(ln(#)tan) is_differentiable_on Z by A1,FDIFF_8:32;
   Z = dom (tan/(id Z)) /\ dom(ln/cos^2) by VALUED_1:def 1,A1;then
A4:Z c= dom (tan/(id Z)) & Z c= dom(ln/cos^2) by XBOOLE_1:18;
A5:for x st x in Z holds f.x=tan.x/x+ln.x/(cos.x)^2
   proof
   let x;
   assume
A6:x in Z;then
   (tan/(id Z)+ln/cos^2).x =(tan/(id Z)).x+(ln/cos^2).x by VALUED_1:def 1,A1
  .=tan.x/(id Z).x+(ln/cos^2).x by RFUNCT_1:def 4,A6,A4
  .=tan.x/x+(ln/cos^2).x by FUNCT_1:35,A6
  .=tan.x/x+ln.x/(cos^2).x by RFUNCT_1:def 4,A6,A4
  .=tan.x/x+ln.x/(cos.x)^2 by VALUED_1:11;
   hence thesis by A1;
   end;
A7:for x st x in dom ((ln(#)tan)`|Z) holds ((ln(#)tan)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((ln(#)tan)`|Z);then
A8:x in Z by A3,FDIFF_1:def 8;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 thesis;
  end;
  dom ((ln(#)tan)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((ln(#)tan)`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_8:32,INTEGRA5:13;
end;

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

theorem
 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)
proof
  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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(ln(#)cot) is_differentiable_on Z by A1,FDIFF_8:33;
   Z = dom (cot/(id Z)) /\ dom(ln/sin^2) by VALUED_1:12,A1;then
A4:Z c= dom (cot/(id Z)) & Z c= dom(ln/sin^2) by XBOOLE_1:18;
A5:for x st x in Z holds f.x=cot.x/x-ln.x/(sin.x)^2
   proof
   let x;
   assume
A6:x in Z;then
   (cot/(id Z)-ln/sin^2).x =(cot/(id Z)).x-(ln/sin^2).x by VALUED_1:13,A1
  .=cot.x/(id Z).x-(ln/sin^2).x by RFUNCT_1:def 4,A6,A4
  .=cot.x/x-(ln/sin^2).x by FUNCT_1:35,A6
  .=cot.x/x-ln.x/(sin^2).x by RFUNCT_1:def 4,A6,A4
  .=cot.x/x-ln.x/(sin.x)^2 by VALUED_1:11;
   hence thesis by A1;
   end;
A7:for x st x in dom ((ln(#)cot)`|Z) holds ((ln(#)cot)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((ln(#)cot)`|Z);then
A8:x in Z by A3,FDIFF_1:def 8;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,FDIFF_8:2,A8,SIN_COS9:16
  .=f.x by A5,A8;
  hence thesis;
  end;
  dom ((ln(#)cot)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((ln(#)cot)`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_8:33,INTEGRA5:13;
end;

::f.x=arctan.x/x+ln.x/(1+x^2)

theorem
 A c= Z & (for x 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)
proof
   assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
   Z = dom (arctan/(id Z)) /\ dom (ln/(f1+( #Z 2))) by VALUED_1:def 1,A1;
    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 4;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 4;
   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 XBOOLE_1:19,A4;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 RFUNCT_1:def 8,A5;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A9:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A8;
A10:for x st x in Z holds f.x=arctan.x/x+ln.x/(1+x^2)
    proof
    let x;
    assume
A11:x in Z;
    then (arctan/(id Z)+ln/(f1+( #Z 2))).x
    =(arctan/(id Z)).x+(ln/(f1+( #Z 2))).x by VALUED_1:def 1,A1
   .=arctan.x*((id Z).x)" +(ln/(f1+( #Z 2))).x by RFUNCT_1:def 4,A3,A11
   .=arctan.x*((id Z).x)"+(ln.x*((f1+( #Z 2)).x)") by RFUNCT_1:def 4,A3,A11
   .=arctan.x/x+(ln.x/(f1+( #Z 2)).x) by FUNCT_1:35,A11
   .=arctan.x/x+ln.x/(f1.x+( #Z 2).x) by VALUED_1:def 1,A9,A11
   .=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 thesis by A1;
   end;
A12:for x st x in dom((ln(#)arctan)`|Z) holds ((ln(#)arctan)`|Z).x=f.x
   proof
     let x;
     assume x in dom((ln(#)arctan)`|Z);then
A13:  x in Z by A7,FDIFF_1:def 8;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 thesis;
   end;
   dom((ln(#)arctan)`|Z)=dom f by A1,A7,FDIFF_1:def 8;
   then ((ln(#)arctan)`|Z)= f by A12,PARTFUN1:34;
   hence thesis by A1,A2,A6,SIN_COS9:127,INTEGRA5:13;
end;

::f.x=arccot.x/x-ln.x/(1+x^2)

theorem
 A c= Z & (for x 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)
proof
   assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
   Z = dom (arccot/(id Z)) /\ dom (ln/(f1+( #Z 2))) by VALUED_1:12,A1;
    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 4;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 4;
   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 XBOOLE_1:19,A4;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 RFUNCT_1:def 8,A5;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A9:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A8;
A10:for x st x in Z holds f.x=arccot.x/x-ln.x/(1+x^2)
   proof
   let x;
   assume
A11:x in Z;
     then (arccot/(id Z)-ln/(f1+( #Z 2))).x
    =(arccot/(id Z)).x-(ln/(f1+( #Z 2))).x by VALUED_1:13,A1
   .=arccot.x*((id Z).x)" -(ln/(f1+( #Z 2))).x by RFUNCT_1:def 4,A3,A11
   .=arccot.x*((id Z).x)"-(ln.x*((f1+( #Z 2)).x)") by RFUNCT_1:def 4,A3,A11
   .=arccot.x/x-(ln.x/(f1+( #Z 2)).x) by FUNCT_1:35,A11
   .=arccot.x/x-ln.x/(f1.x+( #Z 2).x) by VALUED_1:def 1,A9,A11
   .=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 thesis by A1;
   end;
A12:for x st x in dom((ln(#)arccot)`|Z) holds ((ln(#)arccot)`|Z).x=f.x
   proof
     let x;
     assume x in dom((ln(#)arccot)`|Z);then
A13:x in Z by A7,FDIFF_1:def 8;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 thesis;
   end;
  dom((ln(#)arccot)`|Z)=dom f by A1,A7,FDIFF_1:def 8;
  then ((ln(#)arccot)`|Z)= f by A12,PARTFUN1:34;
  hence thesis by A1,A2,A6,SIN_COS9:128,INTEGRA5:13;
end;

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

theorem
 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)
proof
  assume
A1:A c= Z & f=exp_R*tan/cos^2 & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
   Z = dom (exp_R*tan) /\ (dom (cos^2) \ (cos^2)"{0}) by RFUNCT_1:def 4,A1;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 st x in Z holds f.x=exp_R.(tan.x)/(cos.x)^2
    proof
    let x;
    assume
A6:x in Z;
   then (exp_R*tan/cos^2).x=(exp_R*tan).x/(cos^2).x by RFUNCT_1:def 4,A1
  .=exp_R.(tan.x)/(cos^2).x by FUNCT_1:22,A3,A6
  .=exp_R.(tan.x)/(cos.x)^2 by VALUED_1:11;
   hence thesis by A1;
   end;
A7:for x st x in dom ((exp_R*tan)`|Z) holds ((exp_R*tan)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((exp_R*tan)`|Z);then
A8:x in Z by A4,FDIFF_1:def 8;then
  ((exp_R*tan)`|Z).x=exp_R.(tan.x)/(cos.x)^2 by A3,FDIFF_8:16
  .=f.x by A5,A8;
  hence thesis;
  end;
  dom ((exp_R*tan)`|Z)=dom f by A1,A4,FDIFF_1:def 8;
  then ((exp_R*tan)`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,A3,FDIFF_8:16,INTEGRA5:13;
end;

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

theorem
 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)
proof
  assume
A1:A c= Z & f=-exp_R*cot/sin^2 & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 4;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 st x in Z holds f.x=-exp_R.(cot.x)/(sin.x)^2
   proof
    let x;
    assume
A7:x in Z;
   (-exp_R*cot/sin^2).x =-(exp_R*cot/sin^2).x by VALUED_1:8
  .=-(exp_R*cot).x/(sin^2).x by RFUNCT_1:def 4,A7,A3
  .=-exp_R.(cot.x)/(sin^2).x by FUNCT_1:22,A4,A7
  .=-exp_R.(cot.x)/(sin.x)^2 by VALUED_1:11;
   hence thesis by A1;
   end;
A8:for x st x in dom ((exp_R*cot)`|Z) holds ((exp_R*cot)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((exp_R*cot)`|Z);then
A9:x in Z by A5,FDIFF_1:def 8;then
  ((exp_R*cot)`|Z).x=-exp_R.(cot.x)/(sin.x)^2 by A4,FDIFF_8:17
  .=f.x by A6,A9;
  hence thesis;
  end;
  dom ((exp_R*cot)`|Z)=dom f by A1,A5,FDIFF_1:def 8;
  then ((exp_R*cot)`|Z)= f by A8,PARTFUN1:34;
  hence thesis by A1,A2,A4,FDIFF_8:17,INTEGRA5:13;
end;

theorem Th23:
  Z c= dom (exp_R*cot) implies -exp_R*cot is_differentiable_on Z &
  for x st x in Z holds ((-exp_R*cot)`|Z).x = exp_R.(cot.x)/(sin.x)^2
proof
  assume
A1:Z c= dom (exp_R*cot);
then A2:Z c= dom (-exp_R*cot) by VALUED_1:8;
A3:for x st x in Z holds sin.x<>0
  proof
    let x;
    assume x in Z;
    then x in dom (cos/sin) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:2;
  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:28,Lm3;
 for x st x in Z holds ((-exp_R*cot)`|Z).x = exp_R.(cot.x)/(sin.x)^2
   proof
     let x;
     assume
A6:x in Z; 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:70;
A10:exp_R*cot is_differentiable_in x by A4,A6,FDIFF_1:16;
   ((-exp_R*cot)`|Z).x=diff(-exp_R*cot,x) by A5,A6,FDIFF_1:def 8
                     .=(-1)*(diff(exp_R*cot,x)) by A10,FDIFF_1:23,Lm3
                     .=(-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:70
                     .=exp_R.(cot.x)/(sin.x)^2;
     hence thesis;
   end;
   hence thesis by A2,A4,FDIFF_1:28,Lm3;
end;

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

theorem
 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)
proof
  assume
A1: A c= Z & f=exp_R*cot/sin^2 & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
   Z = dom (exp_R*cot) /\ (dom (sin^2) \ (sin^2)"{0}) by RFUNCT_1:def 4,A1;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 st x in Z holds f.x=exp_R.(cot.x)/(sin.x)^2
   proof
   let x;
   assume
A6:x in Z;
   then (exp_R*cot/sin^2).x=(exp_R*cot).x/(sin^2).x by RFUNCT_1:def 4,A1
  .=exp_R.(cot.x)/(sin^2).x by FUNCT_1:22,A3,A6
  .=exp_R.(cot.x)/(sin.x)^2 by VALUED_1:11;
   hence thesis by A1;
   end;
A7:for x st x in dom ((-exp_R*cot)`|Z) holds ((-exp_R*cot)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((-exp_R*cot)`|Z);then
A8:x in Z by A4,FDIFF_1:def 8;then
  ((-exp_R*cot)`|Z).x=exp_R.(cot.x)/(sin.x)^2 by Th23,A3
  .=f.x by A5,A8;
  hence thesis;
  end;
  dom ((-exp_R*cot)`|Z)=dom f by A1,A4,FDIFF_1:def 8;
  then ((-exp_R*cot)`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,Th23,A3,INTEGRA5:13;
end;

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

theorem
 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)
proof
  assume
A1:A c= Z & f=((id Z)(#)(cos*ln)^2)^
   & Z c= dom (tan*ln) & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:tan*ln is_differentiable_on Z by A1,FDIFF_8:14;
Z c= dom ((id Z)(#)(cos*ln)^2) by RFUNCT_1:11,A1;
   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 st x in Z holds f.x=1/(x*(cos.(ln.x))^2)
  proof
  let x;
  assume
A6:x in Z;
   then (((id Z)(#)(cos*ln)^2)^).x
  =1/(((id Z)(#)(cos*ln)^2).x) by RFUNCT_1:def 8,A1
 .=1/((id Z).x*((cos*ln)^2).x) by VALUED_1:5
 .=1/(x*((cos*ln)^2).x) by FUNCT_1:35,A6
 .=1/(x*((cos*ln).x)^2) by VALUED_1:11
 .=1/(x*(cos.(ln.x))^2) by A4,FUNCT_1:22,A6;
     hence thesis by A1;
     end;
A7:for x st x in dom ((tan*ln)`|Z) holds ((tan*ln)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((tan*ln)`|Z);then
A8:x in Z by A3,FDIFF_1:def 8;then
  ((tan*ln)`|Z).x=1/(x*(cos.(ln.x))^2) by A1,FDIFF_8:14
  .=f.x by A5,A8;
  hence thesis;
  end;
  dom ((tan*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((tan*ln)`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_8:14,INTEGRA5:13;
end;

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

theorem
 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)
proof
  assume
A1:A c= Z & f=-((id Z)(#)(sin*ln)^2)^
   & Z c= dom (cot*ln) & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:cot*ln is_differentiable_on Z by A1,FDIFF_8:15;
A4:Z = dom (((id Z)(#)(sin*ln)^2)^) by VALUED_1:8,A1;
then Z c= dom ((id Z)(#)(sin*ln)^2) by RFUNCT_1:11;
   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 st x in Z holds f.x=-1/(x*(sin.(ln.x))^2)
   proof
  let x;
  assume
A7:x in Z;
   (-((id Z)(#)(sin*ln)^2)^).x =-(((id Z)(#)(sin*ln)^2)^).x by VALUED_1:8
 .=-1/(((id Z)(#)(sin*ln)^2).x) by RFUNCT_1:def 8,A4,A7
 .=-1/((id Z).x*((sin*ln)^2).x) by VALUED_1:5
 .=-1/(x*((sin*ln)^2).x) by FUNCT_1:35,A7
 .=-1/(x*((sin*ln).x)^2) by VALUED_1:11
 .=-1/(x*(sin.(ln.x))^2) by A5,FUNCT_1:22,A7;
     hence thesis by A1;
     end;
A8:for x st x in dom ((cot*ln)`|Z) holds ((cot*ln)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((cot*ln)`|Z);then
A9:x in Z by A3,FDIFF_1:def 8;then
  ((cot*ln)`|Z).x= -1/(x*(sin.(ln.x))^2) by A1,FDIFF_8:15
  .=f.x by A6,A9;
  hence thesis;
  end;
  dom ((cot*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((cot*ln)`|Z)= f by A8,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_8:15,INTEGRA5:13;
end;

theorem Th27:
Z c= dom (cot*ln) implies -cot*ln is_differentiable_on Z &
for x st x in Z holds ((-cot*ln)`|Z).x = 1/(x*(sin.(ln.x))^2)
proof
   assume
A1:Z c= dom (cot*ln);
then A2:Z c= dom (-cot*ln) by VALUED_1:8;
dom (cot*ln) c= dom ln by RELAT_1:44;
then A3:Z c= dom ln by A1,XBOOLE_1:1;
A4: for x st x in Z holds x>0
  proof
    let x;
    assume x in Z;
    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 thesis;
  end;
A5: for x st x in Z holds sin.(ln.x)<>0
  proof
    let x;
    assume x in Z;
    then ln.x in dom (cos/sin) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:2;
  end;
A6:for x st x in Z holds diff(ln,x) = 1/x
  proof
    let x;
    assume x in Z;
    then x>0 by A4;
    then x in right_open_halfline(0) by Lm2;
    hence thesis by TAYLOR_1:18;
  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:28,Lm3;
 for x st x in Z holds ((-cot*ln)`|Z).x = 1/(x*(sin.(ln.x))^2)
   proof
     let x;
     assume
A9:x in Z; 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:16;
  ((-cot*ln)`|Z).x=diff(-cot*ln,x) by A8,A9,FDIFF_1:def 8
                 .=(-1)*(diff(cot*ln,x)) by A13,FDIFF_1:23,Lm3
                 .=(-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:79;
    hence thesis;
   end;
   hence thesis by A2,A7,FDIFF_1:28,Lm3;
end;

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

theorem
 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)
proof
  assume
A1:A c= Z & f=((id Z)(#)(sin*ln)^2)^
   & Z c= dom (cot*ln) & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cot*ln is_differentiable_on Z by A1,Th27;
Z c= dom ((id Z)(#)(sin*ln)^2) by RFUNCT_1:11,A1;
   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 st x in Z holds f.x=1/(x*(sin.(ln.x))^2)
   proof
  let x;
  assume
A6:x in Z;
   then (((id Z)(#)(sin*ln)^2)^).x
  =1/(((id Z)(#)(sin*ln)^2).x) by RFUNCT_1:def 8,A1
 .=1/((id Z).x*((sin*ln)^2).x) by VALUED_1:5
 .=1/(x*((sin*ln)^2).x) by FUNCT_1:35,A6
 .=1/(x*((sin*ln).x)^2) by VALUED_1:11
 .=1/(x*(sin.(ln.x))^2) by A4,FUNCT_1:22,A6;
     hence thesis by A1;
     end;
A7:for x st x in dom ((-cot*ln)`|Z) holds ((-cot*ln)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((-cot*ln)`|Z);then
A8:x in Z by A3,FDIFF_1:def 8;then
  ((-cot*ln)`|Z).x= 1/(x*(sin.(ln.x))^2) by A1,Th27
  .=f.x by A5,A8;
  hence thesis;
  end;
  dom ((-cot*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((-cot*ln)`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,Th27,INTEGRA5:13;
end;

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

theorem
 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)
proof
  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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 RFUNCT_1:def 4,A1;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 8;
   dom (((cos*exp_R)^2)^) c= dom ((cos*exp_R)^2) by RFUNCT_1:11;then
Z c= dom ((cos*exp_R)^2) by XBOOLE_1:1,A4;
then A5:Z c= dom (cos*exp_R) by VALUED_1:11;
A6:for x st x in Z holds f.x=exp_R.x/(cos.(exp_R.x))^2
   proof
   let x;
   assume
A7:x in Z;
   then
(exp_R/(cos*exp_R)^2).x =exp_R.x/((cos*exp_R)^2).x by RFUNCT_1:def 4,A1
  .=exp_R.x/((cos*exp_R).x)^2 by VALUED_1:11
  .=exp_R.x/(cos.(exp_R.x))^2 by FUNCT_1:22,A5,A7;
   hence thesis by A1;
   end;
A8:for x st x in dom ((tan*exp_R)`|Z) holds ((tan*exp_R)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((tan*exp_R)`|Z);then
A9:x in Z by A3,FDIFF_1:def 8;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 thesis;
  end;
  dom ((tan*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((tan*exp_R)`|Z)= f by A8,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_8:12,INTEGRA5:13;
end;

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

theorem
 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)
proof
  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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 4;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 8;
   dom (((sin*exp_R)^2)^) c= dom ((sin*exp_R)^2) by RFUNCT_1:11;then
Z c= dom ((sin*exp_R)^2) by XBOOLE_1:1,A5;
then A6:Z c= dom (sin*exp_R) by VALUED_1:11;
A7:for x st x in Z holds f.x=-exp_R.x/(sin.(exp_R.x))^2
   proof
   let x;
   assume
A8:x in Z;
   (-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 RFUNCT_1:def 4,A4,A8
  .=-exp_R.x/((sin*exp_R).x)^2 by VALUED_1:11
  .=-exp_R.x/(sin.(exp_R.x))^2 by FUNCT_1:22,A6,A8;
   hence thesis by A1;
   end;
A9:for x st x in dom ((cot*exp_R)`|Z) holds ((cot*exp_R)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((cot*exp_R)`|Z);then
A10:x in Z by A3,FDIFF_1:def 8;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 thesis;
  end;
  dom ((cot*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((cot*exp_R)`|Z)= f by A9,PARTFUN1:34;
  hence thesis by A1,A2,FDIFF_8:13,INTEGRA5:13;
end;

theorem Th31:
 Z c= dom (cot*exp_R) implies -cot*exp_R is_differentiable_on Z &
 for x st x in Z holds ((-cot*exp_R)`|Z).x = exp_R.x/(sin.(exp_R.x))^2
proof
  assume
A1:Z c= dom (cot*exp_R);
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:28,Lm3;
A5:for x st x in Z holds sin.(exp_R.x)<>0
  proof
    let x;
    assume x in Z;
    then exp_R.x in dom (cos/sin) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:2;
  end;
  for x st x in Z holds ((-cot*exp_R)`|Z).x = exp_R.x/(sin.(exp_R.x))^2
  proof
    let x;
    assume
A6: x in Z;
A7: exp_R is_differentiable_in x by SIN_COS:70;
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:16;
 ((-cot*exp_R)`|Z).x=diff(-cot*exp_R,x) by A4,A6,FDIFF_1:def 8
                   .=(-1)*(diff(cot*exp_R,x)) by A10,FDIFF_1:23,Lm3
                   .=(-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:70;
    hence thesis;
  end;
  hence thesis by A4;
end;

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

theorem
 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)
proof
  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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 RFUNCT_1:def 4,A1;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 8;
   dom (((sin*exp_R)^2)^) c= dom ((sin*exp_R)^2) by RFUNCT_1:11;then
Z c= dom ((sin*exp_R)^2) by XBOOLE_1:1,A4;
then A5:Z c= dom (sin*exp_R) by VALUED_1:11;
A6:for x st x in Z holds f.x=exp_R.x/(sin.(exp_R.x))^2
   proof
   let x;
   assume
A7:x in Z;then
   (exp_R/(sin*exp_R)^2).x=exp_R.x/((sin*exp_R)^2).x by RFUNCT_1:def 4,A1
  .=exp_R.x/((sin*exp_R).x)^2 by VALUED_1:11
  .=exp_R.x/(sin.(exp_R.x))^2 by FUNCT_1:22,A5,A7;
   hence thesis by A1;
   end;
A8:for x st x in dom ((-cot*exp_R)`|Z) holds ((-cot*exp_R)`|Z).x=f.x
   proof
   let x;
   assume x in dom ((-cot*exp_R)`|Z);then
A9:x in Z by A3,FDIFF_1:def 8;then
  ((-cot*exp_R)`|Z).x=exp_R.x/(sin.(exp_R.x))^2 by A1,Th31
  .=f.x by A6,A9;
  hence thesis;
  end;
  dom ((-cot*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((-cot*exp_R)`|Z)= f by A8,PARTFUN1:34;
  hence thesis by A1,A2,Th31,INTEGRA5:13;
end;

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

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3: Z c= dom ((id Z)^) by FUNCT_1:171,A1;
A4:not 0 in Z
    proof
      assume A5: 0 in Z;
      dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 8
       .= dom id Z \ {0} by Lm1,A5; then
      not 0 in {0} by XBOOLE_0:def 5,A5,A3;
      hence thesis by TARSKI:def 1;
   end;
   then
A6:(tan*((id Z)^)) is_differentiable_on Z by A1,FDIFF_8:8;
A7:for x st x in dom ((tan*((id Z)^))`|Z) holds ((tan*((id Z)^))`|Z).x=f.x
   proof
   let x;
   assume x in dom ((tan*((id Z)^))`|Z);then
A8:x in Z by A6,FDIFF_1:def 8;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 thesis;
  end;
  dom ((tan*((id Z)^))`|Z)=dom f by A1,A6,FDIFF_1:def 8;
  then ((tan*((id Z)^))`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,A6,INTEGRA5:13;
end;

theorem Th34:
  Z c= dom (tan*((id Z)^)) implies (-tan*((id Z)^)) is_differentiable_on Z &
  for x st x in Z holds ((-tan*((id Z)^))`|Z).x = 1/(x^2*(cos.(1/x))^2)
proof
  set f = id Z;
  assume
A1:Z c= dom (tan*((id Z)^));
 dom (tan*(f^)) c= dom (f^) by RELAT_1:44; then
A2:Z c= dom (f^) by XBOOLE_1:1,A1;
A3:not 0 in Z
   proof
     assume A4: 0 in Z;
     dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 8
       .= dom id Z \ {0} by Lm1,A4; then
     not 0 in {0} by XBOOLE_0:def 5,A4,A2;
     hence thesis by TARSKI:def 1;
   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:28,Lm3;
A8:f^ is_differentiable_on Z &
  for x st x in Z holds ((f^)`|Z).x = -1/x^2 by A3,FDIFF_5:4;
A9: for x st x in Z holds (cos.((f^).x))<>0
  proof
    let x;
    assume x in Z;
    then f^.x in dom (sin/cos) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:1;
  end;
 for x st x in Z holds ((-tan*(f^))`|Z).x = 1/(x^2*(cos.(1/x))^2)
  proof
    let x;
    assume
A10: x in Z; then
A11: f^ is_differentiable_in x by A8,FDIFF_1:16;
A12: cos.((f^).x)<>0 by A9,A10;then
A13:tan is_differentiable_in (f^).x by FDIFF_7:46;
A14:tan*(f^) is_differentiable_in x by A6,A10,FDIFF_1:16;
  ((-tan*(f^))`|Z).x=diff(-tan*(f^),x) by A7,A10,FDIFF_1:def 8
                   .=(-1)*(diff(tan*(f^),x)) by A14,FDIFF_1:23,Lm3
                   .=(-1)*(diff(tan,(f^).x)*diff((f^),x))
by A11,A13,FDIFF_2:13
                   .=(-1)*((1/(cos.((f^).x))^2) * diff((f^),x))
by A12,FDIFF_7:46
                   .=(-1)*(diff((f^),x)/(cos.((f.x)"))^2)
by A2,A10,RFUNCT_1:def 8
                   .=(-1)*(diff((f^),x)/(cos.(1*x"))^2) by FUNCT_1:35,A10
                   .=(-1)*(((f^)`|Z).x/(cos.(1*x"))^2)
by A8,A10,FDIFF_1:def 8
                   .=(-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:79
                   .=1/(x^2*(cos.(1/x))^2);
    hence thesis;
  end;
  hence thesis by A7;
end;

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

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(-tan*((id Z)^)) is_differentiable_on Z by A1,Th34;
A4:for x st x in dom ((-tan*((id Z)^))`|Z) holds ((-tan*((id Z)^))`|Z).x=f.x
   proof
   let x;
   assume x in dom ((-tan*((id Z)^))`|Z);then
A5:x in Z by A3,FDIFF_1:def 8;then
  ((-tan*((id Z)^))`|Z).x=1/(x^2*(cos.(1/x))^2) by A1,Th34
  .=f.x by A1,A5;
  hence thesis;
  end;
  dom ((-tan*((id Z)^))`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then ((-tan*((id Z)^))`|Z)= f by A4,PARTFUN1:34;
  hence thesis by A1,A2,A3,INTEGRA5:13;
end;

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

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3: Z c= dom ((id Z)^) by FUNCT_1:171,A1;
A4:not 0 in Z
     proof
      assume A5: 0 in Z;
     dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 8
       .= dom id Z \ {0} by Lm1,A5; then
     not 0 in {0} by XBOOLE_0:def 5,A5,A3;
     hence thesis by TARSKI:def 1;
   end;
   then
A6:(cot*((id Z)^)) is_differentiable_on Z by A1,FDIFF_8:9;
A7:for x st x in dom ((cot*((id Z)^))`|Z) holds ((cot*((id Z)^))`|Z).x=f.x
   proof
   let x;
   assume x in dom ((cot*((id Z)^))`|Z);then
A8:x in Z by A6,FDIFF_1:def 8;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 thesis;
  end;
  dom ((cot*((id Z)^))`|Z)=dom f by A1,A6,FDIFF_1:def 8;
  then ((cot*((id Z)^))`|Z)= f by A7,PARTFUN1:34;
  hence thesis by A1,A2,A6,INTEGRA5:13;
end;

::f.x=1/((1+x^2)*arctan.x)

theorem
 A c= Z & (for x 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)
proof
   assume
A1:A c= Z & (for x 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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:for x 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 RFUNCT_1:11,A1; 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 st x in Z holds f.x=1/((1+x^2)*arctan.x)
  proof
  let x;
  assume
A7:x in Z;
    then
(((f1+#Z 2)(#)arctan)^).x =1/((f1+#Z 2)(#)arctan).x by RFUNCT_1:def 8,A1
  .=1/((f1+#Z 2).x*arctan.x) by VALUED_1:5
  .=1/((f1.x+( #Z 2).x)*arctan.x) by VALUED_1:def 1,A5,A7
  .=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 thesis by A1;
   end;
A8:for x st x in dom ((ln*(arctan))`|Z) holds ((ln*(arctan))`|Z).x=f.x
   proof
   let x;
   assume x in dom ((ln*(arctan))`|Z);then
A9:x in Z by A4,FDIFF_1:def 8;then
  ((ln*(arctan))`|Z).x=1/((1+x^2)*arctan.x) by A1,A3,SIN_COS9:89
  .=f.x by A6,A9;
  hence thesis;
  end;
  dom ((ln*(arctan))`|Z)=dom f by A1,A4,FDIFF_1:def 8;
  then ((ln*(arctan))`|Z)= f by A8,PARTFUN1:34;
  hence thesis by A1,A2,A4,INTEGRA5:13;
end;

::f.x=n*(arctan.x) #Z (n-1) / (1+x^2)

theorem
 A c= Z & f=n(#)((( #Z (n-1))*arctan)/(f1+#Z 2))
 & (for x 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)
proof
  assume
A1:A c= Z & f=n(#)((( #Z (n-1))*arctan)/(f1+#Z 2))
   & (for x 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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 4;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 8;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A7:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A6;
A8:for x st x in Z holds f.x=n*(arctan.x) #Z (n-1) / (1+x^2)
    proof
    let x;
    assume
A9:x in Z;
    (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 RFUNCT_1:def 4,A4,A9
  .=n*(( #Z (n-1))*arctan).x/(f1+#Z 2).x
  .=n*(( #Z (n-1)).(arctan.x))/(f1+#Z 2).x by FUNCT_1:22,A5,A9
  .=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,VALUED_1:def 1,A9
  .=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 thesis by A1;
   end;
A10:for x st x in dom((( #Z n)*(arctan))`|Z) holds
   ((( #Z n)*(arctan))`|Z).x=f.x
   proof
   let x;
   assume x in dom((( #Z n)*(arctan))`|Z);then
A11:x in Z by A3,FDIFF_1:def 8;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 thesis;
  end;
  dom((( #Z n)*(arctan))`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then((( #Z n)*(arctan))`|Z)= f by A10,PARTFUN1:34;
  hence thesis by A1,A2,SIN_COS9:91,INTEGRA5:13;
end;

::f.x=-n*(arccot.x) #Z (n-1) / (1+x^2)

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 4;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 8;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A7:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A6;
A8:for x st x in Z holds f.x=-n*(arccot.x) #Z (n-1) / (1+x^2)
   proof
   let x;
   assume
A9: x in Z;
   (-(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 RFUNCT_1:def 4,A4,A9
  .=-n*(( #Z (n-1))*arccot).x/(f1+#Z 2).x
  .=-n*(( #Z (n-1)).(arccot.x))/(f1+#Z 2).x by FUNCT_1:22,A5,A9
  .=-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,VALUED_1:def 1,A9
  .=-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 thesis by A1;
   end;
A10:for x st x in dom((( #Z n)*(arccot))`|Z) holds
   ((( #Z n)*(arccot))`|Z).x=f.x
   proof
   let x;
   assume x in dom((( #Z n)*(arccot))`|Z);then
A11:x in Z by A3,FDIFF_1:def 8;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 thesis;
  end;
  dom((( #Z n)*arccot)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then((( #Z n)*arccot)`|Z)= f by A10,PARTFUN1:34;
  hence thesis by A1,A2,SIN_COS9:92,INTEGRA5:13;
end;

theorem Th40:
  Z c= dom (( #Z n)*arccot) & Z c= ]. -1,1 .[ implies
  -( #Z n)*arccot is_differentiable_on Z & for x st x in Z holds
  ((-( #Z n)*arccot)`|Z).x = n*(arccot.x) #Z (n-1) / (1+x^2)
proof
    assume
A1:Z c= dom (( #Z n)*arccot) & Z c= ]. -1,1 .[;
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:28,Lm3;
 for x st x in Z holds ((-( #Z n)*arccot)`|Z).x
                         = n*(arccot.x) #Z (n-1) / (1+x^2)
   proof
      let x;
      assume
A5:x in Z;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:16;
A8:( #Z n)*(arccot) is_differentiable_in x by A3,A5,FDIFF_1:16;
  ((-( #Z n)*arccot)`|Z).x=diff(-( #Z n)*arccot,x) by A4,A5,FDIFF_1:def 8
     .=(-1)*(diff(( #Z n)*arccot,x)) by A8,FDIFF_1:23,Lm3
     .=(-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 thesis;
   end;
   hence thesis by A2,A3,FDIFF_1:28,Lm3;
end;

::f.x=n*(arccot.x) #Z (n-1) / (1+x^2)

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 4;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 8;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A7:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A6;
A8:for x st x in Z holds f.x=n*(arccot.x) #Z (n-1) / (1+x^2)
    proof
    let x;
    assume
A9:x in Z;
    (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 RFUNCT_1:def 4,A4,A9
  .=n*(( #Z (n-1))*arccot).x/(f1+#Z 2).x
  .=n*(( #Z (n-1)).(arccot.x))/(f1+#Z 2).x by FUNCT_1:22,A5,A9
  .=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,VALUED_1:def 1,A9
  .=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 thesis by A1;
   end;
A10:for x st x in dom((-( #Z n)*(arccot))`|Z) holds
   ((-( #Z n)*arccot)`|Z).x=f.x
   proof
   let x;
   assume x in dom((-( #Z n)*(arccot))`|Z);then
A11:x in Z by A3,FDIFF_1:def 8;then
  ((-( #Z n)*arccot)`|Z).x=n*(arccot.x) #Z (n-1) / (1+x^2) by A1,Th40
  .=f.x by A11,A8;
  hence thesis;
  end;
  dom((-( #Z n)*arccot)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then((-( #Z n)*arccot)`|Z)= f by A10,PARTFUN1:34;
  hence thesis by A1,A2,Th40,INTEGRA5:13;
end;

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

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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;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,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 RFUNCT_1:def 4,A1;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 8;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A6:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A5;
A7:for x st x in Z holds f.x=arctan.x / (1+x^2)
   proof
   let x;
   assume
A8:x in Z;then
   (arctan/(f1+#Z 2)).x =arctan.x/(f1+#Z 2).x by A1,RFUNCT_1:def 4
   .=arctan.x/(f1.x+(( #Z 2).x)) by VALUED_1:def 1,A6,A8
   .=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 thesis by A1;
    end;
A9:for x st x in dom(((1/2)(#)(( #Z 2)*(arctan)))`|Z) holds
   (((1/2)(#)(( #Z 2)*arctan))`|Z).x=f.x
   proof
   let x;
   assume x in dom(((1/2)(#)(( #Z 2)*arctan))`|Z);then
A10:x in Z by A4,FDIFF_1:def 8;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 thesis;
  end;
  dom(((1/2)(#)(( #Z 2)*arctan))`|Z)=dom f by A1,A4,FDIFF_1:def 8;
  then(((1/2)(#)(( #Z 2)*arctan))`|Z)= f by A9,PARTFUN1:34;
  hence thesis by A1,A2,A3,SIN_COS9:93,INTEGRA5:13;
end;

::f.x=-arccot.x / (1+x^2)

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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;
   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,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 4;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 8;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A7:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A6;
A8:for x st x in Z holds f.x=-arccot.x / (1+x^2)
   proof
   let x;
   assume
A9:x in Z;
   (-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 4
  .=-arccot.x/(f1.x+(( #Z 2).x)) by VALUED_1:def 1,A7,A9
  .=-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 thesis by A1;
    end;
A10:for x st x in dom(((1/2)(#)(( #Z 2)*arccot))`|Z) holds
   (((1/2)(#)(( #Z 2)*arccot))`|Z).x=f.x
   proof
   let x;
   assume x in dom(((1/2)(#)(( #Z 2)*arccot))`|Z);then
A11:x in Z by A4,FDIFF_1:def 8;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 thesis;
  end;
  dom(((1/2)(#)(( #Z 2)*(arccot)))`|Z)=dom f by A1,A4,FDIFF_1:def 8;
  then(((1/2)(#)(( #Z 2)*(arccot)))`|Z)= f by A10,PARTFUN1:34;
  hence thesis by A1,A2,A3,SIN_COS9:94,INTEGRA5:13;
end;

theorem Th44:
  Z c= dom (( #Z 2)*(arccot)) & Z c= ]. -1,1 .[ implies
  -(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_on Z & for x st x in Z holds
  ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x = arccot.x / (1+x^2)
proof
   assume
A1:Z c= dom (( #Z 2)*(arccot)) & Z c= ]. -1,1 .[;
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:28,Lm3;
A6:( #Z 2)*(arccot) is_differentiable_on Z & for x 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 st x in Z holds
    ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x = arccot.x / (1+x^2)
    proof
      let x;
      assume
A7: x in Z;then
A8:(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_in x by A4,FDIFF_1:16;
A9:( #Z 2)*(arccot) is_differentiable_in x by A6,A7,FDIFF_1:16;
  ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x=diff(-(1/2)(#)(( #Z 2)*(arccot)),x)
         by A5,A7,FDIFF_1:def 8
      .=(-1)*(diff((1/2)(#)(( #Z 2)*(arccot)),x)) by A8,FDIFF_1:23,Lm3
      .=(-1)*((1/2)*diff(( #Z 2)*(arccot),x)) by A9,FDIFF_1:23,Lm3
      .=(-1)*((1/2)*((( #Z 2)*(arccot))`|Z).x) by A6,A7,FDIFF_1:def 8
      .=(-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:45
      .=arccot.x / (1+x^2);
    hence thesis;
   end;
   hence thesis by A3,A4,FDIFF_1:28,Lm3;
end;

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

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 RFUNCT_1:def 4,A1;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 8;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A5:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A4;
A6:for x st x in Z holds f.x=arccot.x / (1+x^2)
   proof
   let x;
   assume
A7:x in Z;then
   (arccot/(f1+#Z 2)).x =arccot.x/(f1+#Z 2).x by A1,RFUNCT_1:def 4
   .=arccot.x/(f1.x+(( #Z 2).x)) by VALUED_1:def 1,A5,A7
   .=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 thesis by A1;
    end;
A8:for x st x in dom((-(1/2)(#)(( #Z 2)*(arccot)))`|Z) holds
   ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x=f.x
   proof
   let x;
   assume x in dom((-(1/2)(#)(( #Z 2)*(arccot)))`|Z);then
A9:x in Z by A3,FDIFF_1:def 8;then
  ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x=arccot.x / (1+x^2) by A1,Th44
  .=f.x by A6,A9;
  hence thesis;
  end;
  dom((-(1/2)(#)(( #Z 2)*(arccot)))`|Z)=dom f by A1,A3,FDIFF_1:def 8;
  then((-(1/2)(#)(( #Z 2)*(arccot)))`|Z)= f by A8,PARTFUN1:34;
  hence thesis by A1,A2,Th44,INTEGRA5:13;
end;

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

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
   Z = dom arctan /\ dom ((id Z)/(f1+#Z 2)) by VALUED_1:def 1,A1;
   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 4;
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 RFUNCT_1:def 8,A4;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A7:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A6;
A8:for x st x in Z holds f.x=arctan.x + x/(1+x^2)
  proof
  let x;
  assume
A9: x in Z;
   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 RFUNCT_1:def 4,A3,A9
  .=arctan.x+x/(f1+#Z 2).x by FUNCT_1:35,A9
  .=arctan.x+x/(f1.x+( #Z 2).x) by VALUED_1:def 1,A7,A9
  .=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 thesis by A1;
    end;
A10:for x st x in dom(((id Z)(#)(arctan))`|Z) holds
   (((id Z)(#)(arctan))`|Z).x=f.x
   proof
   let x;
   assume x in dom(((id Z)(#)(arctan))`|Z);then
A11:x in Z by A5,FDIFF_1:def 8;then
  (((id Z)(#)(arctan))`|Z).x=arctan.x + x/(1+x^2) by A1,SIN_COS9:95
  .=f.x by A8,A11;
  hence thesis;
  end;
  dom(((id Z)(#)(arctan))`|Z)=dom f by A1,A5,FDIFF_1:def 8;
  then(((id Z)(#)(arctan))`|Z)= f by A10,PARTFUN1:34;
  hence thesis by A1,A2,SIN_COS9:95,INTEGRA5:13;
end;

::f.x=arccot.x - x/(1+x^2)

theorem
 A c= Z & (for x 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)
proof
  assume
A1:A c= Z & (for x 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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
   Z = dom arccot /\ dom ((id Z)/(f1+#Z 2)) by VALUED_1:12,A1;
   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 4;
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 RFUNCT_1:def 8,A4;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A7:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A6;
A8:for x st x in Z holds f.x=arccot.x - x/(1+x^2)
  proof
  let x;
  assume
A9: x in Z;
   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 RFUNCT_1:def 4,A3,A9
  .=arccot.x-x/(f1+#Z 2).x by FUNCT_1:35,A9
  .=arccot.x-x/(f1.x+( #Z 2).x) by VALUED_1:def 1,A7,A9
  .=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 thesis by A1;
    end;
A10:for x st x in dom(((id Z)(#)(arccot))`|Z) holds
   (((id Z)(#)(arccot))`|Z).x=f.x
   proof
   let x;
   assume x in dom(((id Z)(#)(arccot))`|Z);then
A11:x in Z by A5,FDIFF_1:def 8;then
  (((id Z)(#)(arccot))`|Z).x=arccot.x - x/(1+x^2) by A1,SIN_COS9:96
  .=f.x by A11,A8;
  hence thesis;
  end;
  dom(((id Z)(#)(arccot))`|Z)=dom f by A1,A5,FDIFF_1:def 8;
  then(((id Z)(#)(arccot))`|Z)= f by A10,PARTFUN1:34;
  hence thesis by A1,A2,SIN_COS9:96,INTEGRA5:13;
end;

::f.x=exp_R.(arctan.x)/(1+x^2)

theorem
 A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arctan/(f1+#Z 2)
 & (for x 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)
proof
   assume
A1:A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arctan/(f1+#Z 2)
   & (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous;
   then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
   Z = dom (exp_R*arctan) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
   by RFUNCT_1:def 4,A1;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 8;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A5:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A4;
A6:exp_R*arctan is_differentiable_on Z by A1,A3,SIN_COS9:119;
A7:for x st x in Z holds f.x=exp_R.(arctan.x)/(1+x^2)
  proof
  let x;
  assume
A8:x in Z;
  then (exp_R*arctan/(f1+#Z 2)).x
  =(exp_R*arctan).x/(f1+#Z 2).x by RFUNCT_1:def 4,A1
 .=exp_R.(arctan.x)/(f1+#Z 2).x by FUNCT_1:22,A3,A8
 .=exp_R.(arctan.x)/(f1.x+( #Z 2).x) by VALUED_1:def 1,A5,A8
 .=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 thesis by A1;
  end;
A9:for x st x in dom ((exp_R*arctan)`|Z) holds ((exp_R*arctan)`|Z).x=f.x
    proof
     let x;
     assume x in dom ((exp_R*arctan)`|Z);then
A10:  x in Z by A6, FDIFF_1:def 8;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 thesis;
   end;
  dom ((exp_R*arctan)`|Z)=dom f by A1,A6,FDIFF_1:def 8;
  then ((exp_R*arctan)`|Z)= f by A9,PARTFUN1:34;
  hence thesis by A1,A2,A3,SIN_COS9:119,INTEGRA5:13;
end;

::f.x=-exp_R.(arccot.x)/(1+x^2)

theorem
 A c= Z & Z c= ]. -1,1 .[ & f=-exp_R*arccot/(f1+#Z 2)
 & (for x 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)
proof
   assume
A1:A c= Z & Z c= ]. -1,1 .[ & f=-exp_R*arccot/(f1+#Z 2)
   & (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous;
   then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:Z = dom (exp_R*arccot/(f1+#Z 2)) by VALUED_1:8,A1;
   then Z = dom (exp_R*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
   by RFUNCT_1:def 4;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 8;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A6:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A5;
A7:exp_R*arccot is_differentiable_on Z by A1,A4,SIN_COS9:120;
A8:for x st x in Z holds f.x=-exp_R.(arccot.x)/(1+x^2)
  proof
  let x;
  assume
A9:x in Z;
   (-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 RFUNCT_1:def 4,A9,A3
 .=-exp_R.(arccot.x)/(f1+#Z 2).x by FUNCT_1:22,A4,A9
 .=-exp_R.(arccot.x)/(f1.x+( #Z 2).x) by VALUED_1:def 1,A6,A9
 .=-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 thesis by A1;
  end;
A10:for x st x in dom ((exp_R*arccot)`|Z) holds ((exp_R*arccot)`|Z).x=f.x
    proof
     let x;
     assume x in dom ((exp_R*arccot)`|Z);then
A11:  x in Z by A7,FDIFF_1:def 8;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 thesis;
   end;
  dom ((exp_R*arccot)`|Z)=dom f by A1,A7,FDIFF_1:def 8;
  then ((exp_R*arccot)`|Z)= f by A10,PARTFUN1:34;
  hence thesis by A1,A2,A4,SIN_COS9:120,INTEGRA5:13;
end;

theorem Th50:
 Z c= dom (exp_R*arccot) & Z c= ]. -1,1 .[ implies
 -exp_R*arccot is_differentiable_on Z & for x st x in Z holds
 ((-exp_R*arccot)`|Z).x = exp_R.(arccot.x)/(1+x^2)
proof
   assume
A1:Z c= dom (exp_R*arccot) & Z c= ]. -1,1 .[;
then A2:Z c= dom (-exp_R*arccot) by VALUED_1:8;
A3:exp_R*arccot is_differentiable_on Z by SIN_COS9:120,A1;
then A4:(-1)(#)(exp_R*arccot) is_differentiable_on Z by A2,FDIFF_1:28,Lm3;
  for x st x in Z holds ((-exp_R*arccot)`|Z).x = exp_R.(arccot.x)/(1+x^2)
    proof
      let x;
      assume
A5:x in Z;
A6:arccot is_differentiable_on Z by SIN_COS9:82,A1;then
A7:arccot is_differentiable_in x by A5,FDIFF_1:16;
A8:exp_R is_differentiable_in arccot.x by SIN_COS:70;
A9:exp_R*arccot is_differentiable_in x by A3,A5,FDIFF_1:16;
 ((-exp_R*arccot)`|Z).x=diff(-exp_R*arccot,x) by A4,A5,FDIFF_1:def 8
                      .=(-1)*(diff(exp_R*arccot,x)) by A9,FDIFF_1:23,Lm3
                      .=(-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 8
                      .=(-1)*(diff(exp_R,arccot.x)*(-1/(1+x^2)))
        by A5,SIN_COS9:82,A1
                      .=(-1)*(-diff(exp_R,arccot.x)*(1/(1+x^2)))
                      .=exp_R.(arccot.x)/(1+x^2) by SIN_COS:70;
      hence thesis;
   end;
   hence thesis by A2,A3,FDIFF_1:28,Lm3;
end;

::f.x=exp_R.(arccot.x)/(1+x^2)

theorem
 A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arccot/(f1+#Z 2)
 & (for x 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)
proof
   assume
A1:A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arccot/(f1+#Z 2)
   & (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous;
   then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
   Z = dom (exp_R*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
   by RFUNCT_1:def 4,A1;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 8;
   dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:11;then
A5:Z c= dom (f1+#Z 2) by XBOOLE_1:1,A4;
A6:-exp_R*arccot is_differentiable_on Z by A1,A3,Th50;
A7:for x st x in Z holds f.x=exp_R.(arccot.x)/(1+x^2)
  proof
  let x;
  assume
A8:x in Z;
  then (exp_R*arccot/(f1+#Z 2)).x
  =(exp_R*arccot).x/(f1+#Z 2).x by RFUNCT_1:def 4,A1
 .=exp_R.(arccot.x)/(f1+#Z 2).x by FUNCT_1:22,A3,A8
 .=exp_R.(arccot.x)/(f1.x+( #Z 2).x) by VALUED_1:def 1,A5,A8
 .=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 thesis by A1;
  end;
A9:for x st x in dom ((-exp_R*arccot)`|Z) holds ((-exp_R*arccot)`|Z).x=f.x
   proof
     let x;
     assume x in dom ((-exp_R*arccot)`|Z);then
A10:  x in Z by A6,FDIFF_1:def 8;then
     ((-exp_R*arccot)`|Z).x=exp_R.(arccot.x)/(1+x^2) by A1,A3,Th50
                       .=f.x by A7,A10;
     hence thesis;
   end;
   dom ((-exp_R*arccot)`|Z)=dom f by A1,A6,FDIFF_1:def 8;
   then ((-exp_R*arccot)`|Z)= f by A9,PARTFUN1:34;
   hence thesis by A1,A2,A3,Th50,INTEGRA5:13;
end;

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

theorem
 A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(f1+f2)
 & f2=#Z 2 & (for x 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)
proof
  assume
A1:A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(f1+f2)
   & f2=#Z 2 & (for x st x in Z holds f1.x=1) & Z = dom f
   & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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 4; then
   Z c= dom (f1+f2) \ (f1+f2)"{0} by XBOOLE_1:18;then
A4:Z c= dom ((f1+f2)^) by RFUNCT_1:def 8;
   dom ((f1+f2)^) c= dom (f1+f2) by RFUNCT_1:11;then
A5:Z c= dom (f1+f2) by XBOOLE_1:1,A4;
A6:(1/2)(#)(ln*(f1+f2)) is_differentiable_on Z by A1,A3,SIN_COS9:102;
A7: for x st x in Z holds f.x=x/(1+x^2)
    proof
    let x;
    assume
A8: x in Z;
    then ((id Z)/(f1+f2)).x=(id Z).x/(f1+f2).x by RFUNCT_1:def 4,A1
  .=x/(f1+f2).x by A8,FUNCT_1:35
  .=x/(f1.x+f2.x) by VALUED_1:def 1,A5,A8
  .=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 thesis by A1;
   end;
A9:for x st x in dom(((1/2)(#)(ln*(f1+f2)))`|Z) holds
   (((1/2)(#)(ln*(f1+f2)))`|Z).x=f.x
    proof
      let x;
      assume x in dom(((1/2)(#)(ln*(f1+f2)))`|Z);then
A10:   x in Z by A6,FDIFF_1:def 8;then
      (((1/2)(#)(ln*(f1+f2)))`|Z).x=x/(1+x^2) by A1,A3,SIN_COS9:102
                               .=f.x by A10,A7;
      hence thesis;
    end;
   dom(((1/2)(#)(ln*(f1+f2)))`|Z)=dom f by A1,A6,FDIFF_1:def 8;
   then(((1/2)(#)(ln*(f1+f2)))`|Z)= f by A9,PARTFUN1:34;
   hence thesis by A1,A2,A6,INTEGRA5:13;
end;

::f.x=x/(a*(1+(x/a)^2))

theorem
 A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(a(#)(f1+f2))
 & (for x 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)
proof
   assume
A1:A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(a(#)(f1+f2))
   & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:Z c= dom ((a/2)(#)(ln*(f1+f2))) by A1,VALUED_1:def 5;
A4:for x st x in Z holds f1.x=1 by A1;
A5:for x 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 st x in Z holds f.x=x/(a*(1+(x/a)^2))
  proof
  let x;
  assume
A8:x in Z; then
A9:x in dom (f1+f2) by A1,FUNCT_1:21;
   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,RFUNCT_1:def 4,A8
 .=x/(a(#)(f1+f2)).x by FUNCT_1:35,A8
 .=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,FUNCT_1:22,A10
 .=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 thesis by A1;
    end;
A11:for x st x in dom(((a/2)(#)(ln*(f1+f2)))`|Z) holds
  (((a/2)(#)(ln*(f1+f2)))`|Z).x=f.x
   proof
     let x;
     assume x in dom(((a/2)(#)(ln*(f1+f2)))`|Z);then
A12:  x in Z by A6,FDIFF_1:def 8;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 thesis;
   end;
   dom(((a/2)(#)(ln*(f1+f2)))`|Z) = dom f by A1,A6,FDIFF_1:def 8;
   then (((a/2)(#)(ln*(f1+f2)))`|Z) = f by A11,PARTFUN1:34;
   hence thesis by A1,A2,A6,INTEGRA5:13;
end;

theorem Th54:
  Z c= dom ((id Z)^(#)arctan) & Z c= ]. -1,1 .[
  implies (-(id Z)^(#)arctan) is_differentiable_on Z &
  for x st x in Z holds
  ((-(id Z)^(#)arctan)`|Z).x = arctan.x/(x^2)-1/(x*(1+x^2))
proof
  set f = id Z;
  assume that
A1:Z c= dom (f^(#)arctan) and
A2: Z c= ]. -1,1 .[;
A3:Z c= dom (-f^(#)arctan) by A1,VALUED_1:8;
A4:for x st x in Z holds f.x=x by FUNCT_1:35;
    Z c= dom (f^) /\ dom arctan by A1,VALUED_1:def 4;then
A5: Z c= dom (f^) by XBOOLE_1:18;
A6:not 0 in Z
   proof
     assume A7: 0 in Z;
     dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 8
       .= dom id Z \ {0} by Lm1,A7; then
     not 0 in {0} by XBOOLE_0:def 5,A7,A5;
     hence thesis by TARSKI:def 1;
   end; then
A8:f^ is_differentiable_on Z & for x st x in Z holds
    ((f^)`|Z).x = -1/x^2 by FDIFF_5:4;
A9:arctan is_differentiable_on Z by A2,SIN_COS9:81;
A10:(f^(#)arctan) is_differentiable_on Z by A1,A2,A6,SIN_COS9:129;
then A11:(-1)(#)(f^(#)arctan) is_differentiable_on Z by A3,FDIFF_1:28,Lm3;
  for x st x in Z holds ((-f^(#)arctan)`|Z).x = arctan.x/(x^2)-1/(x*(1+x^2))
    proof
      let x;
      assume
A12: x in Z;
then A13:(f^(#)arctan) is_differentiable_in x by A10,FDIFF_1:16;
A14:f^ is_differentiable_in x by A8,A12,FDIFF_1:16;
A15:arctan is_differentiable_in x by A9,A12,FDIFF_1:16;
 ((-f^(#)arctan)`|Z).x=diff(-f^(#)arctan,x) by A11,A12,FDIFF_1:def 8
          .=(-1)*(diff(f^(#)arctan,x)) by A13,FDIFF_1:23,Lm3
          .=(-1)*((arctan.x)*diff(f^,x)+((f^).x)*diff(arctan,x))
      by A14,A15,FDIFF_1:24
          .=(-1)*((arctan.x)*((f^)`|Z).x+((f^).x)*diff(arctan,x))
      by A8,A12,FDIFF_1:def 8
          .=(-1)*((arctan.x)*(-1/x^2)+((f^).x)*diff(arctan,x))
      by A6,A12,FDIFF_5:4
          .=(-1)*(-(arctan.x)*(1/x^2)+((f^).x)*((arctan)`|Z).x)
      by A9,A12,FDIFF_1:def 8
          .=(-1)*(-((arctan.x)*1)/(x^2)+((f^).x)*(1/(1+x^2)))
      by A2,A12,SIN_COS9:81
          .=(-1)*(-arctan.x/(x^2)+(f.x)"*(1/(1+x^2)))
      by A5,A12,RFUNCT_1:def 8
          .=(-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:77
          .=arctan.x/(x^2)-1/(x*(1+x^2));
    hence thesis;
    end;
    hence thesis by A3,A10,FDIFF_1:28,Lm3;
end;

theorem Th55:
  Z c= dom ((id Z)^(#)arccot) & Z c= ]. -1,1 .[
  implies (-(id Z)^(#)arccot) is_differentiable_on Z &
  for x st x in Z holds
  ((-(id Z)^(#)arccot)`|Z).x = arccot.x/(x^2)+1/(x*(1+x^2))
proof
   set f = id Z;
   assume that
A1:Z c= dom (f^(#)arccot) and
A2: Z c= ]. -1,1 .[;
A3:Z c= dom (-f^(#)arccot) by A1,VALUED_1:8;
A4:for x st x in Z holds f.x=x by FUNCT_1:35;
   Z c= dom (f^) /\ dom arccot by A1,VALUED_1:def 4;then
A5:Z c= dom (f^) by XBOOLE_1:18;
A6:not 0 in Z
   proof
     assume A7: 0 in Z;
     dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 8
       .= dom id Z \ {0} by Lm1,A7; then
     not 0 in {0} by XBOOLE_0:def 5,A7,A5;
     hence thesis by TARSKI:def 1;
   end; then
A8:f^ is_differentiable_on Z & for x st x in Z holds
     ((f^)`|Z).x = -1/x^2 by FDIFF_5:4;
A9:arccot is_differentiable_on Z by A2,SIN_COS9:82;
A10:(f^(#)arccot) is_differentiable_on Z by A6,A1,A2,SIN_COS9:130;
then A11:(-1)(#)(f^(#)arccot) is_differentiable_on Z by A3,FDIFF_1:28,Lm3;
   for x st x in Z holds ((-f^(#)arccot)`|Z).x = arccot.x/(x^2)+1/(x*(1+x^2))
   proof
     let x;
     assume
A12:  x in Z;
then A13: (f^(#)arccot) is_differentiable_in x by A10,FDIFF_1:16;
A14: f^ is_differentiable_in x by A8,A12,FDIFF_1:16;
A15: arccot is_differentiable_in x by A9,A12,FDIFF_1:16;
     ((-f^(#)arccot)`|Z).x=diff(-f^(#)arccot,x) by A11,A12,FDIFF_1:def 8
                     .=(-1)*(diff(f^(#)arccot,x)) by A13,FDIFF_1:23,Lm3
                     .=(-1)*((arccot.x)*diff(f^,x)+((f^).x)*diff(arccot,x))
      by A14,A15,FDIFF_1:24
                    .=(-1)*((arccot.x)*((f^)`|Z).x+((f^).x)*diff(arccot,x))
      by A8,A12,FDIFF_1:def 8
                    .=(-1)*((arccot.x)*(-1/x^2)+((f^).x)*diff(arccot,x))
      by A12,FDIFF_5:4,A6
                    .=(-1)*(-(arccot.x)*(1/x^2)+((f^).x)*((arccot)`|Z).x)
      by A9,A12,FDIFF_1:def 8
                    .=(-1)*(-(arccot.x)*(1/x^2)+((f^).x)*(-1/(1+x^2)))
      by A2,A12,SIN_COS9:82
                    .=(-1)*(-((arccot.x)*1)/(x^2)-((f^).x)*(1/(1+x^2)))
                    .=(-1)*(-arccot.x/(x^2)-(f.x)"*(1/(1+x^2)))
      by A5,A12,RFUNCT_1:def 8
                    .=(-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:77
                    .=arccot.x/(x^2)+1/(x*(1+x^2));
     hence thesis;
    end;
    hence thesis by A11;
end;

::f.x=arctan.x/(x^2)-1/(x*(1+x^2))

theorem
 A c= Z & (for x 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)
proof
   assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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:11;then
Z c= dom ((id Z)(#)(f1+#Z 2)) by XBOOLE_1:1,A6;
   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 st x in Z holds f.x=arctan.x/(x^2)-1/(x*(1+x^2))
   proof
   let x;
   assume
A9:x in Z;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 VALUED_1:13,A1,A9
.=(arctan/( #Z 2)).x-1/(((id Z)(#)(f1+#Z 2)).x) by RFUNCT_1:def 8,A10
.=(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 VALUED_1:def 1,A7,A9
.=(arctan/( #Z 2)).x-1/(x*(f1.x+( #Z 2).x)) by FUNCT_1:35,A9
.=(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 RFUNCT_1:def 4,A9,A5
.=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 thesis by A1;
   end;
A11:for x st x in dom((-(id Z)^(#)arctan)`|Z) holds
   ((-(id Z)^(#)arctan)`|Z).x=f.x
   proof
     let x;
     assume x in dom((-(id Z)^(#)arctan)`|Z);then
A12:  x in Z by A3,FDIFF_1:def 8;then
     ((-(id Z)^(#)arctan)`|Z).x=arctan.x/(x^2)-1/(x*(1+x^2)) by A1,Th54
       .=f.x by A8,A12;
     hence thesis;
   end;
   dom((-(id Z)^(#)arctan)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
   then((-(id Z)^(#)arctan)`|Z)= f by A11,PARTFUN1:34;
   hence thesis by A1,A2,A3,INTEGRA5:13;
end;

::f.x=arccot.x/(x^2)+1/(x*(1+x^2))

theorem
 A c= Z & (for x 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)
proof
   assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,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:11;then
Z c= dom ((id Z)(#)(f1+#Z 2)) by XBOOLE_1:1,A6;
   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 st x in Z holds f.x=arccot.x/(x^2)+1/(x*(1+x^2))
   proof
   let x;
   assume
A9:x in Z;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 VALUED_1:def 1,A1,A9
.=(arccot/( #Z 2)).x+1/(((id Z)(#)(f1+#Z 2)).x) by RFUNCT_1:def 8,A10
.=(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 VALUED_1:def 1,A7,A9
.=(arccot/( #Z 2)).x+1/(x*(f1.x+( #Z 2).x)) by FUNCT_1:35,A9
.=(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 RFUNCT_1:def 4,A9,A5
.=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 thesis by A1;
   end;
A11:for x st x in dom((-(id Z)^(#)arccot)`|Z) holds
   ((-(id Z)^(#)arccot)`|Z).x=f.x
   proof
     let x;
     assume x in dom((-(id Z)^(#)arccot)`|Z);then
A12:x in Z by A3,FDIFF_1:def 8;then
     ((-(id Z)^(#)arccot)`|Z).x=arccot.x/(x^2)+1/(x*(1+x^2)) by A1,Th55
      .=f.x by A12,A8;
     hence thesis;
   end;
   dom((-(id Z)^(#)arccot)`|Z)=dom f by A1,A3,FDIFF_1:def 8;
   then((-(id Z)^(#)arccot)`|Z)= f by A11,PARTFUN1:34;
   hence thesis by A1,A2,Th55,INTEGRA5:13;
end;