let A be closed-interval Subset of REAL; :: thesis: 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))
let f1, f 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
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))
let Z be open Subset of REAL; :: thesis: ( 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)))) implies integral (f,A) = (((id Z) (#) arcsin) . (upper_bound A)) - (((id Z) (#) arcsin) . (lower_bound A)) )
assume A1: ( 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)))) ) ; :: thesis: integral (f,A) = (((id Z) (#) arcsin) . (upper_bound A)) - (((id Z) (#) arcsin) . (lower_bound A))
then Z = (dom arcsin) /\ (dom ((id Z) / ((#R (1 / 2)) * (f1 - (#Z 2))))) by VALUED_1:def 1;
then A3: ( Z c= dom arcsin & Z c= dom ((id Z) / ((#R (1 / 2)) * (f1 - (#Z 2)))) ) by XBOOLE_1:18;
A4: Z = dom (id Z) by RELAT_1:71;
then Z c= (dom (id Z)) /\ (dom arcsin) by XBOOLE_1:19, A3;
then A6: Z c= dom ((id Z) (#) arcsin) by VALUED_1:def 4;
A7: arcsin is_differentiable_on Z by A1, FDIFF_1:34, SIN_COS6:84;
for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:35;
then A8: id Z is_differentiable_on Z by FDIFF_1:31, A4;
Z c= (dom (id Z)) /\ ((dom ((#R (1 / 2)) * (f1 - (#Z 2)))) \ (((#R (1 / 2)) * (f1 - (#Z 2))) " {0})) by RFUNCT_1:def 4, A3;
then Z c= (dom ((#R (1 / 2)) * (f1 - (#Z 2)))) \ (((#R (1 / 2)) * (f1 - (#Z 2))) " {0}) by XBOOLE_1:18;
then A11: Z c= dom (((#R (1 / 2)) * (f1 - (#Z 2))) ^) by RFUNCT_1:def 8;
dom (((#R (1 / 2)) * (f1 - (#Z 2))) ^) c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) by RFUNCT_1:11;
then A12: Z c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) by A11, XBOOLE_1:1;
set f2 = #Z 2;
for x being Real st x in Z holds
(f1 - (#Z 2)) . x > 0

proof

let x be Real; :: thesis: ( x in Z implies (f1 - (#Z 2)) . x > 0 )
assume A15: x in Z ; :: thesis: (f1 - (#Z 2)) . x > 0
then ( - 1 < x & x < 1 ) by A1, XXREAL_1:4;
then ( 0 < 1 + x & 0 < 1 - x ) by XREAL_1:150, XREAL_1:52;
then A16: 0 < (1 + x) * (1 - x) by XREAL_1:131;
for x being Real st x in Z holds
x in dom (f1 - (#Z 2)) by FUNCT_1:21, A12;
then (f1 - (#Z 2)) . x = (f1 . x) - ((#Z 2) . x) by A15, VALUED_1:13
.= (f1 . x) - (x #Z (1 + 1)) by TAYLOR_1:def 1
.= (f1 . x) - ((x #Z 1) * (x #Z 1)) by TAYLOR_1:1
.= (f1 . x) - (x * (x #Z 1)) by PREPOWER:45
.= (f1 . x) - (x * x) by PREPOWER:45
.= 1 - (x * x) by A1, A15 ;
hence (f1 - (#Z 2)) . x > 0 by A16; :: thesis: verum

end;

then for x being Real st x in Z holds
( f1 . x = 1 & (f1 - (#Z 2)) . x > 0 ) by A1;
then A24: (#R (1 / 2)) * (f1 - (#Z 2)) is_differentiable_on Z by A12, FDIFF_7:22;
for x being Real st x in Z holds
((#R (1 / 2)) * (f1 - (#Z 2))) . x <> 0 by RFUNCT_1:13, A11;
then (id Z) / ((#R (1 / 2)) * (f1 - (#Z 2))) is_differentiable_on Z by A8, A24, FDIFF_2:21;
then f | Z is continuous by FDIFF_1:33, A1, A7, FDIFF_1:26;
then f | A is continuous by A1, FCONT_1:17;
then A29: ( f is_integrable_on A & f | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A30: (id Z) (#) arcsin is_differentiable_on Z by A1, A6, FDIFF_7:16;
B1: for x being Real st x in Z holds
f . x = (arcsin . x) + (x / (sqrt (1 - (x ^2))))

proof

let x be Real; :: thesis: ( x in Z implies f . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) )
assume B2: x in Z ; :: thesis: f . x = (arcsin . x) + (x / (sqrt (1 - (x ^2))))
then B3: ( x in dom (f1 - (#Z 2)) & (f1 - (#Z 2)) . x in dom (#R (1 / 2)) ) by FUNCT_1:21, A12;
then B4: (f1 - (#Z 2)) . x in right_open_halfline 0 by TAYLOR_1:def 4;
( - 1 < x & x < 1 ) by A1, XXREAL_1:4, B2;
then ( 0 < 1 + x & 0 < 1 - x ) by XREAL_1:150, XREAL_1:52;
then B6: 0 < (1 + x) * (1 - x) by XREAL_1:131;
(arcsin + ((id Z) / ((#R (1 / 2)) * (f1 - (#Z 2))))) . x = (arcsin . x) + (((id Z) / ((#R (1 / 2)) * (f1 - (#Z 2)))) . x) by VALUED_1:def 1, A1, B2
.= (arcsin . x) + (((id Z) . x) / (((#R (1 / 2)) * (f1 - (#Z 2))) . x)) by RFUNCT_1:def 4, A3, B2
.= (arcsin . x) + (x / (((#R (1 / 2)) * (f1 - (#Z 2))) . x)) by FUNCT_1:35, B2
.= (arcsin . x) + (x / ((#R (1 / 2)) . ((f1 - (#Z 2)) . x))) by A12, FUNCT_1:22, B2
.= (arcsin . x) + (x / (((f1 - (#Z 2)) . x) #R (1 / 2))) by TAYLOR_1:def 4, B4
.= (arcsin . x) + (x / (((f1 . x) - ((#Z 2) . x)) #R (1 / 2))) by VALUED_1:13, B3
.= (arcsin . x) + (x / (((f1 . x) - (x #Z 2)) #R (1 / 2))) by TAYLOR_1:def 1
.= (arcsin . x) + (x / (((f1 . x) - (x ^2)) #R (1 / 2))) by FDIFF_7:1
.= (arcsin . x) + (x / ((1 - (x ^2)) #R (1 / 2))) by A1, B2
.= (arcsin . x) + (x / (sqrt (1 - (x ^2)))) by FDIFF_7:2, B6 ;
hence f . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) by A1; :: thesis: verum

end;

A31: for x being Real st x in dom (((id Z) (#) arcsin) `| Z) holds
(((id Z) (#) arcsin) `| Z) . x = f . x

proof

let x be Real; :: thesis: ( x in dom (((id Z) (#) arcsin) `| Z) implies (((id Z) (#) arcsin) `| Z) . x = f . x )
assume x in dom (((id Z) (#) arcsin) `| Z) ; :: thesis: (((id Z) (#) arcsin) `| Z) . x = f . x
then A32: x in Z by A30, FDIFF_1:def 8;
then (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) by A1, A6, FDIFF_7:16
.= f . x by B1, A32 ;
hence (((id Z) (#) arcsin) `| Z) . x = f . x ; :: thesis: verum

end;

dom (((id Z) (#) arcsin) `| Z) = dom f by A1, A30, FDIFF_1:def 8;
then ((id Z) (#) arcsin) `| Z = f by A31, PARTFUN1:34;
hence integral (f,A) = (((id Z) (#) arcsin) . (upper_bound A)) - (((id Z) (#) arcsin) . (lower_bound A)) by A1, A29, A6, FDIFF_7:16, INTEGRA5:13; :: thesis: verum