INTEGRA9

:: Several Integrability Formulas of Some Functions, Orthogonal Polynomials
:: and Norm Functions
::  by Bo Li , Yanping Zhuang , Bing Xie and Pan Wang
::
:: Received October 14, 2008
:: Copyright (c) 2008-2026 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, XBOOLE_0, SUBSET_1, NUMBERS, INTEGRA1, PARTFUN1, RCOMP_1,
      RELAT_1, ARYTM_1, SIN_COS, JGRAPH_2, CARD_1, FDIFF_1, FUNCT_1, ARYTM_3,
      VALUED_1, SEQ_4, ORDINAL2, INTEGRA5, XXREAL_2, TARSKI, PREPOWER, NEWTON,
      REALSET1, XXREAL_0, XXREAL_1, SQUARE_1, ORDINAL4, TAYLOR_1, SIN_COS4,
      INTEGRA9, MEASURE5;
 notations FUNCT_1, SIN_COS, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS,
      VALUED_1, SEQ_4, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, RELSET_1, PARTFUN1,
      RFUNCT_1, RCOMP_1, MEASURE5, INTEGRA1, FCONT_1, FDIFF_9, SQUARE_1,
      INTEGRA5, PARTFUN2, NEWTON, PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2;
 constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER,
      INTEGRA5, PARTFUN2, LIMFUNC1, SEQ_4, RFUNCT_1, FDIFF_9, RELSET_1, SEQ_2,
      NEWTON, INTEGRA1, COMSEQ_2, BINOP_2, NUMBERS;
 registrations VALUED_1, NAT_1, XBOOLE_0, NUMBERS, MEMBERED, VALUED_0, RCOMP_1,
      INT_1, ORDINAL1, FUNCT_2, RELSET_1, FCONT_1, FCONT_3, MEASURE5, XREAL_0,
      PREPOWER, SIN_COS, SQUARE_1, NEWTON;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 equalities SIN_COS, INTEGRA5, VALUED_1, SUBSET_1, FDIFF_9;
 expansions INTEGRA5;
 theorems PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FDIFF_1, INTEGRA2, FUNCT_2,
      XBOOLE_0, XBOOLE_1, SQUARE_1, XCMPLX_1, INTEGRA5, INTEGRA8, INTEGRA6,
      SIN_COS, XREAL_1, FDIFF_4, TAYLOR_1, FDIFF_6, VALUED_1, FCONT_1, RELAT_1,
      FDIFF_2, FDIFF_5, FDIFF_8, FDIFF_9, PREPOWER, XREAL_0;

begin

reserve r,p,x for Real;

reserve n for Element of NAT;
reserve A for non empty closed_interval Subset of REAL;

reserve Z for open Subset of REAL;

Lm1: dom (-(exp_R*(AffineMap(-1,0)))) = [#]REAL by FUNCT_2:def 1;

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

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

theorem
  -(exp_R*(AffineMap(-1,0))) is_differentiable_on REAL & for x holds ((-
  (exp_R*(AffineMap(-1,0))))`|REAL).x = exp_R(-x)
proof
A1: [#]REAL = dom (exp_R*(AffineMap(-1,0))) by FUNCT_2:def 1;
A2: [#]REAL = dom (AffineMap(-jj,0)) by FUNCT_2:def 1;
A3: for x st x in REAL holds AffineMap(-1,0).x=(-1)*x + 0 by FCONT_1:def 4;
  then
A4: (AffineMap(-jj,0)) is_differentiable_on REAL by A2,FDIFF_1:23;
  for x st x in REAL holds
exp_R*(AffineMap(-1,0)) qua PartFunc of REAL, REAL
is_differentiable_in x
  proof
    let x;
    assume x in REAL;
    then (AffineMap(-jj,0)) is_differentiable_in x by A2,A4,FDIFF_1:9;
    hence thesis by TAYLOR_1:19;
  end;
  then
A5:  exp_R*(AffineMap(-1,0)) is_differentiable_on REAL by A1,FDIFF_1:9;
  hence -(exp_R*(AffineMap(-1,0))) is_differentiable_on REAL by Lm1,FDIFF_1:20;
A6:
for x st x in REAL holds ((-(exp_R*(AffineMap(-1,0))))`|REAL).x = exp_R( -x)
  proof
    let x;
    assume
A7:  x in REAL;
    then
A8: (AffineMap(-1,0)) is_differentiable_in x by A2,A4,FDIFF_1:9;
   ((-(exp_R*(AffineMap(-1,0))))`|REAL).x = (-1)*diff(exp_R*(AffineMap(-
    1,0)),x) by A5,Lm1,FDIFF_1:20,A7
      .= (-1)*(exp_R.((AffineMap(-1,0)).x) *diff((AffineMap(-1,0)),x)) by A8,
TAYLOR_1:19
      .= (-1)*(exp_R.((AffineMap(-1,0)).x) *((AffineMap(-1,0))`|REAL).x) by A4,
FDIFF_1:def 7,A7
      .= (-1)*(exp_R.((AffineMap(-1,0)).x)*(-1)) by A2,A3,FDIFF_1:23,A7
      .= (-1)*(exp_R.((-1)*x + 0)*(-1)) by FCONT_1:def 4
      .= exp_R(-x);
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence ((-
  (exp_R*(AffineMap(-1,0))))`|REAL).x = exp_R(-x) by A6;
end;

:: f.x = (1/r)*exp_R.(r*x)

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

::  f.x = exp_R.(r*x)

theorem
  r<>0 implies integral(exp_R*(AffineMap(r,0)),A) = ((1/r)(#)(exp_R*(
  AffineMap(r,0)))).(upper_bound A) -((1/r)(#)(exp_R*(AffineMap(r,0)))).(
  lower_bound A)
proof
A1: dom (exp_R*(AffineMap(r,0))) = REAL by FUNCT_2:def 1;
  assume
A2: r<>0;
  then (1/r)(#)(exp_R*(AffineMap(r,0))) is_differentiable_on REAL by Th2;
  then
A3: dom (((1/r)(#)(exp_R*(AffineMap(r,0))))`|REAL) = dom (exp_R*(AffineMap(
  r,0))) by A1,FDIFF_1:def 7;
  (exp_R*AffineMap(r,0))|A is continuous;
  then
A4: (exp_R*AffineMap(r,0)) is_integrable_on A by A1,INTEGRA5:11;
  for x being Element of REAL
   st x in dom (((1/r)(#)(exp_R*(AffineMap(r,0))))`|REAL) holds (((1/
r)(#)(exp_R*(AffineMap(r,0))))`|REAL).x = (exp_R*(AffineMap(r,0))).x by A2,Th2;
  then
A5: (((1/r)(#)(exp_R*(AffineMap(r,0))))`|REAL) = exp_R*(AffineMap(r,0)) by A3,
PARTFUN1:5;
  (exp_R*AffineMap(r,0))|A is bounded by A1,INTEGRA5:10;
  hence thesis by A2,A4,A5,Th2,INTEGRA5:13;
end;

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

theorem Th4:
  n<>0 implies (-1/n)(#)(cos*(AffineMap(n,0))) is_differentiable_on
  REAL & for x holds (((-1/n)(#)(cos*(AffineMap(n,0))))`|REAL).x =sin(n*x)
proof
  assume
A1: n<>0;
A2: [#]REAL = dom ((-1/n)(#)(cos*(AffineMap(n,0)))) by FUNCT_2:def 1;
A3: [#]REAL = dom (cos*(AffineMap(n,0))) & for x st x in REAL holds
  AffineMap(n, 0).x=n*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A4: cos*(AffineMap(n,0)) is_differentiable_on REAL by FDIFF_4:38;
  hence (-1/n)(#)(cos*(AffineMap(n,0))) is_differentiable_on
  REAL by A2,FDIFF_1:20;
A5:
  for x st x in REAL holds (((-1/n)(#)(cos*(AffineMap(n,0))))`|REAL).x =
  sin(n*x)
  proof
    let x;
    assume
A6:   x in REAL;
    then (((-1/n)(#)(cos*(AffineMap(n,0))))`|REAL).x = (-1/n)*diff((cos*(
    AffineMap(n,0))),x) by A2,A4,FDIFF_1:20
      .= (-1/n)*((cos*(AffineMap(n,0)))`|REAL).x by A4,FDIFF_1:def 7,A6
      .= (-1/n)*(-n * sin.(n*x+0)) by A3,FDIFF_4:38,A6
      .= (1/n)*n * (sin.(n*x+0))
      .= n/n*(sin.(n*x+0)) by XCMPLX_1:99
      .= 1*(sin.(n*x+0)) by A1,XCMPLX_1:60
      .= sin(n*x);
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A5;
end;

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

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

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

theorem Th6:
  n<>0 implies (1/n)(#)(sin*(AffineMap(n,0))) is_differentiable_on
  REAL & for x holds (((1/n)(#)(sin*(AffineMap(n,0))))`|REAL).x = cos(n*x)
proof
  assume
A1: n<>0;
A2: [#]REAL = dom ((1/n)(#)(sin*(AffineMap(n,0)))) by FUNCT_2:def 1;
A3: [#]REAL = dom (sin*(AffineMap(n,0))) & for x st x in REAL holds
  AffineMap(n, 0).x=n*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
  then
A4: sin*(AffineMap(n,0)) is_differentiable_on REAL by FDIFF_4:37;
   hence (1/n)(#)(sin*(AffineMap(n,0))) is_differentiable_on
  REAL by A2,FDIFF_1:20;
A5:
  for x st x in REAL holds (((1/n)(#)(sin*(AffineMap(n,0))))`|REAL).x =cos
  (n*x)
  proof
    let x;
    assume
A6:    x in REAL;
    (((1/n)(#)(sin*(AffineMap(n,0))))`|REAL).x =(1/n)*diff((sin*(AffineMap
    (n,0))),x) by A2,A4,FDIFF_1:20,A6
      .= (1/n)*((sin*(AffineMap(n,0)))`|REAL).x by A4,FDIFF_1:def 7,A6
      .= (1/n)*(n * cos.(n*x+0)) by A3,FDIFF_4:37,A6
      .= n*(1/n)*(cos.(n*x+0))
      .= n/n*(cos.(n*x+0)) by XCMPLX_1:99
      .= 1*(cos.(n*x+0)) by A1,XCMPLX_1:60
      .= cos(n*x);
    hence thesis;
  end;
  let x;
   x in REAL by XREAL_0:def 1;
  hence thesis by A5;
end;

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

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

::  f.x=x*sin.x

theorem
  A c= Z implies integral((id Z)(#)sin,A) = ((-id Z)(#)cos+sin).(
  upper_bound A)-((-id Z)(#)cos+sin).(lower_bound A)
proof
  assume
A1: A c= Z;
A2: dom (-id Z) = dom id Z by VALUED_1:8;
A3: dom ((-id Z)(#)cos+sin) = dom ((-id Z)(#)cos) /\ REAL by SIN_COS:24
,VALUED_1:def 1
    .= dom ((-id Z)(#)cos) by XBOOLE_1:28
    .= dom (-id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (-id Z) by XBOOLE_1:28
    .= Z by A2,RELAT_1:45;
  then
A4: (-id Z)(#)cos+sin is_differentiable_on Z by FDIFF_4:46;
A5: for x st x in Z holds ((id Z)(#)sin).x = x*sin.x
  proof
    let x;
    assume
A6: x in Z;
    ((id Z)(#)sin).x = ((id Z).x)*(sin.x) by VALUED_1:5
      .= x*sin.x by A6,FUNCT_1:18;
    hence thesis;
  end;
A7: for x being Element of REAL
  st x in dom (((-id Z)(#)cos+sin)`|Z) holds (((-id Z)(#)cos+sin)`|
  Z).x = ((id Z)(#)sin).x
  proof
    let x be Element of REAL;
    assume x in dom (((-id Z)(#)cos+sin)`|Z);
    then
A8: x in Z by A4,FDIFF_1:def 7;
    then (((-id Z)(#)cos+sin)`|Z).x =x*sin.x by A3,FDIFF_4:46
      .= ((id Z)(#)sin).x by A5,A8;
    hence thesis;
  end;
A9: dom ((id Z)(#)sin) = dom (id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (id Z) by XBOOLE_1:28
    .= Z by RELAT_1:45;
  then dom (((-id Z)(#)cos+sin)`|Z) = dom ((id Z)(#)sin) by A4,FDIFF_1:def 7;
  then
A10: (((-id Z)(#)cos+sin)`|Z) = (id Z)(#)sin by A7,PARTFUN1:5;
  ((id Z)(#)sin)|A is continuous;
  then
A11: (id Z)(#)sin is_integrable_on A by A1,A9,INTEGRA5:11;
  ((id Z)(#)sin)|A is bounded by A1,A9,INTEGRA5:10;
  hence thesis by A1,A3,A11,A10,FDIFF_4:46,INTEGRA5:13;
end;

::  f.x=x*cos.x

theorem
  A c= Z implies integral((id Z)(#)cos,A) = ((id Z)(#)sin+cos).(
  upper_bound A)-((id Z)(#)sin+cos).(lower_bound A)
proof
  assume
A1: A c= Z;
  dom ((id Z)(#)sin+cos) = dom ((id Z)(#)sin) /\ REAL by SIN_COS:24
,VALUED_1:def 1
    .= dom ((id Z)(#)sin) by XBOOLE_1:28
    .= dom (id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (id Z) by XBOOLE_1:28;
  then
A2: dom ((id Z)(#)sin+cos) = Z by RELAT_1:45;
  then
A3: (id Z)(#)sin+cos is_differentiable_on Z by FDIFF_4:47;
A4: for x st x in Z holds ((id Z)(#)cos).x = x*cos.x
  proof
    let x;
    assume
A5: x in Z;
    ((id Z)(#)cos).x = ((id Z).x)*(cos.x) by VALUED_1:5
      .= x*cos.x by A5,FUNCT_1:18;
    hence thesis;
  end;
A6: for x being Element of REAL
st x in dom (((id Z)(#)sin+cos)`|Z) holds (((id Z)(#)sin+cos)`|Z)
  .x = ((id Z)(#)cos).x
  proof
    let x be Element of REAL;
    assume x in dom (((id Z)(#)sin+cos)`|Z);
    then
A7: x in Z by A3,FDIFF_1:def 7;
    then (((id Z)(#)sin+cos)`|Z).x =x*cos.x by A2,FDIFF_4:47
      .= ((id Z)(#)cos).x by A4,A7;
    hence thesis;
  end;
A8: dom ((id Z)(#)cos) = dom (id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (id Z) by XBOOLE_1:28
    .= Z by RELAT_1:45;
  then dom (((id Z)(#)sin+cos)`|Z) = dom ((id Z)(#)cos) by A3,FDIFF_1:def 7;
  then
A9: (((id Z)(#)sin+cos)`|Z) = (id Z)(#)cos by A6,PARTFUN1:5;
  ((id Z)(#)cos)|A is continuous;
  then
A10: (id Z)(#)cos is_integrable_on A by A1,A8,INTEGRA5:11;
  ((id Z)(#)cos)|A is bounded by A1,A8,INTEGRA5:10;
  hence thesis by A1,A2,A10,A9,FDIFF_4:47,INTEGRA5:13;
end;

:: f.x=x*cos.x

theorem Th10:
  (id Z)(#)cos is_differentiable_on Z & for x st x in Z holds (((
  id Z)(#)cos)`|Z).x =cos.x-x*sin.x
proof
A1: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
A2: dom ((id Z)(#)cos) = dom (id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (id Z) by XBOOLE_1:28
    .= Z by RELAT_1:45;
  then Z c= dom (id Z) /\ dom cos by VALUED_1:def 4;
  then
A3: Z c= dom (id Z) by XBOOLE_1:18;
  for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
  then
A4: id Z is_differentiable_on Z by A3,FDIFF_1:23;
A5: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
  now
    let x;
    assume
A6: x in Z;
    hence
    (((id Z)(#)cos)`|Z).x = (cos.x)*diff((id Z),x) + ((id Z).x)*diff(cos,
    x) by A2,A4,A1,FDIFF_1:21
      .=(cos.x)*((id Z)`|Z).x + ((id Z).x)*diff(cos,x) by A4,A6,FDIFF_1:def 7
      .=(cos.x)*1+ ((id Z).x)*diff(cos,x) by A3,A5,A6,FDIFF_1:23
      .=(cos.x)*1+((id Z).x)*(-sin.x) by SIN_COS:63
      .=cos.x+x*(-sin.x) by A6,FUNCT_1:18
      .=cos.x-x*sin.x;
  end;
  hence thesis by A2,A4,A1,FDIFF_1:21;
end;

Lm2: -sin is_differentiable_in x & diff(-sin,x) = -cos.x
proof
A1: sin is_differentiable_in x by SIN_COS:64;
  then diff(-sin,x) = -diff(sin,x) by INTEGRA8:22
    .= - cos.x by SIN_COS:64;
  hence thesis by A1,INTEGRA8:22;
end;

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

theorem Th11:
  -sin+(id Z)(#)cos is_differentiable_on Z & for x st x in Z holds
  ((-sin+(id Z)(#)cos)`|Z).x =-x*sin.x
proof
  dom (-sin+(id Z)(#)cos) = dom (-sin) /\ dom((id Z)(#)cos) by VALUED_1:def 1
    .= REAL /\ dom((id Z)(#)cos) by SIN_COS:24,VALUED_1:8
    .= dom((id Z)(#)cos) by XBOOLE_1:28
    .= dom (id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (id Z) by XBOOLE_1:28;
  then
A1: Z = dom (-sin+(id Z)(#)cos) by RELAT_1:45;
A2: (id Z)(#)cos is_differentiable_on Z by Th10;
A3: -sin is_differentiable_on Z by FDIFF_1:26,INTEGRA8:24;
  now
    let x;
    assume
A4: x in Z;
    hence
    ((-sin+(id Z)(#)cos)`|Z).x = diff(-sin,x)+diff((id Z)(#)cos,x) by A1,A2,A3,
FDIFF_1:18
      .=(((id Z)(#)cos)`|Z).x + diff(-sin,x) by A2,A4,FDIFF_1:def 7
      .=cos.x- x*sin.x+ diff(-sin,x) by A4,Th10
      .=cos.x- x*sin.x +(-cos.x) by Lm2
      .=-x*sin.x;
  end;
  hence thesis by A1,A2,A3,FDIFF_1:18;
end;

::  f.x=-x*sin.x

theorem
  A c= Z implies integral((-id Z)(#)sin,A) = (-sin+(id Z)(#)cos).(
  upper_bound A)-(-sin+(id Z)(#)cos).(lower_bound A)
proof
  assume
A1: A c= Z;
A2: -sin+(id Z)(#)cos is_differentiable_on Z by Th11;
A3: for x st x in Z holds (-id Z).x =(-1)*x +0
  proof
    let x;
    assume
A4: x in Z;
    (-id Z).x = -(id Z.x) by VALUED_1:8
      .=-x by A4,FUNCT_1:18
      .=(-1)*x +0;
    hence thesis;
  end;
A5: for x st x in Z holds ((-id Z)(#)sin).x = -x*sin.x
  proof
    let x;
    assume
A6: x in Z;
    ((-id Z)(#)sin).x = ((-id Z).x)*(sin.x) by VALUED_1:5
      .= ((-1)*x+0)*(sin.x) by A3,A6
      .= -x*sin.x;
    hence thesis;
  end;
A7: for x being Element of REAL
  st x in dom ((-sin+(id Z)(#)cos)`|Z) holds ((-sin+(id Z)(#)cos)`|
  Z).x = ((-id Z)(#)sin).x
  proof
    let x be Element of REAL;
    assume x in dom ((-sin+(id Z)(#)cos)`|Z);
    then
A8: x in Z by A2,FDIFF_1:def 7;
    then ((-sin+(id Z)(#)cos)`|Z).x =-x*sin.x by Th11
      .= ((-id Z)(#)sin).x by A5,A8;
    hence thesis;
  end;
  dom ((-id Z)(#)sin) = dom (-id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (-id Z) by XBOOLE_1:28
    .= dom (id Z) by VALUED_1:8;
  then
A9: Z = dom ((-id Z)(#)sin) by RELAT_1:45;
  then dom ((-sin+(id Z)(#)cos)`|Z) = dom ((-id Z)(#)sin) by A2,FDIFF_1:def 7;
  then
A10: ((-sin+(id Z)(#)cos)`|Z) = (-id Z)(#)sin by A7,PARTFUN1:5;
  ((-id Z)(#)sin)|A is continuous;
  then
A11: (-id Z)(#)sin is_integrable_on A by A1,A9,INTEGRA5:11;
  ((-id Z)(#)sin)|A is bounded by A1,A9,INTEGRA5:10;
  hence thesis by A1,A11,A10,Th11,INTEGRA5:13;
end;

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

theorem Th13:
  -cos-(id Z)(#)sin is_differentiable_on Z & for x st x in Z holds
  ((-cos-(id Z)(#)sin)`|Z).x =-x*cos.x
proof
  dom (-cos-(id Z)(#)sin) = dom (-cos) /\ dom ((id Z)(#)sin) by VALUED_1:12
    .= REAL /\ dom ((id Z)(#)sin) by SIN_COS:24,VALUED_1:8
    .= dom((id Z)(#)sin) by XBOOLE_1:28
    .= dom (id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (id Z) by XBOOLE_1:28;
  then
A1: Z = dom (-cos-(id Z)(#)sin) by RELAT_1:45;
  then Z c= dom (-cos) /\ dom ((id Z)(#)sin) by VALUED_1:12;
  then
A2: Z c= dom ((id Z)(#)sin) by XBOOLE_1:18;
  then
A3: (id Z)(#)sin is_differentiable_on Z by FDIFF_4:45;
A4: -cos is_differentiable_on Z by FDIFF_1:26,INTEGRA8:26;
  now
    let x;
    assume
A5: x in Z;
    hence
    ((-cos-(id Z)(#)sin)`|Z).x = diff(-cos,x)-diff((id Z)(#)sin,x) by A1,A3,A4,
FDIFF_1:19
      .= sin.x - diff((id Z)(#)sin,x) by INTEGRA8:26,A5
      .= sin.x - (((id Z)(#)sin)`|Z).x by A3,A5,FDIFF_1:def 7
      .= sin.x - (sin.x+x*cos.x) by A2,A5,FDIFF_4:45
      .= -x*cos.x;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:19;
end;

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

theorem
  A c= Z implies integral((-id Z)(#)cos,A) = (-cos-(id Z)(#)sin).(
  upper_bound A)-(-cos-(id Z)(#)sin).(lower_bound A)
proof
  assume
A1: A c= Z;
A2: -cos-(id Z)(#)sin is_differentiable_on Z by Th13;
A3: for x st x in Z holds (-id Z).x =(-1)*x +0
  proof
    let x;
    assume
A4: x in Z;
    (-id Z).x = -(id Z.x) by VALUED_1:8
      .=-x by A4,FUNCT_1:18
      .=(-1)*x +0;
    hence thesis;
  end;
A5: for x st x in Z holds ((-id Z)(#)cos).x = -x*cos.x
  proof
    let x;
    assume
A6: x in Z;
    ((-id Z)(#)cos).x = ((-id Z).x)*(cos.x) by VALUED_1:5
      .= ((-1)*x+0)*(cos.x) by A3,A6
      .= -x*cos.x;
    hence thesis;
  end;
A7: for x being Element of REAL
st x in dom ((-cos-(id Z)(#)sin)`|Z) holds ((-cos-(id Z)(#)sin)`|
  Z).x = ((-id Z)(#)cos).x
  proof
    let x be Element of REAL;
    assume x in dom ((-cos-(id Z)(#)sin)`|Z);
    then
A8: x in Z by A2,FDIFF_1:def 7;
    then ((-cos-(id Z)(#)sin)`|Z).x =-x*cos.x by Th13
      .= ((-id Z)(#)cos).x by A5,A8;
    hence thesis;
  end;
  dom ((-id Z)(#)cos) = dom (-id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (-id Z) by XBOOLE_1:28
    .= dom (id Z) by VALUED_1:8;
  then
A9: Z = dom ((-id Z)(#)cos) by RELAT_1:45;
  then dom ((-cos-(id Z)(#)sin)`|Z) = dom ((-id Z)(#)cos) by A2,FDIFF_1:def 7;
  then
A10: ((-cos-(id Z)(#)sin)`|Z) = (-id Z)(#)cos by A7,PARTFUN1:5;
  ((-id Z)(#)cos)|A is continuous;
  then
A11: (-id Z)(#)cos is_integrable_on A by A1,A9,INTEGRA5:11;
  ((-id Z)(#)cos)|A is bounded by A1,A9,INTEGRA5:10;
  hence thesis by A1,A11,A10,Th13,INTEGRA5:13;
end;

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

theorem
  A c= Z implies integral(sin+(id Z)(#)cos,A) = ((id Z)(#)sin).(
  upper_bound A)-((id Z)(#)sin).(lower_bound A)
proof
  assume
A1: A c= Z;
  dom (sin+(id Z)(#)cos) = REAL /\ dom ((id Z)(#)cos) by SIN_COS:24
,VALUED_1:def 1
    .= dom ((id Z)(#)cos) by XBOOLE_1:28
    .= dom (id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (id Z) by XBOOLE_1:28;
  then
A2: Z = dom (sin+(id Z)(#)cos) by RELAT_1:45;
  (sin+(id Z)(#)cos)|A is continuous;
  then
A3: sin+(id Z)(#)cos is_integrable_on A by A1,A2,INTEGRA5:11;
A4: dom ((id Z)(#)sin) = dom (id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (id Z) by XBOOLE_1:28
    .= Z by RELAT_1:45;
  then
A5: (id Z)(#)sin is_differentiable_on Z by FDIFF_4:45;
A6: for x st x in Z holds (sin+(id Z)(#)cos).x = sin.x+x*cos.x
  proof
    let x;
    assume
A7: x in Z;
    then (sin+(id Z)(#)cos).x = sin.x+((id Z)(#)cos).x by A2,VALUED_1:def 1
      .= sin.x+((id Z).x)*(cos.x) by VALUED_1:5
      .= sin.x+x*cos.x by A7,FUNCT_1:18;
    hence thesis;
  end;
A8: for x being Element of REAL
st x in dom (((id Z)(#)sin)`|Z) holds (((id Z)(#)sin)`|Z).x = (
  sin+(id Z)(#)cos).x
  proof
    let x be Element of REAL;
    assume x in dom (((id Z)(#)sin)`|Z);
    then
A9: x in Z by A5,FDIFF_1:def 7;
    then (((id Z)(#)sin)`|Z).x =sin.x+x*cos.x by A4,FDIFF_4:45
      .= (sin+(id Z)(#)cos).x by A6,A9;
    hence thesis;
  end;
  dom (((id Z)(#)sin)`|Z) = dom (sin+(id Z)(#)cos) by A2,A5,FDIFF_1:def 7;
  then
A10: (((id Z)(#)sin)`|Z) = sin+(id Z)(#)cos by A8,PARTFUN1:5;
  (sin+(id Z)(#)cos)|A is bounded by A1,A2,INTEGRA5:10;
  hence thesis by A1,A4,A3,A10,FDIFF_4:45,INTEGRA5:13;
end;

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

theorem
  A c= Z implies integral(-cos+(id Z)(#)sin,A) = ((-id Z)(#)cos).(
  upper_bound A)-((-id Z)(#)cos).(lower_bound A)
proof
  assume
A1: A c= Z;
  dom (-cos+(id Z)(#)sin) = dom (-cos) /\ dom((id Z)(#)sin) by VALUED_1:def 1
    .= REAL /\ dom((id Z)(#)sin) by SIN_COS:24,VALUED_1:8
    .= dom((id Z)(#)sin) by XBOOLE_1:28
    .= dom (id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (id Z) by XBOOLE_1:28;
  then
A2: Z = dom (-cos+(id Z)(#)sin) by RELAT_1:45;
  (-cos+(id Z)(#)sin)|A is continuous;
  then
A3: -cos+(id Z)(#)sin is_integrable_on A by A1,A2,INTEGRA5:11;
  dom ((-id Z)(#)cos) = dom (-id Z) /\ REAL by SIN_COS:24,VALUED_1:def 4
    .= dom (-id Z) by XBOOLE_1:28
    .= dom (id Z) by VALUED_1:8;
  then
A4: dom ((-id Z)(#)cos) = Z by RELAT_1:45;
  then
A5: (-id Z)(#)cos is_differentiable_on Z by FDIFF_4:44;
A6: for x st x in Z holds (-cos+(id Z)(#)sin).x = -cos.x+x*sin.x
  proof
    let x;
    assume
A7: x in Z;
    then (-cos+(id Z)(#)sin).x = (-cos).x+((id Z)(#)sin).x by A2,VALUED_1:def 1
      .= (-cos).x+((id Z).x)*(sin.x) by VALUED_1:5
      .= (-cos).x+x*sin.x by A7,FUNCT_1:18
      .= -cos.x+x*sin.x by VALUED_1:8;
    hence thesis;
  end;
A8: for x being Element of REAL
st x in dom (((-id Z)(#)cos)`|Z) holds (((-id Z)(#)cos)`|Z).x = (
  -cos+(id Z)(#)sin).x
  proof
    let x be Element of REAL;
    assume x in dom (((-id Z)(#)cos)`|Z);
    then
A9: x in Z by A5,FDIFF_1:def 7;
    then (((-id Z)(#)cos)`|Z).x =-cos.x+x*sin.x by A4,FDIFF_4:44
      .= (-cos+(id Z)(#)sin).x by A6,A9;
    hence thesis;
  end;
  dom (((-id Z)(#)cos)`|Z) = dom (-cos+(id Z)(#)sin) by A2,A5,FDIFF_1:def 7;
  then
A10: (((-id Z)(#)cos)`|Z) = -cos+(id Z)(#)sin by A8,PARTFUN1:5;
  (-cos+(id Z)(#)sin)|A is bounded by A1,A2,INTEGRA5:10;
  hence thesis by A1,A4,A3,A10,FDIFF_4:44,INTEGRA5:13;
end;

:: f.x = x*(exp_R.x)

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

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

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

::  f.x = x^n

theorem
  integral( #Z n,A) = ((1/(n+1))*((upper_bound A) |^ (n+1))) - ((1/(n+1)
  )*((lower_bound A) |^ (n+1)))
proof
A1: dom ( #Z n) = [#]REAL by FUNCT_2:def 1;
A2: for x being Element of REAL
st x in dom (((1/(n+1))(#)( #Z (n+1)))`|REAL) holds (((1/(n+1))(#)
  ( #Z (n+1)))`|REAL).x = ( #Z n).x
  proof
    let x be Element of REAL;
    assume x in dom (((1/(n+1))(#)( #Z (n+1)))`|REAL);
    (((1/(n+1))(#)( #Z (n+1)))`|REAL).x =x #Z n by Th18
      .= ( #Z n).x by TAYLOR_1:def 1;
    hence thesis;
  end;
  dom ( #Z (n+1)) = [#]REAL & for x st x in REAL holds ( #Z (n+1))
  is_differentiable_in x by FUNCT_2:def 1,TAYLOR_1:2;
  then [#]REAL = dom ((1/(n+1))(#)( #Z (n+1))) & ( #Z (n+1))
  is_differentiable_on REAL by FDIFF_1:9,FUNCT_2:def 1;
  then (1/(n+1))(#)( #Z (n+1)) is_differentiable_on REAL by FDIFF_1:20;
  then dom (((1/(n+1))(#)( #Z (n+1)))`|REAL) = dom ( #Z n) by A1,FDIFF_1:def 7;
  then
A3: (((1/(n+1))(#)( #Z (n+1)))`|REAL) = ( #Z n) by A2,PARTFUN1:5;
A4: ( #Z (n+1)).(upper_bound A) = (upper_bound A) #Z (n+1) by TAYLOR_1:def 1
    .= (upper_bound A) |^ (n+1) by PREPOWER:36;
  for x st x in REAL holds ( #Z n) is_differentiable_in x by TAYLOR_1:2;
  then ( #Z n) is_differentiable_on REAL by A1,FDIFF_1:9;
  then
A5: ( #Z n)|REAL is continuous by FDIFF_1:25;
  then ( #Z n)|A is continuous by FCONT_1:16;
  then
A6: ( #Z n) is_integrable_on A by A1,INTEGRA5:11;
A7: ( #Z (n+1)).(lower_bound A) = (lower_bound A) #Z (n+1) by TAYLOR_1:def 1
    .= (lower_bound A) |^ (n+1) by PREPOWER:36;
  ( #Z n)|A is bounded by A1,A5,FCONT_1:16,INTEGRA5:10;
  then
  integral( #Z n,A) = ((1/(n+1))(#)( #Z (n+1))).(upper_bound A) -((1/(n+1
  ))(#)( #Z (n+1))).(lower_bound A) by A6,A3,Th18,INTEGRA5:13
    .= ((1/(n+1))*( #Z (n+1)).(upper_bound A)) -((1/(n+1))(#)( #Z (n+1))).(
  lower_bound A) by VALUED_1:6
    .= (1/(n+1))*( #Z (n+1)).(upper_bound A) -(1/(n+1))*( #Z (n+1)).(
  lower_bound A) by VALUED_1:6
    .= (1/(n+1))*((upper_bound A) |^ (n+1)) -(1/(n+1))*((lower_bound A) |^ (
  n+1)) by A4,A7;
  hence thesis;
end;

begin

theorem Th20:
  for f,g being PartFunc of REAL,REAL, C being non empty Subset of
  REAL holds (f-g)||C = f||C - g||C
proof
  let f,g be PartFunc of REAL,REAL;
  let C be non empty Subset of REAL;
A1: dom (f||C-g||C) = dom (f|C) /\ dom (g|C) by VALUED_1:12
    .= (dom f /\ C) /\ dom (g|C) by RELAT_1:61
    .= (dom f /\ C) /\ (dom g /\ C) by RELAT_1:61
    .= dom f /\ (C /\ (dom g /\ C)) by XBOOLE_1:16
    .= dom f /\ (dom g /\ (C /\ C)) by XBOOLE_1:16
    .= dom f /\ (dom g /\ C);
A2: dom ((f-g)||C) = dom (f-g) /\ C by RELAT_1:61
    .= dom f /\ dom g /\ C by VALUED_1:12;
  then
A3: dom ((f-g)||C) = dom (f||C - g||C) by A1,XBOOLE_1:16;
  for c being Element of C st c in dom ((f-g)||C) holds (f-g)||C.c = (f||C
  - g||C).c
  proof
    let c be Element of C;
    assume
A4: c in dom((f-g)||C);
    then c in dom(f-g) /\ C by RELAT_1:61;
    then
A5: c in dom(f-g) by XBOOLE_0:def 4;
A6: c in dom(f||C) /\ dom(g||C) by A3,A4,VALUED_1:12;
    then
A7: c in dom(f|C) by XBOOLE_0:def 4;
A8: (f-g)||C.c = (f-g).c by A4,FUNCT_1:47
      .= f.c - g.c by A5,VALUED_1:13;
A9: c in dom(g|C) by A6,XBOOLE_0:def 4;
    (f||C-g||C).c = f||C.c - g||C.c by A3,A4,VALUED_1:13
      .= f.c - g|C.c by A7,FUNCT_1:47;
    hence thesis by A8,A9,FUNCT_1:47;
  end;
  hence thesis by A2,A1,PARTFUN1:5,XBOOLE_1:16;
end;

theorem Th21:
  for f1,f2,g being PartFunc of REAL,REAL, C being non empty
  Subset of REAL holds ((f1+f2)||C)(#)(g||C)=(f1(#)g+f2(#)g)||C
proof
  let f1,f2,g be PartFunc of REAL,REAL;
  let C be non empty Subset of REAL;
A1: dom ((f1(#)g+f2(#)g)||C) = dom (f1(#)g+f2(#)g) /\ C by RELAT_1:61
    .= (dom (f1(#)g) /\ dom (f2(#)g))/\ C by VALUED_1:def 1
    .= (dom f1 /\ dom g) /\ dom (f2(#)g) /\ C by VALUED_1:def 4
    .= dom f1 /\ dom g /\ (dom f2 /\ dom g) /\ C by VALUED_1:def 4
    .= dom f1 /\ (dom g /\ dom f2 /\ dom g) /\ C by XBOOLE_1:16
    .= dom f1 /\ (dom f2 /\ (dom g /\ dom g)) /\ C by XBOOLE_1:16
    .= (dom f1 /\ dom f2 /\ dom g) /\ C by XBOOLE_1:16;
A2: dom (((f1+f2)||C)(#)(g||C)) = dom ((f1+f2)||C) /\ dom (g||C) by
VALUED_1:def 4
    .= (dom (f1+f2) /\ C) /\ dom (g|C) by RELAT_1:61
    .= (dom (f1+f2) /\ C) /\ (dom g /\ C) by RELAT_1:61
    .= (dom f1 /\ dom f2 /\ C) /\ (dom g /\ C) by VALUED_1:def 1
    .= (dom f1 /\ dom f2) /\ (C /\ dom g /\ C) by XBOOLE_1:16
    .= (dom f1 /\ dom f2) /\ (dom g /\ (C /\ C)) by XBOOLE_1:16
    .= (dom f1 /\ dom f2 /\ dom g) /\ C by XBOOLE_1:16;
  for c being Element of C st c in dom(((f1+f2)||C)(#)(g||C)) holds (((f1+
  f2)||C)(#)(g||C)).c = ((f1(#)g+f2(#)g)||C).c
  proof
    let c be Element of C;
    assume
A3: c in dom(((f1+f2)||C)(#)(g||C));
    then
A4: c in dom((f1+f2)||C) /\ dom (g||C) by VALUED_1:def 4;
    then
A5: c in dom (g|C) by XBOOLE_0:def 4;
    c in dom (f1(#)g+f2(#)g) /\ C by A2,A1,A3,RELAT_1:61;
    then
A6: c in dom (f1(#)g+f2(#)g) by XBOOLE_0:def 4;
    then
A7: c in dom (f1(#)g) /\ dom(f2(#)g) by VALUED_1:def 1;
    then
A8: c in dom (f1(#)g) by XBOOLE_0:def 4;
A9: c in dom ((f1+f2)|C) by A4,XBOOLE_0:def 4;
    then c in dom(f1+f2) /\ C by RELAT_1:61;
    then
A10: c in dom(f1+f2) by XBOOLE_0:def 4;
A11: (((f1+f2)||C)(#)(g||C)).c = ((f1+f2)||C).c * (g||C).c by A3,VALUED_1:def 4
      .= (f1+f2).c * (g|C).c by A9,FUNCT_1:47
      .= (f1.c + f2.c) * (g|C).c by A10,VALUED_1:def 1;
A12: c in dom(f2(#)g) by A7,XBOOLE_0:def 4;
    ((f1(#)g)+(f2(#)g))||C.c = (f1(#)g+f2(#)g).c by A2,A1,A3,FUNCT_1:47
      .= (f1(#)g).c+(f2(#)g).c by A6,VALUED_1:def 1
      .= f1.c * g.c+(f2(#)g).c by A8,VALUED_1:def 4
      .= f1.c * g.c+f2.c * g.c by A12,VALUED_1:def 4
      .= (f1.c+f2.c) * g.c;
    hence thesis by A5,A11,FUNCT_1:47;
  end;
  hence thesis by A2,A1,PARTFUN1:5;
end;

theorem Th22:
  for f1,f2,g being PartFunc of REAL,REAL, C being non empty
  Subset of REAL holds ((f1-f2)||C)(#)(g||C)=(f1(#)g-f2(#)g)||C
proof
  let f1,f2,g be PartFunc of REAL,REAL;
  let C be non empty Subset of REAL;
A1: dom ((f1(#)g-f2(#)g)||C) = dom (f1(#)g-f2(#)g) /\ C by RELAT_1:61
    .= (dom (f1(#)g) /\ dom (f2(#)g))/\ C by VALUED_1:12
    .= (dom f1 /\ dom g) /\ dom (f2(#)g) /\ C by VALUED_1:def 4
    .= dom f1 /\ dom g /\ (dom f2 /\ dom g) /\ C by VALUED_1:def 4
    .= dom f1 /\ (dom g /\ dom f2 /\ dom g) /\ C by XBOOLE_1:16
    .= dom f1 /\ (dom f2 /\ (dom g /\ dom g)) /\ C by XBOOLE_1:16
    .= (dom f1 /\ dom f2 /\ dom g) /\ C by XBOOLE_1:16;
A2: dom (((f1-f2)||C)(#)(g||C)) = dom ((f1-f2)|C) /\ dom (g|C) by
VALUED_1:def 4
    .= (dom (f1-f2) /\ C) /\ dom (g|C) by RELAT_1:61
    .= (dom (f1-f2) /\ C) /\ (dom g /\ C) by RELAT_1:61
    .= (dom f1 /\ dom f2 /\ C) /\ (dom g /\ C) by VALUED_1:12
    .= (dom f1 /\ dom f2) /\ (C /\ dom g /\ C) by XBOOLE_1:16
    .= (dom f1 /\ dom f2) /\ (dom g /\ (C /\ C)) by XBOOLE_1:16
    .= (dom f1 /\ dom f2 /\ dom g) /\ C by XBOOLE_1:16;
  for c being Element of C st c in dom(((f1-f2)||C)(#)(g||C)) holds (((f1-
  f2)||C)(#)(g||C)).c = ((f1(#)g-f2(#)g)||C).c
  proof
    let c be Element of C;
    assume
A3: c in dom(((f1-f2)||C)(#)(g||C));
    then
A4: c in dom((f1-f2)||C) /\ dom (g||C) by VALUED_1:def 4;
    then
A5: c in dom (g|C) by XBOOLE_0:def 4;
    c in dom (f1(#)g-f2(#)g) /\ C by A2,A1,A3,RELAT_1:61;
    then
A6: c in dom (f1(#)g-f2(#)g) by XBOOLE_0:def 4;
    then
A7: c in dom (f1(#)g) /\ dom(f2(#)g) by VALUED_1:12;
    then
A8: c in dom (f1(#)g) by XBOOLE_0:def 4;
A9: c in dom ((f1-f2)|C) by A4,XBOOLE_0:def 4;
    then c in dom(f1-f2) /\ C by RELAT_1:61;
    then
A10: c in dom(f1-f2) by XBOOLE_0:def 4;
A11: (((f1-f2)||C)(#)(g||C)).c =((f1-f2)|C).c * (g|C).c by A3,VALUED_1:def 4
      .= (f1-f2).c * (g|C).c by A9,FUNCT_1:47
      .= (f1.c - f2.c) * (g|C).c by A10,VALUED_1:13;
A12: c in dom(f2(#)g) by A7,XBOOLE_0:def 4;
    ((f1(#)g)-(f2(#)g))||C.c = (f1(#)g-f2(#)g).c by A2,A1,A3,FUNCT_1:47
      .= (f1(#)g).c-(f2(#)g).c by A6,VALUED_1:13
      .= f1.c * g.c-(f2(#)g).c by A8,VALUED_1:def 4
      .= f1.c * g.c-f2.c * g.c by A12,VALUED_1:def 4
      .= (f1.c-f2.c) * g.c;
    hence thesis by A5,A11,FUNCT_1:47;
  end;
  hence thesis by A2,A1,PARTFUN1:5;
end;

theorem
  for f1,f2,g being PartFunc of REAL,REAL, C being non empty Subset of
  REAL holds ((f1(#)f2)||C)(#)(g||C)=(f1||C)(#)((f2(#)g)||C)
proof
  let f1,f2,g be PartFunc of REAL,REAL;
  let C be non empty Subset of REAL;
  ((f1(#)f2)||C)(#)(g||C) = (f1||C)(#)(f2||C)(#)(g||C) & (f1||C)(#)((f2(#)
  g)|| C) = (f1||C)(#)((f2||C)(#)(g||C)) by INTEGRA5:4;
  hence thesis by RFUNCT_1:9;
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let f,g be PartFunc of REAL,REAL;
  func |||(f,g,A)||| -> Real equals
  integral((f(#)g),A);
  correctness;
end;

theorem
  for f,g being PartFunc of REAL,REAL,
  A being non empty closed_interval Subset of
  REAL holds |||(f,g,A)||| = |||(g,f,A)|||;

theorem
  for f1,f2,g being PartFunc of REAL,REAL, A being non empty closed_interval
  Subset of REAL st (f1(#)g)||A is total & (f2(#)g)||A is total & (f1(#)g)||A|A
is bounded & (f1(#)g)||A is integrable & (f2(#)g)||A|A is bounded & (f2(#)g)||A
  is integrable holds |||(f1+f2,g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)|||
proof
  let f1,f2,g be PartFunc of REAL,REAL;
  let A be non empty closed_interval Subset of REAL;
  assume
A1: (f1(#)g)||A is total & (f2(#)g)||A is total;
  assume
A2: (f1(#)g)||A|A is bounded & (f1(#)g)||A is integrable & (f2(#)g)||A|A
  is bounded & (f2(#)g)||A is integrable;
  |||(f1+f2,g,A)||| = integral(((f1+f2)||A)(#)(g||A)) by INTEGRA5:4
    .= integral(((f1(#)g)+(f2(#)g))||A) by Th21
    .= integral(((f1(#)g)||A)+((f2(#)g)||A)) by INTEGRA5:5
    .= integral((f1(#)g)||A) + integral((f2(#)g)||A) by A1,A2,INTEGRA1:57;
  hence thesis;
end;

theorem
  for f1,f2,g being PartFunc of REAL,REAL, A being non empty closed_interval
  Subset of REAL st (f1(#)g)||A is total & (f2(#)g)||A is total & (f1(#)g)||A|A
is bounded & (f1(#)g)||A is integrable & (f2(#)g)||A|A is bounded & (f2(#)g)||A
  is integrable holds |||(f1-f2,g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)|||
proof
  let f1,f2,g be PartFunc of REAL,REAL;
  let A be non empty closed_interval Subset of REAL;
  assume
A1: (f1(#)g)||A is total & (f2(#)g)||A is total;
  assume
A2: (f1(#)g)||A|A is bounded & (f1(#)g)||A is integrable & (f2(#)g)||A|A
  is bounded & (f2(#)g)||A is integrable;
  |||(f1-f2,g,A)||| = integral(((f1-f2)||A)(#)(g||A)) by INTEGRA5:4
    .= integral(((f1(#)g)-(f2(#)g))||A) by Th22
    .= integral(((f1(#)g)||A)-((f2(#)g)||A)) by Th20
    .= integral((f1(#)g)||A) - integral((f2(#)g)||A) by A1,A2,INTEGRA2:33;
  hence thesis;
end;

theorem
  for f,g being PartFunc of REAL,REAL,
  A being non empty closed_interval Subset of
REAL st (f(#)g)|A is bounded & f(#)g is_integrable_on A & A c= dom(f(#)g) holds
  |||(-f,g,A)||| = - |||(f,g,A)|||
proof
  let f,g being PartFunc of REAL,REAL;
  let A being non empty closed_interval Subset of REAL;
  assume
A1: (f(#)g)|A is bounded & f(#)g is_integrable_on A & A c= dom(f(#)g);
  |||(-f,g,A)||| = integral(((-1)(#)(f(#)g)),A) by RFUNCT_1:12
    .= (-1)*integral((f(#)g),A) by A1,INTEGRA6:9
    .= - |||(f,g,A)|||;
  hence thesis;
end;

theorem
  for f,g being PartFunc of REAL,REAL,
  A being non empty closed_interval Subset of
REAL st (f(#)g)|A is bounded & f(#)g is_integrable_on A & A c= dom(f(#)g) holds
  |||((r(#)f),g,A)||| = r*|||(f,g,A)|||
proof
  let f,g be PartFunc of REAL,REAL;
  let A be non empty closed_interval Subset of REAL;
  assume
A1: (f(#)g)|A is bounded & f(#)g is_integrable_on A & A c= dom(f(#)g);
  |||((r(#)f),g,A)||| = integral((r(#)(f(#)g)),A) by RFUNCT_1:12
    .= r*integral((f(#)g),A) by A1,INTEGRA6:9;
  hence thesis;
end;

theorem
  for f,g being PartFunc of REAL,REAL, A being
  non empty closed_interval Subset of
REAL st (f(#)g)|A is bounded & f(#)g is_integrable_on A & A c= dom(f(#)g) holds
  |||((r(#)f),(p(#)g),A)||| = r*p*|||(f,g,A)|||
proof
  let f,g be PartFunc of REAL,REAL;
  let A be non empty closed_interval Subset of REAL;
  assume
A1: (f(#)g)|A is bounded & f(#)g is_integrable_on A & A c= dom(f(#)g);
  |||((r(#)f),(p(#)g),A)||| = integral((r(#)(f(#)(p(#)g))),A) by RFUNCT_1:12
    .= integral((r(#)(p(#)(f(#)g))),A) by RFUNCT_1:13
    .= integral(((r*p)(#)(f(#)g)),A) by RFUNCT_1:17
    .= (r*p)*integral((f(#)g),A) by A1,INTEGRA6:9;
  hence thesis;
end;

theorem
  for f,g,h being PartFunc of REAL,REAL,
  A being non empty closed_interval Subset
  of REAL holds |||((f(#)g),h,A)||| = |||(f,(g(#)h),A)||| by RFUNCT_1:9;

theorem Th31:
  for f,g being PartFunc of REAL,REAL, A being non empty closed_interval
  Subset of REAL st (f(#)f)||A is total & (f(#)g)||A is total & (g(#)g)||A is
  total & (f(#)f)||A|A is bounded & (f(#)g)||A|A is bounded & (g(#)g)||A|A is
  bounded & (f(#)f) is_integrable_on A & (f(#)g) is_integrable_on A & (g(#)g)
is_integrable_on A holds |||(f+g,f+g,A)||| = |||(f,f,A)||| + 2*|||(f,g,A)||| +
  |||(g,g,A)|||
proof
  let f,g be PartFunc of REAL,REAL;
  let A be non empty closed_interval Subset of REAL;
  assume that
A1: (f(#)f)||A is total and
A2: (f(#)g)||A is total and
A3: (g(#)g)||A is total;
  assume that
A4: (f(#)f)||A|A is bounded and
A5: (f(#)g)||A|A is bounded and
A6: (g(#)g)||A|A is bounded;
  assume that
A7: (f(#)f) is_integrable_on A and
A8: (f(#)g) is_integrable_on A and
A9: (g(#)g) is_integrable_on A;
A10: (f(#)g)||A is integrable by A8;
A11: (g(#)g)||A is integrable by A9;
  then
A12: ((f(#)g)||A+(g(#)g)||A) is integrable by A2,A3,A5,A6,A10,INTEGRA1:57;
A13: (f(#)f)||A is integrable by A7;
  then
A14: ((f(#)f)||A+(f(#)g)||A) is integrable by A1,A2,A4,A5,A10,INTEGRA1:57;
A15: ((f(#)f)||A+(f(#)g)||A)|(A /\ A) is bounded & ((f(#)g)||A+(g(#)g)||A)|(A
  /\ A) is bounded by A4,A5,A6,RFUNCT_1:83;
  |||(f+g,f+g,A)||| = integral(((f(#)(f+g))+(g(#)(f+g)))||A) by RFUNCT_1:10
    .= integral(((f(#)(f+g))||A)+((g(#)(f+g))||A)) by INTEGRA5:5
    .= integral((((f(#)f)+(f(#)g))||A)+((g(#)(f+g))||A)) by RFUNCT_1:11
    .= integral((((f(#)f)+(f(#)g))||A) +(((g(#)f)+(g(#)g))||A)) by RFUNCT_1:11
    .= integral(((f(#)f)||A+(f(#)g)||A) +(((g(#)f)+(g(#)g))||A)) by INTEGRA5:5
    .= integral(((f(#)f)||A+(f(#)g)||A) +((g(#)f)||A+(g(#)g)||A)) by INTEGRA5:5
    .= integral((f(#)f)||A+(f(#)g)||A) +integral((f(#)g)||A+(g(#)g)||A) by A1
,A2,A3,A15,A14,A12,INTEGRA1:57
    .= integral((f(#)f)||A)+integral((f(#)g)||A) +integral((f(#)g)||A+(g(#)g
  )||A) by A1,A2,A4,A5,A13,A10,INTEGRA1:57
    .= integral((f(#)f)||A)+integral((f(#)g)||A) +(integral((f(#)g)||A)+
  integral((g(#)g)||A)) by A2,A3,A5,A6,A10,A11,INTEGRA1:57;
  hence thesis;
end;

begin :: Orthogonal polynomials

definition
  let A be non empty closed_interval Subset of REAL;
  let f,g be PartFunc of REAL,REAL;
  pred f is_orthogonal_with g,A means

  |||(f,g,A)||| = 0;
end;

theorem Th32:
  for f,g being PartFunc of REAL,REAL, A being non empty closed_interval
  Subset of REAL st (f(#)f)||A is total & (f(#)g)||A is total & (g(#)g)||A is
  total & (f(#)f)||A|A is bounded & (f(#)g)||A|A is bounded & (g(#)g)||A|A is
  bounded & (f(#)f) is_integrable_on A & (f(#)g) is_integrable_on A & (g(#)g)
is_integrable_on A & f is_orthogonal_with g,A holds |||(f+g,f+g,A)||| = |||(f,f
  ,A)||| + |||(g,g,A)|||
proof
  let f,g be PartFunc of REAL,REAL;
  let A be non empty closed_interval Subset of REAL;
  assume (f(#)f)||A is total & (f(#)g)||A is total & (g(#)g)||A is total & (f
(#)f ) ||A|A is bounded & (f(#)g)||A|A is bounded & (g(#)g)||A|A is bounded & (
  f(#)f ) is_integrable_on A & (f(#)g) is_integrable_on A & (g(#)g)
  is_integrable_on A;
  then
A1: |||(f+g,f+g,A)||| = |||(f,f,A)||| + 2*|||(f,g,A)||| + |||(g,g,A)||| by Th31
;
  assume f is_orthogonal_with g,A;
  then |||(f,g,A)||| = 0;
  hence thesis by A1;
end;

theorem
  for f being PartFunc of REAL,REAL,
  A being non empty closed_interval Subset of
  REAL st (f(#)f)||A is total & (f(#)f)||A|A is bounded & (f(#)f)||A is
integrable & (for x st x in A holds (f(#)f)||A.x >= 0) holds |||(f,f,A)||| >= 0
  by INTEGRA2:32;

theorem
  A = [.0,PI.] implies sin is_orthogonal_with cos,A
by INTEGRA8:92;

theorem
  A = [.0,PI*2.] implies sin is_orthogonal_with cos,A
by INTEGRA8:94;

theorem
  A = [.2*n*PI,(2*n+1)*PI.] implies sin is_orthogonal_with cos,A
by INTEGRA8:95;

theorem
  A = [.x+2*n*PI,x+(2*n+1)*PI.] implies sin is_orthogonal_with cos,A
by INTEGRA8:96;

theorem
  A = [.-PI,PI.] implies sin is_orthogonal_with cos,A
proof
  assume A = [.-PI,PI.];
  then
A1: upper_bound A = PI & lower_bound A = -PI by INTEGRA8:37;
  |||(sin,cos,A)||| = 1/2*(cos.(lower_bound A)*cos.(lower_bound A) -cos.(
  upper_bound A)*cos.(upper_bound A)) by INTEGRA8:90
    .= 1/2*(cos.(PI)*cos.(-PI)-cos.PI*cos.PI) by A1,SIN_COS:30
    .= 1/2*(cos.(PI)*cos.(PI)-cos.PI*cos.PI) by SIN_COS:30;
  hence thesis;
end;

theorem
  A = [.-PI/2,PI/2.] implies sin is_orthogonal_with cos,A
proof
  assume A = [.-PI/2,PI/2.];
  then
A1: upper_bound A = PI/2 & lower_bound A = -PI/2 by INTEGRA8:37;
  |||(sin,cos,A)||| = 1/2*(cos.(lower_bound A)*cos.(lower_bound A) -cos.(
  upper_bound A)*cos.(upper_bound A)) by INTEGRA8:90
    .= 1/2*(cos.(PI/2)*cos.(-PI/2) -cos.(PI/2)*cos.(PI/2)) by A1,SIN_COS:30
    .= 1/2*(cos.(PI/2)*cos.(PI/2) -cos.(PI/2)*cos.(PI/2)) by SIN_COS:30;
  hence thesis;
end;

theorem
  A = [.-2*PI,2*PI.] implies sin is_orthogonal_with cos,A
proof
  assume A = [.-2*PI,2*PI.];
  then
A1: upper_bound A = 2*PI & lower_bound A = -2*PI by INTEGRA8:37;
  |||(sin,cos,A)||| = 1/2*(cos.(lower_bound A)*cos.(lower_bound A) -cos.(
  upper_bound A)*cos.(upper_bound A)) by INTEGRA8:90
    .= 1/2*(cos.(2*PI)*cos.(-2*PI) -cos.(2*PI)*cos.(2*PI)) by A1,SIN_COS:30
    .= 1/2*(cos.(2*PI)*cos.(2*PI) -cos.(2*PI)*cos.(2*PI)) by SIN_COS:30;
  hence thesis;
end;

theorem
  A = [.-2*n*PI,2*n*PI.] implies sin is_orthogonal_with cos,A
proof
  assume A = [.-2*n*PI,2*n*PI.];
  then
A1: upper_bound A = 2*n*PI & lower_bound A = -2*n*PI by INTEGRA8:37;
  |||(sin,cos,A)||| = 1/2*(cos.(lower_bound A)*cos.(lower_bound A) -cos.(
  upper_bound A)*cos.(upper_bound A)) by INTEGRA8:90
    .= 1/2*(cos.(2*n*PI)*cos.(-2*n*PI) -cos.(2*n*PI)*cos.(2*n*PI)) by A1,
SIN_COS:30
    .= 1/2*(cos.(2*n*PI)*cos.(2*n*PI) -cos.(2*n*PI)*cos.(2*n*PI)) by SIN_COS:30
;
  hence thesis;
end;

theorem
  A = [.x-2*n*PI,x+2*n*PI.] implies sin is_orthogonal_with cos,A
proof
  assume A = [.x-2*n*PI,x+2*n*PI.];
  then
A1: upper_bound A = x+2*n*PI & lower_bound A = x-2*n*PI by INTEGRA8:37;
  |||(sin,cos,A)||| = 1/2*(cos.(lower_bound A)*cos.(lower_bound A) -cos.(
  upper_bound A)*cos.(upper_bound A)) by INTEGRA8:90
    .= 1/2*(cos.(2*n*PI-x)*cos.(-(2*n*PI-x)) -cos.(x+2*n*PI)*cos.(x+2*n*PI))
  by A1,SIN_COS:30
    .= 1/2*(cos.(-x+2*n*PI)*cos.(-x+2*n*PI) -cos.(x+2*n*PI)*cos.(x+2*n*PI))
  by SIN_COS:30
    .= 1/2*(cos(-x)*cos(-x+2*n*PI) -cos.(x+2*n*PI)*cos.(x+2*n*PI)) by
INTEGRA8:3
    .= 1/2*(cos(-x)*cos(-x) -cos.(x+2*n*PI)*cos.(x+2*n*PI)) by INTEGRA8:3
    .= 1/2*(cos(x)*cos(-x) -cos.(x+2*n*PI)*cos.(x+2*n*PI)) by SIN_COS:31
    .= 1/2*(cos(x)*cos(x) -cos(x+2*n*PI)*cos.(x+2*n*PI)) by SIN_COS:31
    .= 1/2*(cos(x)*cos(x) -cos(x)*cos(x+2*n*PI)) by INTEGRA8:3
    .= 1/2*(cos(x)*cos(x) - cos(x)*cos(x)) by INTEGRA8:3;
  hence thesis;
end;

begin :: Definition and properties of norm function

definition
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of REAL,REAL;
  func ||..f,A..|| -> Real equals
  sqrt (|||(f,f,A)|||);
  correctness;
end;

theorem
  for f being PartFunc of REAL,REAL,
  A being non empty closed_interval Subset of
REAL st (f(#)f)||A is total & (f(#)f)||A|A is bounded & (for x st x in A holds
  (f(#)f)||A.x >= 0) holds 0 <= ||..f,A..||
proof
  let f be PartFunc of REAL,REAL;
  let A be non empty closed_interval Subset of REAL;
  assume
A1: (f(#)f)||A is total;
  assume (f(#)f)||A|A is bounded & for x st x in A holds (f(#)f)||A.x >= 0;
  then |||(f,f,A)||| >= 0 by A1,INTEGRA2:32;
  hence thesis by SQUARE_1:def 2;
end;

theorem
  for f being PartFunc of REAL,REAL,
  A being non empty closed_interval Subset of
  REAL holds ||..(1(#)f),A..|| = ||..f,A..|| by RFUNCT_1:21;

theorem
  for f,g being PartFunc of REAL,REAL,
  A being non empty closed_interval Subset of
REAL st (f(#)f)||A is total & (f(#)g)||A is total & (g(#)g)||A is total & (f(#)
f)||A|A is bounded & (f(#)g)||A|A is bounded & (g(#)g)||A|A is bounded & (f(#)f
) is_integrable_on A & (f(#)g) is_integrable_on A & (g(#)g) is_integrable_on A
& f is_orthogonal_with g,A & (for x st x in A holds (f(#)f)||A.x >= 0) & (for x
  st x in A holds (g(#)g)||A.x >= 0) holds ||..(f+g),A..||^2 = ||..f,A..||^2 +
  ||..g,A..||^2
proof
  let f,g be PartFunc of REAL,REAL;
  let A be non empty closed_interval Subset of REAL;
  assume that
A1: (f(#)f)||A is total and
A2: (f(#)g)||A is total and
A3: (g(#)g)||A is total and
A4: (f(#)f)||A|A is bounded and
A5: (f(#)g)||A|A is bounded and
A6: (g(#)g)||A|A is bounded and
A7: (f(#)f) is_integrable_on A & (f(#)g) is_integrable_on A & (g(#)g)
  is_integrable_on A;
  assume
A8: f is_orthogonal_with g,A;
  assume for x st x in A holds (f(#)f)||A.x >= 0;
  then
A9: |||(f,f,A)||| >= 0 by A1,A4,INTEGRA2:32;
  assume for x st x in A holds (g(#)g)||A.x >= 0;
  then
A10: |||(g,g,A)||| >= 0 by A3,A6,INTEGRA2:32;
  then
A11: ||..g,A..||^2 = |||(g,g,A)||| by SQUARE_1:def 2;
  |||(f+g,f+g,A)||| = |||(f,f,A)||| + |||(g,g,A)||| by A1,A2,A3,A4,A5,A6,A7,A8
,Th32;
  then |||((f+g),(f+g),A)||| >=0 by A9,A10,XREAL_1:33;
  then
A12: ||..(f+g),A..||^2 = |||((f+g),(f+g),A)||| by SQUARE_1:def 2;
  ||..f,A..||^2 = |||(f,f,A)||| by A9,SQUARE_1:def 2;
  hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A12,A11,Th32;
end;

begin :: To be revised

reserve a,b,x for Real;

reserve n for Element of NAT;
reserve A for non empty closed_interval Subset of REAL;
reserve f,f1,f2 for PartFunc of REAL,REAL;
reserve Z for open Subset of REAL;

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

theorem
  not -a in A implies (AffineMap (1,a))^|A is continuous
proof
  set g2 = AffineMap (1,a);
  assume
A1: not -a in A;
  not 0 in rng (g2|A)
  proof
    set h2 = g2|A;
    assume 0 in rng (g2|A);
    then consider x being object such that
A2: x in dom h2 and
A3: h2.x = 0 by FUNCT_1:def 3;
    reconsider d = x as Element of REAL by A2;
A4: g2.d = a+1*d by FCONT_1:def 4;
    d in A by A2,RELAT_1:57;
    then dom h2 c= A & a+d = 0 by A3,A4,FUNCT_1:49,RELAT_1:58;
    hence thesis by A1,A2;
  end;
  then
A5: (g2|A)"{0} = {} by FUNCT_1:72;
  thus thesis by A5,FCONT_1:23;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

::  f.x= (a-x)/(a+x)

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

::  f.x= (x-a)/(x+a)

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

::  f.x= (x+a)/(x-a)

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

::  f.x= (x+a)/(x+b)

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

::  f.x= (x+a)/(x-b)

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

::  f.x= (x-a)/(x+b)

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

::  f.x= (x-a)/(x-b)

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

:: f.x=1/x

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

:: f.x=n/x

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

:: f.x=-1/x

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

:: irrational function
:: f.x = (a+x) #R (1/2)

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

:: f.x = (a-x) #R (1/2)

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

:: f.x = (a+x) #R (-1/2)

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

:: f.x = (a-x) #R (-1/2)

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

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

theorem
  A c= Z & dom ((-id Z)(#)cos+sin) = Z & (for x st x in Z holds f.x =x*
sin.x) & Z = dom f & f|A is continuous implies integral(f,A) = ((-id Z)(#)cos+
  sin).(upper_bound A)-((-id Z)(#)cos+sin).(lower_bound A)
proof
  assume that
A1: A c= Z and
A2: dom ((-id Z)(#)cos+sin) = Z and
A3: for x st x in Z holds f.x =x*sin.x and
A4: Z = dom f and
A5: f|A is continuous;
A6: (-id Z)(#)cos+sin is_differentiable_on Z by A2,FDIFF_4:46;
A7: for x being Element of REAL
st x in dom (((-id Z)(#)cos+sin)`|Z) holds (((-id Z)(#)cos+sin)`|Z)
  .x = f.x
  proof
    let x be Element of REAL;
    assume x in dom (((-id Z)(#)cos+sin)`|Z);
    then
A8: x in Z by A6,FDIFF_1:def 7;
    then (((-id Z)(#)cos+sin)`|Z).x =x*sin.x by A2,FDIFF_4:46
      .= f.x by A3,A8;
    hence thesis;
  end;
  dom (((-id Z)(#)cos+sin)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
  then
A9: (((-id Z)(#)cos+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,A9,FDIFF_4:46,INTEGRA5:13;
end;

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

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

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

theorem Th70:
  Z c= dom (-cosec) implies -cosec is_differentiable_on Z & for x
  st x in Z holds ( (-cosec)`|Z).x = cos.x/(sin.x)^2
proof
A1: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
  assume
A2: Z c= dom (-cosec);
  then
A3: Z c= dom cosec by VALUED_1:8;
  then for x st x in Z holds sin.x<>0 by RFUNCT_1:3;
  then
A4: cosec is_differentiable_on Z by A1,FDIFF_2:22;
A5: for x st x in Z holds ( (-cosec)`|Z).x= cos.x/(sin.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then
A7: sin.x<>0 & sin is_differentiable_in x by A3,A1,FDIFF_1:9,RFUNCT_1:3;
    ((-cosec)`|Z).x = (-1)*diff(sin^,x) by A2,A4,A6,FDIFF_1:20
      .= (-1)*(- diff(sin,x)/(sin.x)^2) by A7,FDIFF_2:15
      .= cos.x/(sin.x)^2 by SIN_COS:64;
    hence thesis;
  end;
  (-1)(#)cosec is_differentiable_on Z by A2,A4,FDIFF_1:20;
  hence thesis by A5;
end;

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

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