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 arcsin = Z & Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) holds
integral (arcsin,A) = ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) arcsin) + ((#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 arcsin = Z & Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) holds
integral (arcsin,A) = ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) arcsin) + ((#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 arcsin = Z & Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) implies integral (arcsin,A) = ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (lower_bound A)) )
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 arcsin = Z
and
A4:
Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f))
; integral (arcsin,A) = ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (lower_bound A))
A5:
arcsin | A is bounded
by A1, A3, INTEGRA5:10;
A6:
((id Z) (#) arcsin) + ((#R (1 / 2)) * f) is_differentiable_on Z
by A2, A4, FDIFF_7:23;
A7:
for x being Element of REAL st x in dom ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) holds
((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x
dom ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) = dom arcsin
by A3, A6, FDIFF_1:def 7;
then
(((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z = arcsin
by A7, PARTFUN1:5;
hence
integral (arcsin,A) = ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (lower_bound A))
by A1, A3, A5, A6, INTEGRA5:11, INTEGRA5:13; verum