:: Integrability Formulas -- Part {I}
:: by Bo Li and Na Ma
::
:: Received November 7, 2009
:: Copyright (c) 2009-2011 Association of Mizar Users

begin

Lm1: - 1 is Real
by XREAL_0:def 1;

theorem Th1: :: INTEGR12:1

for f1, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st Z c= dom ((f1 + f2) ^) & ( for x being Real st x in Z holds
f1 . x = 1 ) & f2 = #Z 2 holds
( (f1 + f2) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) ^) `| Z) . x = - ((2 * x) / ((1 + (x |^ 2)) ^2)) ) )

proof end;

theorem :: INTEGR12:2

for A being closed-interval Subset of REAL
for f, g1, g2, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ((g1 + g2) ^) / f2 & f2 = arccot & Z c= ].(- 1),1.[ & g2 = #Z 2 & ( for x being Real st x in Z holds
( g1 . x = 1 & f2 . x > 0 ) ) & Z = dom f holds
integral (f,A) = ((- (ln * arccot)) . (upper_bound A)) - ((- (ln * arccot)) . (lower_bound A))

proof end;

theorem :: INTEGR12:3

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( exp_R . x < 1 & f1 . x = 1 ) ) & Z c= dom (arctan * exp_R) & Z = dom f & f = exp_R / (f1 + (exp_R ^2)) holds
integral (f,A) = ((arctan * exp_R) . (upper_bound A)) - ((arctan * exp_R) . (lower_bound A))

proof end;

theorem :: INTEGR12:4

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( exp_R . x < 1 & f1 . x = 1 ) ) & Z c= dom (arccot * exp_R) & Z = dom f & f = (- exp_R) / (f1 + (exp_R ^2)) holds
integral (f,A) = ((arccot * exp_R) . (upper_bound A)) - ((arccot * exp_R) . (lower_bound A))

proof end;

theorem :: INTEGR12:5

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = (exp_R (#) (sin / cos)) + (exp_R / (cos ^2)) holds
integral (f,A) = ((exp_R (#) tan) . (upper_bound A)) - ((exp_R (#) tan) . (lower_bound A))

proof end;

theorem :: INTEGR12:6

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = (exp_R (#) (cos / sin)) - (exp_R / (sin ^2)) holds
integral (f,A) = ((exp_R (#) cot) . (upper_bound A)) - ((exp_R (#) cot) . (lower_bound A))

proof end;

theorem :: INTEGR12:7

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = (exp_R (#) arctan) + (exp_R / (f1 + (#Z 2))) holds
integral (f,A) = ((exp_R (#) arctan) . (upper_bound A)) - ((exp_R (#) arctan) . (lower_bound A))

proof end;

theorem :: INTEGR12:8

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = (exp_R (#) arccot) - (exp_R / (f1 + (#Z 2))) holds
integral (f,A) = ((exp_R (#) arccot) . (upper_bound A)) - ((exp_R (#) arccot) . (lower_bound A))

proof end;

theorem :: INTEGR12:9

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = (exp_R * sin) (#) cos holds
integral (f,A) = ((exp_R * sin) . (upper_bound A)) - ((exp_R * sin) . (lower_bound A))

proof end;

theorem :: INTEGR12:10

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = (exp_R * cos) (#) sin holds
integral (f,A) = ((- (exp_R * cos)) . (upper_bound A)) - ((- (exp_R * cos)) . (lower_bound A))

proof end;

theorem :: INTEGR12:11

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & Z = dom f & f = (cos * ln) (#) ((id Z) ^) holds
integral (f,A) = ((sin * ln) . (upper_bound A)) - ((sin * ln) . (lower_bound A))

proof end;

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

theorem :: INTEGR12:12

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & Z = dom f & f = (sin * ln) (#) ((id Z) ^) holds
integral (f,A) = ((- (cos * ln)) . (upper_bound A)) - ((- (cos * ln)) . (lower_bound A))

proof end;

theorem :: INTEGR12:13

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = exp_R (#) (cos * exp_R) holds
integral (f,A) = ((sin * exp_R) . (upper_bound A)) - ((sin * exp_R) . (lower_bound A))

proof end;

theorem :: INTEGR12:14

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = exp_R (#) (sin * exp_R) holds
integral (f,A) = ((- (cos * exp_R)) . (upper_bound A)) - ((- (cos * exp_R)) . (lower_bound A))

proof end;

theorem :: INTEGR12:15

for r being Real
for A being closed-interval Subset of REAL
for f1, f2, g, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (ln * (f1 + f2)) & r <> 0 & ( for x being Real st x in Z holds
( g . x = x / r & g . x > - 1 & g . x < 1 & f1 . x = 1 ) ) & f2 = (#Z 2) * g & Z = dom f & f = arctan * g holds
integral (f,A) = ((((id Z) (#) (arctan * g)) - ((r / 2) (#) (ln * (f1 + f2)))) . (upper_bound A)) - ((((id Z) (#) (arctan * g)) - ((r / 2) (#) (ln * (f1 + f2)))) . (lower_bound A))

proof end;

theorem :: INTEGR12:16

for r being Real
for A being closed-interval Subset of REAL
for f1, f2, g, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (ln * (f1 + f2)) & r <> 0 & ( for x being Real st x in Z holds
( g . x = x / r & g . x > - 1 & g . x < 1 & f1 . x = 1 ) ) & f2 = (#Z 2) * g & Z = dom f & f = arccot * g holds
integral (f,A) = ((((id Z) (#) (arccot * g)) + ((r / 2) (#) (ln * (f1 + f2)))) . (upper_bound A)) - ((((id Z) (#) (arccot * g)) + ((r / 2) (#) (ln * (f1 + f2)))) . (lower_bound A))

proof end;

theorem :: INTEGR12:17

for r being Real
for A being closed-interval Subset of REAL
for f, f1, g being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (arctan * f1) + ((id Z) / (r (#) (g + (f1 ^2)))) & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / r & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (((id Z) (#) (arctan * f1)) . (upper_bound A)) - (((id Z) (#) (arctan * f1)) . (lower_bound A))

proof end;

theorem :: INTEGR12:18

for r being Real
for A being closed-interval Subset of REAL
for f, f1, g being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (arccot * f1) - ((id Z) / (r (#) (g + (f1 ^2)))) & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / r & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (((id Z) (#) (arccot * f1)) . (upper_bound A)) - (((id Z) (#) (arccot * f1)) . (lower_bound A))

proof end;

theorem :: INTEGR12:19

for n being Element of NAT
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & Z c= dom ((#Z n) * arcsin) & 1 < n & f = (n (#) ((#Z (n - 1)) * arcsin)) / ((#R (1 / 2)) * (f1 - (#Z 2))) holds
integral (f,A) = (((#Z n) * arcsin) . (upper_bound A)) - (((#Z n) * arcsin) . (lower_bound A))

proof end;

theorem :: INTEGR12:20

for n being Element of NAT
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= dom ((#Z n) * arccos) & Z = dom f & 1 < n & f = (n (#) ((#Z (n - 1)) * arccos)) / ((#R (1 / 2)) * (f1 - (#Z 2))) holds
integral (f,A) = ((- ((#Z n) * arccos)) . (upper_bound A)) - ((- ((#Z n) * arccos)) . (lower_bound A))

proof end;

theorem :: INTEGR12:21

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = arcsin + ((id Z) / ((#R (1 / 2)) * (f1 - (#Z 2)))) holds
integral (f,A) = (((id Z) (#) arcsin) . (upper_bound A)) - (((id Z) (#) arcsin) . (lower_bound A))

proof end;

theorem :: INTEGR12:22

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = arccos - ((id Z) / ((#R (1 / 2)) * (f1 - (#Z 2)))) holds
integral (f,A) = (((id Z) (#) arccos) . (upper_bound A)) - (((id Z) (#) arccos) . (lower_bound A))

proof end;

theorem :: INTEGR12:23

for a, b being Real
for A being closed-interval Subset of REAL
for f1, f2, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = (a * x) + b & f2 . x = 1 ) ) & Z = dom f & f = (a (#) arcsin) + (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) holds
integral (f,A) = ((f1 (#) arcsin) . (upper_bound A)) - ((f1 (#) arcsin) . (lower_bound A))

proof end;

theorem :: INTEGR12:24

for a, b being Real
for A being closed-interval Subset of REAL
for f1, f2, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = (a * x) + b & f2 . x = 1 ) ) & Z = dom f & f = (a (#) arccos) - (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) holds
integral (f,A) = ((f1 (#) arccos) . (upper_bound A)) - ((f1 (#) arccos) . (lower_bound A))

proof end;

theorem :: INTEGR12:25

for a being Real
for A being closed-interval Subset of REAL
for g, f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous & f = (arcsin * f1) + ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2))))) holds
integral (f,A) = (((id Z) (#) (arcsin * f1)) . (upper_bound A)) - (((id Z) (#) (arcsin * f1)) . (lower_bound A))

proof end;

theorem :: INTEGR12:26

for a being Real
for A being closed-interval Subset of REAL
for g, f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous & f = (arccos * f1) - ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2))))) holds
integral (f,A) = (((id Z) (#) (arccos * f1)) . (upper_bound A)) - (((id Z) (#) (arccos * f1)) . (lower_bound A))

proof end;

theorem :: INTEGR12:27

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (n (#) ((#Z (n - 1)) * sin)) / ((#Z (n + 1)) * cos) & 1 <= n & Z c= dom ((#Z n) * tan) & Z = dom f holds
integral (f,A) = (((#Z n) * tan) . (upper_bound A)) - (((#Z n) * tan) . (lower_bound A))

proof end;

theorem :: INTEGR12:28

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = (n (#) ((#Z (n - 1)) * cos)) / ((#Z (n + 1)) * sin) & 1 <= n & Z c= dom ((#Z n) * cot) & Z = dom f holds
integral (f,A) = ((- ((#Z n) * cot)) . (upper_bound A)) - ((- ((#Z n) * cot)) . (lower_bound A))

proof end;

theorem :: INTEGR12:29

for a being Real
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (tan * f1) & f = ((sin * f1) ^2) / ((cos * f1) ^2) & ( for x being Real st x in Z holds
( f1 . x = a * x & a <> 0 ) ) & Z = dom f holds
integral (f,A) = ((((1 / a) (#) (tan * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (tan * f1)) - (id Z)) . (lower_bound A))

proof end;

theorem :: INTEGR12:30

for a being Real
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (cot * f1) & f = ((cos * f1) ^2) / ((sin * f1) ^2) & ( for x being Real st x in Z holds
( f1 . x = a * x & a <> 0 ) ) & Z = dom f holds
integral (f,A) = ((((- (1 / a)) (#) (cot * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cot * f1)) - (id Z)) . (lower_bound A))

proof end;

theorem :: INTEGR12:31

for a, b being Real
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = (a * x) + b ) & Z = dom f & f = (a (#) (sin / cos)) + (f1 / (cos ^2)) holds
integral (f,A) = ((f1 (#) tan) . (upper_bound A)) - ((f1 (#) tan) . (lower_bound A))

proof end;

theorem :: INTEGR12:32

for a, b being Real
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = (a * x) + b ) & Z = dom f & f = (a (#) (cos / sin)) - (f1 / (sin ^2)) holds
integral (f,A) = ((f1 (#) cot) . (upper_bound A)) - ((f1 (#) cot) . (lower_bound A))

proof end;

theorem :: INTEGR12:33

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f . x = ((sin . x) ^2) / ((cos . x) ^2) ) & Z c= dom (tan - (id Z)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan - (id Z)) . (upper_bound A)) - ((tan - (id Z)) . (lower_bound A))

proof end;

theorem :: INTEGR12:34

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f . x = ((cos . x) ^2) / ((sin . x) ^2) ) & Z c= dom ((- cot) - (id Z)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((- cot) - (id Z)) . (upper_bound A)) - (((- cot) - (id Z)) . (lower_bound A))

proof end;

theorem :: INTEGR12:35

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = 1 / (x * (1 + ((ln . x) ^2))) & ln . x > - 1 & ln . x < 1 ) ) & Z c= dom (arctan * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((arctan * ln) . (upper_bound A)) - ((arctan * ln) . (lower_bound A))

proof end;

theorem :: INTEGR12:36

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = - (1 / (x * (1 + ((ln . x) ^2)))) & ln . x > - 1 & ln . x < 1 ) ) & Z c= dom (arccot * ln) & Z = dom f & f | A is continuous holds
integral (f,A) = ((arccot * ln) . (upper_bound A)) - ((arccot * ln) . (lower_bound A))

proof end;

theorem :: INTEGR12:37

for a, b being Real
for A being closed-interval Subset of REAL
for f, f1 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 / (sqrt (1 - (((a * x) + b) ^2))) & f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 ) ) & Z c= dom (arcsin * f1) & Z = dom f & f | A is continuous holds
integral (f,A) = ((arcsin * f1) . (upper_bound A)) - ((arcsin * f1) . (lower_bound A))

proof end;

theorem :: INTEGR12:38

for a, b being Real
for A being closed-interval Subset of REAL
for f, f1 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 / (sqrt (1 - (((a * x) + b) ^2))) & f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 ) ) & Z c= dom (arccos * f1) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (arccos * f1)) . (upper_bound A)) - ((- (arccos * f1)) . (lower_bound A))

proof end;

theorem :: INTEGR12:39

for A being closed-interval Subset of REAL
for f1, g, f2, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f1 = g - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = x * ((1 - (x #Z 2)) #R (- (1 / 2))) & g . x = 1 & f1 . x > 0 ) ) & Z c= dom ((#R (1 / 2)) * f1) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- ((#R (1 / 2)) * f1)) . (upper_bound A)) - ((- ((#R (1 / 2)) * f1)) . (lower_bound A))

proof end;

theorem :: INTEGR12:40

for a being Real
for A being closed-interval Subset of REAL
for g, f1, f2, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & g = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = x * (((a ^2) - (x #Z 2)) #R (- (1 / 2))) & f1 . x = a ^2 & g . x > 0 ) ) & Z c= dom ((#R (1 / 2)) * g) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- ((#R (1 / 2)) * g)) . (upper_bound A)) - ((- ((#R (1 / 2)) * g)) . (lower_bound A))

proof end;

theorem :: INTEGR12:41

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & n > 0 & ( for x being Real st x in Z holds
( f . x = (cos . x) / ((sin . x) #Z (n + 1)) & sin . x <> 0 ) ) & Z c= dom ((#Z n) * (sin ^)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((- (1 / n)) (#) ((#Z n) * (sin ^))) . (upper_bound A)) - (((- (1 / n)) (#) ((#Z n) * (sin ^))) . (lower_bound A))

proof end;

theorem :: INTEGR12:42

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & n > 0 & ( for x being Real st x in Z holds
( f . x = (sin . x) / ((cos . x) #Z (n + 1)) & cos . x <> 0 ) ) & Z c= dom ((#Z n) * (cos ^)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / n) (#) ((#Z n) * (cos ^))) . (upper_bound A)) - (((1 / n) (#) ((#Z n) * (cos ^))) . (lower_bound A))

proof end;

theorem :: INTEGR12:43

for A being closed-interval Subset of REAL
for f, g1, g2, f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ((g1 + g2) ^) / f2 & f2 = arccot & Z c= ].(- 1),1.[ & g2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = 1 / ((1 + (x ^2)) * (arccot . x)) & g1 . x = 1 & f2 . x > 0 ) ) & Z = dom f holds
integral (f,A) = ((- (ln * arccot)) . (upper_bound A)) - ((- (ln * arccot)) . (lower_bound A))

proof end;

theorem :: INTEGR12:44

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( arcsin . x > 0 & f1 . x = 1 ) ) & Z c= dom (ln * arcsin) & Z = dom f & f = (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arcsin) ^ holds
integral (f,A) = ((ln * arcsin) . (upper_bound A)) - ((ln * arcsin) . (lower_bound A))

proof end;

theorem :: INTEGR12:45

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = 1 & arccos . x > 0 ) ) & Z c= dom (ln * arccos) & Z = dom f & f = (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) ^ holds
integral (f,A) = ((- (ln * arccos)) . (upper_bound A)) - ((- (ln * arccos)) . (lower_bound A))

proof end;