:: INTEGRA9 semantic presentation

begin

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

theorem :: INTEGRA9:1
( - (exp_R * (AffineMap ((- 1),0))) is_differentiable_on REAL & ( for x being Real 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 ((- 1),0)) by FUNCT_2:def_1;
A3: for x being Real st x in REAL holds
(AffineMap ((- 1),0)) . x = ((- 1) * x) + 0 by FCONT_1:def_4;
then A4: AffineMap ((- 1),0) is_differentiable_on REAL by A2, FDIFF_1:23;
 for x being Real st x in REAL holds
exp_R * (AffineMap ((- 1),0)) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in REAL implies exp_R * (AffineMap ((- 1),0)) is_differentiable_in x )
assume  x in REAL ; ::_thesis: exp_R * (AffineMap ((- 1),0)) is_differentiable_in x
 AffineMap ((- 1),0) is_differentiable_in x by A2, A4, FDIFF_1:9;
hence  exp_R * (AffineMap ((- 1),0)) is_differentiable_in x by TAYLOR_1:19; ::_thesis: verum
end;
then A5: exp_R * (AffineMap ((- 1),0)) is_differentiable_on REAL by A1, FDIFF_1:9;
 for x being Real st x in REAL holds
((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x)
proof
let x be Real; ::_thesis: ( x in REAL implies ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) )
assume  x in REAL ; ::_thesis: ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x)
A6: 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
.= (- 1) * ((exp_R . ((AffineMap ((- 1),0)) . x)) * (diff ((AffineMap ((- 1),0)),x))) by A6, TAYLOR_1:19
.= (- 1) * ((exp_R . ((AffineMap ((- 1),0)) . x)) * (((AffineMap ((- 1),0)) `| REAL) . x)) by A4, FDIFF_1:def_7
.= (- 1) * ((exp_R . ((AffineMap ((- 1),0)) . x)) * (- 1)) by A2, A3, FDIFF_1:23
.= (- 1) * ((exp_R . (((- 1) * x) + 0)) * (- 1)) by FCONT_1:def_4
.= exp_R (- x) ;
hence  ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ; ::_thesis: verum
end;
hence  ( - (exp_R * (AffineMap ((- 1),0))) is_differentiable_on REAL & ( for x being Real holds ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ) ) by A5, Lm1, FDIFF_1:20; ::_thesis: verum
end;

theorem Th2: :: INTEGRA9:2
for r being Real st r <> 0 holds
( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) )
proof
let r be Real; ::_thesis: ( r <> 0 implies ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) ) )
A1: [#] REAL = dom (exp_R * (AffineMap (r,0))) by FUNCT_2:def_1;
A2: [#] REAL = dom (AffineMap (r,0)) by FUNCT_2:def_1;
A3: for x being Real st x in REAL holds
(AffineMap (r,0)) . x = (r * x) + 0 by FCONT_1:def_4;
then A4: AffineMap (r,0) is_differentiable_on REAL by A2, FDIFF_1:23;
 for x being Real st x in REAL holds
exp_R * (AffineMap (r,0)) is_differentiable_in x
proof
let x be Real; ::_thesis: ( x in REAL implies exp_R * (AffineMap (r,0)) is_differentiable_in x )
assume  x in REAL ; ::_thesis: exp_R * (AffineMap (r,0)) is_differentiable_in x
 AffineMap (r,0) is_differentiable_in x by A2, A4, FDIFF_1:9;
hence  exp_R * (AffineMap (r,0)) is_differentiable_in x by TAYLOR_1:19; ::_thesis: verum
end;
then A5: ( [#] REAL = dom ((1 / r) (#) (exp_R * (AffineMap (r,0)))) & exp_R * (AffineMap (r,0)) is_differentiable_on REAL ) by A1, FDIFF_1:9, FUNCT_2:def_1;
assume A6: r <> 0 ; ::_thesis: ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) )
 for x being Real st x in REAL holds
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
proof
let x be Real; ::_thesis: ( x in REAL implies (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x )
assume  x in REAL ; ::_thesis: (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
A7: AffineMap (r,0) is_differentiable_in x by A2, A4, FDIFF_1:9;
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (1 / r) * (diff ((exp_R * (AffineMap (r,0))),x)) by A5, FDIFF_1:20
.= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (diff ((AffineMap (r,0)),x))) by A7, TAYLOR_1:19
.= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (((AffineMap (r,0)) `| REAL) . x)) by A4, FDIFF_1:def_7
.= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * r) by A2, A3, FDIFF_1:23
.= (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 A6, XCMPLX_1:60
.= (exp_R * (AffineMap (r,0))) . x by A1, FUNCT_1:12 ;
hence  (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ; ::_thesis: verum
end;
hence  ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) ) by A5, FDIFF_1:20; ::_thesis: verum
end;

theorem :: INTEGRA9:3
for r being Real
for A being non empty closed_interval Subset of REAL st r <> 0 holds
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
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL st r <> 0 holds
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))
let A be non empty closed_interval Subset of REAL; ::_thesis: ( 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)) )
A1: dom (exp_R * (AffineMap (r,0))) = REAL by FUNCT_2:def_1;
A2: (AffineMap (r,0)) | A is continuous ;
assume A3: r <> 0 ; ::_thesis: 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))
then  (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL by Th2;
then A4: dom (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) = dom (exp_R * (AffineMap (r,0))) by A1, FDIFF_1:def_7;
 exp_R | REAL is continuous by FDIFF_1:25, SIN_COS:66;
then A5: exp_R | ((AffineMap (r,0)) .: A) is continuous by FCONT_1:16;
then  (exp_R * (AffineMap (r,0))) | A is continuous by A2, FCONT_1:25;
then A6: exp_R * (AffineMap (r,0)) is_integrable_on A by A1, INTEGRA5:11;
 for x being 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 A3, Th2;
then A7: ((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL = exp_R * (AffineMap (r,0)) by A4, PARTFUN1:5;
 (exp_R * (AffineMap (r,0))) | A is bounded by A1, A2, A5, FCONT_1:25, INTEGRA5:10;
hence  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)) by A3, A6, A7, Th2, INTEGRA5:13; ::_thesis: verum
end;

theorem Th4: :: INTEGRA9:4
for n being Element of NAT st n <> 0 holds
( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) )
proof
let n be Element of NAT ; ::_thesis: ( n <> 0 implies ( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) ) )
A1: [#] REAL = dom ((- (1 / n)) (#) (cos * (AffineMap (n,0)))) by FUNCT_2:def_1;
A2: ( [#] REAL = dom (cos * (AffineMap (n,0))) & ( for x being Real st x in REAL holds
(AffineMap (n,0)) . x = (n * x) + 0 ) ) by FCONT_1:def_4, FUNCT_2:def_1;
then A3: cos * (AffineMap (n,0)) is_differentiable_on REAL by FDIFF_4:38;
assume A4: n <> 0 ; ::_thesis: ( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) )
 for x being Real st x in REAL holds
(((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x)
proof
let x be Real; ::_thesis: ( x in REAL implies (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) )
assume  x in REAL ; ::_thesis: (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x)
(((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (- (1 / n)) * (diff ((cos * (AffineMap (n,0))),x)) by A1, A3, FDIFF_1:20
.= (- (1 / n)) * (((cos * (AffineMap (n,0))) `| REAL) . x) by A3, FDIFF_1:def_7
.= (- (1 / n)) * (- (n * (sin . ((n * x) + 0)))) by A2, FDIFF_4:38
.= ((1 / n) * n) * (sin . ((n * x) + 0))
.= (n / n) * (sin . ((n * x) + 0)) by XCMPLX_1:99
.= 1 * (sin . ((n * x) + 0)) by A4, XCMPLX_1:60
.= sin (n * x) ;
hence  (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ; ::_thesis: verum
end;
hence  ( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) ) by A1, A3, FDIFF_1:20; ::_thesis: verum
end;

theorem :: INTEGRA9:5
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st n <> 0 holds
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
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st n <> 0 holds
integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: ( 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)) )
assume A1: n <> 0 ; ::_thesis: integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A))
A2: [#] REAL = dom (sin * (AffineMap (n,0))) by FUNCT_2:def_1;
A3: for x being Real st x in REAL holds
(AffineMap (n,0)) . x = n * x
proof
let x be Real; ::_thesis: ( x in REAL implies (AffineMap (n,0)) . x = n * x )
assume  x in REAL ; ::_thesis: (AffineMap (n,0)) . x = n * x
(AffineMap (n,0)) . x = (n * x) + 0 by FCONT_1:def_4
.= n * x ;
hence  (AffineMap (n,0)) . x = n * x ; ::_thesis: verum
end;
A4: for x being 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 Real; ::_thesis: ( x in dom (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) implies (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (sin * (AffineMap (n,0))) . x )
assume  x in dom (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) ; ::_thesis: (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (sin * (AffineMap (n,0))) . x
(((- (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  (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (sin * (AffineMap (n,0))) . x ; ::_thesis: verum
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;
A6: (AffineMap (n,0)) | A is continuous ;
 sin | REAL is continuous by FDIFF_1:25, SIN_COS:68;
then A7: sin | ((AffineMap (n,0)) .: A) is continuous by FCONT_1:16;
then  (sin * (AffineMap (n,0))) | A is continuous by A6, FCONT_1:25;
then A8: sin * (AffineMap (n,0)) is_integrable_on A by A2, INTEGRA5:11;
 (sin * (AffineMap (n,0))) | A is bounded by A2, A6, A7, FCONT_1:25, INTEGRA5:10;
hence  integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A)) by A1, A8, A5, Th4, INTEGRA5:13; ::_thesis: verum
end;

theorem Th6: :: INTEGRA9:6
for n being Element of NAT st n <> 0 holds
( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) )
proof
let n be Element of NAT ; ::_thesis: ( n <> 0 implies ( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) ) )
A1: [#] REAL = dom ((1 / n) (#) (sin * (AffineMap (n,0)))) by FUNCT_2:def_1;
A2: ( [#] REAL = dom (sin * (AffineMap (n,0))) & ( for x being Real st x in REAL holds
(AffineMap (n,0)) . x = (n * x) + 0 ) ) by FCONT_1:def_4, FUNCT_2:def_1;
then A3: sin * (AffineMap (n,0)) is_differentiable_on REAL by FDIFF_4:37;
assume A4: n <> 0 ; ::_thesis: ( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) )
 for x being Real st x in REAL holds
(((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x)
proof
let x be Real; ::_thesis: ( x in REAL implies (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) )
assume  x in REAL ; ::_thesis: (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x)
(((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (1 / n) * (diff ((sin * (AffineMap (n,0))),x)) by A1, A3, FDIFF_1:20
.= (1 / n) * (((sin * (AffineMap (n,0))) `| REAL) . x) by A3, FDIFF_1:def_7
.= (1 / n) * (n * (cos . ((n * x) + 0))) by A2, FDIFF_4:37
.= (n * (1 / n)) * (cos . ((n * x) + 0))
.= (n / n) * (cos . ((n * x) + 0)) by XCMPLX_1:99
.= 1 * (cos . ((n * x) + 0)) by A4, XCMPLX_1:60
.= cos (n * x) ;
hence  (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ; ::_thesis: verum
end;
hence  ( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) ) by A1, A3, FDIFF_1:20; ::_thesis: verum
end;

theorem :: INTEGRA9:7
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st n <> 0 holds
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
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st n <> 0 holds
integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: ( 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)) )
assume A1: n <> 0 ; ::_thesis: integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A))
A2: [#] REAL = dom (cos * (AffineMap (n,0))) by FUNCT_2:def_1;
A3: for x being Real st x in REAL holds
(AffineMap (n,0)) . x = n * x
proof
let x be Real; ::_thesis: ( x in REAL implies (AffineMap (n,0)) . x = n * x )
assume  x in REAL ; ::_thesis: (AffineMap (n,0)) . x = n * x
(AffineMap (n,0)) . x = (n * x) + 0 by FCONT_1:def_4
.= n * x ;
hence  (AffineMap (n,0)) . x = n * x ; ::_thesis: verum
end;
A4: for x being 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 Real; ::_thesis: ( x in dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) implies (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x )
assume  x in dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) ; ::_thesis: (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x
(((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  (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x ; ::_thesis: verum
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;
A6: (AffineMap (n,0)) | A is continuous ;
 cos | REAL is continuous by FDIFF_1:25, SIN_COS:67;
then A7: cos | ((AffineMap (n,0)) .: A) is continuous by FCONT_1:16;
then  (cos * (AffineMap (n,0))) | A is continuous by A6, FCONT_1:25;
then A8: cos * (AffineMap (n,0)) is_integrable_on A by A2, INTEGRA5:11;
 (cos * (AffineMap (n,0))) | A is bounded by A2, A6, A7, FCONT_1:25, INTEGRA5:10;
hence  integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A)) by A1, A8, A5, Th6, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:8
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z holds
integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) )
assume A1: A c= Z ; ::_thesis: integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))
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 being Real st x in Z holds
((id Z) (#) sin) . x = x * (sin . x)
proof
let x be Real; ::_thesis: ( x in Z implies ((id Z) (#) sin) . x = x * (sin . x) )
assume A6: x in Z ; ::_thesis: ((id Z) (#) sin) . x = x * (sin . x)
((id Z) (#) sin) . x = ((id Z) . x) * (sin . x) by VALUED_1:5
.= x * (sin . x) by A6, FUNCT_1:18 ;
hence  ((id Z) (#) sin) . x = x * (sin . x) ; ::_thesis: verum
end;
A7: for x being 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 Real; ::_thesis: ( x in dom ((((- (id Z)) (#) cos) + sin) `| Z) implies ((((- (id Z)) (#) cos) + sin) `| Z) . x = ((id Z) (#) sin) . x )
assume  x in dom ((((- (id Z)) (#) cos) + sin) `| Z) ; ::_thesis: ((((- (id Z)) (#) cos) + sin) `| Z) . x = ((id Z) (#) sin) . x
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  ((((- (id Z)) (#) cos) + sin) `| Z) . x = ((id Z) (#) sin) . x ; ::_thesis: verum
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;
A11: ((id Z) (#) sin) | Z is continuous by A9, FDIFF_1:25, FDIFF_4:45;
then  ((id Z) (#) sin) | A is continuous by A1, FCONT_1:16;
then A12: (id Z) (#) sin is_integrable_on A by A1, A9, INTEGRA5:11;
 ((id Z) (#) sin) | A is bounded by A1, A9, A11, FCONT_1:16, INTEGRA5:10;
hence  integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) by A1, A3, A12, A10, FDIFF_4:46, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:9
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z holds
integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A)) )
assume A1: A c= Z ; ::_thesis: integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A))
A2: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
A3: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
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 A4: dom (((id Z) (#) sin) + cos) = Z by RELAT_1:45;
then A5: ((id Z) (#) sin) + cos is_differentiable_on Z by FDIFF_4:47;
A6: for x being Real st x in Z holds
((id Z) (#) cos) . x = x * (cos . x)
proof
let x be Real; ::_thesis: ( x in Z implies ((id Z) (#) cos) . x = x * (cos . x) )
assume A7: x in Z ; ::_thesis: ((id Z) (#) cos) . x = x * (cos . x)
((id Z) (#) cos) . x = ((id Z) . x) * (cos . x) by VALUED_1:5
.= x * (cos . x) by A7, FUNCT_1:18 ;
hence  ((id Z) (#) cos) . x = x * (cos . x) ; ::_thesis: verum
end;
A8: for x being 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 Real; ::_thesis: ( x in dom ((((id Z) (#) sin) + cos) `| Z) implies ((((id Z) (#) sin) + cos) `| Z) . x = ((id Z) (#) cos) . x )
assume  x in dom ((((id Z) (#) sin) + cos) `| Z) ; ::_thesis: ((((id Z) (#) sin) + cos) `| Z) . x = ((id Z) (#) cos) . x
then A9: x in Z by A5, FDIFF_1:def_7;
then ((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) by A4, FDIFF_4:47
.= ((id Z) (#) cos) . x by A6, A9 ;
hence  ((((id Z) (#) sin) + cos) `| Z) . x = ((id Z) (#) cos) . x ; ::_thesis: verum
end;
A10: 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 A5, FDIFF_1:def_7;
then A11: (((id Z) (#) sin) + cos) `| Z = (id Z) (#) cos by A8, PARTFUN1:5;
 Z = (dom (id Z)) /\ (dom cos) by A10, VALUED_1:def_4;
then  Z c= dom (id Z) by XBOOLE_1:18;
then  id Z is_differentiable_on Z by A3, FDIFF_1:23;
then A12: ((id Z) (#) cos) | Z is continuous by A10, A2, FDIFF_1:21, FDIFF_1:25;
then  ((id Z) (#) cos) | A is continuous by A1, FCONT_1:16;
then A13: (id Z) (#) cos is_integrable_on A by A1, A10, INTEGRA5:11;
 ((id Z) (#) cos) | A is bounded by A1, A10, A12, FCONT_1:16, INTEGRA5:10;
hence  integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A)) by A1, A4, A13, A11, FDIFF_4:47, INTEGRA5:13; ::_thesis: verum
end;

theorem Th10: :: INTEGRA9:10
for Z being open Subset of REAL holds
( (id Z) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( (id Z) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) ) )
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 being Real 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 being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((id_Z)_(#)_cos)_`|_Z)_._x_=_(cos_._x)_-_(x_*_(sin_._x))
let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) )
assume A6: x in Z ; ::_thesis: (((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x))
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)) ;
::_thesis: verum
end;
hence  ( (id Z) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) ) ) by A2, A4, A1, FDIFF_1:21; ::_thesis: verum
end;

Lm2:  for x being Real holds
( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) )
proof
let x be Real; ::_thesis: ( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) )
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  ( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) ) by A1, INTEGRA8:22; ::_thesis: verum
end;

theorem Th11: :: INTEGRA9:11
for Z being open Subset of REAL holds
( (- sin) + ((id Z) (#) cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( (- sin) + ((id Z) (#) cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) ) )
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__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((-_sin)_+_((id_Z)_(#)_cos))_`|_Z)_._x_=_-_(x_*_(sin_._x))
let x be Real; ::_thesis: ( x in Z implies (((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) )
assume A4: x in Z ; ::_thesis: (((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x))
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)) ;
::_thesis: verum
end;
hence  ( (- sin) + ((id Z) (#) cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) ) ) by A1, A2, A3, FDIFF_1:18; ::_thesis: verum
end;

theorem :: INTEGRA9:12
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z holds
integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A)) )
assume A1: A c= Z ; ::_thesis: integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A))
A2: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
A3: (- sin) + ((id Z) (#) cos) is_differentiable_on Z by Th11;
A4: for x being Real st x in Z holds
(- (id Z)) . x = ((- 1) * x) + 0
proof
let x be Real; ::_thesis: ( x in Z implies (- (id Z)) . x = ((- 1) * x) + 0 )
assume A5: x in Z ; ::_thesis: (- (id Z)) . x = ((- 1) * x) + 0
(- (id Z)) . x = - ((id Z) . x) by VALUED_1:8
.= - x by A5, FUNCT_1:18
.= ((- 1) * x) + 0 ;
hence  (- (id Z)) . x = ((- 1) * x) + 0 ; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
((- (id Z)) (#) sin) . x = - (x * (sin . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((- (id Z)) (#) sin) . x = - (x * (sin . x)) )
assume A7: x in Z ; ::_thesis: ((- (id Z)) (#) sin) . x = - (x * (sin . x))
((- (id Z)) (#) sin) . x = ((- (id Z)) . x) * (sin . x) by VALUED_1:5
.= (((- 1) * x) + 0) * (sin . x) by A4, A7
.= - (x * (sin . x)) ;
hence  ((- (id Z)) (#) sin) . x = - (x * (sin . x)) ; ::_thesis: verum
end;
A8: for x being 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 Real; ::_thesis: ( x in dom (((- sin) + ((id Z) (#) cos)) `| Z) implies (((- sin) + ((id Z) (#) cos)) `| Z) . x = ((- (id Z)) (#) sin) . x )
assume  x in dom (((- sin) + ((id Z) (#) cos)) `| Z) ; ::_thesis: (((- sin) + ((id Z) (#) cos)) `| Z) . x = ((- (id Z)) (#) sin) . x
then A9: x in Z by A3, FDIFF_1:def_7;
then (((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) by Th11
.= ((- (id Z)) (#) sin) . x by A6, A9 ;
hence  (((- sin) + ((id Z) (#) cos)) `| Z) . x = ((- (id Z)) (#) sin) . x ; ::_thesis: verum
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 A10: Z = dom ((- (id Z)) (#) sin) by RELAT_1:45;
then  dom (((- sin) + ((id Z) (#) cos)) `| Z) = dom ((- (id Z)) (#) sin) by A3, FDIFF_1:def_7;
then A11: ((- sin) + ((id Z) (#) cos)) `| Z = (- (id Z)) (#) sin by A8, PARTFUN1:5;
 Z c= (dom (- (id Z))) /\ (dom sin) by A10, VALUED_1:def_4;
then  Z c= dom (- (id Z)) by XBOOLE_1:18;
then  - (id Z) is_differentiable_on Z by A4, FDIFF_1:23;
then A12: ((- (id Z)) (#) sin) | Z is continuous by A10, A2, FDIFF_1:21, FDIFF_1:25;
then  ((- (id Z)) (#) sin) | A is continuous by A1, FCONT_1:16;
then A13: (- (id Z)) (#) sin is_integrable_on A by A1, A10, INTEGRA5:11;
 ((- (id Z)) (#) sin) | A is bounded by A1, A10, A12, FCONT_1:16, INTEGRA5:10;
hence  integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A)) by A1, A13, A11, Th11, INTEGRA5:13; ::_thesis: verum
end;

theorem Th13: :: INTEGRA9:13
for Z being open Subset of REAL holds
( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) )
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__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
(((-_cos)_-_((id_Z)_(#)_sin))_`|_Z)_._x_=_-_(x_*_(cos_._x))
let x be Real; ::_thesis: ( x in Z implies (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) )
assume A5: x in Z ; ::_thesis: (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x))
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
.= (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)) ;
::_thesis: verum
end;
hence  ( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) ) by A1, A3, A4, FDIFF_1:19; ::_thesis: verum
end;

theorem :: INTEGRA9:14
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z holds
integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A)) )
assume A1: A c= Z ; ::_thesis: integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A))
A2: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
A3: (- cos) - ((id Z) (#) sin) is_differentiable_on Z by Th13;
A4: for x being Real st x in Z holds
(- (id Z)) . x = ((- 1) * x) + 0
proof
let x be Real; ::_thesis: ( x in Z implies (- (id Z)) . x = ((- 1) * x) + 0 )
assume A5: x in Z ; ::_thesis: (- (id Z)) . x = ((- 1) * x) + 0
(- (id Z)) . x = - ((id Z) . x) by VALUED_1:8
.= - x by A5, FUNCT_1:18
.= ((- 1) * x) + 0 ;
hence  (- (id Z)) . x = ((- 1) * x) + 0 ; ::_thesis: verum
end;
A6: for x being Real st x in Z holds
((- (id Z)) (#) cos) . x = - (x * (cos . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((- (id Z)) (#) cos) . x = - (x * (cos . x)) )
assume A7: x in Z ; ::_thesis: ((- (id Z)) (#) cos) . x = - (x * (cos . x))
((- (id Z)) (#) cos) . x = ((- (id Z)) . x) * (cos . x) by VALUED_1:5
.= (((- 1) * x) + 0) * (cos . x) by A4, A7
.= - (x * (cos . x)) ;
hence  ((- (id Z)) (#) cos) . x = - (x * (cos . x)) ; ::_thesis: verum
end;
A8: for x being 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 Real; ::_thesis: ( x in dom (((- cos) - ((id Z) (#) sin)) `| Z) implies (((- cos) - ((id Z) (#) sin)) `| Z) . x = ((- (id Z)) (#) cos) . x )
assume  x in dom (((- cos) - ((id Z) (#) sin)) `| Z) ; ::_thesis: (((- cos) - ((id Z) (#) sin)) `| Z) . x = ((- (id Z)) (#) cos) . x
then A9: x in Z by A3, FDIFF_1:def_7;
then (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) by Th13
.= ((- (id Z)) (#) cos) . x by A6, A9 ;
hence  (((- cos) - ((id Z) (#) sin)) `| Z) . x = ((- (id Z)) (#) cos) . x ; ::_thesis: verum
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 A10: Z = dom ((- (id Z)) (#) cos) by RELAT_1:45;
then  dom (((- cos) - ((id Z) (#) sin)) `| Z) = dom ((- (id Z)) (#) cos) by A3, FDIFF_1:def_7;
then A11: ((- cos) - ((id Z) (#) sin)) `| Z = (- (id Z)) (#) cos by A8, PARTFUN1:5;
 Z = (dom (- (id Z))) /\ (dom cos) by A10, VALUED_1:def_4;
then  Z c= dom (- (id Z)) by XBOOLE_1:18;
then  - (id Z) is_differentiable_on Z by A4, FDIFF_1:23;
then A12: ((- (id Z)) (#) cos) | Z is continuous by A10, A2, FDIFF_1:21, FDIFF_1:25;
then  ((- (id Z)) (#) cos) | A is continuous by A1, FCONT_1:16;
then A13: (- (id Z)) (#) cos is_integrable_on A by A1, A10, INTEGRA5:11;
 ((- (id Z)) (#) cos) | A is bounded by A1, A10, A12, FCONT_1:16, INTEGRA5:10;
hence  integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A)) by A1, A13, A11, Th13, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:15
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z holds
integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A)) )
assume A1: A c= Z ; ::_thesis: integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A))
A2: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
A3: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
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 A4: Z = dom (sin + ((id Z) (#) cos)) by RELAT_1:45;
then  Z = (dom sin) /\ (dom ((id Z) (#) cos)) by VALUED_1:def_1;
then A5: Z c= dom ((id Z) (#) cos) by XBOOLE_1:18;
then  Z c= (dom (id Z)) /\ (dom cos) by VALUED_1:def_4;
then  Z c= dom (id Z) by XBOOLE_1:18;
then  id Z is_differentiable_on Z by A3, FDIFF_1:23;
then  ( sin is_differentiable_on Z & (id Z) (#) cos is_differentiable_on Z ) by A5, A2, FDIFF_1:21, FDIFF_1:26, SIN_COS:68;
then A6: (sin + ((id Z) (#) cos)) | Z is continuous by A4, FDIFF_1:18, FDIFF_1:25;
then  (sin + ((id Z) (#) cos)) | A is continuous by A1, FCONT_1:16;
then A7: sin + ((id Z) (#) cos) is_integrable_on A by A1, A4, INTEGRA5:11;
A8: 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 A9: (id Z) (#) sin is_differentiable_on Z by FDIFF_4:45;
A10: for x being Real st x in Z holds
(sin + ((id Z) (#) cos)) . x = (sin . x) + (x * (cos . x))
proof
let x be Real; ::_thesis: ( x in Z implies (sin + ((id Z) (#) cos)) . x = (sin . x) + (x * (cos . x)) )
assume A11: x in Z ; ::_thesis: (sin + ((id Z) (#) cos)) . x = (sin . x) + (x * (cos . x))
then (sin + ((id Z) (#) cos)) . x = (sin . x) + (((id Z) (#) cos) . x) by A4, VALUED_1:def_1
.= (sin . x) + (((id Z) . x) * (cos . x)) by VALUED_1:5
.= (sin . x) + (x * (cos . x)) by A11, FUNCT_1:18 ;
hence  (sin + ((id Z) (#) cos)) . x = (sin . x) + (x * (cos . x)) ; ::_thesis: verum
end;
A12: for x being Real st x in dom (((id Z) (#) sin) `| Z) holds
(((id Z) (#) sin) `| Z) . x = (sin + ((id Z) (#) cos)) . x
proof
let x be Real; ::_thesis: ( x in dom (((id Z) (#) sin) `| Z) implies (((id Z) (#) sin) `| Z) . x = (sin + ((id Z) (#) cos)) . x )
assume  x in dom (((id Z) (#) sin) `| Z) ; ::_thesis: (((id Z) (#) sin) `| Z) . x = (sin + ((id Z) (#) cos)) . x
then A13: x in Z by A9, FDIFF_1:def_7;
then (((id Z) (#) sin) `| Z) . x = (sin . x) + (x * (cos . x)) by A8, FDIFF_4:45
.= (sin + ((id Z) (#) cos)) . x by A10, A13 ;
hence  (((id Z) (#) sin) `| Z) . x = (sin + ((id Z) (#) cos)) . x ; ::_thesis: verum
end;
 dom (((id Z) (#) sin) `| Z) = dom (sin + ((id Z) (#) cos)) by A4, A9, FDIFF_1:def_7;
then A14: ((id Z) (#) sin) `| Z = sin + ((id Z) (#) cos) by A12, PARTFUN1:5;
 (sin + ((id Z) (#) cos)) | A is bounded by A1, A4, A6, FCONT_1:16, INTEGRA5:10;
hence  integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A)) by A1, A8, A7, A14, FDIFF_4:45, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:16
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z holds
integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A)) )
assume A1: A c= Z ; ::_thesis: integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A))
A2: - cos is_differentiable_on Z by FDIFF_1:26, INTEGRA8:26;
A3: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
A4: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
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 A5: Z = dom ((- cos) + ((id Z) (#) sin)) by RELAT_1:45;
then  Z = (dom (- cos)) /\ (dom ((id Z) (#) sin)) by VALUED_1:def_1;
then A6: Z c= dom ((id Z) (#) sin) by XBOOLE_1:18;
then  Z c= (dom (id Z)) /\ (dom sin) by VALUED_1:def_4;
then  Z c= dom (id Z) by XBOOLE_1:18;
then  id Z is_differentiable_on Z by A4, FDIFF_1:23;
then  (id Z) (#) sin is_differentiable_on Z by A6, A3, FDIFF_1:21;
then A7: ((- cos) + ((id Z) (#) sin)) | Z is continuous by A5, A2, FDIFF_1:18, FDIFF_1:25;
then  ((- cos) + ((id Z) (#) sin)) | A is continuous by A1, FCONT_1:16;
then A8: (- cos) + ((id Z) (#) sin) is_integrable_on A by A1, A5, 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 A9: dom ((- (id Z)) (#) cos) = Z by RELAT_1:45;
then A10: (- (id Z)) (#) cos is_differentiable_on Z by FDIFF_4:44;
A11: for x being Real st x in Z holds
((- cos) + ((id Z) (#) sin)) . x = (- (cos . x)) + (x * (sin . x))
proof
let x be Real; ::_thesis: ( x in Z implies ((- cos) + ((id Z) (#) sin)) . x = (- (cos . x)) + (x * (sin . x)) )
assume A12: x in Z ; ::_thesis: ((- cos) + ((id Z) (#) sin)) . x = (- (cos . x)) + (x * (sin . x))
then ((- cos) + ((id Z) (#) sin)) . x = ((- cos) . x) + (((id Z) (#) sin) . x) by A5, VALUED_1:def_1
.= ((- cos) . x) + (((id Z) . x) * (sin . x)) by VALUED_1:5
.= ((- cos) . x) + (x * (sin . x)) by A12, FUNCT_1:18
.= (- (cos . x)) + (x * (sin . x)) by VALUED_1:8 ;
hence  ((- cos) + ((id Z) (#) sin)) . x = (- (cos . x)) + (x * (sin . x)) ; ::_thesis: verum
end;
A13: for x being Real st x in dom (((- (id Z)) (#) cos) `| Z) holds
(((- (id Z)) (#) cos) `| Z) . x = ((- cos) + ((id Z) (#) sin)) . x
proof
let x be Real; ::_thesis: ( x in dom (((- (id Z)) (#) cos) `| Z) implies (((- (id Z)) (#) cos) `| Z) . x = ((- cos) + ((id Z) (#) sin)) . x )
assume  x in dom (((- (id Z)) (#) cos) `| Z) ; ::_thesis: (((- (id Z)) (#) cos) `| Z) . x = ((- cos) + ((id Z) (#) sin)) . x
then A14: x in Z by A10, FDIFF_1:def_7;
then (((- (id Z)) (#) cos) `| Z) . x = (- (cos . x)) + (x * (sin . x)) by A9, FDIFF_4:44
.= ((- cos) + ((id Z) (#) sin)) . x by A11, A14 ;
hence  (((- (id Z)) (#) cos) `| Z) . x = ((- cos) + ((id Z) (#) sin)) . x ; ::_thesis: verum
end;
 dom (((- (id Z)) (#) cos) `| Z) = dom ((- cos) + ((id Z) (#) sin)) by A5, A10, FDIFF_1:def_7;
then A15: ((- (id Z)) (#) cos) `| Z = (- cos) + ((id Z) (#) sin) by A13, PARTFUN1:5;
 ((- cos) + ((id Z) (#) sin)) | A is bounded by A1, A5, A7, FCONT_1:16, INTEGRA5:10;
hence  integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A)) by A1, A9, A8, A15, FDIFF_4:44, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:17
for A being non empty closed_interval Subset of REAL holds integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A))
A1: for x being Real st x in REAL holds
(AffineMap (1,(- 1))) . x = x - 1
proof
let x be Real; ::_thesis: ( x in REAL implies (AffineMap (1,(- 1))) . x = x - 1 )
assume  x in REAL ; ::_thesis: (AffineMap (1,(- 1))) . x = x - 1
(AffineMap (1,(- 1))) . x = (1 * x) + (- 1) by FCONT_1:def_4
.= x - 1 ;
hence  (AffineMap (1,(- 1))) . x = x - 1 ; ::_thesis: verum
end;
A2: dom (exp_R (#) (AffineMap (1,(- 1)))) = [#] REAL by FUNCT_2:def_1;
A3: for x being Real st x in REAL holds
((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x)
proof
let x be Real; ::_thesis: ( x in REAL implies ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x) )
assume  x in REAL ; ::_thesis: ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x)
((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  ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x) ; ::_thesis: verum
end;
A4: for x being 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 Real; ::_thesis: ( x in dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) implies ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x )
assume  x in dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) ; ::_thesis: ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x
((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  ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x ; ::_thesis: verum
end;
A5: [#] REAL = dom ((AffineMap (1,0)) (#) exp_R) by FUNCT_2:def_1;
 ( dom (AffineMap (1,0)) = [#] REAL & ( for x being Real 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  (AffineMap (1,0)) (#) exp_R is_differentiable_on REAL by A5, FDIFF_1:21, TAYLOR_1:16;
then A6: ((AffineMap (1,0)) (#) exp_R) | REAL is continuous by FDIFF_1:25;
then  ((AffineMap (1,0)) (#) exp_R) | A is continuous by FCONT_1:16;
then A7: (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 A8: (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, A6, FCONT_1:16, INTEGRA5:10;
hence  integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A)) by A2, A1, A7, A8, FDIFF_4:55, INTEGRA5:13; ::_thesis: verum
end;

theorem Th18: :: INTEGRA9:18
for n being Element of NAT holds
( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ) )
proof
let n be Element of NAT ; ::_thesis: ( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ) )
A1: [#] REAL = dom ((1 / (n + 1)) (#) (#Z (n + 1))) by FUNCT_2:def_1;
 ( [#] REAL = dom (#Z (n + 1)) & ( for x being Real 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;
A3: for x being Real st x in REAL holds
((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n)
proof
set m = n + 1;
let x be Real; ::_thesis: ( x in REAL implies ((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n) )
assume  x in REAL ; ::_thesis: ((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n)
 diff ((#Z (n + 1)),x) = (n + 1) * (x #Z ((n + 1) - 1)) by TAYLOR_1:2;
hence  ((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n) by A2, FDIFF_1:def_7; ::_thesis: verum
end;
 for x being Real st x in REAL holds
(((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n
proof
let x be Real; ::_thesis: ( x in REAL implies (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n )
assume  x in REAL ; ::_thesis: (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n
(((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = (1 / (n + 1)) * (diff ((#Z (n + 1)),x)) by A1, A2, FDIFF_1:20
.= (1 / (n + 1)) * (((#Z (n + 1)) `| REAL) . x) by A2, FDIFF_1:def_7
.= (1 / (n + 1)) * ((n + 1) * (x #Z n)) by A3
.= ((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  (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ; ::_thesis: verum
end;
hence  ( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ) ) by A1, A2, FDIFF_1:20; ::_thesis: verum
end;

theorem :: INTEGRA9:19
for n being Element of NAT
for A being non empty closed_interval Subset of REAL holds integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1)))
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL holds integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1)))
let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1)))
A1: dom (#Z n) = [#] REAL by FUNCT_2:def_1;
A2: for x being 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 Real; ::_thesis: ( x in dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) implies (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = (#Z n) . x )
assume  x in dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) ; ::_thesis: (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = (#Z n) . x
(((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n by Th18
.= (#Z n) . x by TAYLOR_1:def_1 ;
hence  (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = (#Z n) . x ; ::_thesis: verum
end;
 ( dom (#Z (n + 1)) = [#] REAL & ( for x being Real 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 being Real 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  integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1))) ; ::_thesis: verum
end;

begin

theorem Th20: :: INTEGRA9:20
for f, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds (f - g) || C = (f || C) - (g || C)
proof
let f, g be PartFunc of REAL,REAL; ::_thesis: for C being non empty Subset of REAL holds (f - g) || C = (f || C) - (g || C)
let C be non empty Subset of REAL; ::_thesis: (f - g) || C = (f || C) - (g || C)
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; ::_thesis: ( c in dom ((f - g) || C) implies ((f - g) || C) . c = ((f || C) - (g || C)) . c )
assume A4: c in dom ((f - g) || C) ; ::_thesis: ((f - g) || C) . c = ((f || C) - (g || C)) . 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  ((f - g) || C) . c = ((f || C) - (g || C)) . c by A8, A9, FUNCT_1:47; ::_thesis: verum
end;
hence  (f - g) || C = (f || C) - (g || C) by A2, A1, PARTFUN1:5, XBOOLE_1:16; ::_thesis: verum
end;

theorem Th21: :: INTEGRA9:21
for f1, f2, g being PartFunc of REAL,REAL
for 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; ::_thesis: for C being non empty Subset of REAL holds ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C
let C be non empty Subset of REAL; ::_thesis: ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C
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; ::_thesis: ( c in dom (((f1 + f2) || C) (#) (g || C)) implies (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c )
assume A3: c in dom (((f1 + f2) || C) (#) (g || C)) ; ::_thesis: (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . 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  (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c by A5, A11, FUNCT_1:47; ::_thesis: verum
end;
hence  ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C by A2, A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th22: :: INTEGRA9:22
for f1, f2, g being PartFunc of REAL,REAL
for 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; ::_thesis: for C being non empty Subset of REAL holds ((f1 - f2) || C) (#) (g || C) = ((f1 (#) g) - (f2 (#) g)) || C
let C be non empty Subset of REAL; ::_thesis: ((f1 - f2) || C) (#) (g || C) = ((f1 (#) g) - (f2 (#) g)) || C
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; ::_thesis: ( c in dom (((f1 - f2) || C) (#) (g || C)) implies (((f1 - f2) || C) (#) (g || C)) . c = (((f1 (#) g) - (f2 (#) g)) || C) . c )
assume A3: c in dom (((f1 - f2) || C) (#) (g || C)) ; ::_thesis: (((f1 - f2) || C) (#) (g || C)) . c = (((f1 (#) g) - (f2 (#) g)) || C) . 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  (((f1 - f2) || C) (#) (g || C)) . c = (((f1 (#) g) - (f2 (#) g)) || C) . c by A5, A11, FUNCT_1:47; ::_thesis: verum
end;
hence  ((f1 - f2) || C) (#) (g || C) = ((f1 (#) g) - (f2 (#) g)) || C by A2, A1, PARTFUN1:5; ::_thesis: verum
end;

theorem :: INTEGRA9:23
for f1, f2, g being PartFunc of REAL,REAL
for 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; ::_thesis: for C being non empty Subset of REAL holds ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C)
let C be non empty Subset of REAL; ::_thesis: ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C)
 ( ((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  ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C) by RFUNCT_1:9; ::_thesis: verum
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 :: INTEGRA9:def 1
 integral ((f (#) g),A);
correctness
coherence
integral ((f (#) g),A) is Real;
;
end;

:: deftheorem  defines |||( INTEGRA9:def_1_:_
 for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL holds |||(f,g,A)||| = integral ((f (#) g),A);

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

theorem :: INTEGRA9:25
for f1, f2, g being PartFunc of REAL,REAL
for 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; ::_thesis: for 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)|||
let A be non empty closed_interval Subset of REAL; ::_thesis: ( (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 implies |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| )
assume A1: ( (f1 (#) g) || A is total & (f2 (#) g) || A is total ) ; ::_thesis: ( not ((f1 (#) g) || A) | A is bounded or not (f1 (#) g) || A is integrable or not ((f2 (#) g) || A) | A is bounded or not (f2 (#) g) || A is integrable or |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| )
assume A2: ( ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable ) ; ::_thesis: |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)|||
|||((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  |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| ; ::_thesis: verum
end;

theorem :: INTEGRA9:26
for f1, f2, g being PartFunc of REAL,REAL
for 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; ::_thesis: for 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)|||
let A be non empty closed_interval Subset of REAL; ::_thesis: ( (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 implies |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| )
assume A1: ( (f1 (#) g) || A is total & (f2 (#) g) || A is total ) ; ::_thesis: ( not ((f1 (#) g) || A) | A is bounded or not (f1 (#) g) || A is integrable or not ((f2 (#) g) || A) | A is bounded or not (f2 (#) g) || A is integrable or |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| )
assume A2: ( ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable ) ; ::_thesis: |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)|||
|||((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  |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| ; ::_thesis: verum
end;

theorem :: INTEGRA9:27
for f, g being PartFunc of REAL,REAL
for 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 be PartFunc of REAL,REAL; ::_thesis: for 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)|||
let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) implies |||((- f),g,A)||| = - |||(f,g,A)||| )
assume A1: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) ) ; ::_thesis: |||((- f),g,A)||| = - |||(f,g,A)|||
|||((- 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  |||((- f),g,A)||| = - |||(f,g,A)||| ; ::_thesis: verum
end;

theorem :: INTEGRA9:28
for r being Real
for f, g being PartFunc of REAL,REAL
for 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 r be Real; ::_thesis: for f, g being PartFunc of REAL,REAL
for 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)|||
let f, g be PartFunc of REAL,REAL; ::_thesis: for 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)|||
let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) implies |||((r (#) f),g,A)||| = r * |||(f,g,A)||| )
assume A1: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) ) ; ::_thesis: |||((r (#) f),g,A)||| = r * |||(f,g,A)|||
|||((r (#) f),g,A)||| = integral ((r (#) (f (#) g)),A) by RFUNCT_1:12
.= r * (integral ((f (#) g),A)) by A1, INTEGRA6:9 ;
hence  |||((r (#) f),g,A)||| = r * |||(f,g,A)||| ; ::_thesis: verum
end;

theorem :: INTEGRA9:29
for r, p being Real
for f, g being PartFunc of REAL,REAL
for 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 r, p be Real; ::_thesis: for f, g being PartFunc of REAL,REAL
for 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)|||
let f, g be PartFunc of REAL,REAL; ::_thesis: for 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)|||
let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) implies |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| )
assume A1: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) ) ; ::_thesis: |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)|||
|||((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  |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| ; ::_thesis: verum
end;

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

theorem Th31: :: INTEGRA9:31
for f, g being PartFunc of REAL,REAL
for 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; ::_thesis: for 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)|||
let A be non empty closed_interval Subset of REAL; ::_thesis: ( (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 implies |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| )
assume that
A1: (f (#) f) || A is total and
A2: (f (#) g) || A is total and
A3: (g (#) g) || A is total ; ::_thesis: ( not ((f (#) f) || A) | A is bounded or not ((f (#) g) || A) | A is bounded or not ((g (#) g) || A) | A is bounded or not f (#) f is_integrable_on A or not f (#) g is_integrable_on A or not g (#) g is_integrable_on A or |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| )
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 ; ::_thesis: ( not f (#) f is_integrable_on A or not f (#) g is_integrable_on A or not g (#) g is_integrable_on A or |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| )
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 ; ::_thesis: |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)|||
A10: (f (#) g) || A is integrable by A8, INTEGRA5:def_1;
A11: (g (#) g) || A is integrable by A9, INTEGRA5:def_1;
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, INTEGRA5:def_1;
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  |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| ; ::_thesis: verum
end;

begin

definition
let A be non empty closed_interval Subset of REAL;
let f, g be PartFunc of REAL,REAL;
predf is_orthogonal_with g,A means :Def2: :: INTEGRA9:def 2
|||(f,g,A)||| = 0 ;
end;

:: deftheorem Def2 defines is_orthogonal_with INTEGRA9:def_2_:_
 for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL holds
( f is_orthogonal_with g,A iff |||(f,g,A)||| = 0 );

theorem Th32: :: INTEGRA9:32
for f, g being PartFunc of REAL,REAL
for 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; ::_thesis: for 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)|||
let A be non empty closed_interval Subset of REAL; ::_thesis: ( (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 implies |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| )
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 ) ; ::_thesis: ( not f is_orthogonal_with g,A or |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,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 ; ::_thesis: |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)|||
then  |||(f,g,A)||| = 0 by Def2;
hence  |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| by A1; ::_thesis: verum
end;

theorem :: INTEGRA9:33
for f being PartFunc of REAL,REAL
for 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 being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
|||(f,f,A)||| >= 0 by INTEGRA2:32;

theorem :: INTEGRA9:34
for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds
sin is_orthogonal_with cos ,A
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,PI.] implies sin is_orthogonal_with cos ,A )
assume  A = [.0,PI.] ; ::_thesis: sin is_orthogonal_with cos ,A
then  |||(sin,cos,A)||| = 0 by INTEGRA8:92;
hence  sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum
end;

theorem :: INTEGRA9:35
for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds
sin is_orthogonal_with cos ,A
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI * 2).] implies sin is_orthogonal_with cos ,A )
assume  A = [.0,(PI * 2).] ; ::_thesis: sin is_orthogonal_with cos ,A
then  |||(sin,cos,A)||| = 0 by INTEGRA8:94;
hence  sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum
end;

theorem :: INTEGRA9:36
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
sin is_orthogonal_with cos ,A
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
sin is_orthogonal_with cos ,A
let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] implies sin is_orthogonal_with cos ,A )
assume  A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] ; ::_thesis: sin is_orthogonal_with cos ,A
then  |||(sin,cos,A)||| = 0 by INTEGRA8:95;
hence  sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum
end;

theorem :: INTEGRA9:37
for x being Real
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
sin is_orthogonal_with cos ,A
proof
let x be Real; ::_thesis: for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
sin is_orthogonal_with cos ,A
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
sin is_orthogonal_with cos ,A
let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] implies sin is_orthogonal_with cos ,A )
assume  A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] ; ::_thesis: sin is_orthogonal_with cos ,A
then  |||(sin,cos,A)||| = 0 by INTEGRA8:96;
hence  sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum
end;

theorem :: INTEGRA9:38
for A being non empty closed_interval Subset of REAL st A = [.(- PI),PI.] holds
sin is_orthogonal_with cos ,A
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- PI),PI.] implies sin is_orthogonal_with cos ,A )
assume  A = [.(- PI),PI.] ; ::_thesis: sin is_orthogonal_with cos ,A
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  sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum
end;

theorem :: INTEGRA9:39
for A being non empty closed_interval Subset of REAL st A = [.(- (PI / 2)),(PI / 2).] holds
sin is_orthogonal_with cos ,A
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- (PI / 2)),(PI / 2).] implies sin is_orthogonal_with cos ,A )
assume  A = [.(- (PI / 2)),(PI / 2).] ; ::_thesis: sin is_orthogonal_with cos ,A
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  sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum
end;

theorem :: INTEGRA9:40
for A being non empty closed_interval Subset of REAL st A = [.(- (2 * PI)),(2 * PI).] holds
sin is_orthogonal_with cos ,A
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- (2 * PI)),(2 * PI).] implies sin is_orthogonal_with cos ,A )
assume  A = [.(- (2 * PI)),(2 * PI).] ; ::_thesis: sin is_orthogonal_with cos ,A
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  sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum
end;

theorem :: INTEGRA9:41
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(- ((2 * n) * PI)),((2 * n) * PI).] holds
sin is_orthogonal_with cos ,A
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.(- ((2 * n) * PI)),((2 * n) * PI).] holds
sin is_orthogonal_with cos ,A
let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- ((2 * n) * PI)),((2 * n) * PI).] implies sin is_orthogonal_with cos ,A )
assume  A = [.(- ((2 * n) * PI)),((2 * n) * PI).] ; ::_thesis: sin is_orthogonal_with cos ,A
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  sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum
end;

theorem :: INTEGRA9:42
for x being Real
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds
sin is_orthogonal_with cos ,A
proof
let x be Real; ::_thesis: for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds
sin is_orthogonal_with cos ,A
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds
sin is_orthogonal_with cos ,A
let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] implies sin is_orthogonal_with cos ,A )
assume  A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] ; ::_thesis: sin is_orthogonal_with cos ,A
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  sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum
end;

begin

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

:: deftheorem  defines ||.. INTEGRA9:def_3_:_
 for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL holds ||..f,A..|| = sqrt |||(f,f,A)|||;

theorem :: INTEGRA9:43
for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
0 <= ||..f,A..||
proof
let f be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
0 <= ||..f,A..||
let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) implies 0 <= ||..f,A..|| )
assume A1: (f (#) f) || A is total ; ::_thesis: ( not ((f (#) f) || A) | A is bounded or ex x being Real st
( x in A & not ((f (#) f) || A) . x >= 0 ) or 0 <= ||..f,A..|| )
assume  ( ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) ) ; ::_thesis: 0 <= ||..f,A..||
then  |||(f,f,A)||| >= 0 by A1, INTEGRA2:32;
hence  0 <= ||..f,A..|| by SQUARE_1:def_2; ::_thesis: verum
end;

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

theorem :: INTEGRA9:45
for f, g being PartFunc of REAL,REAL
for 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 being Real st x in A holds
((f (#) f) || A) . x >= 0 ) & ( for x being Real 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; ::_thesis: for 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 being Real st x in A holds
((f (#) f) || A) . x >= 0 ) & ( for x being Real st x in A holds
((g (#) g) || A) . x >= 0 ) holds
||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2)
let A be non empty closed_interval Subset of REAL; ::_thesis: ( (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 being Real st x in A holds
((f (#) f) || A) . x >= 0 ) & ( for x being Real st x in A holds
((g (#) g) || A) . x >= 0 ) implies ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) )
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 ) ; ::_thesis: ( not f is_orthogonal_with g,A or ex x being Real st
( x in A & not ((f (#) f) || A) . x >= 0 ) or ex x being Real st
( x in A & not ((g (#) g) || A) . x >= 0 ) or ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) )
assume A8: f is_orthogonal_with g,A ; ::_thesis: ( ex x being Real st
( x in A & not ((f (#) f) || A) . x >= 0 ) or ex x being Real st
( x in A & not ((g (#) g) || A) . x >= 0 ) or ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) )
assume  for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ; ::_thesis: ( ex x being Real st
( x in A & not ((g (#) g) || A) . x >= 0 ) or ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) )
then A9: |||(f,f,A)||| >= 0 by A1, A4, INTEGRA2:32;
assume  for x being Real st x in A holds
((g (#) g) || A) . x >= 0 ; ::_thesis: ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2)
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  ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) by A1, A2, A3, A4, A5, A6, A7, A8, A12, A11, Th32; ::_thesis: verum
end;

begin


theorem :: INTEGRA9:46
for a being Real
for A being non empty closed_interval Subset of REAL st not - a in A holds
((AffineMap (1,a)) ^) | A is continuous
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL st not - a in A holds
((AffineMap (1,a)) ^) | A is continuous
let A be non empty closed_interval Subset of REAL; ::_thesis: ( not - a in A implies ((AffineMap (1,a)) ^) | A is continuous )
set g2 = AffineMap (1,a);
assume A1: not - a in A ; ::_thesis: ((AffineMap (1,a)) ^) | A is continuous
 not 0 in rng ((AffineMap (1,a)) | A)
proof
set h2 = (AffineMap (1,a)) | A;
assume  0 in rng ((AffineMap (1,a)) | A) ; ::_thesis: contradiction
then consider x being set  such that
A2: x in dom ((AffineMap (1,a)) | A) and
A3: ((AffineMap (1,a)) | A) . x = 0 by FUNCT_1:def_3;
reconsider d = x as Real by A2;
A4: (AffineMap (1,a)) . d = a + (1 * d) by FCONT_1:def_4;
 d in A by A2, RELAT_1:57;
then  ( dom ((AffineMap (1,a)) | A) c= A & a + d = 0 ) by A3, A4, FUNCT_1:49, RELAT_1:58;
hence  contradiction by A1, A2; ::_thesis: verum
end;
then A5: ((AffineMap (1,a)) | A) " {0} = {} by FUNCT_1:72;
thus  ((AffineMap (1,a)) ^) | A is continuous by A5, FCONT_1:23; ::_thesis: verum
end;

theorem :: INTEGRA9:47
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = - (1 / ((a + x) ^2)) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
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 Real st x in dom ((f ^) `| Z) holds
((f ^) `| Z) . x = f2 . x
proof
let x be Real; ::_thesis: ( x in dom ((f ^) `| Z) implies ((f ^) `| Z) . x = f2 . x )
assume  x in dom ((f ^) `| Z) ; ::_thesis: ((f ^) `| Z) . x = f2 . x
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  ((f ^) `| Z) . x = f2 . x ; ::_thesis: verum
end;
 dom ((f ^) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7;
then  (f ^) `| Z = f2 by A9, PARTFUN1:5;
hence  integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:48
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = 1 / ((a + x) ^2) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A))
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 Real st x in dom (((- 1) (#) (f ^)) `| Z) holds
(((- 1) (#) (f ^)) `| Z) . x = f2 . x
proof
let x be Real; ::_thesis: ( x in dom (((- 1) (#) (f ^)) `| Z) implies (((- 1) (#) (f ^)) `| Z) . x = f2 . x )
assume  x in dom (((- 1) (#) (f ^)) `| Z) ; ::_thesis: (((- 1) (#) (f ^)) `| Z) . x = f2 . x
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  (((- 1) (#) (f ^)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:49
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = 1 / ((a - x) ^2) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))
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 Real st x in dom ((f ^) `| Z) holds
((f ^) `| Z) . x = f2 . x
proof
let x be Real; ::_thesis: ( x in dom ((f ^) `| Z) implies ((f ^) `| Z) . x = f2 . x )
assume  x in dom ((f ^) `| Z) ; ::_thesis: ((f ^) `| Z) . x = f2 . x
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  ((f ^) `| Z) . x = f2 . x ; ::_thesis: verum
end;
 dom ((f ^) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7;
then  (f ^) `| Z = f2 by A9, PARTFUN1:5;
hence  integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:50
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = 1 / (a + x) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
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 Real st x in dom ((ln * f) `| Z) holds
((ln * f) `| Z) . x = f2 . x
proof
let x be Real; ::_thesis: ( x in dom ((ln * f) `| Z) implies ((ln * f) `| Z) . x = f2 . x )
assume  x in dom ((ln * f) `| Z) ; ::_thesis: ((ln * f) `| Z) . x = f2 . x
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  ((ln * f) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:51
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = 1 / (x - a) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))
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 Real st x in dom ((ln * f) `| Z) holds
((ln * f) `| Z) . x = f2 . x
proof
let x be Real; ::_thesis: ( x in dom ((ln * f) `| Z) implies ((ln * f) `| Z) . x = f2 . x )
assume  x in dom ((ln * f) `| Z) ; ::_thesis: ((ln * f) `| Z) . x = f2 . x
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  ((ln * f) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:52
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a - x) ) & f2 | A is continuous holds
integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a - x) ) & f2 | A is continuous holds
integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a - x) ) & f2 | A is continuous holds
integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a - x) ) & f2 | A is continuous holds
integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = 1 / (a - x) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A))
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 Real st x in dom ((- (ln * f)) `| Z) holds
((- (ln * f)) `| Z) . x = f2 . x
proof
let x be Real; ::_thesis: ( x in dom ((- (ln * f)) `| Z) implies ((- (ln * f)) `| Z) . x = f2 . x )
assume  x in dom ((- (ln * f)) `| Z) ; ::_thesis: ((- (ln * f)) `| Z) . x = f2 . x
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  ((- (ln * f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:53
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = x / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = x / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = x / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A))
let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = x / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: ( f = ln * f1 & ( for x being Real 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 being Real st x in Z holds
f2 . x = x / (a + x) and
A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A))
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 Real st x in dom (((id Z) - (a (#) f)) `| Z) holds
(((id Z) - (a (#) f)) `| Z) . x = f2 . x
proof
let x be Real; ::_thesis: ( x in dom (((id Z) - (a (#) f)) `| Z) implies (((id Z) - (a (#) f)) `| Z) . x = f2 . x )
assume  x in dom (((id Z) - (a (#) f)) `| Z) ; ::_thesis: (((id Z) - (a (#) f)) `| Z) . x = f2 . x
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  (((id Z) - (a (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:54
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A))
let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: ( f = ln * f1 & ( for x being Real 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 being Real st x in Z holds
f2 . x = (a - x) / (a + x) and
A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom ((((2 * a) (#) f) - (id Z)) `| Z) implies ((((2 * a) (#) f) - (id Z)) `| Z) . x = f2 . x )
assume  x in dom ((((2 * a) (#) f) - (id Z)) `| Z) ; ::_thesis: ((((2 * a) (#) f) - (id Z)) `| Z) . x = f2 . x
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  ((((2 * a) (#) f) - (id Z)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:55
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A))
let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: ( f = ln * f1 & ( for x being Real 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 being Real st x in Z holds
f2 . x = (x - a) / (x + a) and
A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom (((id Z) - ((2 * a) (#) f)) `| Z) implies (((id Z) - ((2 * a) (#) f)) `| Z) . x = f2 . x )
assume  x in dom (((id Z) - ((2 * a) (#) f)) `| Z) ; ::_thesis: (((id Z) - ((2 * a) (#) f)) `| Z) . x = f2 . x
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  (((id Z) - ((2 * a) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:56
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A))
let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: ( f = ln * f1 & ( for x being Real 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 being Real st x in Z holds
f2 . x = (x + a) / (x - a) and
A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom (((id Z) + ((2 * a) (#) f)) `| Z) implies (((id Z) + ((2 * a) (#) f)) `| Z) . x = f2 . x )
assume  x in dom (((id Z) + ((2 * a) (#) f)) `| Z) ; ::_thesis: (((id Z) + ((2 * a) (#) f)) `| Z) . x = f2 . x
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  (((id Z) + ((2 * a) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:57
for b, a being Real
for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A))
proof
let b, a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A))
let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: ( f = ln * f1 & ( for x being Real 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 being Real st x in Z holds
f2 . x = (x + a) / (x + b) and
A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom (((id Z) + ((a - b) (#) f)) `| Z) implies (((id Z) + ((a - b) (#) f)) `| Z) . x = f2 . x )
assume  x in dom (((id Z) + ((a - b) (#) f)) `| Z) ; ::_thesis: (((id Z) + ((a - b) (#) f)) `| Z) . x = f2 . x
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  (((id Z) + ((a - b) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:58
for b, a being Real
for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A))
proof
let b, a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A))
let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x + a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: ( f = ln * f1 & ( for x being Real 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 being Real st x in Z holds
f2 . x = (x + a) / (x - b) and
A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom (((id Z) + ((a + b) (#) f)) `| Z) implies (((id Z) + ((a + b) (#) f)) `| Z) . x = f2 . x )
assume  x in dom (((id Z) + ((a + b) (#) f)) `| Z) ; ::_thesis: (((id Z) + ((a + b) (#) f)) `| Z) . x = f2 . x
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  (((id Z) + ((a + b) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:59
for b, a being Real
for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A))
proof
let b, a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A))
let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x + b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: ( f = ln * f1 & ( for x being Real 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 being Real st x in Z holds
f2 . x = (x - a) / (x + b) and
A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom (((id Z) - ((a + b) (#) f)) `| Z) implies (((id Z) - ((a + b) (#) f)) `| Z) . x = f2 . x )
assume  x in dom (((id Z) - ((a + b) (#) f)) `| Z) ; ::_thesis: (((id Z) - ((a + b) (#) f)) `| Z) . x = f2 . x
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  (((id Z) - ((a + b) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:60
for b, a being Real
for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A))
proof
let b, a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A))
let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds
f2 . x = (x - a) / (x - b) ) & f2 | A is continuous holds
integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: ( f = ln * f1 & ( for x being Real 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 being Real st x in Z holds
f2 . x = (x - a) / (x - b) and
A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom (((id Z) + ((b - a) (#) f)) `| Z) implies (((id Z) + ((b - a) (#) f)) `| Z) . x = f2 . x )
assume  x in dom (((id Z) + ((b - a) (#) f)) `| Z) ; ::_thesis: (((id Z) + ((b - a) (#) f)) `| Z) . x = f2 . x
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  (((id Z) + ((b - a) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:61
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z & dom ln = Z & Z = dom ((id Z) ^) & ((id Z) ^) | A is continuous holds
integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & dom ln = Z & Z = dom ((id Z) ^) & ((id Z) ^) | A is continuous holds
integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( 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)) )
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 ; ::_thesis: integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A))
A5: (id Z) ^ 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 Real st x in dom (ln `| Z) holds
(ln `| Z) . x = ((id Z) ^) . x
proof
let x be Real; ::_thesis: ( x in dom (ln `| Z) implies (ln `| Z) . x = ((id Z) ^) . x )
assume  x in dom (ln `| Z) ; ::_thesis: (ln `| Z) . x = ((id Z) ^) . x
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
.= ((id Z) ^) . x by A3, A8, RFUNCT_1:def_2 ;
hence  (ln `| Z) . x = ((id Z) ^) . x ; ::_thesis: verum
end;
 dom (ln `| Z) = dom ((id Z) ^) by A3, A6, FDIFF_1:def_7;
then  ln `| Z = (id Z) ^ by A7, PARTFUN1:5;
hence  integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A)) by A1, A3, A4, A5, A6, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:62
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = n / x ) & f2 | A is continuous holds
integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A))
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = n / x ) & f2 | A is continuous holds
integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = n / x ) & f2 | A is continuous holds
integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A))
let f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = n / x ) & f2 | A is continuous holds
integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = n / x and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A))
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 Real st x in dom ((ln * (#Z n)) `| Z) holds
((ln * (#Z n)) `| Z) . x = f2 . x
proof
let x be Real; ::_thesis: ( x in dom ((ln * (#Z n)) `| Z) implies ((ln * (#Z n)) `| Z) . x = f2 . x )
assume  x in dom ((ln * (#Z n)) `| Z) ; ::_thesis: ((ln * (#Z n)) `| Z) . x = f2 . x
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  ((ln * (#Z n)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:63
for A being non empty closed_interval Subset of REAL
for f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A))
let f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real 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)) )
set f = id Z;
assume that
A1: not 0 in Z and
A2: A c= Z and
A3: dom (ln * ((id Z) ^)) = Z and
A4: dom (ln * ((id Z) ^)) = dom f2 and
A5: for x being Real st x in Z holds
f2 . x = - (1 / x) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A))
A7: f2 is_integrable_on A by A2, A3, A4, A6, INTEGRA5:11;
A8: ln * ((id Z) ^) is_differentiable_on Z by A1, A3, FDIFF_8:5;
A9: for x being Real st x in dom ((ln * ((id Z) ^)) `| Z) holds
((ln * ((id Z) ^)) `| Z) . x = f2 . x
proof
let x be Real; ::_thesis: ( x in dom ((ln * ((id Z) ^)) `| Z) implies ((ln * ((id Z) ^)) `| Z) . x = f2 . x )
assume  x in dom ((ln * ((id Z) ^)) `| Z) ; ::_thesis: ((ln * ((id Z) ^)) `| Z) . x = f2 . x
then A10: x in Z by A8, FDIFF_1:def_7;
then ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) by A1, A3, FDIFF_8:5
.= f2 . x by A5, A10 ;
hence  ((ln * ((id Z) ^)) `| Z) . x = f2 . x ; ::_thesis: verum
end;
 dom ((ln * ((id Z) ^)) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7;
then  (ln * ((id Z) ^)) `| Z = f2 by A9, PARTFUN1:5;
hence  integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A)) by A2, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:64
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = (a + x) #R (1 / 2) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) implies (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x )
assume  x in dom (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) ; ::_thesis: (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x
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  (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:65
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = (a - x) #R (1 / 2) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) implies (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x )
assume  x in dom (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) ; ::_thesis: (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x
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  (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:66
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = (a + x) #R (- (1 / 2)) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom ((2 (#) ((#R (1 / 2)) * f)) `| Z) implies ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x )
assume  x in dom ((2 (#) ((#R (1 / 2)) * f)) `| Z) ; ::_thesis: ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x
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  ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:67
for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A))
proof
let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A))
let f, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: for x being Real 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 being Real st x in Z holds
f2 . x = (a - x) #R (- (1 / 2)) and
A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A))
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 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 Real; ::_thesis: ( x in dom (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) implies (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x )
assume  x in dom (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) ; ::_thesis: (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x
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  (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x ; ::_thesis: verum
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  integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:68
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & dom (((- (id Z)) (#) cos) + sin) = Z & ( for x being Real st x in Z holds
f . x = x * (sin . x) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & dom (((- (id Z)) (#) cos) + sin) = Z & ( for x being Real st x in Z holds
f . x = x * (sin . x) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & dom (((- (id Z)) (#) cos) + sin) = Z & ( for x being Real st x in Z holds
f . x = x * (sin . x) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & dom (((- (id Z)) (#) cos) + sin) = Z & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: dom (((- (id Z)) (#) cos) + sin) = Z and
A3: for x being Real st x in Z holds
f . x = x * (sin . x) and
A4: Z = dom f and
A5: f | A is continuous ; ::_thesis: integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))
A6: ((- (id Z)) (#) cos) + sin is_differentiable_on Z by A2, FDIFF_4:46;
A7: for x being Real st x in dom ((((- (id Z)) (#) cos) + sin) `| Z) holds
((((- (id Z)) (#) cos) + sin) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((((- (id Z)) (#) cos) + sin) `| Z) implies ((((- (id Z)) (#) cos) + sin) `| Z) . x = f . x )
assume  x in dom ((((- (id Z)) (#) cos) + sin) `| Z) ; ::_thesis: ((((- (id Z)) (#) cos) + sin) `| Z) . x = f . x
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  ((((- (id Z)) (#) cos) + sin) `| Z) . x = f . x ; ::_thesis: verum
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, INTEGRA5:11;
hence  integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) by A1, A2, A9, FDIFF_4:46, INTEGRA5:13; ::_thesis: verum
end;

theorem :: INTEGRA9:69
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & dom sec = Z & ( for x being Real st x in Z holds
f . x = (sin . x) / ((cos . x) ^2) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & dom sec = Z & ( for x being Real st x in Z holds
f . x = (sin . x) / ((cos . x) ^2) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & dom sec = Z & ( for x being Real st x in Z holds
f . x = (sin . x) / ((cos . x) ^2) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & dom sec = Z & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: dom sec = Z and
A3: for x being Real st x in Z holds
f . x = (sin . x) / ((cos . x) ^2) and
A4: Z = dom f and
A5: f | A is continuous ; ::_thesis: integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A))
A6: sec is_differentiable_on Z by A2, FDIFF_9:4;
A7: for x being Real st x in dom (sec `| Z) holds
(sec `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom (sec `| Z) implies (sec `| Z) . x = f . x )
assume  x in dom (sec `| Z) ; ::_thesis: (sec `| Z) . x = f . x
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  (sec `| Z) . x = f . x ; ::_thesis: verum
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, INTEGRA5:11;
hence  integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A)) by A1, A2, A9, FDIFF_9:4, INTEGRA5:13; ::_thesis: verum
end;

theorem Th70: :: INTEGRA9:70
for Z being open Subset of REAL st Z c= dom (- cosec) holds
( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) )
proof
let Z be open Subset of REAL; ::_thesis: ( Z c= dom (- cosec) implies ( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) ) )
A1: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
assume A2: Z c= dom (- cosec) ; ::_thesis: ( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) )
then A3: Z c= dom cosec by VALUED_1:8;
then  for x being Real 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 being Real st x in Z holds
((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2)
proof
let x be Real; ::_thesis: ( x in Z implies ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) )
assume A6: x in Z ; ::_thesis: ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2)
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  ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ; ::_thesis: verum
end;
 (- 1) (#) cosec is_differentiable_on Z by A2, A4, FDIFF_1:20;
hence  ( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) ) by A5; ::_thesis: verum
end;

theorem :: INTEGRA9:71
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & dom (- cosec) = Z & ( for x being Real st x in Z holds
f . x = (cos . x) / ((sin . x) ^2) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & dom (- cosec) = Z & ( for x being Real st x in Z holds
f . x = (cos . x) / ((sin . x) ^2) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & dom (- cosec) = Z & ( for x being Real st x in Z holds
f . x = (cos . x) / ((sin . x) ^2) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A))
let Z be open Subset of REAL; ::_thesis: ( A c= Z & dom (- cosec) = Z & ( for x being Real 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)) )
assume that
A1: A c= Z and
A2: dom (- cosec) = Z and
A3: for x being Real st x in Z holds
f . x = (cos . x) / ((sin . x) ^2) and
A4: Z = dom f and
A5: f | A is continuous ; ::_thesis: integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A))
A6: - cosec is_differentiable_on Z by A2, Th70;
A7: for x being Real st x in dom ((- cosec) `| Z) holds
((- cosec) `| Z) . x = f . x
proof
let x be Real; ::_thesis: ( x in dom ((- cosec) `| Z) implies ((- cosec) `| Z) . x = f . x )
assume  x in dom ((- cosec) `| Z) ; ::_thesis: ((- cosec) `| Z) . x = f . x
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  ((- cosec) `| Z) . x = f . x ; ::_thesis: verum
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, INTEGRA5:11;
hence  integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A)) by A1, A2, A9, Th70, INTEGRA5:13; ::_thesis: verum
end;