:: Several Integrability Formulas of Special Functions -- Part {II}
::  by Bo Li , Yanping Zhuang , Yanhong Men and Xiquan Liang
::
:: Received October 14, 2008
:: Copyright (c) 2008-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies REAL_1, SUBSET_1, NUMBERS, INTEGRA1, RCOMP_1, RELAT_1, JGRAPH_2,
      ARYTM_3, CARD_1, SIN_COS, VALUED_1, ARYTM_1, FDIFF_1, FUNCT_1, SQUARE_1,
      PREPOWER, SIN_COS2, ORDINAL2, XXREAL_2, XXREAL_1, INTEGRA5, XBOOLE_0,
      PARTFUN1, TARSKI, ORDINAL4, SIN_COS4, SIN_COS9, XXREAL_0, TAYLOR_1,
      SIN_COS6, SEQ_4, MEASURE5;
 notations TARSKI, XBOOLE_0, FUNCT_1, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS,
      RELAT_1, VALUED_1, XXREAL_0, XCMPLX_0, REAL_1, XREAL_0, PARTFUN1,
      PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, FCONT_1, SQUARE_1, INTEGRA5,
      PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2, SIN_COS2, FDIFF_9, SIN_COS4,
      SIN_COS6, SIN_COS9, SEQ_4;
 constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER,
      INTEGRA5, SIN_COS2, SEQ_4, SIN_COS9, PARTFUN2, SIN_COS6, RFUNCT_1,
      FDIFF_9, SIN_COS4, RELSET_1, INTEGRA1, COMSEQ_2, COMPLEX1, SERIES_1,
      BINOP_2;
 registrations VALUED_1, NAT_1, NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1,
      ORDINAL1, FUNCT_2, RCOMP_1, FCONT_1, TOPREALB, FCONT_3, MEASURE5,
      XREAL_0, SIN_COS, PREPOWER, SQUARE_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 equalities SIN_COS, VALUED_1, SUBSET_1, SQUARE_1, SIN_COS4, FDIFF_9, XBOOLE_0;
 theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, FUNCT_2, SQUARE_1, XCMPLX_1,
      INTEGRA5, INTEGRA8, SIN_COS, FDIFF_4, TAYLOR_1, VALUED_1, FCONT_1,
      SIN_COS5, SIN_COS4, SIN_COS2, SIN_COS6, XXREAL_1, XBOOLE_1, FDIFF_5,
      FDIFF_7, FDIFF_8, FDIFF_9, SIN_COS9, PREPOWER, FDIFF_6, XREAL_0;

begin :: Differentiation Formulas

reserve r,x,x0,a,b for Real;
reserve n,m for Element of NAT;
reserve A for non empty closed_interval Subset of REAL;
reserve Z for open Subset of REAL;

Lm1: [#]REAL = dom (AffineMap(1/2,0)) by FUNCT_2:def 1;

Lm2: [#]REAL = dom (sin*AffineMap(2,0)) by FUNCT_2:def 1;

Lm3: dom ((1/4)(#)(sin*AffineMap(2,0)))=[#]REAL by FUNCT_2:def 1;

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

theorem Th1:
  AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))
  is_differentiable_on REAL & for x holds ((AffineMap(1/2,0)-(1/4)(#)(sin*
  AffineMap(2,0)))`|REAL).x = (sin.x)^2
proof
A1: for x st x in REAL holds AffineMap(2,0).x=2*x + 0 by FCONT_1:def 4;
  then
A2: sin*AffineMap(2,0) is_differentiable_on REAL by Lm2,FDIFF_4:37;
  then
A3: (1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL by Lm3,FDIFF_1:20;
A4: dom (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))) = [#]REAL by
FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(1/2,0).x=(1/2)*x + 0 by FCONT_1:def 4;
  then
A6: AffineMap(1/2,0) is_differentiable_on REAL by Lm1,FDIFF_1:23;
  hence AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))
  is_differentiable_on REAL by A4,A3,FDIFF_1:19;
A7: for x st x in REAL holds (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/2)
  *cos(2*x)
  proof
    let x;
    assume
A8: x in REAL;
    (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/4)*diff((sin*AffineMap(2,
    0)),x) by A2,Lm3,FDIFF_1:20,A8
      .=(1/4)*((sin*AffineMap(2,0))`|REAL).x by A2,FDIFF_1:def 7,A8
      .=(1/4)*(2*cos.(2*x+0)) by A1,Lm2,FDIFF_4:37,A8
      .=(1/2)*cos(2*x);
    hence thesis;
  end;
A9:
  for x st x in REAL holds ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))
  )`|REAL).x = (sin.x)^2
  proof
    let x;
    assume
A10: x in REAL;
    ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =diff(
AffineMap(1/2,0),x) - diff((1/4)(#)(sin*AffineMap(2,0)),x) by A4,A6,A3,
FDIFF_1:19,A10
      .=((AffineMap(1/2,0))`|REAL).x -diff((1/4)(#)(sin*AffineMap(2,0)),x)
    by A6,FDIFF_1:def 7,A10
      .=(1/2)-diff((1/4)(#)(sin*AffineMap(2,0)),x) by A5,Lm1,FDIFF_1:23,A10
      .=(1/2)-(((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x by A3,FDIFF_1:def 7,A10
      .=(1/2)-(1/2)*cos(2*x) by A7,A10
      .=(1-cos(2*x))/2
      .=(sin(x))^2 by SIN_COS5:20;
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A9;
end;

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

theorem Th2:
  AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))
  is_differentiable_on REAL & for x holds ((AffineMap(1/2,0)+(1/4)(#)(sin*
  AffineMap(2,0)))`|REAL).x = (cos.x)^2
proof
A1: for x st x in REAL holds AffineMap(2,0).x=2*x + 0 by FCONT_1:def 4;
  then
A2: sin*AffineMap(2,0) is_differentiable_on REAL by Lm2,FDIFF_4:37;
  then
A3: (1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL by Lm3,FDIFF_1:20;
A4: dom (AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))) = [#]REAL by
FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(1/2,0).x=(1/2)*x + 0 by FCONT_1:def 4;
  then
A6: AffineMap(1/2,0) is_differentiable_on REAL by Lm1,FDIFF_1:23;
  hence AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))
  is_differentiable_on REAL by A4,A3,FDIFF_1:18;
A7: for x st x in REAL holds (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/2)
  *cos(2*x)
  proof
    let x;
    assume
A8:  x in REAL;
    (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/4)*diff((sin*AffineMap(2,
    0)),x) by A2,Lm3,FDIFF_1:20,A8
      .=(1/4)*((sin*AffineMap(2,0))`|REAL).x by A2,FDIFF_1:def 7,A8
      .=(1/4)*(2*cos.(2*x+0)) by A1,Lm2,FDIFF_4:37,A8
      .=(1/2)*cos(2*x);
    hence thesis;
  end;
A9:
  for x st x in REAL holds ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))
  )`|REAL).x = (cos.x)^2
  proof
    let x;
    assume
A10: x in REAL;
    ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =diff(
AffineMap(1/2,0),x) + diff((1/4)(#)(sin*AffineMap(2,0)),x) by A4,A6,A3,
FDIFF_1:18,A10
      .=((AffineMap(1/2,0))`|REAL).x +diff((1/4)(#)(sin*AffineMap(2,0)),x)
    by A6,FDIFF_1:def 7,A10
      .=(1/2)+diff((1/4)(#)(sin*AffineMap(2,0)),x) by A5,Lm1,FDIFF_1:23,A10
      .=(1/2)+(((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x by A3,FDIFF_1:def 7,A10
      .=(1/2)+(1/2)*cos(2*x) by A7,A10
      .=(1+cos(2*x))/2
      .=(cos(x))^2 by SIN_COS5:21;
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A9;
end;

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

theorem Th3:
  (1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL & for x
  holds (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x = ((sin.x) #Z n)*cos.x
proof
A1: [#]REAL = dom((1/(n+1))(#)( #Z (n+1)*sin)) by FUNCT_2:def 1;
  #Z (n+1)*sin is_differentiable_in x0
  proof
    sin is_differentiable_in x0 by SIN_COS:64;
    hence thesis by TAYLOR_1:3;
  end;
  then
  [#]REAL = dom ( #Z (n+1)*sin) & for x0 st x0 in REAL holds #Z (n+1)*sin
  is_differentiable_in x0 by FUNCT_2:def 1;
  then
A2: #Z (n+1)*sin is_differentiable_on REAL by FDIFF_1:9;
  hence (1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL by A1,FDIFF_1:20;
A3: for x st x in REAL holds (( #Z (n+1)*sin)`|REAL).x=(n+1) * ((sin.x) #Z n
  )*cos.x
  proof
    set m=n+1;
    let x;
    assume
A4: x in REAL;
    sin is_differentiable_in x by SIN_COS:64;
    then diff(( #Z m*sin),x) = m * (sin.x) #Z (m-1) *diff(sin,x) by TAYLOR_1:3
      .= m * (sin.x) #Z (m-1) *(cos .x) by SIN_COS:64;
    hence thesis by A2,FDIFF_1:def 7,A4;
  end;
A5:
  for x st x in REAL holds (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x =(sin.x
  ) #Z n *cos.x
  proof
    let x;
    assume
A6: x in REAL;
    (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x =(1/(n+1))*diff( #Z (n+1)*sin
    ,x) by A1,A2,FDIFF_1:20,A6
      .=(1/(n+1))*((( #Z (n+1)*sin)`|REAL).x) by A2,FDIFF_1:def 7,A6
      .=(1/(n+1))*((n+1) * (sin.x) #Z n *cos.x) by A3,A6
      .=(1/(n+1))*(n+1) * (sin.x) #Z n *cos.x
      .=(n+1)/(n+1) * (sin.x) #Z n *cos.x by XCMPLX_1:99
      .=1*(sin.x) #Z n *cos.x by XCMPLX_1:60;
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A5;
end;

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

theorem Th4:
  (-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL & for x
  holds (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x = ((cos.x) #Z n)*sin.x
proof
A1: [#]REAL = dom((-1/(n+1))(#)( #Z (n+1)*cos)) by FUNCT_2:def 1;
  #Z (n+1)*cos is_differentiable_in x0
  proof
    cos is_differentiable_in x0 by SIN_COS:63;
    hence thesis by TAYLOR_1:3;
  end;
  then
A2: for x0 st x0 in REAL holds #Z (n+1)*cos is_differentiable_in x0;
  [#]REAL = dom ( #Z (n+1)) & REAL = dom ( #Z (n+1)*cos) by FUNCT_2:def 1;
  then
A3: #Z (n+1)*cos is_differentiable_on REAL by A2,FDIFF_1:9;
 hence(-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL by A1,FDIFF_1:20;
A4: for x st x in REAL holds (( #Z (n+1)*cos)`|REAL).x=(-(n+1)) * ((cos.x)
  #Z n)*sin.x
  proof
    set m=n+1;
    let x;
    assume
A5:x in REAL;
    cos is_differentiable_in x by SIN_COS:63;
    then diff(( #Z m*cos),x) = m * (cos.x) #Z (m-1) *diff(cos,x) by TAYLOR_1:3
      .= m * (cos.x) #Z (m-1) *(-sin .x) by SIN_COS:63
      .= (-m) * (cos.x) #Z (m-1) *sin .x;
    hence thesis by A3,FDIFF_1:def 7,A5;
  end;
A6:
  for x st x in REAL holds (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x =(cos
  .x) #Z n *sin.x
  proof
    let x;
    assume
A7:x in REAL;
    (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x =(-1/(n+1))*diff( #Z (n+1)*
    cos,x) by A1,A3,FDIFF_1:20,A7
      .=(-1/(n+1))*((( #Z (n+1)*cos)`|REAL).x) by A3,FDIFF_1:def 7,A7
      .=(-1/(n+1))*((-(n+1)) * (cos.x) #Z n *sin.x) by A4,A7
      .=(1/(n+1))*(n+1) * (cos.x) #Z n *sin.x
      .=(n+1)/(n+1) * (cos.x) #Z n *sin.x by XCMPLX_1:99
      .=1*(cos.x) #Z n *sin.x by XCMPLX_1:60;
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A6;
end;

:: f.x=sin.((m+n)*x)/(2*(m+n))+sin.((m-n)*x)/(2*(m-n))

theorem Th5:
  m+n<>0 & m-n<>0 implies ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+
(1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) is_differentiable_on REAL & for x holds
(((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)
  ))`|REAL).x = cos.(m*x) *cos.(n*x)
proof
  assume that
A1: m+n <> 0 and
A2: m-n<>0;
A3: dom (sin*AffineMap(m-n,0)) = [#]REAL & for x st x in REAL holds
  AffineMap(m- n,0).x=(m-n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A4: sin*AffineMap(m-n,0) is_differentiable_on REAL by FDIFF_4:37;
A5: dom ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1;
  then
A6: (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)) is_differentiable_on REAL by A4,
FDIFF_1:20;
A7: for x st x in REAL holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|
  REAL).x=(1/2)*cos((m-n)*x)
  proof
    let x;
    assume
A8: x in REAL;
    (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x =(1/(2*(m-n)))*
    diff((sin*AffineMap(m-n,0)),x) by A5,A4,FDIFF_1:20,A8
      .=(1/(2*(m-n)))*((sin*AffineMap(m-n,0))`|REAL).x by A4,FDIFF_1:def 7,A8
      .=(1/(2*(m-n)))*((m-n)* cos.((m-n)*x+0)) by A3,FDIFF_4:37,A8
      .=(m-n)*(1/(2*(m-n)))* cos.((m-n)*x+0)
      .=((1*(m-n))/(2*(m-n)))* cos.((m-n)*x+0) by XCMPLX_1:74
      .=(1/2)* cos((m-n)*x) by A2,XCMPLX_1:91;
    hence thesis;
  end;
A9: dom ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
  AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1;
A10: dom (sin*AffineMap(m+n,0)) = [#]REAL & for x st x in REAL holds
  AffineMap(m+ n,0).x=(m+n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A11: sin*AffineMap(m+n,0) is_differentiable_on REAL by FDIFF_4:37;
A12: [#]REAL = dom ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) by FUNCT_2:def 1;
  then
A13: (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)) is_differentiable_on REAL by A11,
FDIFF_1:20;
  hence((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+
(1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) is_differentiable_on REAL
        by A9,A6,FDIFF_1:18;
A14: for x st x in REAL holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL
  ).x=(1/2)*cos((m+n)*x)
  proof
    let x;
    assume
A15: x in REAL;
    (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x =(1/(2*(m+n)))*
    diff((sin*AffineMap(m+n,0)),x) by A12,A11,FDIFF_1:20,A15
      .=(1/(2*(m+n)))*((sin*AffineMap(m+n,0))`|REAL).x by A11,FDIFF_1:def 7,A15
      .=(1/(2*(m+n)))*((m+n)* cos.((m+n)*x+0)) by A10,FDIFF_4:37,A15
      .=(m+n)*(1/(2*(m+n)))* cos.((m+n)*x+0)
      .=((1*(m+n))/(2*(m+n)))* cos.((m+n)*x+0) by XCMPLX_1:74
      .=(1/2)* cos((m+n)*x) by A1,XCMPLX_1:91;
    hence thesis;
  end;
A16:
  for x st x in REAL holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(
  2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x = cos.(m*x) *cos.(n*x)
  proof
    let x;
    assume
A17: x in REAL;
    (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0)))`|REAL).x = diff((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)),x) +
    diff((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)),x) by A9,A13,A6,FDIFF_1:18,A17
      .= (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x +diff((1/(2*(m-n
    )))(#)(sin*AffineMap(m-n,0)),x) by A13,FDIFF_1:def 7,A17
      .= (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x +(((1/(2*(m-n)))
    (#)(sin*AffineMap(m-n,0)))`|REAL).x by A6,FDIFF_1:def 7,A17
      .= (1/2)*cos((m+n)*x)+(((1/(2*(m-n))) (#)(sin*AffineMap(m-n,0)))`|REAL
    ).x by A14,A17
      .= (1/2)*cos((m+n)*x)+(1/2)* cos((m-n)*x) by A7,A17
      .= (1/2)*(cos((m+n)*x)+cos((m-n)*x))
      .= (1/2)*(2*(cos(((m+n)*x+(m-n)*x)/2) *cos(((m+n)*x-(m-n)*x)/2))) by
SIN_COS4:17
      .= cos.(m*x)*cos.(n*x);
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A16;
end;

:: f.x=sin.((m-n)*x)/(2*(m-n))-sin.((m+n)*x)/(2*(m+n))

theorem Th6:
  m+n<>0 & m-n<>0 implies ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))-
(1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) is_differentiable_on REAL & for x holds
(((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)
  ))`|REAL).x = sin.(m*x)*sin.(n*x)
proof
  assume that
A1: m+n <> 0 and
A2: m-n <> 0;
A3: dom ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1;
A4: dom (sin*AffineMap(m-n,0)) = [#]REAL & for x st x in REAL holds
  AffineMap(m- n,0).x=(m-n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A5: sin*AffineMap(m-n,0) is_differentiable_on REAL by FDIFF_4:37;
  then
A6: (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)) is_differentiable_on REAL by A3,
FDIFF_1:20;
A7: for x st x in REAL holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|
  REAL).x=(1/2)*cos((m-n)*x)
  proof
    let x;
    assume
A8: x in REAL;
    (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x =(1/(2*(m-n)))*
    diff((sin*AffineMap(m-n,0)),x) by A3,A5,FDIFF_1:20,A8
      .=(1/(2*(m-n)))*((sin*AffineMap(m-n,0))`|REAL).x by A5,FDIFF_1:def 7,A8
      .=(1/(2*(m-n)))*((m-n)* cos.((m-n)*x+0)) by A4,FDIFF_4:37,A8
      .=(m-n)*(1/(2*(m-n)))* cos.((m-n)*x+0)
      .=((1*(m-n))/(2*(m-n)))* cos.((m-n)*x+0) by XCMPLX_1:74
      .=(1/2)* cos((m-n)*x) by A2,XCMPLX_1:91;
    hence thesis;
  end;
A9: dom ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
  AffineMap(m+n,0))) = [#]REAL by FUNCT_2:def 1;
A10: dom (sin*AffineMap(m+n,0)) = [#]REAL & for x st x in REAL holds
  AffineMap(m+ n,0).x=(m+n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A11: sin*AffineMap(m+n,0) is_differentiable_on REAL by FDIFF_4:37;
A12: REAL = dom ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) by FUNCT_2:def 1;
  then
A13: (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)) is_differentiable_on REAL by A3,A11
,FDIFF_1:20;
 hence ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))-
(1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) is_differentiable_on REAL
    by A9,A6,FDIFF_1:19;
A14: for x st x in REAL holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL
  ).x=(1/2)*cos((m+n)*x)
  proof
    let x;
    assume
A15: x in REAL;
    (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x =(1/(2*(m+n)))*
    diff((sin*AffineMap(m+n,0)),x) by A12,A3,A11,FDIFF_1:20,A15
      .=(1/(2*(m+n)))*((sin*AffineMap(m+n,0))`|REAL).x by A11,FDIFF_1:def 7,A15
      .=(1/(2*(m+n)))*((m+n)* cos.((m+n)*x+0)) by A10,FDIFF_4:37,A15
      .=(m+n)*(1/(2*(m+n)))* cos.((m+n)*x+0)
      .=((1*(m+n))/(2*(m+n)))* cos.((m+n)*x+0) by XCMPLX_1:74
      .=(1/2)* cos((m+n)*x) by A1,XCMPLX_1:91;
    hence thesis;
  end;
A16:
  for x st x in REAL holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(
  2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x = sin.(m*x) *sin.(n*x)
  proof
    let x;
    assume
A17: x in REAL;
    (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0)))`|REAL).x = diff((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)),x) -
    diff((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)),x) by A9,A13,A6,FDIFF_1:19,A17
      .= (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x -diff((1/(2*(m+n
    )))(#)(sin*AffineMap(m+n,0)),x) by A6,FDIFF_1:def 7,A17
      .= (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x -(((1/(2*(m+n)))
    (#)(sin*AffineMap(m+n,0)))`|REAL).x by A13,FDIFF_1:def 7,A17
      .= (1/2)*cos((m-n)*x)-(((1/(2*(m+n))) (#)(sin*AffineMap(m+n,0)))`|REAL
    ).x by A7,A17
      .= (1/2)*cos((m-n)*x)-(1/2)* cos((m+n)*x) by A14,A17
      .= (1/2)*(cos((m-n)*x)-cos((m+n)*x))
      .= (1/2)*(-2*(sin(((m-n)*x+(m+n)*x)/2) *sin(((m-n)*x-(m+n)*x)/2))) by
SIN_COS4:18
      .= (1/2)*(-2*(sin(m*x)*sin(-(n*x))))
      .= (1/2)*(-2*(sin(m*x)*(-sin(n*x)))) by SIN_COS:31
      .= sin.(m*x)*sin.(n*x);
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A16;
end;

:: f.x=-cos.((m+n)*x)/(2*(m+n))-cos.((m-n)*x)/(2*(m-n))

theorem Th7:
  m+n<>0 & m-n<>0 implies ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))
  ) - (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) is_differentiable_on REAL & for x
  holds ((-((1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
  AffineMap(m-n,0)))`|REAL).x = sin.(m*x) * cos.(n*x)
proof
  assume that
A1: m+n <> 0 and
A2: m-n <> 0;
A3: dom (cos*AffineMap(m+n,0)) = [#]REAL & for x st x in REAL holds
  AffineMap(m+ n,0).x=(m+n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A4: cos*AffineMap(m+n,0) is_differentiable_on REAL by FDIFF_4:38;
A5: for x st x in REAL holds ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|
  REAL).x=(1/2)*sin((m+n)*x)
  proof
    let x;
    assume
A6: x in REAL;
A7: dom (((-1)/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))=[#]REAL by FUNCT_2:def 1;
    ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x =((((-1)*(1/(2*(m
    +n)))) (#)(cos*AffineMap(m+n,0)))`|REAL).x by RFUNCT_1:17
      .=(((-(1/(2*(m+n))))(#)(cos*AffineMap(m+n,0)))`|REAL).x
      .=((((-1)/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x by XCMPLX_1:187
      .=((-1)/(2*(m+n)))*diff((cos*AffineMap(m+n,0)),x) by A4,A7,FDIFF_1:20,A6
      .=((-1)/(2*(m+n)))*((cos*AffineMap(m+n,0))`|REAL).x by A4,FDIFF_1:def 7,
A6
      .=((-1)/(2*(m+n)))*(-(m+n)* sin.((m+n)*x+0)) by A3,FDIFF_4:38,A6
      .=(-(-1)/(2*(m+n)))*(m+n)* sin.((m+n)*x+0)
      .=(1/(2*(m+n)))*(m+n)* sin.((m+n)*x+0) by XCMPLX_1:190
      .=((1*(m+n))/(2*(m+n)))* sin.((m+n)*x+0) by XCMPLX_1:74
      .=(1/2)* sin((m+n)*x) by A1,XCMPLX_1:91;
    hence thesis;
  end;
A8: dom (-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) = [#]REAL by FUNCT_2:def 1;
  dom ((1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) = [#]REAL by FUNCT_2:def 1;
  then (-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) = (-1)(#) ((1/(2*(m+n)))(#)(
  cos* AffineMap(m+n,0))) & (1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))
  is_differentiable_on REAL by A4,FDIFF_1:20;
  then
A9: (-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) is_differentiable_on REAL by A8,
FDIFF_1:20;
A10: REAL = dom ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(
  cos*AffineMap(m-n,0))) by FUNCT_2:def 1;
A11: dom (cos*AffineMap(m-n,0)) = [#]REAL & for x st x in REAL holds
  AffineMap(m- n,0).x=(m-n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A12: cos*(AffineMap(m-n,0)) is_differentiable_on REAL by FDIFF_4:38;
A13: dom ((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1;
  then
A14: (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)) is_differentiable_on REAL by A12,
FDIFF_1:20;
 hence ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))
  ) - (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) is_differentiable_on REAL
 by A8,A10,A9,FDIFF_1:19;
A15: for x st x in REAL holds (((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|
  REAL).x=-(1/2)*sin((m-n)*x)
  proof
    let x;
    assume
A16: x in REAL;
    (((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|REAL).x =(1/(2*(m-n)))*
    diff((cos*AffineMap(m-n,0)),x) by A13,A12,FDIFF_1:20,A16
      .=(1/(2*(m-n)))*((cos*AffineMap(m-n,0))`|REAL).x by A12,FDIFF_1:def 7,A16
      .=(1/(2*(m-n)))*(-(m-n)* sin.((m-n)*x+0)) by A11,FDIFF_4:38,A16
      .=(-1/(2*(m-n)))*(m-n)* sin.((m-n)*x+0)
      .=((-1)/(2*(m-n)))*(m-n)* sin.((m-n)*x+0) by XCMPLX_1:187
      .=(((-1)*(m-n))/(2*(m-n)))* sin.((m-n)*x+0) by XCMPLX_1:74
      .=(-1)/2* sin((m-n)*x) by A2,XCMPLX_1:91;
    hence thesis;
  end;
A17:
  for x st x in REAL holds ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))- (1/
  (2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|REAL).x = sin.(m*x) *cos.(n*x)
  proof
    let x;
    assume
A18: x in REAL;
    ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0)))`|REAL).x = diff((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))),x)
    -diff((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)),x)
         by A8,A10,A9,A14,FDIFF_1:19,A18
      .= ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x -diff((1/(2*(m-
    n)))(#)(cos*AffineMap(m-n,0)),x) by A9,FDIFF_1:def 7,A18
      .= ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x -(((1/(2*(m-n))
    )(#)(cos*AffineMap(m-n,0)))`|REAL).x by A14,FDIFF_1:def 7,A18
      .= (1/2)*sin((m+n)*x)-(((1/(2*(m-n))) (#)(cos*AffineMap(m-n,0)))`|REAL
    ).x by A5,A18
      .= (1/2)*sin((m+n)*x)-(-(1/2)* sin((m-n)*x)) by A15,A18
      .= (1/2)*(sin((m+n)*x)+sin((m-n)*x))
      .= (1/2)*(2*(cos(((m+n)*x-(m-n)*x)/2) *sin(((m+n)*x+(m-n)*x)/2))) by
SIN_COS4:15
      .= sin.(m*x)*cos.(n*x);
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A17;
end;

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

theorem Th8:
  n<>0 implies ((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0)
  )(#)(cos*AffineMap(n,0))) is_differentiable_on REAL & for x holds (((1/(n^2))
(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x=x*
  sin.(n*x)
proof
A1: dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*
  AffineMap(n,0)))) = [#]REAL by FUNCT_2:def 1;
A2: dom (AffineMap(1/n,0))=REAL & for x st x in REAL holds AffineMap(1/n,0)
  .x=(1 /n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A3: AffineMap(1/n,0) is_differentiable_on REAL by A1,FDIFF_1:23;
A4: for x st x in REAL holds AffineMap(n,0).x=n*x + 0 by FCONT_1:def 4;
A5: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
  then
A6: sin*(AffineMap(n,0)) is_differentiable_on REAL by A4,FDIFF_4:37;
A7: dom ((1/(n^2))(#)(sin*AffineMap(n,0)))=REAL by FUNCT_2:def 1;
  then
A8: (1/(n^2))(#)(sin*AffineMap(n,0)) is_differentiable_on REAL by A1,A6,
FDIFF_1:20;
  assume
A9: n<>0;
A10: for x st x in REAL holds (((1/(n^2))(#)(sin*AffineMap(n,0)))`|REAL).x =
  (1/n)*cos(n*x)
  proof
    let x;
    assume
A11: x in REAL;
    (((1/(n^2))(#)(sin*AffineMap(n,0)))`|REAL).x =(1/(n^2))*diff((sin*
    AffineMap(n,0)),x) by A7,A1,A6,FDIFF_1:20,A11
      .=(1/(n^2))*((sin*AffineMap(n,0))`|REAL).x by A6,FDIFF_1:def 7,A11
      .=(1/(n^2))*(n * cos.(n*x+0)) by A5,A4,FDIFF_4:37,A11
      .= n*(1/(n*n))*(cos.(n*x+0))
      .= (n*1)/(n*n)*(cos.(n*x+0)) by XCMPLX_1:74
      .= (1/n)*(cos.(n*x+0)) by A9,XCMPLX_1:91;
    hence thesis;
  end;
A12: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
  then
A13: cos*AffineMap(n,0) is_differentiable_on REAL by A4,FDIFF_4:38;
A14: dom ((AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))=REAL by FUNCT_2:def 1;
  then
A15: ((AffineMap(1/n,0))(#)(cos*AffineMap(n,0))) is_differentiable_on REAL
  by A1,A3,A13,FDIFF_1:21;
 hence ((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0)
  )(#)(cos*AffineMap(n,0))) is_differentiable_on REAL
 by A1,A8,FDIFF_1:19;
A16: for x st x in REAL holds (((AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|
  REAL).x = (1/n)*cos.(n*x)-x* sin.(n*x)
  proof
    let x;
    assume
A17: x in REAL;
    (((AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x = ((cos*
AffineMap(n,0)).x)*diff(AffineMap(1/n,0),x) + (AffineMap(1/n,0).x)*diff(cos*(
    AffineMap(n,0)),x) by A14,A1,A3,A13,FDIFF_1:21,A17
      .= ((cos*AffineMap(n,0)).x)*((AffineMap(1/n,0)`|REAL).x) +(AffineMap(1
    /n,0).x)*diff((cos*AffineMap(n,0)),x) by A3,FDIFF_1:def 7,A17
      .= ((cos*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *diff((cos*
    AffineMap(n,0)),x) by A1,A2,FDIFF_1:23,A17
      .= ((cos*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *(((cos*
    AffineMap(n,0))`|REAL).x) by A13,FDIFF_1:def 7,A17
      .= ((cos*AffineMap(n,0)).x)*(1/n) +(AffineMap(1/n,0).x)*(-n* sin.(n*x+
    0)) by A12,A4,FDIFF_4:38,A17
      .= ((cos*AffineMap(n,0)).x)*(1/n) +((1/n)*x + 0)*(-n* sin.(n*x+0)) by
FCONT_1:def 4
      .= (cos.(AffineMap(n,0).x))*(1/n) +((1/n)*x)*(-n* sin.(n*x+0)) by A12,
FUNCT_1:12,A17
      .= (1/n)*cos.(n*x)+(-((1/n)*n*x* sin.(n*x))) by FCONT_1:def 4
      .= (1/n)*cos.(n*x)+(-(1*x* sin.(n*x))) by A9,XCMPLX_1:87
      .= (1/n)*cos.(n*x)-x* sin.(n*x);
    hence thesis;
  end;
A18:
  for x st x in REAL holds (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap
  (1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x = x*sin.(n*x)
  proof
    let x;
    assume
A19: x in REAL;
    (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*
AffineMap(n,0)))`|REAL).x = diff((1/(n^2))(#)(sin*AffineMap(n,0)),x) - diff((
    AffineMap(1/n,0))(#)(cos*AffineMap(n,0)),x) by A1,A8,A15,FDIFF_1:19,A19
      .= ((((1/(n^2))(#)(sin*AffineMap(n,0)))`|REAL).x) - diff(AffineMap(1/n
    ,0)(#)(cos*AffineMap(n,0)),x) by A8,FDIFF_1:def 7,A19
      .= (1/n)*cos(n*x)-diff(AffineMap(1/n,0) (#)(cos*AffineMap(n,0)),x)
          by A10,A19
      .= (1/n)*cos(n*x)-(((AffineMap(1/n,0) (#)(cos*AffineMap(n,0)))`|REAL).
    x) by A15,FDIFF_1:def 7,A19
      .= (1/n)*cos(n*x)-((1/n)*cos.(n*x)-x* sin.(n*x)) by A16,A19
      .= x* sin.(n*x);
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A18;
end;

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

theorem Th9:
  n<>0 implies ((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0)
  )(#)(sin*AffineMap(n,0))) is_differentiable_on REAL & for x holds (((1/(n^2))
(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x=x*
  cos.(n*x)
proof
A1: dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*
  AffineMap(n,0)))) = [#]REAL by FUNCT_2:def 1;
A2: dom (AffineMap(1/n,0))=REAL & for x st x in REAL holds AffineMap(1/n,0)
  .x=(1 /n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A3: AffineMap(1/n,0) is_differentiable_on REAL by A1,FDIFF_1:23;
A4: for x st x in REAL holds AffineMap(n,0).x=n*x + 0 by FCONT_1:def 4;
A5: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
  then
A6: cos*AffineMap(n,0) is_differentiable_on REAL by A4,FDIFF_4:38;
A7: dom ((1/(n^2))(#)(cos*AffineMap(n,0)))=REAL by FUNCT_2:def 1;
  then
A8: (1/(n^2))(#)(cos*AffineMap(n,0)) is_differentiable_on REAL by A1,A6,
FDIFF_1:20;
  assume
A9: n<>0;
A10: for x st x in REAL holds (((1/(n^2))(#)(cos*AffineMap(n,0)))`|REAL).x =
  -(1/n)*sin(n*x)
  proof
    let x;
    assume
A11: x in REAL;
    (((1/(n^2))(#)(cos*AffineMap(n,0)))`|REAL).x =(1/(n^2))*diff((cos*
    AffineMap(n,0)),x) by A7,A1,A6,FDIFF_1:20,A11
      .=(1/(n^2))*((cos*AffineMap(n,0))`|REAL).x by A6,FDIFF_1:def 7,A11
      .=(1/(n^2))*(-n * sin.(n*x+0)) by A5,A4,FDIFF_4:38,A11
      .=(-1)*(n*(1/(n*n)))*(sin.(n*x+0))
      .=(-1)*(n/((n*n)/1))*(sin.(n*x+0)) by XCMPLX_1:79
      .=(-1)*((n*1)/(n*n))*(sin.(n*x+0))
      .=(-1)*(1/n)*(sin.(n*x+0)) by A9,XCMPLX_1:91;
    hence thesis;
  end;
A12: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
  then
A13: sin*AffineMap(n,0) is_differentiable_on REAL by A4,FDIFF_4:37;
A14: dom ((AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))=REAL by FUNCT_2:def 1;
  then
A15: ((AffineMap(1/n,0))(#)(sin*AffineMap(n,0))) is_differentiable_on REAL
  by A1,A3,A13,FDIFF_1:21;
 hence((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0)
  )(#)(sin*AffineMap(n,0))) is_differentiable_on REAL
 by A1,A8,FDIFF_1:18;
A16: for x st x in REAL holds (((AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|
  REAL).x = (1/n)*sin.(n*x)+x* cos.(n*x)
  proof
    let x;
    assume
A17: x in REAL;
    (((AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x = ((sin*
AffineMap(n,0)).x)*diff((AffineMap(1/n,0)),x) + ((AffineMap(1/n,0)).x)*diff((
    sin*AffineMap(n,0)),x) by A14,A1,A3,A13,FDIFF_1:21,A17
      .= ((sin*AffineMap(n,0)).x)*((AffineMap(1/n,0)`|REAL).x) +((AffineMap(
    1/n,0)).x)*diff((sin*AffineMap(n,0)),x) by A3,FDIFF_1:def 7,A17
      .= ((sin*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *diff((sin*
    AffineMap(n,0)),x) by A1,A2,FDIFF_1:23,A17
      .= ((sin*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *(((sin*
    AffineMap(n,0))`|REAL).x) by A13,FDIFF_1:def 7,A17
      .= ((sin*AffineMap(n,0)).x)*(1/n) +(AffineMap(1/n,0).x)*(n* cos.(n*x+0
    )) by A12,A4,FDIFF_4:37,A17
      .= ((sin*AffineMap(n,0)).x)*(1/n) +((1/n)*x + 0)*(n* cos.(n*x+0)) by
FCONT_1:def 4
      .= (sin.(AffineMap(n,0).x))*(1/n) +((1/n)*x)*(n* cos.(n*x+0)) by A12,
FUNCT_1:12,A17
      .= (1/n)*sin.(n*x)+(1/n)*n*x* cos.(n*x) by FCONT_1:def 4
      .= (1/n)*sin.(n*x)+1*x* cos.(n*x) by A9,XCMPLX_1:87
      .= (1/n)*sin.(n*x)+x* cos.(n*x);
    hence thesis;
  end;
A18:
  for x st x in REAL holds (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap
  (1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x = x*cos.(n*x)
  proof
    let x;
    assume
A19: x in REAL;
    (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*
AffineMap(n,0)))`|REAL).x = diff((1/(n^2))(#)(cos*AffineMap(n,0)),x) + diff((
    AffineMap(1/n,0))(#)(sin*AffineMap(n,0)),x) by A1,A8,A15,FDIFF_1:18,A19
      .= ((((1/(n^2))(#)(cos*AffineMap(n,0)))`|REAL).x) + diff((AffineMap(1/
    n,0))(#)(sin*AffineMap(n,0)),x) by A8,FDIFF_1:def 7,A19
      .= -(1/n)*sin(n*x)+diff(AffineMap(1/n,0) (#)(sin*AffineMap(n,0)),x) by
A10,A19
      .= -(1/n)*sin(n*x)+(((AffineMap(1/n,0) (#)(sin*AffineMap(n,0)))`|REAL)
    .x) by A15,FDIFF_1:def 7,A19
      .= -(1/n)*sin(n*x)+((1/n)*sin.(n*x)+x* cos.(n*x)) by A16,A19
      .= x* cos.(n*x);
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A18;
end;

:: f.x = x*cosh.x-sinh.x

theorem Th10:
  (AffineMap(1,0))(#)cosh-sinh is_differentiable_on REAL & for x
  holds (((AffineMap(1,0))(#)cosh-sinh)`|REAL).x=x*sinh.x
proof
A1: dom ((AffineMap(1,0))(#)cosh-sinh) = [#]REAL by FUNCT_2:def 1;
A2: dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0)
  .x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A3: AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23;
A4: dom ((AffineMap(1,0))(#)cosh) = [#]REAL by FUNCT_2:def 1;
  then
A5: ((AffineMap(1,0))(#)cosh) is_differentiable_on REAL by A3,FDIFF_1:21
,SIN_COS2:35;
 hence (AffineMap(1,0))(#)cosh-sinh is_differentiable_on REAL
 by A1,FDIFF_1:19,SIN_COS2:34;
A6: for x st x in REAL holds (((AffineMap(1,0))(#)cosh)`|REAL).x = cosh.x+x*
  sinh.x
  proof
    let x;
    assume
A7: x in REAL;
    (((AffineMap(1,0))(#)cosh)`|REAL).x = cosh.x*diff((AffineMap(1,0)),x)+
    ((AffineMap(1,0)).x) *diff(cosh,x) by A4,A3,FDIFF_1:21,SIN_COS2:35,A7
      .= cosh.x*(((AffineMap(1,0))`|REAL).x) +((AffineMap(1,0)).x)*diff(cosh
    ,x) by A3,FDIFF_1:def 7,A7
      .= cosh.x*1+((AffineMap(1,0)).x)*diff(cosh,x) by A2,FDIFF_1:23,A7
      .= cosh.x+((AffineMap(1,0)).x)*sinh.x by SIN_COS2:35
      .= cosh.x+(1*x + 0)*sinh.x by FCONT_1:def 4
      .= cosh.x+x*sinh.x;
    hence thesis;
  end;
A8:
  for x st x in REAL holds (((AffineMap(1,0))(#)cosh-sinh)`|REAL).x = x* sinh.x
  proof
    let x;
    assume
A9: x in REAL;
    (((AffineMap(1,0))(#)cosh - sinh)`|REAL).x = diff(((AffineMap(1,0))(#)
    cosh),x) - diff(sinh,x) by A1,A5,FDIFF_1:19,SIN_COS2:34,A9
      .= (((AffineMap(1,0))(#)cosh)`|REAL).x - diff(sinh,x)
by A5,FDIFF_1:def 7,A9
      .= cosh.x+x*sinh.x-diff(sinh,x) by A6,A9
      .= cosh.x+x*sinh.x-cosh.x by SIN_COS2:34
      .= x*sinh.x;
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A8;
end;

:: f.x = x*sinh.x-cosh.x

theorem Th11:
  (AffineMap(1,0))(#)sinh-cosh is_differentiable_on REAL & for x
  holds (((AffineMap(1,0))(#)sinh-cosh)`|REAL).x=x*cosh.x
proof
A1: dom ((AffineMap(1,0))(#)sinh-cosh) = [#]REAL by FUNCT_2:def 1;
A2: dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0)
  .x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A3: AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23;
A4: dom ((AffineMap(1,0))(#)sinh) = [#]REAL by FUNCT_2:def 1;
  then
A5: ((AffineMap(1,0))(#)sinh) is_differentiable_on REAL by A3,FDIFF_1:21
,SIN_COS2:34;
 hence (AffineMap(1,0))(#)sinh-cosh is_differentiable_on REAL
   by A1,FDIFF_1:19,SIN_COS2:35;
A6: for x st x in REAL holds (((AffineMap(1,0))(#)sinh)`|REAL).x = sinh.x+x*
  cosh.x
  proof
    let x;
    assume
A7: x in REAL;
    (((AffineMap(1,0))(#)sinh)`|REAL).x = sinh.x*diff((AffineMap(1,0)),x)+
    ((AffineMap(1,0)).x) *diff(sinh,x) by A4,A3,FDIFF_1:21,SIN_COS2:34,A7
      .= sinh.x*(((AffineMap(1,0))`|REAL).x) +((AffineMap(1,0)).x)*diff(sinh
    ,x) by A3,FDIFF_1:def 7,A7
      .= sinh.x*1+((AffineMap(1,0)).x)*diff(sinh,x) by A2,FDIFF_1:23,A7
      .= sinh.x+((AffineMap(1,0)).x)*(cosh.x) by SIN_COS2:34
      .= sinh.x+(1*x + 0)*cosh.x by FCONT_1:def 4
      .= sinh.x+x*cosh.x;
    hence thesis;
  end;
A8:
  for x st x in REAL holds (((AffineMap(1,0))(#)sinh-cosh)`|REAL).x = x*(
  cosh.x)
  proof
    let x;
    assume
A9: x in REAL;
    (((AffineMap(1,0))(#)sinh - cosh)`|REAL).x = diff(((AffineMap(1,0))(#)
    sinh),x) - diff(cosh,x) by A1,A5,FDIFF_1:19,SIN_COS2:35,A9
      .= (((AffineMap(1,0))(#)sinh)`|REAL).x - diff(cosh,x)
by A5,FDIFF_1:def 7,A9
      .= sinh.x+x*cosh.x-diff(cosh,x) by A6,A9
      .= sinh.x+x*cosh.x-sinh.x by SIN_COS2:35
      .= x*cosh.x;
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A8;
end;

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

theorem Th12:
  a*(n+1) <> 0 implies (1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b))
is_differentiable_on REAL & for x holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(
  a,b)))`|REAL).x = (a*x+b) #Z n
proof
  assume
A1: a*(n+1) <> 0;
A2: [#]REAL = dom((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b))) by FUNCT_2:def 1;
A3: [#]REAL = dom (AffineMap(a,b)) by FUNCT_2:def 1;
A4: for x st x in REAL holds AffineMap(a,b).x=a*x + b by FCONT_1:def 4;
  then
A5: AffineMap(a,b) is_differentiable_on REAL by A3,FDIFF_1:23;
  #Z (n+1)*AffineMap(a,b) is_differentiable_in x
  proof
    x in REAL by XREAL_0:def 1;
    then AffineMap(a,b) is_differentiable_in x by A3,A5,FDIFF_1:9;
    hence thesis by TAYLOR_1:3;
  end;
  then
  [#]REAL = dom ( #Z (n+1)*AffineMap(a,b)) & for x st x in REAL holds #Z (
  n+1) *AffineMap(a,b) is_differentiable_in x by FUNCT_2:def 1;
  then
A6: #Z (n+1)*AffineMap(a,b) is_differentiable_on REAL by FDIFF_1:9;
 hence (1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b))
is_differentiable_on REAL by A2,FDIFF_1:20;
A7: for x st x in REAL holds (( #Z (n+1)*AffineMap(a,b))`|REAL).x=a*(n+1)*(
  AffineMap(a,b).x) #Z n
  proof
    set m=n+1;
    let x;
    assume
A8: x in REAL;
    AffineMap(a,b) is_differentiable_in x by A3,A5,FDIFF_1:9,A8;
    then diff(( #Z m*AffineMap(a,b)),x) = m * (AffineMap(a,b).x) #Z (m-1) *
    diff(AffineMap(a,b),x) by TAYLOR_1:3
      .= m * (AffineMap(a,b).x) #Z (m-1) * ((AffineMap(a,b))`|REAL).x by A5,
FDIFF_1:def 7,A8
      .= m * (AffineMap(a,b).x) #Z (m-1) *a by A3,A4,FDIFF_1:23,A8;
    hence thesis by A6,FDIFF_1:def 7,A8;
  end;
A9:
  for x st x in REAL holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))
  `|REAL).x =(a*x+b) #Z n
  proof
    let x;
    assume
A10: x in REAL;
    (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL).x =(1/(a*(n+1)))
    *diff( #Z (n+1)*AffineMap(a,b),x) by A2,A6,FDIFF_1:20,A10
      .=(1/(a*(n+1)))*((( #Z (n+1)*AffineMap(a,b))`|REAL).x) by A6,
FDIFF_1:def 7,A10
      .=(1/(a*(n+1)))*(a*(n+1) * (AffineMap(a,b).x) #Z n ) by A7,A10
      .=(1/(a*(n+1)))*(a*(n+1)) * (AffineMap(a,b).x) #Z n
      .=(a*(n+1))/(a*(n+1)) * (AffineMap(a,b).x) #Z n by XCMPLX_1:99
      .=1*(AffineMap(a,b).x) #Z n by A1,XCMPLX_1:60
      .=(a*x+b) #Z n by FCONT_1:def 4;
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A9;
end;

begin :: Integrability Formulas
:: f.x = (sin.x)^2

theorem Th13:
  integral(sin^2,A) = (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0
  ))).(upper_bound A) -(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).
  (lower_bound A)
proof
A1: for x being Element of REAL
st x in dom ((AffineMap(1/2,0) -(1/4)(#)(sin*AffineMap(2,0)))`|REAL
  ) holds ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (sin^2).x
  proof
    let x be Element of REAL;
    assume x in dom ((AffineMap(1/2,0) -(1/4)(#)(sin*AffineMap(2,0)))`|REAL);
    ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (sin.x)^2
    by Th1
      .= (sin^2).x by VALUED_1:11;
    hence thesis;
  end;
A2: dom (sin^2)=REAL by SIN_COS:24,VALUED_1:11;
  then
  dom ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = dom (sin^2
  ) by Th1,FDIFF_1:def 7;
  then
A3: ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = sin^2 by A1,
PARTFUN1:5;
  (sin^2)|A is bounded by A2,INTEGRA5:10;
  hence thesis by A2,A3,Th1,INTEGRA5:11,13;
end;

Lm4: dom (AffineMap(2,0)) = [#]REAL by FUNCT_2:def 1;

Lm5: dom (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))=REAL by FUNCT_2:def 1;

  reconsider pp = PI as Element of REAL by XREAL_0:def 1;

Lm6: 0 in REAL by XREAL_0:def 1;

theorem
  A = [.0,PI.] implies integral(sin^2,A) = PI/2
proof
  assume A=[.0,PI.];
  then upper_bound A=PI & lower_bound A=0 by INTEGRA8:37;
  then
  integral(sin^2,A)
     =(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).pp -
  (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Th13
    .= AffineMap(1/2,0).(PI)-((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap
  (1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Lm5,VALUED_1:13
    .= AffineMap(1/2,0).(PI)-((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap
  (1/2,0).0-((1/4)(#)(sin*AffineMap(2,0))).0) by Lm5,VALUED_1:13,Lm6
    .= (1/2)*(PI)+0 -((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap(1/2,0).
  0-((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4
    .= (1/2)*(PI)-(1/4)*(sin*AffineMap(2,0)).pp -(AffineMap(1/2,0).0-((1/4
  )(#)(sin*AffineMap(2,0))).0) by VALUED_1:6
    .= (1/2)*(PI)-(1/4)*(sin.(AffineMap(2,0).(PI))) -(AffineMap(1/2,0).0-((1
  /4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13
    .= (1/2)*(PI)-(1/4)*(sin.(2*PI+0)) -(AffineMap(1/2,0).0-((1/4)(#)(sin*
  AffineMap(2,0))).0) by FCONT_1:def 4
    .= (1/2)*(PI)-(1/4)*sin.(2*PI+0) -(0-((1/4)(#)(sin*AffineMap(2,0))).0)
  by FCONT_1:48
    .= (1/2)*(PI)-(1/4)*sin.(2*PI+0) -0+((1/4)(#)(sin*AffineMap(2,0))).0
    .= (1/2)*(PI)-(1/4)*sin.(2*PI+0) +(1/4)*(sin*AffineMap(2,0)).0 by
VALUED_1:6
    .= (1/2)*(PI)-(1/4)*sin.(2*PI+0) +(1/4)*(sin.(AffineMap(2,0).0)) by Lm4,
FUNCT_1:13,Lm6
    .= (1/2)*(PI)-(1/4)*sin.(0+2*PI*1)+(1/4)*sin.0 by FCONT_1:48
    .= (1/2)*(PI)-(1/4)*sin.0+(1/4)*sin.0 by SIN_COS6:8
    .= PI/2;
  hence thesis;
end;

  reconsider dp = 2*PI, ddp = 2*(2*PI)+0 as Element of REAL by XREAL_0:def 1;

theorem
  A = [.0,2*PI.] implies integral(sin^2,A) = PI
proof
  assume A=[.0,2*PI.];
  then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37;
  then
  integral(sin^2,A)
    =(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).dp
  -(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Th13
   .= AffineMap(1/2,0).(2*PI)-((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(
  AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Lm5,VALUED_1:13
    .= AffineMap(1/2,0).(2*PI)-((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(
  AffineMap(1/2,0).0-((1/4)(#)(sin*AffineMap(2,0))).0) by Lm5,VALUED_1:13,Lm6
    .= (1/2)*(2*PI)+0 -((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(AffineMap(1/2
  ,0).0-((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4
    .= (1/2)*(2*PI)-(1/4)*(sin*AffineMap(2,0)).(2*PI) -(AffineMap(1/2,0).0-(
  (1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:6
    .= (1/2)*(2*PI)-(1/4)*(sin.(AffineMap(2,0).dp)) -(AffineMap(1/2,0).0
  -((1/4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13
    .= (1/2)*(2*PI)-(1/4)*(sin.ddp) -(AffineMap(1/2,0).0-((1/4)(#)(
  sin*AffineMap(2,0))).0) by FCONT_1:def 4
    .= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) -(0-((1/4)(#)(sin*AffineMap(2,0))).
  0) by FCONT_1:48
    .= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) -0+((1/4)(#)(sin*AffineMap(2,0))).0
    .= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) +(1/4)*(sin*AffineMap(2,0)).0 by
VALUED_1:6
    .= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) +(1/4)*(sin.(AffineMap(2,0).0))
          by Lm4,Lm6
,FUNCT_1:13
    .= (1/2)*(2*PI)-(1/4)*sin.(0+2*PI*2)+(1/4)*sin.0 by FCONT_1:48
    .= (1/2)*(2*PI)-(1/4)*sin.0+(1/4)*sin.0 by SIN_COS6:8
    .= PI;
  hence thesis;
end;

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

theorem Th16:
  integral(cos^2,A) = (AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0
  ))).(upper_bound A) -(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).
  (lower_bound A)
proof
A1: for x being Element of REAL
st x in dom ((AffineMap(1/2,0) +(1/4)(#)(sin*AffineMap(2,0)))`|
REAL) holds ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (cos^2)
  .x
  proof
    let x be Element of REAL;
    assume x in dom ((AffineMap(1/2,0) +(1/4)(#)(sin*AffineMap(2,0)))`|REAL);
    ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (cos.x)^2
    by Th2
      .= (cos^2).x by VALUED_1:11;
    hence thesis;
  end;
A2: dom (cos^2)=REAL by SIN_COS:24,VALUED_1:11;
  then
  dom ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = dom (cos^2
  ) by Th2,FDIFF_1:def 7;
  then
A3: ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = cos^2 by A1,
PARTFUN1:5;
  (cos^2)|A is bounded by A2,INTEGRA5:10;
  hence thesis by A2,A3,Th2,INTEGRA5:11,13;
end;

theorem
  A = [.0,PI.] implies integral(cos^2,A) = PI/2
proof
  assume A=[.0,PI.];
  then upper_bound A=PI & lower_bound A=0 by INTEGRA8:37;
  then
  integral(cos^2,A)=(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).(PI) -
  (AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by Th16
    .= AffineMap(1/2,0).(PI)+((1/4)(#)(sin*AffineMap(2,0))).pp -(AffineMap
  (1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by VALUED_1:1
    .= AffineMap(1/2,0).(PI)+((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap
  (1/2,0).0+((1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:1,Lm6
    .= (1/2)*(PI)+0 +((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap(1/2,0).
  0+((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4
    .= (1/2)*(PI)+(1/4)*(sin*AffineMap(2,0)).(PI) -(AffineMap(1/2,0).0+((1/4
  )(#)(sin*AffineMap(2,0))).0) by VALUED_1:6
    .= (1/2)*(PI)+(1/4)*(sin.(AffineMap(2,0).pp)) -(AffineMap(1/2,0).0+((1
  /4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13
    .= (1/2)*(PI)+(1/4)*(sin.(2*PI+0)) -(AffineMap(1/2,0).0+((1/4)(#)(sin*
  AffineMap(2,0))).0) by FCONT_1:def 4
    .= (1/2)*(PI)+(1/4)*sin.(2*PI+0) -(0+((1/4)(#)(sin*AffineMap(2,0))).0)
  by FCONT_1:48
    .= (1/2)*(PI)+(1/4)*sin.(2*PI+0) -(1/4)*(sin*AffineMap(2,0)).0 by
VALUED_1:6
    .= (1/2)*(PI)+(1/4)*sin.(2*PI+0) -(1/4)*(sin.(AffineMap(2,0).0)) by Lm4,
FUNCT_1:13,Lm6
    .= (1/2)*(PI)+(1/4)*sin.(0+2*PI*1)-(1/4)*sin.0 by FCONT_1:48
    .= (1/2)*(PI)+(1/4)*sin.0-(1/4)*sin.0 by SIN_COS6:8
    .= PI/2;
  hence thesis;
end;

theorem
  A = [.0,2*PI.] implies integral(cos^2,A) = PI
proof
  assume A=[.0,2*PI.];
  then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37;
  then
  integral(cos^2,A)=(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).(2*PI)
  -(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by Th16
    .= AffineMap(1/2,0).(2*PI)+((1/4)(#)(sin*AffineMap(2,0))).dp -(
  AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by VALUED_1:1
    .= AffineMap(1/2,0).(2*PI)+((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(
  AffineMap(1/2,0).0+((1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:1,Lm6
    .= (1/2)*(2*PI)+0 +((1/4)(#)(sin*AffineMap(2,0))).dp -(AffineMap(1/2
  ,0).0+((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4
    .= (1/2)*(2*PI)+(1/4)*(sin*AffineMap(2,0)).(2*PI) -(AffineMap(1/2,0).0+(
  (1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:6
    .= (1/2)*(2*PI)+(1/4)*(sin.(AffineMap(2,0).dp)) -(AffineMap(1/2,0).0
  +((1/4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13
    .= (1/2)*(2*PI)+(1/4)*(sin.ddp) -(AffineMap(1/2,0).0+((1/4)(#)(
  sin*AffineMap(2,0))).0) by FCONT_1:def 4
    .= (1/2)*(2*PI)+(1/4)*sin.(2*2*PI+0) -(0+((1/4)(#)(sin*AffineMap(2,0))).
  0) by FCONT_1:48
    .= (1/2)*(2*PI)+(1/4)*sin.(2*2*PI+0) -(1/4)*(sin*AffineMap(2,0)).0 by
VALUED_1:6
    .= (1/2)*(2*PI)+(1/4)*sin.(2*2*PI+0) -(1/4)*(sin.(AffineMap(2,0).0)) by Lm4
,FUNCT_1:13,Lm6
    .= (1/2)*(2*PI)+(1/4)*sin.(0+2*PI*2)-(1/4)*sin.0 by FCONT_1:48
    .= (1/2)*(2*PI)+(1/4)*sin.0-(1/4)*sin.0 by SIN_COS6:8
    .= PI;
  hence thesis;
end;

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

theorem Th19:
  integral(( #Z n*sin)(#)cos,A) = ((1/(n+1))(#)( #Z (n+1)*sin)).(
  upper_bound A) -((1/(n+1))(#)( #Z (n+1)*sin)).(lower_bound A)
proof
A1: [#]REAL = dom (( #Z n*sin)(#)cos) by FUNCT_2:def 1;
A2: for x being Element of REAL
st x in dom (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL) holds (((1/(n+1)
  )(#)( #Z (n+1)*sin))`|REAL).x = (( #Z n*sin)(#)cos).x
  proof
    let x be Element of REAL;
    assume x in dom (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL);
    (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x =(sin.x) #Z n *cos.x by Th3
      .=( #Z n).(sin.x)*cos.x by TAYLOR_1:def 1
      .=(( #Zn)*sin).x*cos.x by FUNCT_1:13,SIN_COS:24
      .= ((( #Z n)*sin)(#)cos).x by A1,VALUED_1:def 4;
    hence thesis;
  end;
  #Z n*sin is_differentiable_in x0
  proof
    sin is_differentiable_in x0 by SIN_COS:64;
    hence thesis by TAYLOR_1:3;
  end;
  then dom ( #Z n*sin)=REAL & for x0 st x0 in REAL holds #Z n*sin
  is_differentiable_in x0 by FUNCT_2:def 1;
  then #Z n*sin is_differentiable_on REAL by A1,FDIFF_1:9;
  then
A3: (( #Z n*sin)(#)cos)|REAL is continuous by A1,FDIFF_1:21,25,SIN_COS:67;
  then (( #Z n*sin)(#)cos)|A is continuous by FCONT_1:16;
  then
A4: ( #Z n)*sin(#)cos is_integrable_on A by A1,INTEGRA5:11;
  (1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL by Th3;
  then dom (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL) = dom (( #Z n*sin)(#)cos) by
A1,FDIFF_1:def 7;
  then
A5: (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL) = (( #Z n*sin)(#)cos) by A2,
PARTFUN1:5;
  (( #Z n)*sin(#)cos)|A is bounded by A1,A3,INTEGRA5:10;
  hence thesis by A4,A5,Th3,INTEGRA5:13;
end;

theorem
  A = [.0,PI.] implies integral(( #Z n*sin)(#)cos,A) = 0
proof
  assume A=[.0,PI.];
  then upper_bound A=PI & lower_bound A=0 by INTEGRA8:37;
  then
  integral(( #Z n*sin)(#)cos,A)=((1/(n+1))(#)( #Z (n+1)*sin)).(PI) -((1/(n
  +1))(#)( #Z (n+1)*sin)).0 by Th19
    .= 1/(n+1)*( #Z (n+1)*sin).PI -((1/(n+1))(#)( #Z (n+1)*sin)).0 by
VALUED_1:6
    .= 1/(n+1)*( #Z (n+1)*sin).PI -1/(n+1)*( #Z (n+1)*sin).0 by VALUED_1:6
    .= 1/(n+1)*(( #Z (n+1)).(sin.pp)) -1/(n+1)*( #Z (n+1)*sin).0 by FUNCT_1:13
,SIN_COS:24
    .= 1/(n+1)*(( #Z (n+1)).(sin.PI)) -1/(n+1)*(( #Z (n+1)).(sin.0)) by
FUNCT_1:13,SIN_COS:24,Lm6
    .= 0 by SIN_COS:30,76;
  hence thesis;
end;

theorem
  A = [.0,2*PI.] implies integral(( #Z n*sin)(#)cos,A) = 0
proof
  assume A=[.0,2*PI.];
  then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37;
  then
  integral(( #Z n*sin)(#)cos,A)=((1/(n+1))(#)( #Z (n+1)*sin)).(2*PI) -((1/
  (n+1))(#)( #Z (n+1)*sin)).0 by Th19
    .= 1/(n+1)*( #Z (n+1)*sin).(2*PI) -((1/(n+1))(#)( #Z (n+1)*sin)).0 by
VALUED_1:6
    .= 1/(n+1)*( #Z (n+1)*sin).dp -1/(n+1)*( #Z (n+1)*sin).0 by VALUED_1:6
    .= 1/(n+1)*(( #Z (n+1)).(sin.(2*PI))) -1/(n+1)*( #Z (n+1)*sin).0 by
FUNCT_1:13,SIN_COS:24
    .= 1/(n+1)*(( #Z (n+1)).(sin.(2*PI))) -1/(n+1)*(( #Z (n+1)).(sin.0)) by
FUNCT_1:13,SIN_COS:24,Lm6
    .= 0 by SIN_COS:30,76;
  hence thesis;
end;

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

theorem Th22:
  integral(( #Z n*cos)(#)sin,A) = ((-1/(n+1))(#)( #Z (n+1)*cos)).(
  upper_bound A) -((-1/(n+1))(#)( #Z (n+1)*cos)).(lower_bound A)
proof
A1: [#]REAL=dom (( #Z n*cos)(#)sin) by FUNCT_2:def 1;
A2: for x being Element of REAL
st x in dom (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL) holds (((-1/(n+
  1))(#)( #Z (n+1)*cos))`|REAL).x = (( #Z n*cos)(#)sin).x
  proof
    let x be Element of REAL;
    assume x in dom (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL);
    (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x =(cos.x) #Z n *sin.x by Th4
      .=( #Z n).(cos.x)*sin.x by TAYLOR_1:def 1
      .=(( #Zn)*cos).x*sin.x by FUNCT_1:13,SIN_COS:24
      .= ((( #Z n)*cos)(#)sin).x by A1,VALUED_1:def 4;
    hence thesis;
  end;
  #Z n*cos is_differentiable_in x0
  proof
    cos is_differentiable_in x0 by SIN_COS:63;
    hence thesis by TAYLOR_1:3;
  end;
  then dom ( #Z n*cos)=REAL & for x0 st x0 in REAL holds #Z n*cos
  is_differentiable_in x0 by FUNCT_2:def 1;
  then #Z n*cos is_differentiable_on REAL by A1,FDIFF_1:9;
  then
A3: (( #Z n*cos)(#)sin)|REAL is continuous by A1,FDIFF_1:21,25,SIN_COS:68;
  then (( #Z n*cos)(#)sin)|A is continuous by FCONT_1:16;
  then
A4: ( #Z n*cos)(#)sin is_integrable_on A by A1,INTEGRA5:11;
  (-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL by Th4;
  then
  dom (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL) = dom (( #Z n*cos)(#)sin) by A1,
FDIFF_1:def 7;
  then
A5: (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL) = (( #Z n*cos)(#)sin) by A2,
PARTFUN1:5;
  (( #Z n*cos)(#)sin)|A is bounded by A1,A3,INTEGRA5:10;
  hence thesis by A4,A5,Th4,INTEGRA5:13;
end;

theorem
  A = [.0,2*PI.] implies integral(( #Z n*cos)(#)sin,A) = 0
proof
  assume A=[.0,2*PI.];
  then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37;
  then
  integral(( #Z n*cos)(#)sin,A)=((-1/(n+1))(#)( #Z (n+1)*cos)).(2*PI) -((-
  1/(n+1))(#)( #Z (n+1)*cos)).0 by Th22
    .= (-1/(n+1))*( #Z (n+1)*cos).(2*PI) -((-1/(n+1))(#)( #Z (n+1)*cos)).0
  by VALUED_1:6
    .= (-1/(n+1))*( #Z (n+1)*cos).(2*PI) -(-1/(n+1))*( #Z (n+1)*cos).0 by
VALUED_1:6
    .= (-1/(n+1))*(( #Z (n+1)).(cos.dp)) -(-1/(n+1))*( #Z (n+1)*cos).0
  by FUNCT_1:13,SIN_COS:24
    .= (-1/(n+1))*(( #Z (n+1)).(cos.(2*PI))) -(-1/(n+1))*(( #Z (n+1)).(cos.0
  )) by FUNCT_1:13,SIN_COS:24,Lm6
    .= 0 by SIN_COS:30,76;
  hence thesis;
end;

reconsider pd = PI/2, mpd = - PI/2 as Element of REAL by XREAL_0:def 1;

theorem
  A = [.-PI/2,PI/2.] implies integral(( #Z n*cos)(#)sin,A) = 0
proof
  assume A=[.-PI/2,PI/2.];
  then upper_bound A=PI/2 & lower_bound A=-PI/2 by INTEGRA8:37;
  then
  integral(( #Z n*cos)(#)sin,A)=((-1/(n+1))(#)( #Z (n+1)*cos)).(PI/2) -((-
  1/(n+1))(#)( #Z (n+1)*cos)).(-PI/2) by Th22
    .= (-1/(n+1))*( #Z (n+1)*cos).(PI/2) -((-1/(n+1))(#)( #Z (n+1)*cos)).(-
  PI/2) by VALUED_1:6
    .= (-1/(n+1))*( #Z (n+1)*cos).(PI/2) -(-1/(n+1))*( #Z (n+1)*cos).(-PI/2)
  by VALUED_1:6
    .= (-1/(n+1))*(( #Z (n+1)).(cos.pd)) -(-1/(n+1))*( #Z (n+1)*cos).mpd
   by FUNCT_1:13,SIN_COS:24
    .= (-1/(n+1))*(( #Z (n+1)).(cos.pd)) -(-1/(n+1))*(( #Z (n+1)).(cos.(
  -PI/2))) by FUNCT_1:13,SIN_COS:24
    .= (-1/(n+1))*(( #Z (n+1)).(cos.(PI/2))) -(-1/(n+1))*(( #Z (n+1)).(cos.(
  PI/2))) by SIN_COS:30
    .= 0;
  hence thesis;
end;

:: f.x = cos.(m*x)*cos.(n*x)

theorem
  m+n<>0 & m-n<>0 implies integral((cos*AffineMap(m,0))(#)(cos*AffineMap
  (n,0)),A) = ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0))).(upper_bound A) -((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+
 (1/(2*(m-n
  )))(#)(sin*AffineMap(m-n,0))).(lower_bound A)
proof
  assume
A1: m+n<>0 & m-n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
  proof
    let x;
    assume x in REAL;
    (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
      .=n*x;
    hence thesis;
  end;
A3: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: dom (cos*AffineMap(m,0)) = [#]REAL by FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(m,0).x=m*x
  proof
    let x;
    assume x in REAL;
    (AffineMap(m,0)).x = m*x + 0 by FCONT_1:def 4
      .=m*x;
    hence thesis;
  end;
A6: for x being Element of REAL
st x in dom (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)
))(#)(sin*AffineMap(m-n,0)))`|REAL) holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,
  0))+ (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x = ((cos*AffineMap(m,0))
  (#)(cos*AffineMap(n,0))).x
  proof
    let x be Element of REAL;
    assume x in dom (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(
    sin*AffineMap(m-n,0)))`|REAL);
    (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
    AffineMap(m-n,0)))`|REAL).x = cos.(m*x)*cos.(n*x) by A1,Th5
      .= cos.(AffineMap(m,0).x)*cos.(n*x) by A5
      .= (cos.(AffineMap(m,0).x))*(cos.((AffineMap(n,0)).x)) by A2
      .= ((cos*AffineMap(m,0)).x) *(cos.(AffineMap(n,0).x)) by A4,FUNCT_1:12
      .= ((cos*AffineMap(m,0)).x)*((cos*AffineMap(n,0)).x) by A3,FUNCT_1:12
      .= ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))).x by VALUED_1:5;
    hence thesis;
  end;
A7: [#]REAL = dom ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))) by
FUNCT_2:def 1;
  ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*AffineMap
  (m-n,0))) is_differentiable_on REAL by A1,Th5;
  then dom (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
  AffineMap(m-n,0)))`|REAL) = dom ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)))
  by A7,FDIFF_1:def 7;
  then
A8: (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0)))`|REAL) = (cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)) by A6,
PARTFUN1:5;
  ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is continuous;
  then
A9: ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))) is_integrable_on A by A7,
INTEGRA5:11;
  ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is bounded by A7,INTEGRA5:10;
  hence thesis by A1,A9,A8,Th5,INTEGRA5:13;
end;

:: f.x = sin.(m*x)*sin.(n*x)

theorem
  m+n<>0 & m-n<>0 implies integral((sin*AffineMap(m,0))(#)(sin*AffineMap
  (n,0)),A) = ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0))).(upper_bound A) -((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))-
 (1/(2*(m+n
  )))(#)(sin*AffineMap(m+n,0))).(lower_bound A)
proof
  assume
A1: m+n<>0 & m-n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
  proof
    let x;
    assume x in REAL;
    (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
      .=n*x;
    hence thesis;
  end;
A3: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: dom (sin*AffineMap(m,0)) = [#]REAL by FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(m,0).x=m*x
  proof
    let x;
    assume x in REAL;
    (AffineMap(m,0)).x = m*x + 0 by FCONT_1:def 4
      .=m*x;
    hence thesis;
  end;
A6: for x being Element of REAL
st x in dom (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)
))(#)(sin*AffineMap(m+n,0)))`|REAL) holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,
  0))- (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x = ((sin*AffineMap(m,0))
  (#)(sin*AffineMap(n,0))).x
  proof
    let x be Element of REAL;
    assume x in dom (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(
    sin*AffineMap(m+n,0)))`|REAL);
    (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
    AffineMap(m+n,0)))`|REAL).x = sin.(m*x)*sin.(n*x) by A1,Th6
      .= sin.(AffineMap(m,0).x)*sin.(n*x) by A5
      .= (sin.(AffineMap(m,0).x))*(sin.(AffineMap(n,0).x)) by A2
      .= ((sin*(AffineMap(m,0))).x) *(sin.(AffineMap(n,0).x)) by A4,FUNCT_1:12
      .= ((sin*AffineMap(m,0)).x)*((sin*AffineMap(n,0)).x) by A3,FUNCT_1:12
      .= ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))).x by VALUED_1:5;
    hence thesis;
  end;
A7: REAL=dom ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))) by FUNCT_2:def 1;
  ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)))|A is continuous;
  then
A8: ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))) is_integrable_on A by A7,
INTEGRA5:11;
  ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*AffineMap
  (m+n,0))) is_differentiable_on REAL by A1,Th6;
  then dom (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
  AffineMap(m+n,0)))`|REAL) = dom ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)))
  by A7,FDIFF_1:def 7;
  then
A9: (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0)))`|REAL) = (sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)) by A6,
PARTFUN1:5;
  ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)))|A is bounded by A7,INTEGRA5:10;
  hence thesis by A1,A8,A9,Th6,INTEGRA5:13;
end;

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

theorem
  m+n<>0 & m-n<>0 implies integral((sin*AffineMap(m,0))(#)(cos*AffineMap
  (n,0)),A) = ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0))).(upper_bound A) -((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))
- (1/(2*(
  m-n)))(#)(cos*AffineMap(m-n,0))).(lower_bound A)
proof
  assume
A1: m+n<>0 & m-n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
  proof
    let x;
    assume x in REAL;
    (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
      .=n*x;
    hence thesis;
  end;
A3: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: dom (sin*AffineMap(m,0)) = [#]REAL by FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(m,0).x=m*x
  proof
    let x;
    assume x in REAL;
    (AffineMap(m,0)).x = m*x + 0 by FCONT_1:def 4
      .=m*x;
    hence thesis;
  end;
A6: for x being Element of REAL
st x in dom (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m
-n)))(#)(cos*AffineMap(m-n,0)))`|REAL) holds (((-(1/(2*(m+n)))(#)(cos*AffineMap
(m+n,0)))- (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|REAL).x = ((sin*AffineMap(m
  ,0))(#)(cos*AffineMap(n,0))).x
  proof
    let x be Element of REAL;
    assume
    x in dom (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)
    (cos*AffineMap(m-n,0)))`|REAL);
    (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
    AffineMap(m-n,0)))`|REAL).x = sin.(m*x)*cos.(n*x) by A1,Th7
      .= sin.(AffineMap(m,0).x)*cos.(n*x) by A5
      .= (sin.(AffineMap(m,0).x))*(cos.(AffineMap(n,0).x)) by A2
      .= ((sin*AffineMap(m,0)).x)*(cos.(AffineMap(n,0).x)) by A4,FUNCT_1:12
      .= ((sin*AffineMap(m,0)).x)*((cos*AffineMap(n,0)).x) by A3,FUNCT_1:12
      .= ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))).x by VALUED_1:5;
    hence thesis;
  end;
A7: [#]REAL=dom ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))) by FUNCT_2:def 1;
  ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is continuous;
  then
A8: ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))) is_integrable_on A by A7,
INTEGRA5:11;
  ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
  AffineMap(m-n,0))) is_differentiable_on REAL by A1,Th7;
  then dom (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
  AffineMap(m-n,0)))`|REAL) = dom ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)))
  by A7,FDIFF_1:def 7;
  then
A9: (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0)))`|REAL) = (sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)) by A6,
PARTFUN1:5;
  ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is bounded by A7,INTEGRA5:10;
  hence thesis by A1,A8,A9,Th7,INTEGRA5:13;
end;

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

theorem
  n<>0 implies integral((AffineMap(1,0))(#)(sin*AffineMap(n,0)),A) = ((1
/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0))).
(upper_bound
A) -((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0)
  )).(lower_bound A)
proof
  assume
A1: n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
  proof
    let x;
    assume x in REAL;
    (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
      .=n*x;
    hence thesis;
  end;
A3: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: for x st x in REAL holds AffineMap(1,0).x=x
  proof
    let x;
    assume x in REAL;
    (AffineMap(1,0)).x = 1*x + 0 by FCONT_1:def 4
      .=x;
    hence thesis;
  end;
A5: for x being Element of REAL
st x in dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))
  (#)(cos*AffineMap(n,0)))`|REAL) holds (((1/(n^2))(#)(sin*AffineMap(n,0))- (
AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x = ((AffineMap(1,0))(#)(sin*
  AffineMap(n,0))).x
  proof
    let x be Element of REAL;
    assume
    x in dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos
    *AffineMap(n,0)))`|REAL);
    (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*
    AffineMap(n,0)))`|REAL).x = x*sin.(n*x) by A1,Th8
      .= x*(sin.(AffineMap(n,0).x)) by A2
      .= x*(sin*AffineMap(n,0)).x by A3,FUNCT_1:12
      .= (AffineMap(1,0).x)*(sin*AffineMap(n,0)).x by A4
      .= ((AffineMap(1,0))(#)(sin*AffineMap(n,0))).x by VALUED_1:5;
    hence thesis;
  end;
A6: dom ((AffineMap(1,0))(#)(sin*AffineMap(n,0))) = [#]REAL by FUNCT_2:def 1;
  ((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(
  n,0))) is_differentiable_on REAL by A1,Th8;
  then dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*
AffineMap(n,0)))`|REAL) = dom ((AffineMap(1,0))(#)(sin*AffineMap(n,0))) by A6,
FDIFF_1:def 7;
  then
A7: (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap
  (n,0)))`|REAL) = (AffineMap(1,0))(#)(sin*AffineMap(n,0)) by A5,PARTFUN1:5;
  ((AffineMap(1,0))(#)(sin*AffineMap(n,0)))|A is continuous;
  then
A8: ((AffineMap(1,0))(#)(sin*AffineMap(n,0))) is_integrable_on A by A6,
INTEGRA5:11;
  ((AffineMap(1,0))(#)(sin*AffineMap(n,0)))|A is bounded by A6,INTEGRA5:10;
  hence thesis by A1,A8,A7,Th8,INTEGRA5:13;
end;

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

theorem
  n<>0 implies integral((AffineMap(1,0))(#)(cos*AffineMap(n,0)),A) = ((1
/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0))).
(upper_bound
A) -((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0)
  )).(lower_bound A)
proof
  assume
A1: n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
  proof
    let x;
    assume x in REAL;
    (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
      .=n*x;
    hence thesis;
  end;
A3: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: for x st x in REAL holds AffineMap(1,0).x=x
  proof
    let x;
    assume x in REAL;
    (AffineMap(1,0)).x = 1*x + 0 by FCONT_1:def 4
      .=x;
    hence thesis;
  end;
A5: for x being Element of REAL
st x in dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))
  (#)(sin*AffineMap(n,0)))`|REAL) holds (((1/(n^2))(#)(cos*AffineMap(n,0))+ (
AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x = ((AffineMap(1,0))(#)(cos*
  AffineMap(n,0))).x
  proof
    let x be Element of REAL;
    assume
    x in dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin
    *AffineMap(n,0)))`|REAL);
    (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*
    AffineMap(n,0)))`|REAL).x = x*cos.(n*x) by A1,Th9
      .= x*(cos.(AffineMap(n,0).x)) by A2
      .= x*(cos*AffineMap(n,0)).x by A3,FUNCT_1:12
      .= (AffineMap(1,0).x)*(cos*AffineMap(n,0)).x by A4
      .= ((AffineMap(1,0))(#)(cos*AffineMap(n,0))).x by VALUED_1:5;
    hence thesis;
  end;
A6: dom ((AffineMap(1,0))(#)(cos*AffineMap(n,0))) = [#]REAL by FUNCT_2:def 1;
  ((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(
  n,0))) is_differentiable_on REAL by A1,Th9;
  then dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*
AffineMap(n,0)))`|REAL) = dom ((AffineMap(1,0))(#)(cos*AffineMap(n,0))) by A6,
FDIFF_1:def 7;
  then
A7: (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap
  (n,0)))`|REAL) = (AffineMap(1,0))(#)(cos*AffineMap(n,0)) by A5,PARTFUN1:5;
  ((AffineMap(1,0))(#)(cos*AffineMap(n,0)))|A is continuous;
  then
A8: ((AffineMap(1,0))(#)(cos*AffineMap(n,0))) is_integrable_on A by A6,
INTEGRA5:11;
  ((AffineMap(1,0))(#)(cos*AffineMap(n,0)))|A is bounded by A6,INTEGRA5:10;
  hence thesis by A1,A8,A7,Th9,INTEGRA5:13;
end;

theorem
  integral((AffineMap(1,0))(#)sinh,A) = ((AffineMap(1,0))(#)cosh-sinh).(
  upper_bound A) -((AffineMap(1,0))(#)cosh-sinh).(lower_bound A)
proof
A1: for x being Element of REAL
st x in dom (((AffineMap(1,0))(#)cosh-sinh)`|REAL) holds (((
  AffineMap(1,0))(#)cosh-sinh)`|REAL).x = ((AffineMap(1,0))(#)sinh).x
  proof
    let x be Element of REAL;
    assume x in dom (((AffineMap(1,0))(#)cosh-sinh)`|REAL);
    (((AffineMap(1,0))(#)cosh-sinh)`|REAL).x = (1*x+0)*sinh.x by Th10
      .= ((AffineMap(1,0)).x)*sinh.x by FCONT_1:def 4
      .= ((AffineMap(1,0))(#)sinh).x by VALUED_1:5;
    hence thesis;
  end;
A2: dom ((AffineMap(1,0))(#)sinh) = [#]REAL by FUNCT_2:def 1;
  then dom (((AffineMap(1,0))(#)cosh-sinh)`|REAL) = dom ((AffineMap(1,0))(#)
  sinh) by Th10,FDIFF_1:def 7;
  then
A3: (((AffineMap(1,0))(#)cosh-sinh)`|REAL) = (AffineMap(1,0))(#)sinh by A1,
PARTFUN1:5;
  dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0)
  .x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23;
  then
A4: ((AffineMap(1,0))(#)sinh)|REAL is continuous by A2,FDIFF_1:21,25
,SIN_COS2:34;
  then
A5: ((AffineMap(1,0))(#)sinh)|A is continuous by FCONT_1:16;
  ((AffineMap(1,0))(#)sinh)|A is bounded by A2,A4,INTEGRA5:10;
  hence thesis by A2,A5,A3,Th10,INTEGRA5:11,13;
end;

theorem
  integral((AffineMap(1,0))(#)cosh,A) = ((AffineMap(1,0))(#)sinh-cosh).(
  upper_bound A) -((AffineMap(1,0))(#)sinh-cosh).(lower_bound A)
proof
A1: for x being Element of REAL
st x in dom (((AffineMap(1,0))(#)sinh-cosh)`|REAL) holds (((
  AffineMap(1,0))(#)sinh-cosh)`|REAL).x = ((AffineMap(1,0))(#)cosh).x
  proof
    let x be Element of REAL;
    assume x in dom (((AffineMap(1,0))(#)sinh-cosh)`|REAL);
    (((AffineMap(1,0))(#)sinh-cosh)`|REAL).x = (1*x+0)*cosh.x by Th11
      .= ((AffineMap(1,0)).x)*(cosh.x) by FCONT_1:def 4
      .= ((AffineMap(1,0))(#)cosh).x by VALUED_1:5;
    hence thesis;
  end;
A2: dom ((AffineMap(1,0))(#)cosh) = [#]REAL by FUNCT_2:def 1;
  then dom (((AffineMap(1,0))(#)sinh-cosh)`|REAL) = dom ((AffineMap(1,0))(#)
  cosh) by Th11,FDIFF_1:def 7;
  then
A3: (((AffineMap(1,0))(#)sinh-cosh)`|REAL) = (AffineMap(1,0))(#)cosh by A1,
PARTFUN1:5;
  dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0)
  .x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23;
  then
A4: ((AffineMap(1,0))(#)cosh)|REAL is continuous by A2,FDIFF_1:21,25
,SIN_COS2:35;
  then
A5: ((AffineMap(1,0))(#)cosh)|A is continuous by FCONT_1:16;
  ((AffineMap(1,0))(#)cosh)|A is bounded by A2,A4,INTEGRA5:10;
  hence thesis by A2,A5,A3,Th11,INTEGRA5:11,13;
end;

:: f.x = (a*x+b)^n

theorem
  a*(n+1) <> 0 implies integral( #Z n*AffineMap(a,b),A) = ((1/(a*(n+1)))
(#)( #Z (n+1)*AffineMap(a,b))).(upper_bound A) -
((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a
  ,b))).(lower_bound A)
proof
  assume
A1: a*(n+1) <> 0;
A2: [#]REAL=dom (AffineMap(a,b)) by FUNCT_2:def 1;
A3: for x being Element of REAL
 st x in dom (((1/(a*(n+1))) (#)( #Z (n+1)*AffineMap(a,b)))`|REAL)
holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL).x = ( #Z n*AffineMap
  (a,b)).x
  proof
    let x be Element of REAL;
    assume x in dom (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL);
    (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL).x =(a*x+b) #Z n
    by A1,Th12
      .= (AffineMap(a,b).x) #Z n by FCONT_1:def 4
      .= ( #Z n).(AffineMap(a,b).x) by TAYLOR_1:def 1
      .=( #Z n*AffineMap(a,b)).x by A2,FUNCT_1:13;
    hence thesis;
  end;
A4: [#]REAL=dom ( #Z n*AffineMap(a,b)) by FUNCT_2:def 1;
  for x st x in REAL holds AffineMap(a,b).x=a*x + b by FCONT_1:def 4;
  then
A5: AffineMap(a,b) is_differentiable_on REAL by A2,FDIFF_1:23;
  #Z n*AffineMap(a,b) is_differentiable_in x
  proof
    x in REAL by XREAL_0:def 1;
    then AffineMap(a,b) is_differentiable_in x by A2,A5,FDIFF_1:9;
    hence thesis by TAYLOR_1:3;
  end;
  then for x st x in REAL holds #Z n*AffineMap(a,b) is_differentiable_in x;
  then #Z n*AffineMap(a,b) is_differentiable_on REAL by A4,FDIFF_1:9;
  then
A6: ( #Z n*AffineMap(a,b))|REAL is continuous by FDIFF_1:25;
  then ( #Z n*AffineMap(a,b))|A is continuous by FCONT_1:16;
  then
A7: #Z n*AffineMap(a,b) is_integrable_on A by A4,INTEGRA5:11;
  (1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)) is_differentiable_on REAL by A1
,Th12;
  then dom (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL) = dom ( #Z n*
  AffineMap(a,b)) by A4,FDIFF_1:def 7;
  then
A8: (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL) = #Z n*AffineMap(a
  ,b) by A3,PARTFUN1:5;
  ( #Z n*AffineMap(a,b))|A is bounded by A4,A6,INTEGRA5:10;
  hence thesis by A1,A7,A8,Th12,INTEGRA5:13;
end;

begin :: Addenda

reserve f, f1, f2, f3 for PartFunc of REAL, REAL;

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

theorem Th33:
  Z c= dom ((1/2)(#)f) & f=#Z 2 implies (1/2)(#)f
  is_differentiable_on Z & for x st x in Z holds (((1/2)(#)f)`|Z).x = x
proof
  assume that
A1: Z c= dom ((1/2)(#)f) and
A2: f=#Z 2;
  Z c= dom f & for x st x in Z holds f is_differentiable_in x by A1,A2,
TAYLOR_1:2,VALUED_1:def 5;
  then
A3: f is_differentiable_on Z by FDIFF_1:9;
A4: for x st x in Z holds (f`|Z).x=2*x
  proof
    let x;
    2 * (x #Z (2-1)) = 2 * x by PREPOWER:35;
    then
A5: diff(f,x) = 2 * x by A2,TAYLOR_1:2;
    assume x in Z;
    hence thesis by A3,A5,FDIFF_1:def 7;
  end;
  for x st x in Z holds (((1/2)(#)f)`|Z).x=x
  proof
    let x;
    assume
A6: x in Z;
    then (((1/2)(#)f)`|Z).x=(1/2)*diff(f,x) by A1,A3,FDIFF_1:20
      .=(1/2)*(f`|Z).x by A3,A6,FDIFF_1:def 7
      .=(1/2)*(2*x) by A4,A6
      .=x;
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:20;
end;

:: f.x = x

theorem
  A c= Z & f=#Z 2 & Z = dom ((1/2)(#)f) implies integral(id Z,A) = ((1/2
  )(#)f).(upper_bound A)-((1/2)(#)f).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: f=#Z 2 & Z = dom ((1/2)(#)f);
A3: A c= dom id Z by A1;
  then
A4: (id Z)|A is bounded by INTEGRA5:10;
A5: ((1/2)(#)f) is_differentiable_on Z by A2,Th33;
A6: for x being Element of REAL
st x in dom (((1/2)(#)f)`|Z) holds (((1/2)(#)f)`|Z).x = (id Z).x
  proof
    let x be Element of REAL;
    assume x in dom (((1/2)(#)f)`|Z);
    then
A7: x in Z by A5,FDIFF_1:def 7;
    then (((1/2)(#)f)`|Z).x = x by A2,Th33
      .= (id Z).x by A7,FUNCT_1:18;
    hence thesis;
  end;
  dom (((1/2)(#)f)`|Z) = dom (id Z) by A5,FDIFF_1:def 7;
  then
A8: (((1/2)(#)f)`|Z) = id Z by A6,PARTFUN1:5;
  (id Z)|A is continuous;
  then id Z is_integrable_on A by A3,INTEGRA5:11;
  hence thesis by A1,A2,A4,A8,Th33,INTEGRA5:13;
end;

:: f.x = -1/x^2 :: INTEGRA9

theorem
  not 0 in Z & A c= Z & (for x st x in Z holds x<>0 & f.x = -1/x^2) &
dom f = Z & f|A is continuous implies integral(f,A) =
 ((id Z)^).(upper_bound A)-((id Z)
  ^).(lower_bound A)
proof
  set g = id Z;
  assume that
A1: not 0 in Z and
A2: A c= Z and
A3: for x st x in Z holds x<>0 & f.x = -1/x^2 and
A4: dom f = Z and
A5: f|A is continuous;
A6: f is_integrable_on A by A2,A4,A5,INTEGRA5:11;
A7: g^ is_differentiable_on Z by A1,FDIFF_5:4;
A8: for x being Element of REAL st x in dom ((g^)`|Z) holds ((g^)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((g^)`|Z);
    then
A9: x in Z by A7,FDIFF_1:def 7;
    then ((g^)`|Z).x = -1/x^2 by A1,FDIFF_5:4
      .= f.x by A3,A9;
    hence thesis;
  end;
  dom ((g^)`|Z) = dom f by A4,A7,FDIFF_1:def 7;
  then ((g^)`|Z) = f by A8,PARTFUN1:5;
  hence thesis by A2,A4,A5,A6,A7,INTEGRA5:10,13;
end;

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

theorem
  A c= Z & f1=#Z 2 & (for x st x in Z holds f2.x=1 & x<>0 & f.x=2*x/(1+x
^2)^2) & dom (f1/(f2+f1))=Z & Z = dom f & f|A is continuous implies integral(f,
  A) = (f1/(f2+f1)).(upper_bound A)-(f1/(f2+f1)).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: f1=#Z 2 and
A3: for x st x in Z holds f2.x=1 & x<>0 & f.x=2*x/(1+x^2)^2 and
A4: dom (f1/(f2+f1))=Z and
A5: Z = dom f and
A6: f|A is continuous;
A7: f is_integrable_on A by A1,A5,A6,INTEGRA5:11;
A8: for x st x in Z holds f2.x=1 & x<>0 by A3;
  then
A9: (f1/(f2+f1)) is_differentiable_on Z by A2,A4,FDIFF_6:7;
A10: for x being Element of REAL
st x in dom ((f1/(f2+f1))`|Z) holds ((f1/(f2+f1))`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((f1/(f2+f1))`|Z);
    then
A11: x in Z by A9,FDIFF_1:def 7;
    then ((f1/(f2+f1))`|Z).x = 2*x/(1+x^2)^2 by A2,A4,A8,FDIFF_6:7
      .= f.x by A3,A11;
    hence thesis;
  end;
  dom ((f1/(f2+f1))`|Z) = dom f by A5,A9,FDIFF_1:def 7;
  then ((f1/(f2+f1))`|Z) = f by A10,PARTFUN1:5;
  hence thesis by A1,A5,A6,A7,A9,INTEGRA5:10,13;
end;

theorem Th37:
  (Z c= dom (tan+sec) & for x st x in Z holds (1+sin.x)<>0 & (1-
sin.x)<>0) implies tan+sec is_differentiable_on Z & for x st x in Z holds ((tan
  +sec)`|Z).x = 1/(1-sin.x)
proof
  assume that
A1: Z c= dom (tan+sec) and
A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0;
  Z c= dom tan /\ dom (cos^) by A1,VALUED_1:def 1;
  then
A3: Z c= dom tan by XBOOLE_1:18;
  then
A4: for x st x in Z holds cos.x<>0 by FDIFF_8:1;
  then
A5: cos^ is_differentiable_on Z by FDIFF_4:39;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A3,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A6: tan is_differentiable_on Z by A3,FDIFF_1:9;
  for x st x in Z holds ((tan+sec)`|Z).x = 1/(1-sin.x)
  proof
    let x;
    assume
A7: x in Z;
    then
A8: cos.x<>0 by A3,FDIFF_8:1;
A9: 1+sin.x<>0 by A2,A7;
    ((tan+sec)`|Z).x = diff(tan,x) + diff(cos^,x) by A1,A5,A6,A7,FDIFF_1:18
      .=1/(cos.x)^2 + diff(cos^,x) by A8,FDIFF_7:46
      .=1/(cos.x)^2 + ((cos^)`|Z).x by A5,A7,FDIFF_1:def 7
      .=1/(cos.x)^2 + sin.x/(cos.x)^2 by A4,A7,FDIFF_4:39
      .=(1+sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2) by XCMPLX_1:62
      .=(1+sin.x)/(1-(sin.x)^2) by SIN_COS:28
      .=(1+sin.x)/((1+sin.x)*(1-sin.x))
      .=(1+sin.x)/(1+sin.x)/(1-sin.x) by XCMPLX_1:78
      .=1/(1-sin.x) by A9,XCMPLX_1:60;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:18;
end;

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

theorem
  A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/
(1-sin.x)) & dom (tan+sec)=Z & Z = dom f & f|A is continuous implies integral(f
  ,A) = (tan+sec).(upper_bound A)-(tan+sec).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/(1-sin. x) and
A3: dom (tan+sec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2;
  then
A8: (tan+sec) is_differentiable_on Z by A3,Th37;
A9: for x being Element of REAL
st x in dom ((tan+sec)`|Z) holds ((tan+sec)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((tan+sec)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then ((tan+sec)`|Z).x = 1/(1-sin.x) by A3,A7,Th37
      .= f.x by A2,A10;
    hence thesis;
  end;
  dom ((tan+sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
  then ((tan+sec)`|Z) = f by A9,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;

theorem Th39:
  (Z c= dom (tan-sec) & for x st x in Z holds (1+sin.x)<>0 & (1-
sin.x)<>0) implies tan-sec is_differentiable_on Z & for x st x in Z holds ((tan
  -sec)`|Z).x = 1/(1+sin.x)
proof
  assume that
A1: Z c= dom (tan-sec) and
A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0;
  Z c= dom tan /\ dom (cos^) by A1,VALUED_1:12;
  then
A3: Z c= dom tan by XBOOLE_1:18;
  then
A4: for x st x in Z holds cos.x<>0 by FDIFF_8:1;
  then
A5: cos^ is_differentiable_on Z by FDIFF_4:39;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A3,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A6: tan is_differentiable_on Z by A3,FDIFF_1:9;
  for x st x in Z holds ((tan-sec)`|Z).x = 1/(1+sin.x)
  proof
    let x;
    assume
A7: x in Z;
    then
A8: cos.x<>0 by A3,FDIFF_8:1;
A9: 1-sin.x<>0 by A2,A7;
    ((tan-sec)`|Z).x = diff(tan,x) - diff(cos^,x) by A1,A5,A6,A7,FDIFF_1:19
      .=1/(cos.x)^2 - diff(cos^,x) by A8,FDIFF_7:46
      .=1/(cos.x)^2 - ((cos^)`|Z).x by A5,A7,FDIFF_1:def 7
      .=1/(cos.x)^2 - sin.x/(cos.x)^2 by A4,A7,FDIFF_4:39
      .=(1-sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2) by XCMPLX_1:120
      .=(1-sin.x)/(1-(sin.x)^2) by SIN_COS:28
      .=(1-sin.x)/((1+sin.x)*(1-sin.x))
      .=(1-sin.x)/(1-sin.x)/(1+sin.x) by XCMPLX_1:78
      .=1/(1+sin.x) by A9,XCMPLX_1:60;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:19;
end;

:: f.x = 1/(1+sin.x)

theorem
  A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/
(1+sin.x)) & dom (tan-sec)=Z & Z = dom f & f|A is continuous implies integral(f
  ,A) = (tan-sec).(upper_bound A)-(tan-sec).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/(1+sin. x) and
A3: dom (tan-sec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2;
  then
A8: (tan-sec) is_differentiable_on Z by A3,Th39;
A9: for x being Element of REAL st x in dom ((tan-sec)`|Z)
holds ((tan-sec)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((tan-sec)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then ((tan-sec)`|Z).x = 1/(1+sin.x) by A3,A7,Th39
      .= f.x by A2,A10;
    hence thesis;
  end;
  dom ((tan-sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
  then ((tan-sec)`|Z) = f by A9,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;

theorem Th41:
  (Z c= dom (-cot+cosec) & for x st x in Z holds (1+cos.x)<>0 & (1
-cos.x)<>0) implies -cot+cosec is_differentiable_on Z & for x st x in Z holds (
  (-cot+cosec)`|Z).x = 1/(1+cos.x)
proof
  assume that
A1: Z c= dom (-cot+cosec) and
A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0;
  Z c= dom (-cot) /\ dom (sin^) by A1,VALUED_1:def 1;
  then
A3: Z c= dom (-cot) by XBOOLE_1:18;
  then
A4: Z c= dom cot by VALUED_1:8;
  for x st x in Z holds cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A4,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
  then
A6: (-1)(#)cot is_differentiable_on Z by A3,FDIFF_1:20;
A7: for x st x in Z holds sin.x<>0 by A4,FDIFF_8:2;
  then
A8: sin^ is_differentiable_on Z by FDIFF_4:40;
  for x st x in Z holds ((-cot+cosec)`|Z).x = 1/(1+cos.x)
  proof
    let x;
    assume
A9: x in Z;
    then
A10: sin.x<>0 by A4,FDIFF_8:2;
A11: 1-cos.x<>0 by A2,A9;
    ((-cot+cosec)`|Z).x = diff(-cot,x) + diff(sin^,x) by A1,A8,A6,A9,FDIFF_1:18
      .=(((-1)(#)cot)`|Z).x + diff(sin^,x) by A6,A9,FDIFF_1:def 7
      .=(-1)*diff(cot,x) + diff(sin^,x) by A3,A5,A9,FDIFF_1:20
      .=(-1)*(-1/(sin.x)^2)+ diff(sin^,x) by A10,FDIFF_7:47
      .=1/(sin.x)^2 + ((sin^)`|Z).x by A8,A9,FDIFF_1:def 7
      .=1/(sin.x)^2 + (-cos.x/(sin.x)^2) by A7,A9,FDIFF_4:40
      .=1/(sin.x)^2 - cos.x/(sin.x)^2
      .=(1-cos.x)/((sin.x)^2+(cos.x)^2-(cos.x)^2) by XCMPLX_1:120
      .=(1-cos.x)/(1-(cos.x)^2) by SIN_COS:28
      .=(1-cos.x)/((1-cos.x)*(1+cos.x))
      .=(1-cos.x)/(1-cos.x)/(1+cos.x) by XCMPLX_1:78
      .=1/(1+cos.x) by A11,XCMPLX_1:60;
    hence thesis;
  end;
  hence thesis by A1,A8,A6,FDIFF_1:18;
end;

:: f.x = 1/(1+cos.x)

theorem
  A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/
  (1+cos.x)) & dom (-cot+cosec)=Z & Z = dom f & f|A is continuous implies
  integral(f,A) = (-cot+cosec).(upper_bound A)-(-cot+cosec).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/(1+cos. x) and
A3: dom (-cot+cosec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2;
  then
A8: (-cot+cosec) is_differentiable_on Z by A3,Th41;
A9: for x being Element of REAL
st x in dom ((-cot+cosec)`|Z) holds ((-cot+cosec)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((-cot+cosec)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then ((-cot+cosec)`|Z).x = 1/(1+cos.x) by A3,A7,Th41
      .= f.x by A2,A10;
    hence thesis;
  end;
  dom ((-cot+cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
  then ((-cot+cosec)`|Z) = f by A9,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;

theorem Th43:
  (Z c= dom (-cot-cosec) & for x st x in Z holds (1+cos.x)<>0 & (1
-cos.x)<>0) implies -cot-cosec is_differentiable_on Z & for x st x in Z holds (
  (-cot-cosec)`|Z).x = 1/(1-cos.x)
proof
  assume that
A1: Z c= dom (-cot-cosec) and
A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0;
  Z c= dom (-cot) /\ dom (sin^) by A1,VALUED_1:12;
  then
A3: Z c= dom (-cot) by XBOOLE_1:18;
  then
A4: Z c= dom cot by VALUED_1:8;
  for x st x in Z holds cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A4,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
  then
A6: (-1)(#)cot is_differentiable_on Z by A3,FDIFF_1:20;
A7: for x st x in Z holds sin.x<>0 by A4,FDIFF_8:2;
  then
A8: sin^ is_differentiable_on Z by FDIFF_4:40;
  for x st x in Z holds ((-cot-cosec)`|Z).x = 1/(1-cos.x)
  proof
    let x;
    assume
A9: x in Z;
    then
A10: sin.x<>0 by A4,FDIFF_8:2;
A11: 1+cos.x<>0 by A2,A9;
    ((-cot-cosec)`|Z).x = diff(-cot,x) - diff(sin^,x) by A1,A8,A6,A9,FDIFF_1:19
      .=(((-1)(#)cot)`|Z).x - diff(sin^,x) by A6,A9,FDIFF_1:def 7
      .=(-1)*diff(cot,x) - diff(sin^,x) by A3,A5,A9,FDIFF_1:20
      .=(-1)*(-1/(sin.x)^2)- diff(sin^,x) by A10,FDIFF_7:47
      .=1/(sin.x)^2 - ((sin^)`|Z).x by A8,A9,FDIFF_1:def 7
      .=1/(sin.x)^2 - (-cos.x/(sin.x)^2) by A7,A9,FDIFF_4:40
      .=1/(sin.x)^2 + cos.x/(sin.x)^2
      .=(1+cos.x)/((sin.x)^2+(cos.x)^2-(cos.x)^2) by XCMPLX_1:62
      .=(1+cos.x)/(1-(cos.x)^2) by SIN_COS:28
      .=(1+cos.x)/((1+cos.x)*(1-cos.x))
      .=(1+cos.x)/(1+cos.x)/(1-cos.x) by XCMPLX_1:78
      .=1/(1-cos.x) by A11,XCMPLX_1:60;
    hence thesis;
  end;
  hence thesis by A1,A8,A6,FDIFF_1:19;
end;

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

theorem
  A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/
  (1-cos.x)) & dom (-cot-cosec)=Z & Z = dom f & f|A is continuous implies
  integral(f,A) = (-cot-cosec).(upper_bound A)-(-cot-cosec).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/(1-cos. x) and
A3: dom (-cot-cosec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2;
  then
A8: (-cot-cosec) is_differentiable_on Z by A3,Th43;
A9: for x being Element of REAL
st x in dom ((-cot-cosec)`|Z) holds ((-cot-cosec)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((-cot-cosec)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then ((-cot-cosec)`|Z).x = 1/(1-cos.x) by A3,A7,Th43
      .= f.x by A2,A10;
    hence thesis;
  end;
  dom ((-cot-cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
  then ((-cot-cosec)`|Z) = f by A9,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;

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

theorem
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=1/(1+x^2)) & Z =
dom f & f|A is continuous implies integral(f,A)
 = arctan.(upper_bound A) - arctan.(lower_bound
  A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=1/(1+x^2) and
A4: Z = dom f and
A5: f|A is continuous;
A6: arctan is_differentiable_on Z by A2,SIN_COS9:81;
A7: for x being Element of REAL st x in dom ((arctan)`|Z)
holds ((arctan)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((arctan)`|Z);
    then
A8: x in Z by A6,FDIFF_1:def 7;
    then ((arctan)`|Z).x = 1/(1+x^2) by A2,SIN_COS9:81
      .= f.x by A3,A8;
    hence thesis;
  end;
  dom ((arctan)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
  then
A9: ((arctan)`|Z) = f by A7,PARTFUN1:5;
  f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
  hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:81;
end;

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

theorem
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=r/(1+x^2)) & Z =
dom f & f|A is continuous implies integral(f,A) = (r(#)arctan).(upper_bound A)
 - (r(#)
  arctan).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=r/(1+x^2) and
A4: Z = dom f and
A5: f|A is continuous;
A6: r(#)arctan is_differentiable_on Z by A2,SIN_COS9:83;
A7: for x being Element of REAL
st x in dom ((r(#)arctan)`|Z) holds ((r(#)arctan)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((r(#)arctan)`|Z);
    then
A8: x in Z by A6,FDIFF_1:def 7;
    then ((r(#)arctan)`|Z).x = r/(1+x^2) by A2,SIN_COS9:83
      .= f.x by A3,A8;
    hence thesis;
  end;
  dom ((r(#)arctan)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
  then
A9: ((r(#)arctan)`|Z) = f by A7,PARTFUN1:5;
  f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
  hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:83;
end;

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

theorem
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-1/(1+x^2)) & Z
  = dom f & f|A is continuous implies integral(f,A) = arccot.(upper_bound A)
   - arccot.(
  lower_bound A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=-1/(1+x^2) and
A4: Z = dom f and
A5: f|A is continuous;
A6: arccot is_differentiable_on Z by A2,SIN_COS9:82;
A7: for x being Element of REAL
st x in dom ((arccot)`|Z) holds ((arccot)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((arccot)`|Z);
    then
A8: x in Z by A6,FDIFF_1:def 7;
    then ((arccot)`|Z).x = -1/(1+x^2) by A2,SIN_COS9:82
      .= f.x by A3,A8;
    hence thesis;
  end;
  dom ((arccot)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
  then
A9: ((arccot)`|Z) = f by A7,PARTFUN1:5;
  f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
  hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:82;
end;

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

theorem
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-r/(1+x^2)) & Z
  = dom f & f|A is continuous implies integral(f,A)
   = (r(#)arccot).(upper_bound A) - (r
  (#)arccot).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=-r/(1+x^2) and
A4: Z = dom f and
A5: f|A is continuous;
A6: r(#)arccot is_differentiable_on Z by A2,SIN_COS9:84;
A7: for x being Element of REAL
st x in dom ((r(#)arccot)`|Z) holds ((r(#)arccot)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((r(#)arccot)`|Z);
    then
A8: x in Z by A6,FDIFF_1:def 7;
    then ((r(#)arccot)`|Z).x = -r/(1+x^2) by A2,SIN_COS9:84
      .= f.x by A3,A8;
    hence thesis;
  end;
  dom ((r(#)arccot)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
  then
A9: ((r(#)arccot)`|Z) = f by A7,PARTFUN1:5;
  f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
  hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:84;
end;

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

theorem Th49:
  (Z c= dom ((id Z)+cot-cosec) & for x st x in Z holds (1+cos.x)<>
0 & (1-cos.x)<>0) implies (id Z)+cot-cosec is_differentiable_on Z & for x st x
  in Z holds ((id Z+cot-cosec)`|Z).x = cos.x/(1+cos.x)
proof
  assume that
A1: Z c= dom ((id Z)+cot-cosec) and
A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0;
A3: Z c= dom ((id Z)+cot) /\ dom cosec by A1,VALUED_1:12;
  then
A4: Z c= dom (id Z+cot) by XBOOLE_1:18;
  then
 Z c= dom id Z /\ dom cot by VALUED_1:def 1;
  then
A5: Z c= dom cot by XBOOLE_1:18;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A7: Z c= dom id Z;
  then
A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23;
  for x st x in Z holds cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A5,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A9: cot is_differentiable_on Z by A5,FDIFF_1:9;
  then
A10: id Z + cot is_differentiable_on Z by A4,A8,FDIFF_1:18;
A11: Z c= dom cosec by A3,XBOOLE_1:18;
  then
A12: cosec is_differentiable_on Z by FDIFF_9:5;
A13: for x st x in Z holds (((id Z) + cot)`|Z).x = -(cos.x)^2/(sin.x)^2
  proof
    let x;
    assume
A14: x in Z;
    then
A15: sin.x<>0 by A5,FDIFF_8:2;
    then
A16: (sin.x)^2 >0 by SQUARE_1:12;
    ((id Z + cot)`|Z).x = diff((id Z),x) + diff(cot,x) by A4,A9,A8,A14,
FDIFF_1:18
      .=((id Z)`|Z).x + diff(cot,x) by A8,A14,FDIFF_1:def 7
      .=1+diff(cot,x) by A7,A6,A14,FDIFF_1:23
      .=1+(-1/(sin.x)^2) by A15,FDIFF_7:47
      .=1-1/(sin.x)^2
      .=(sin.x)^2/(sin.x)^2-1/(sin.x)^2 by A16,XCMPLX_1:60
      .=((sin.x)^2-1)/(sin.x)^2 by XCMPLX_1:120
      .=((sin.x)^2-((sin.x)^2+(cos.x)^2))/(sin.x)^2 by SIN_COS:28
      .=(-(cos.x)^2)/(sin.x)^2
      .=-(cos.x)^2/(sin.x)^2 by XCMPLX_1:187;
    hence thesis;
  end;
  for x st x in Z holds ((id Z + cot-cosec)`|Z).x = cos.x/(1+cos.x)
  proof
    let x;
    assume
A17: x in Z;
    then
A18: 1-cos.x<>0 by A2;
    ((id Z + cot-cosec)`|Z).x=diff((id Z + cot),x) -diff(cosec,x) by A1,A12,A10
,A17,FDIFF_1:19
      .=((id Z + cot)`|Z).x-diff(cosec,x) by A10,A17,FDIFF_1:def 7
      .=-(cos.x)^2/(sin.x)^2-diff(cosec,x) by A13,A17
      .=-(cos.x)^2/(sin.x)^2-((cosec)`|Z).x by A12,A17,FDIFF_1:def 7
      .=-(cos.x)^2/(sin.x)^2-(-cos.x/(sin.x)^2) by A11,A17,FDIFF_9:5
      .=cos.x/(sin.x)^2-(cos.x)^2/(sin.x)^2
      .=(cos.x-(cos.x)*(cos.x))/(sin.x)^2 by XCMPLX_1:120
      .=cos.x*(1-cos.x)/((sin.x)^2+(cos.x)^2-(cos.x)^2)
      .=cos.x*(1-cos.x)/(1-(cos.x)^2) by SIN_COS:28
      .=cos.x*(1-cos.x)/((1-cos.x)*(1+cos.x))
      .=cos.x*(1-cos.x)/(1-cos.x)/(1+cos.x) by XCMPLX_1:78
      .=cos.x*((1-cos.x)/(1-cos.x))/(1+cos.x) by XCMPLX_1:74
      .=cos.x*1/(1+cos.x) by A18,XCMPLX_1:60
      .=cos.x/(1+cos.x);
    hence thesis;
  end;
  hence thesis by A1,A12,A10,FDIFF_1:19;
end;

:: f.x = cos.x/(1+cos.x)

theorem
  A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x =
  cos.x/(1+cos.x)) & dom (id Z+cot-cosec)=Z & Z = dom f & f|A is continuous
  implies integral(f,A) =
   (id Z+cot-cosec).(upper_bound A)-(id Z+cot-cosec).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = cos.x/(1+
  cos.x) and
A3: dom (id Z+cot-cosec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2;
  then
A8: (id Z+cot-cosec) is_differentiable_on Z by A3,Th49;
A9: for x being Element of REAL
st x in dom ((id Z+cot-cosec)`|Z) holds ((id Z+cot-cosec)`|Z).x = f
  .x
  proof
    let x be Element of REAL;
    assume x in dom ((id Z+cot-cosec)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then ((id Z+cot-cosec)`|Z).x = cos.x/(1+cos.x) by A3,A7,Th49
      .= f.x by A2,A10;
    hence thesis;
  end;
  dom ((id Z+cot-cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
  then ((id Z+cot-cosec)`|Z) = f by A9,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;

:: f.x = x+cot.x+cosec.x

theorem Th51:
  (Z c= dom ((id Z)+cot+cosec) & for x st x in Z holds (1+cos.x)<>
0 & (1-cos.x)<>0) implies (id Z)+cot+cosec is_differentiable_on Z & for x st x
  in Z holds ((id Z+cot+cosec)`|Z).x = cos.x/(cos.x-1)
proof
  assume that
A1: Z c= dom ((id Z)+cot+cosec) and
A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0;
A3: Z c= dom ((id Z)+cot) /\ dom cosec by A1,VALUED_1:def 1;
  then
A4: Z c= dom (id Z+cot) by XBOOLE_1:18;
  then
 Z c= dom id Z /\ dom cot by VALUED_1:def 1;
  then
A5: Z c= dom cot by XBOOLE_1:18;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A7: Z c= dom id Z;
  then
A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23;
  for x st x in Z holds cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A5,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A9: cot is_differentiable_on Z by A5,FDIFF_1:9;
  then
A10: id Z + cot is_differentiable_on Z by A4,A8,FDIFF_1:18;
A11: Z c= dom cosec by A3,XBOOLE_1:18;
  then
A12: cosec is_differentiable_on Z by FDIFF_9:5;
A13: for x st x in Z holds (((id Z) + cot)`|Z).x = -(cos.x)^2/(sin.x)^2
  proof
    let x;
    assume
A14: x in Z;
    then
A15: sin.x<>0 by A5,FDIFF_8:2;
    then
A16: (sin.x)^2 >0 by SQUARE_1:12;
    ((id Z + cot)`|Z).x = diff((id Z),x) + diff(cot,x) by A4,A9,A8,A14,
FDIFF_1:18
      .=((id Z)`|Z).x + diff(cot,x) by A8,A14,FDIFF_1:def 7
      .=1+diff(cot,x) by A7,A6,A14,FDIFF_1:23
      .=1+(-1/(sin.x)^2) by A15,FDIFF_7:47
      .=1-1/(sin.x)^2
      .=(sin.x)^2/(sin.x)^2-1/(sin.x)^2 by A16,XCMPLX_1:60
      .=((sin.x)^2-1)/(sin.x)^2 by XCMPLX_1:120
      .=((sin.x)^2-((sin.x)^2+(cos.x)^2))/(sin.x)^2 by SIN_COS:28
      .=(-(cos.x)^2)/(sin.x)^2
      .=-(cos.x)^2/(sin.x)^2 by XCMPLX_1:187;
    hence thesis;
  end;
  for x st x in Z holds ((id Z + cot+cosec)`|Z).x = cos.x/(cos.x-1)
  proof
    let x;
    assume
A17: x in Z;
    then
A18: 1+cos.x<>0 by A2;
    ((id Z + cot+cosec)`|Z).x=diff((id Z + cot),x) +diff(cosec,x) by A1,A12,A10
,A17,FDIFF_1:18
      .=((id Z + cot)`|Z).x+diff(cosec,x) by A10,A17,FDIFF_1:def 7
      .=-(cos.x)^2/(sin.x)^2+diff(cosec,x) by A13,A17
      .=-(cos.x)^2/(sin.x)^2+((cosec)`|Z).x by A12,A17,FDIFF_1:def 7
      .=-(cos.x)^2/(sin.x)^2+(-cos.x/(sin.x)^2) by A11,A17,FDIFF_9:5
      .=-((cos.x)^2/(sin.x)^2+cos.x/(sin.x)^2)
      .=-((cos.x)*(cos.x)+cos.x)/(sin.x)^2 by XCMPLX_1:62
      .=-(cos.x)*(cos.x+1)/((sin.x)^2+(cos.x)^2-(cos.x)^2)
      .=-(cos.x)*(cos.x+1)/(1-(cos.x)^2) by SIN_COS:28
      .=-(cos.x)*(cos.x+1)/((1+cos.x)*(1-cos.x))
      .=-(cos.x)*(cos.x+1)/(1+cos.x)/(1-cos.x) by XCMPLX_1:78
      .=-(cos.x)*((1+cos.x)/(1+cos.x))/(1-cos.x) by XCMPLX_1:74
      .=-(cos.x)*1/(1-cos.x) by A18,XCMPLX_1:60
      .=(cos.x)/(-(1-cos.x)) by XCMPLX_1:188
      .=(cos.x)/(cos.x-1);
    hence thesis;
  end;
  hence thesis by A1,A12,A10,FDIFF_1:18;
end;

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

theorem
  A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x =
  cos.x/(cos.x-1)) & dom (id Z+cot+cosec)=Z & Z = dom f & f|A is continuous
  implies integral(f,A) =
   (id Z+cot+cosec).(upper_bound A)-(id Z+cot+cosec).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = cos.x/(
  cos.x-1) and
A3: dom (id Z+cot+cosec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2;
  then
A8: (id Z+cot+cosec) is_differentiable_on Z by A3,Th51;
A9: for x being Element of REAL
st x in dom ((id Z+cot+cosec)`|Z) holds ((id Z+cot+cosec)`|Z).x = f
  .x
  proof
    let x be Element of REAL;
    assume x in dom ((id Z+cot+cosec)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then ((id Z+cot+cosec)`|Z).x = cos.x/(cos.x-1) by A3,A7,Th51
      .= f.x by A2,A10;
    hence thesis;
  end;
  dom ((id Z+cot+cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
  then ((id Z+cot+cosec)`|Z) = f by A9,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;

:: f.x = x-tan.x+sec.x

theorem Th53:
  (Z c= dom (id Z-tan+sec) & for x st x in Z holds (1+sin.x)<>0 &
  (1-sin.x)<>0) implies (id Z)-tan+sec is_differentiable_on Z & for x st x in Z
  holds ((id Z-tan+sec)`|Z).x = sin.x/(sin.x+1)
proof
  assume that
A1: Z c= dom (id Z-tan+sec) and
A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0;
A3: Z c= dom (id Z-tan) /\ dom sec by A1,VALUED_1:def 1;
  then
A4: Z c= dom (id Z-tan) by XBOOLE_1:18;
  then
A5: Z c= dom id Z /\ dom tan by VALUED_1:12;
A6: Z c= dom (id Z);
A7: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
  then
A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23;
A9: Z c= dom tan by A5,XBOOLE_1:18;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A9,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A10: tan is_differentiable_on Z by A9,FDIFF_1:9;
  then
A11: id Z-tan is_differentiable_on Z by A4,A8,FDIFF_1:19;
A12: Z c= dom sec by A3,XBOOLE_1:18;
  then
A13: sec is_differentiable_on Z by FDIFF_9:4;
A14: for x st x in Z holds ((id Z - tan)`|Z).x = -(sin.x)^2/(cos.x)^2
  proof
    let x;
    assume
A15: x in Z;
    then
A16: cos.x<>0 by A9,FDIFF_8:1;
    then
A17: (cos.x)^2 >0 by SQUARE_1:12;
    ((id Z - tan)`|Z).x = diff(id Z,x) - diff(tan,x) by A4,A10,A8,A15,
FDIFF_1:19
      .=((id Z)`|Z).x - diff(tan,x) by A8,A15,FDIFF_1:def 7
      .=1-diff(tan,x) by A6,A7,A15,FDIFF_1:23
      .=1-1/(cos.x)^2 by A16,FDIFF_7:46
      .=1-((cos.x)^2+(sin.x)^2)/(cos.x)^2 by SIN_COS:28
      .=1-((cos.x)^2/(cos.x)^2+(sin.x)^2/(cos.x)^2) by XCMPLX_1:62
      .=1-(1+(sin.x)^2/(cos.x)^2) by A17,XCMPLX_1:60
      .=-(sin.x)^2/(cos.x)^2;
    hence thesis;
  end;
  for x st x in Z holds ((id Z-tan+sec)`|Z).x = sin.x/(sin.x+1)
  proof
    let x;
    assume
A18: x in Z;
    then
A19: 1-sin.x<>0 by A2;
    ((id Z-tan+sec)`|Z).x=diff((id Z-tan),x) +diff(sec,x) by A1,A13,A11,A18,
FDIFF_1:18
      .=((id Z-tan)`|Z).x+diff(sec,x) by A11,A18,FDIFF_1:def 7
      .=-(sin.x)^2/(cos.x)^2+diff(sec,x) by A14,A18
      .=-(sin.x)^2/(cos.x)^2+((sec)`|Z).x by A13,A18,FDIFF_1:def 7
      .=-(sin.x)^2/(cos.x)^2+sin.x/(cos.x)^2 by A12,A18,FDIFF_9:4
      .=sin.x/(cos.x)^2-(sin.x)^2/(cos.x)^2
      .=(sin.x-(sin.x)*(sin.x))/(cos.x)^2 by XCMPLX_1:120
      .=(sin.x)*(1-sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2)
      .=(sin.x)*(1-sin.x)/(1-(sin.x)^2) by SIN_COS:28
      .=(sin.x)*(1-sin.x)/((1-sin.x)*(1+sin.x))
      .=(sin.x)*(1-sin.x)/(1-sin.x)/(1+sin.x) by XCMPLX_1:78
      .=(sin.x)*((1-sin.x)/(1-sin.x))/(1+sin.x) by XCMPLX_1:74
      .=(sin.x)*1/(1+sin.x) by A19,XCMPLX_1:60
      .=sin.x/(1+sin.x);
    hence thesis;
  end;
  hence thesis by A1,A13,A11,FDIFF_1:18;
end;

:: f.x = sin.x/(1+sin.x)

theorem
  A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x =
  sin.x/(1+sin.x)) & Z c= dom (id Z-tan+sec) & Z = dom f & f|A is continuous
  implies integral(f,A) =
   (id Z-tan+sec).(upper_bound A)-(id Z-tan+sec).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = sin.x/(1+
  sin.x) and
A3: Z c= dom (id Z-tan+sec) and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2;
  then
A8: (id Z-tan+sec) is_differentiable_on Z by A3,Th53;
A9: for x being Element of REAL
st x in dom ((id Z-tan+sec)`|Z) holds ((id Z-tan+sec)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((id Z-tan+sec)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then ((id Z-tan+sec)`|Z).x = sin.x/(1+sin.x) by A3,A7,Th53
      .= f.x by A2,A10;
    hence thesis;
  end;
  dom ((id Z-tan+sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
  then ((id Z-tan+sec)`|Z) = f by A9,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;

:: f.x = x-tan.x-sec.x

theorem Th55:
  (Z c= dom (id Z-tan-sec) & for x st x in Z holds (1+sin.x)<>0 &
  (1-sin.x)<>0) implies id Z-tan-sec is_differentiable_on Z & for x st x in Z
  holds ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1)
proof
  assume that
A1: Z c= dom (id Z-tan-sec) and
A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0;
A3: Z c= dom (id Z-tan) /\ dom sec by A1,VALUED_1:12;
  then
A4: Z c= dom (id Z-tan) by XBOOLE_1:18;
  then
 Z c= dom id Z /\ dom tan by VALUED_1:12;
  then
A5: Z c= dom tan by XBOOLE_1:18;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A7: Z c= dom id Z;
  then
A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A5,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A9: tan is_differentiable_on Z by A5,FDIFF_1:9;
  then
A10: id Z-tan is_differentiable_on Z by A4,A8,FDIFF_1:19;
A11: Z c= dom sec by A3,XBOOLE_1:18;
  then
A12: sec is_differentiable_on Z by FDIFF_9:4;
A13: for x st x in Z holds ((id Z-tan)`|Z).x = -(sin.x)^2/(cos.x)^2
  proof
    let x;
    assume
A14: x in Z;
    then
A15: cos.x<>0 by A5,FDIFF_8:1;
    then
A16: (cos.x)^2 >0 by SQUARE_1:12;
    ((id Z - tan)`|Z).x = diff(id Z,x) - diff(tan,x) by A4,A9,A8,A14,FDIFF_1:19
      .=((id Z)`|Z).x - diff(tan,x) by A8,A14,FDIFF_1:def 7
      .=1-diff(tan,x) by A7,A6,A14,FDIFF_1:23
      .=1-1/(cos.x)^2 by A15,FDIFF_7:46
      .=1-((cos.x)^2+(sin.x)^2)/(cos.x)^2 by SIN_COS:28
      .=1-((cos.x)^2/(cos.x)^2+(sin.x)^2/(cos.x)^2) by XCMPLX_1:62
      .=1-(1+(sin.x)^2/(cos.x)^2) by A16,XCMPLX_1:60
      .=-(sin.x)^2/(cos.x)^2;
    hence thesis;
  end;
  for x st x in Z holds ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1)
  proof
    let x;
    assume
A17: x in Z;
    then
A18: 1+sin.x<>0 by A2;
    ((id Z-tan-sec)`|Z).x=diff((id Z-tan),x) -diff(sec,x) by A1,A12,A10,A17,
FDIFF_1:19
      .=((id Z-tan)`|Z).x-diff(sec,x) by A10,A17,FDIFF_1:def 7
      .=-(sin.x)^2/(cos.x)^2-diff(sec,x) by A13,A17
      .=-(sin.x)^2/(cos.x)^2-((sec)`|Z).x by A12,A17,FDIFF_1:def 7
      .=-(sin.x)^2/(cos.x)^2-sin.x/(cos.x)^2 by A11,A17,FDIFF_9:4
      .=-(sin.x/(cos.x)^2+(sin.x)^2/(cos.x)^2)
      .=-((sin.x+(sin.x)^2)/(cos.x)^2) by XCMPLX_1:62
      .=-(sin.x)*(1+sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2)
      .=-(sin.x)*(1+sin.x)/(1-(sin.x)^2) by SIN_COS:28
      .=-(sin.x)*(1+sin.x)/((1+sin.x)*(1-sin.x))
      .=-(sin.x)*(1+sin.x)/(1+sin.x)/(1-sin.x) by XCMPLX_1:78
      .=-(sin.x)*((1+sin.x)/(1+sin.x))/(1-sin.x) by XCMPLX_1:74
      .=-(sin.x)*1/(1-sin.x) by A18,XCMPLX_1:60
      .=sin.x/(-(1-sin.x)) by XCMPLX_1:188
      .=sin.x/(sin.x-1);
    hence thesis;
  end;
  hence thesis by A1,A12,A10,FDIFF_1:19;
end;

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

theorem
  A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x =
  sin.x/(sin.x-1)) & Z c= dom (id Z-tan-sec) & Z = dom f & f|A is continuous
  implies integral(f,A) =
   (id Z-tan-sec).(upper_bound A)-(id Z-tan-sec).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = sin.x/(
  sin.x-1) and
A3: Z c= dom (id Z-tan-sec) and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2;
  then
A8: (id Z-tan-sec) is_differentiable_on Z by A3,Th55;
A9: for x being Element of REAL
st x in dom ((id Z-tan-sec)`|Z) holds ((id Z-tan-sec)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((id Z-tan-sec)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1) by A3,A7,Th55
      .= f.x by A2,A10;
    hence thesis;
  end;
  dom ((id Z-tan-sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
  then ((id Z-tan-sec)`|Z) = f by A9,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;

:: f.x = tan.x-x

theorem Th57:
  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=(tan.x)^2
proof
A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
  assume
A2: Z c= dom (tan-id Z);
  then
 Z c= dom tan /\ dom (id Z) by VALUED_1:12;
  then
A3: Z c= dom tan by XBOOLE_1:18;
A4: Z c= dom (id Z);
  then
A5: id Z is_differentiable_on Z by A1,FDIFF_1:23;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A3,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A6: tan is_differentiable_on Z by A3,FDIFF_1:9;
  for x st x in Z holds ((tan-id Z)`|Z).x=(tan.x)^2
  proof
    let x;
    assume
A7: x in Z;
    then
A8: cos.x<>0 by A3,FDIFF_8:1;
    then
A9: (cos.x)^2 >0 by SQUARE_1:12;
    ((tan-id Z)`|Z).x= diff(tan,x) - diff(id Z,x) by A2,A5,A6,A7,FDIFF_1:19
      .=1/(cos.x)^2-diff(id Z,x) by A8,FDIFF_7:46
      .=1/(cos.x)^2-((id Z)`|Z).x by A5,A7,FDIFF_1:def 7
      .=1/(cos.x)^2-1 by A4,A1,A7,FDIFF_1:23
      .=1/(cos.x)^2-(cos.x)^2/(cos.x)^2 by A9,XCMPLX_1:60
      .=(1-(cos.x)^2)/(cos.x)^2 by XCMPLX_1:120
      .=((sin.x)^2+(cos.x)^2-(cos.x)^2)/(cos.x)^2 by SIN_COS:28
      .=(sin(x)/cos(x))*((sin.x)/(cos.x)) by XCMPLX_1:76
      .=(tan.x)*tan(x) by A3,A7,FDIFF_8:1,SIN_COS9:15
      .=(tan.x)^2 by A3,A7,FDIFF_8:1,SIN_COS9:15;
    hence thesis;
  end;
  hence thesis by A2,A5,A6,FDIFF_1:19;
end;

:: f.x = (tan.x)^2

theorem
  A c= Z & (for x st x in Z holds cos.x >0 & f.x = (tan.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 that
A1: A c= Z and
A2: for x st x in Z holds cos.x >0 & f.x = (tan.x)^2 and
A3: Z c= dom (tan-id Z) and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: (tan-id Z) is_differentiable_on Z by A3,Th57;
A8: for x being Element of REAL
st x in dom ((tan-id Z)`|Z) holds ((tan-id Z)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((tan-id Z)`|Z);
    then
A9: x in Z by A7,FDIFF_1:def 7;
    then ((tan-id Z)`|Z).x = (tan.x)^2 by A3,Th57
      .= f.x by A2,A9;
    hence thesis;
  end;
  dom ((tan-id Z)`|Z) = dom f by A4,A7,FDIFF_1:def 7;
  then ((tan-id Z)`|Z) = f by A8,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13;
end;

:: f.x = -cot.x-x

theorem Th59:
  Z c= dom (-cot-id Z) implies -cot-id Z is_differentiable_on Z &
  for x st x in Z holds ((-cot-id Z)`|Z).x = (cot.x)^2
proof
  set f = -cot;
A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
  assume
A2: Z c= dom (-cot-id Z);
  then
 Z c= dom (-cot) /\ dom (id Z) by VALUED_1:12;
  then
A3: Z c= dom (-cot) by XBOOLE_1:18;
  then
A4: Z c= dom cot by VALUED_1:8;
  for x st x in Z holds cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A4,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
  then
A6: (-1)(#)cot is_differentiable_on Z by A3,FDIFF_1:20;
A7: Z c= dom (id Z);
  then
A8: id Z is_differentiable_on Z by A1,FDIFF_1:23;
  for x st x in Z holds ((-cot-id Z)`|Z).x = (cot.x)^2
  proof
    let x;
    assume
A9: x in Z;
    then
A10: sin.x<>0 by A4,FDIFF_8:2;
    then
A11: (sin.x)^2 >0 by SQUARE_1:12;
    ((f-id Z)`|Z).x=diff(f,x) - diff(id Z,x) by A2,A8,A6,A9,FDIFF_1:19
      .=(((-1)(#)cot)`|Z).x-diff(id Z,x) by A6,A9,FDIFF_1:def 7
      .=(-1)*diff(cot,x)-diff(id Z,x) by A3,A5,A9,FDIFF_1:20
      .=(-1)*(-1/(sin.x)^2)-diff(id Z,x) by A10,FDIFF_7:47
      .=1/(sin.x)^2-((id Z)`|Z).x by A8,A9,FDIFF_1:def 7
      .=1/(sin.x)^2-1 by A7,A1,A9,FDIFF_1:23
      .=1/(sin.x)^2-(sin.x)^2/(sin.x)^2 by A11,XCMPLX_1:60
      .=(1-(sin.x)^2)/(sin.x)^2 by XCMPLX_1:120
      .=((cos.x)^2+(sin.x)^2-(sin.x)^2)/(sin.x)^2 by SIN_COS:28
      .=(cos(x)/sin(x))*((cos.x)/(sin.x)) by XCMPLX_1:76
      .=(cot.x)*cot(x) by A4,A9,FDIFF_8:2,SIN_COS9:16
      .=(cot.x)^2 by A4,A9,FDIFF_8:2,SIN_COS9:16;
    hence thesis;
  end;
  hence thesis by A2,A8,A6,FDIFF_1:19;
end;

:: f.x = (cot.x)^2

theorem
  A c= Z & (for x st x in Z holds sin.x >0 & f.x = (cot.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 that
A1: A c= Z and
A2: for x st x in Z holds sin.x >0 & f.x = (cot.x)^2 and
A3: Z c= dom (-cot-id Z) and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: (-cot-id Z) is_differentiable_on Z by A3,Th59;
A8: for x being Element of REAL
st x in dom ((-cot-id Z)`|Z) holds ((-cot-id Z)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((-cot-id Z)`|Z);
    then
A9: x in Z by A7,FDIFF_1:def 7;
    then ((-cot-id Z)`|Z).x = (cot.x)^2 by A3,Th59
      .= f.x by A2,A9;
    hence thesis;
  end;
  dom ((-cot-id Z)`|Z) = dom f by A4,A7,FDIFF_1:def 7;
  then ((-cot-id Z)`|Z) = f by A8,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13;
end;

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

theorem
  A c= Z & (for x st x in Z holds f.x = 1/(cos.x)^2 & cos.x <> 0) & dom
tan=Z & Z = dom f & f|A is continuous implies
 integral(f,A) = tan.(upper_bound A)-tan.(
  lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds f.x = 1/(cos.x)^2 & cos.x <> 0 and
A3: dom tan=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: tan is_differentiable_on Z by A3,INTEGRA8:33;
A8: for x being Element of REAL st x in dom (tan`|Z) holds (tan`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom (tan`|Z);
    then
A9: x in Z by A7,FDIFF_1:def 7;
    then (tan`|Z).x = 1/(cos.x)^2 by A3,INTEGRA8:33
      .= f.x by A2,A9;
    hence thesis;
  end;
  dom (tan`|Z) = dom f by A4,A7,FDIFF_1:def 7;
  then (tan`|Z) = f by A8,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13;
end;

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

theorem
  A c= Z & (for x st x in Z holds f.x = -1/(sin.x)^2 & sin.x <> 0) & dom
cot=Z & Z = dom f & f|A is continuous implies
 integral(f,A) = cot.(upper_bound A)-cot.(
  lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds f.x = -1/(sin.x)^2 & sin.x <> 0 and
A3: dom cot=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: cot is_differentiable_on Z by A3,INTEGRA8:34;
A8: for x being Element of REAL st x in dom (cot`|Z) holds (cot`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom (cot`|Z);
    then
A9: x in Z by A7,FDIFF_1:def 7;
    then (cot`|Z).x = -1/(sin.x)^2 by A3,INTEGRA8:34
      .= f.x by A2,A9;
    hence thesis;
  end;
  dom (cot`|Z) = dom f by A4,A7,FDIFF_1:def 7;
  then (cot`|Z) = f by A8,PARTFUN1:5;
  hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13;
end;

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

theorem
  A c= Z & (for x st x in Z holds f.x = (sin.x-(cos.x)^2)/(cos.x)^2) & Z
c= dom (sec-id Z) & Z = dom f & f|A is continuous implies integral(f,A) = (sec-
  id Z).(upper_bound A)-(sec-id Z).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds f.x = (sin.x-(cos.x)^2)/(cos.x)^2 and
A3: Z c= dom (sec-id Z) and
A4: Z = dom f and
A5: f|A is continuous;
A6: (sec-id Z) is_differentiable_on Z by A3,FDIFF_9:22;
A7: for x being Element of REAL
st x in dom ((sec-id Z)`|Z) holds ((sec-id Z)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((sec-id Z)`|Z);
    then
A8: x in Z by A6,FDIFF_1:def 7;
    then ((sec-id Z)`|Z).x = (sin.x-(cos.x)^2)/(cos.x)^2 by A3,FDIFF_9:22
      .= f.x by A2,A8;
    hence thesis;
  end;
  dom ((sec-id Z)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
  then
A9: ((sec-id Z)`|Z) = f by A7,PARTFUN1:5;
  f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
  hence thesis by A1,A3,A9,FDIFF_9:22,INTEGRA5:13;
end;

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

theorem
  A c= Z & (for x st x in Z holds f.x = (cos.x-(sin.x)^2)/(sin.x)^2) & Z
c= dom (-cosec-id Z) & Z = dom f & f|A is continuous implies integral(f,A) =(-
  cosec-id Z).(upper_bound A)-(-cosec-id Z).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: for x st x in Z holds f.x = (cos.x-(sin.x)^2)/(sin.x)^2 and
A3: Z c= dom (-cosec-id Z) and
A4: Z = dom f and
A5: f|A is continuous;
A6: (-cosec-id Z) is_differentiable_on Z by A3,FDIFF_9:23;
A7: for x being Element of REAL
st x in dom ((-cosec-id Z)`|Z) holds ((-cosec-id Z)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((-cosec-id Z)`|Z);
    then
A8: x in Z by A6,FDIFF_1:def 7;
    then ((-cosec-id Z)`|Z).x = (cos.x-(sin.x)^2)/(sin.x)^2 by A3,FDIFF_9:23
      .= f.x by A2,A8;
    hence thesis;
  end;
  dom ((-cosec-id Z)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
  then
A9: ((-cosec-id Z)`|Z) = f by A7,PARTFUN1:5;
  f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
  hence thesis by A1,A3,A9,FDIFF_9:23,INTEGRA5:13;
end;

:: f.x = cot(x)

theorem
  A c= Z & (for x st x in Z holds sin.x >0) & Z c= dom (ln*sin) & Z =
  dom cot & cot|A is continuous implies
   integral(cot,A) = (ln*sin).(upper_bound A)-(ln*
  sin).(lower_bound A)
proof
  set f = cot;
  assume that
A1: A c= Z and
A2: for x st x in Z holds sin.x >0 and
A3: Z c= dom (ln*sin) and
A4: Z = dom cot and
A5: f|A is continuous;
A6: (ln*sin) is_differentiable_on Z by A2,A3,FDIFF_4:43;
A7: for x being Element of REAL
st x in dom ((ln*sin)`|Z) holds ((ln*sin)`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom ((ln*sin)`|Z);
    then
A8: x in Z by A6,FDIFF_1:def 7;
    then
A9: sin.x <> 0 by A2;
    ((ln*sin)`|Z).x = cot(x) by A2,A3,A8,FDIFF_4:43
      .= f.x by A9,SIN_COS9:16;
    hence thesis;
  end;
  dom ((ln*sin)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
  then
A10: ((ln*sin)`|Z) = f by A7,PARTFUN1:5;
  f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
  hence thesis by A1,A2,A3,A10,FDIFF_4:43,INTEGRA5:13;
end;

:: f.x = arcsin.x / sqrt(1-x^2)

theorem
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=arcsin.x/sqrt(1-
  x^2)) & Z c= dom ((1/2)(#)(( #Z 2)*(arcsin))) & Z = dom f & f|A is continuous
implies integral(f,A) = ((1/2)(#)(( #Z 2)*(arcsin))).(upper_bound A)
 -((1/2)(#)(( #Z 2)
  *(arcsin))).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=arcsin.x/sqrt(1-x^2) and
A4: Z c= dom ((1/2)(#)(( #Z 2)*(arcsin))) and
A5: Z = dom f and
A6: f|A is continuous;
A7: ((1/2)(#)(( #Z 2)*(arcsin))) is_differentiable_on Z by A2,A4,FDIFF_7:12;
A8: for x being Element of REAL
st x in dom (((1/2)(#)(( #Z 2)*(arcsin)))`|Z) holds (((1/2)(#)(( #Z
  2)*(arcsin)))`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom (((1/2)(#)(( #Z 2)*(arcsin)))`|Z);
    then
A9: x in Z by A7,FDIFF_1:def 7;
    then
    (((1/2)(#)(( #Z 2)*(arcsin)))`|Z).x = arcsin.x / sqrt(1-x^2) by A2,A4,
FDIFF_7:12
      .= f.x by A3,A9;
    hence thesis;
  end;
  dom (((1/2)(#)(( #Z 2)*(arcsin)))`|Z) = dom f by A5,A7,FDIFF_1:def 7;
  then
A10: (((1/2)(#)(( #Z 2)*(arcsin)))`|Z) = f by A8,PARTFUN1:5;
  f is_integrable_on A & f|A is bounded by A1,A5,A6,INTEGRA5:10,11;
  hence thesis by A1,A2,A4,A10,FDIFF_7:12,INTEGRA5:13;
end;

:: f.x = -arccos.x / sqrt(1-x^2)

theorem
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-arccos.x / sqrt
  (1-x^2)) & Z c= dom ((1/2)(#)(( #Z 2)*(arccos))) & Z = dom f & f|A is
continuous implies integral(f,A) = ((1/2)(#)(( #Z 2)*(arccos))).(upper_bound A)
 -((1/2)
  (#)(( #Z 2)*(arccos))).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=-arccos.x / sqrt(1-x^2) and
A4: Z c= dom ((1/2)(#)(( #Z 2)*(arccos))) and
A5: Z = dom f and
A6: f|A is continuous;
A7: ((1/2)(#)(( #Z 2)*(arccos))) is_differentiable_on Z by A2,A4,FDIFF_7:13;
A8: for x being Element of REAL
st x in dom (((1/2)(#)(( #Z 2)*(arccos)))`|Z) holds (((1/2)(#)(( #Z
  2)*(arccos)))`|Z).x = f.x
  proof
    let x be Element of REAL;
    assume x in dom (((1/2)(#)(( #Z 2)*(arccos)))`|Z);
    then
A9: x in Z by A7,FDIFF_1:def 7;
    then (((1/2)(#)(( #Z 2)*(arccos)))`|Z).x = -arccos.x / sqrt(1-x^2) by A2,A4
,FDIFF_7:13
      .= f.x by A3,A9;
    hence thesis;
  end;
  dom (((1/2)(#)(( #Z 2)*(arccos)))`|Z) = dom f by A5,A7,FDIFF_1:def 7;
  then
A10: (((1/2)(#)(( #Z 2)*(arccos)))`|Z) = f by A8,PARTFUN1:5;
  f is_integrable_on A & f|A is bounded by A1,A5,A6,INTEGRA5:10,11;
  hence thesis by A1,A2,A4,A10,FDIFF_7:13,INTEGRA5:13;
end;

:: f.x = arcsin.x

theorem
  A c= Z & Z c= ]. -1,1 .[ & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds
f1.x=1 & f.x >0 & x<>0) & dom arcsin=Z & Z c= dom ((id Z)(#)(arcsin)+( #R (1/2)
)*f) implies integral(arcsin,A) =
 ((id Z)(#)(arcsin)+( #R (1/2))*f).(upper_bound A) -((
  id Z)(#)(arcsin) + ( #R (1/2))*f).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ & f=f1-f2 &( f2=#Z 2 & for x st x in Z holds f1.x=1
  & f.x >0 & x<>0 ) and
A3: dom arcsin=Z and
A4: Z c= dom ((id Z)(#)(arcsin)+( #R (1/2))*f);
A5: arcsin|A is bounded by A1,A3,INTEGRA5:10;
A6: ((id Z)(#)(arcsin)+( #R (1/2))*f) is_differentiable_on Z by A2,A4,
FDIFF_7:23;
A7: for x being Element of REAL
st x in dom (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z) holds (((id Z)
  (#)(arcsin)+( #R (1/2))*f)`|Z).x = arcsin.x
  proof
    let x be Element of REAL;
    assume x in dom (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z);
    then x in Z by A6,FDIFF_1:def 7;
    hence thesis by A2,A4,FDIFF_7:23;
  end;
  dom (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z) = dom arcsin by A3,A6,
FDIFF_1:def 7;
  then (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z) = arcsin by A7,PARTFUN1:5;
  hence thesis by A1,A3,A5,A6,INTEGRA5:11,13;
end;

:: f.x = arcsin.(x/a)

theorem
  A c= Z & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & f.x >0
  & f3.x=x/a & f3.x > -1 & f3.x < 1 & x<>0 & a>0) & dom ((arcsin)*f3)=Z & Z c=
  dom ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) & ((arcsin)*f3)|A is continuous
implies integral((arcsin)*f3,A) =
 ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f).(upper_bound A
  ) -((id Z)(#)((arcsin)*f3)+( #R (1/2))*f).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: f=f1-f2 & f2=#Z 2 and
A3: for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3
  .x < 1 & x<>0 & a>0 and
A4: dom ((arcsin)*f3)=Z and
A5: Z c= dom ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) and
A6: ((arcsin)*f3)|A is continuous;
A7: (arcsin)*f3 is_integrable_on A by A1,A4,A6,INTEGRA5:11;
A8: ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) is_differentiable_on Z by A2,A3,A5,
FDIFF_7:28;
A9: for x being Element of REAL
st x in dom (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z) holds (((id
  Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z).x = ((arcsin)*f3).x
  proof
    let x be Element of REAL;
    assume x in dom (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then
    (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z).x = arcsin.(x/a) by A2,A3,A5,
FDIFF_7:28
      .= arcsin.(f3.x) by A3,A10
      .= ((arcsin)*f3).x by A4,A10,FUNCT_1:12;
    hence thesis;
  end;
  dom (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z) = dom ((arcsin)*f3) by A4,A8,
FDIFF_1:def 7;
  then (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z) = (arcsin)*f3 by A9,
PARTFUN1:5;
  hence thesis by A1,A4,A6,A7,A8,INTEGRA5:10,13;
end;

:: f.x = arccos.x

theorem
  A c= Z & Z c= ]. -1,1 .[ & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds
f1.x=1 & f.x >0 & x<>0) & dom arccos=Z & Z c= dom ((id Z)(#)(arccos)-( #R (1/2)
)*f) implies integral(arccos,A)
 = ((id Z)(#)(arccos)-( #R (1/2))*f).(upper_bound A) -((
  id Z)(#)(arccos)-( #R (1/2))*f).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ & f=f1-f2 &( f2=#Z 2 & for x st x in Z holds f1.x=1
  & f.x >0 & x<>0 ) and
A3: dom arccos=Z and
A4: Z c= dom ((id Z)(#)(arccos)-( #R (1/2))*f);
A5: arccos|A is bounded by A1,A3,INTEGRA5:10;
A6: ((id Z)(#)(arccos)-( #R (1/2))*f) is_differentiable_on Z by A2,A4,
FDIFF_7:24;
A7: for x being Element of REAL
st x in dom (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z) holds (((id Z)
  (#)(arccos)-( #R (1/2))*f)`|Z).x = arccos.x
  proof
    let x be Element of REAL;
    assume x in dom (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z);
    then x in Z by A6,FDIFF_1:def 7;
    hence thesis by A2,A4,FDIFF_7:24;
  end;
  dom (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z) = dom arccos by A3,A6,
FDIFF_1:def 7;
  then (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z) = arccos by A7,PARTFUN1:5;
  hence thesis by A1,A3,A5,A6,INTEGRA5:11,13;
end;

:: f.x = arccos.(x/a)

theorem
  A c= Z & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & f.x >0
& f3.x=x/a & f3.x > -1 & f3.x < 1 & x<>0 & a>0) & dom ((arccos)*f3)=Z & Z = dom
((id Z)(#)((arccos)*f3)-( #R (1/2))*f) & ((arccos)*f3)|A is continuous implies
integral((arccos)*f3,A) =
 ((id Z)(#)((arccos)*f3)-( #R (1/2))*f).(upper_bound A) -((id
  Z)(#)((arccos)*f3)-( #R (1/2))*f).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: f=f1-f2 & f2=#Z 2 and
A3: for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3
  .x < 1 & x<>0 & a>0 and
A4: dom ((arccos)*f3)=Z and
A5: Z = dom ((id Z)(#)((arccos)*f3)-( #R (1/2))*f) and
A6: ((arccos)*f3)|A is continuous;
A7: (arccos)*f3 is_integrable_on A by A1,A4,A6,INTEGRA5:11;
A8: ((id Z)(#)((arccos)*f3)-( #R (1/2))*f) is_differentiable_on Z by A2,A3,A5,
FDIFF_7:29;
A9: for x being Element of REAL
st x in dom (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z) holds (((id
  Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z).x = ((arccos)*f3).x
  proof
    let x be Element of REAL;
    assume x in dom (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z);
    then
A10: x in Z by A8,FDIFF_1:def 7;
    then
    (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z).x = arccos.(x/a) by A2,A3,A5,
FDIFF_7:29
      .= arccos.(f3.x) by A3,A10
      .= ((arccos)*f3).x by A4,A10,FUNCT_1:12;
    hence thesis;
  end;
  dom (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z) = dom ((arccos)*f3) by A4,A8,
FDIFF_1:def 7;
  then (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z) = (arccos)*f3 by A9,
PARTFUN1:5;
  hence thesis by A1,A4,A6,A7,A8,INTEGRA5:10,13;
end;

:: f.x = arctan.x

theorem
  A c= Z & Z c= ]. -1,1 .[ & f2=#Z 2 & (for x st x in Z holds f1.x=1 ) &
  Z = dom arctan & Z = dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) implies
integral(arctan,A) =
 ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z)
  (#)(arctan)-(1/2)(#)(ln*(f1+f2))).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: f2=#Z 2 & for x st x in Z holds f1.x=1 and
A4: Z = dom arctan and
A5: Z = dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)));
  ].-1,1 .[ c= [.-1,1 .] & A c= ].-1,1 .[ by A1,A2,XBOOLE_1:1,XXREAL_1:25;
  then arctan|A is continuous by FCONT_1:16,SIN_COS9:53,XBOOLE_1:1;
  then
A6: arctan is_integrable_on A & arctan|A is bounded by A1,A4,INTEGRA5:10,11;
A7: ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A2,A3,A5
,SIN_COS9:103;
A8: for x being Element of REAL
st x in dom (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z) holds ((
  (id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z).x = arctan.x
  proof
    let x be Element of REAL;
    assume x in dom (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z);
    then x in Z by A7,FDIFF_1:def 7;
    hence thesis by A2,A3,A5,SIN_COS9:103;
  end;
  dom (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z) = dom arctan by A4,A7,
FDIFF_1:def 7;
  then (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z) = arctan by A8,PARTFUN1:5;
  hence thesis by A1,A2,A3,A5,A6,INTEGRA5:13,SIN_COS9:103;
end;

:: f.x = arccot.x

theorem
  A c= Z & Z c= ]. -1,1 .[ & f2=#Z 2 & (for x st x in Z holds f1.x=1) &
  dom arccot=Z & Z = dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) implies
integral(arccot,A) =
 ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z)
  (#)(arccot)+(1/2)(#)(ln*(f1+f2))).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: f2=#Z 2 & for x st x in Z holds f1.x=1 and
A4: dom arccot=Z and
A5: Z = dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)));
  ].-1,1 .[ c= [.-1,1 .] & A c= ].-1,1 .[ by A1,A2,XBOOLE_1:1,XXREAL_1:25;
  then arccot|A is continuous by FCONT_1:16,SIN_COS9:54,XBOOLE_1:1;
  then
A6: arccot is_integrable_on A & arccot|A is bounded by A1,A4,INTEGRA5:10,11;
A7: ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A2,A3,A5
,SIN_COS9:104;
A8: for x being Element of REAL
st x in dom (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z) holds ((
  (id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z).x = arccot.x
  proof
    let x be Element of REAL;
    assume x in dom (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z);
    then x in Z by A7,FDIFF_1:def 7;
    hence thesis by A2,A3,A5,SIN_COS9:104;
  end;
  dom (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z) = dom arccot by A4,A7,
FDIFF_1:def 7;
  then (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z) = arccot by A8,PARTFUN1:5;
  hence thesis by A1,A2,A3,A5,A6,INTEGRA5:13,SIN_COS9:104;
end;