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