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 & 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 ) . (sup A)) - ((ln * arcsin ) . (inf A))
let f1, f be PartFunc of REAL ,REAL ; :: thesis: 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 ) . (sup A)) - ((ln * arcsin ) . (inf A))
let Z be open Subset of REAL ; :: thesis: ( 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 ) ^ implies integral f,A = ((ln * arcsin ) . (sup A)) - ((ln * arcsin ) . (inf A)) )
assume A1: ( 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 ) ^ ) ; :: thesis: integral f,A = ((ln * arcsin ) . (sup A)) - ((ln * arcsin ) . (inf A))
set g = ((#R (1 / 2)) * (f1 - (#Z 2))) (#) arcsin ;
A3: Z c= dom (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arcsin ) by A1, RFUNCT_1:11;
A4: dom (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arcsin ) = (dom ((#R (1 / 2)) * (f1 - (#Z 2)))) /\ (dom arcsin ) by VALUED_1:def 4;
A5: ( Z c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) & Z c= dom arcsin ) by A3, XBOOLE_1:18, A4;
A6: arcsin is_differentiable_on Z by A1, FDIFF_1:34, SIN_COS6:84;
set f2 = #Z 2;
A8: 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 A9: 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 A10: 0 < (1 + x) * (1 - x) by XREAL_1:131;
A13: for x being Real st x in Z holds
x in dom (f1 - (#Z 2)) by FUNCT_1:21, A5;
(f1 - (#Z 2)) . x = (f1 . x) - ((#Z 2) . x) by A9, A13, 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, A9 ;
hence (f1 - (#Z 2)) . x > 0 by A10; :: thesis: verum

end;

A17: for x being Real st x in Z holds
( f1 . x = 1 & (f1 - (#Z 2)) . x > 0 ) by A1, A8;
A18: (#R (1 / 2)) * (f1 - (#Z 2)) is_differentiable_on Z by A5, A17, FDIFF_7:22;
A19: ((#R (1 / 2)) * (f1 - (#Z 2))) (#) arcsin is_differentiable_on Z by A3, A6, A18, FDIFF_1:29;
A20: for x being Real st x in Z holds
(((#R (1 / 2)) * (f1 - (#Z 2))) (#) arcsin ) . x <> 0 by RFUNCT_1:13, A1;
A21: f is_differentiable_on Z by A1, A19, A20, FDIFF_2:22;
f | Z is continuous by A21, FDIFF_1:33;
then A22: f | A is continuous by A1, FCONT_1:17;
A23: ( f is_integrable_on A & f | A is bounded ) by A1, A22, INTEGRA5:10, INTEGRA5:11;
A24: for x being Real st x in Z holds
arcsin . x > 0 by A1;
A25: ln * arcsin is_differentiable_on Z by A1, A24, FDIFF_7:8;
B1: for x being Real st x in Z holds
f . x = 1 / ((sqrt (1 - (x ^2 ))) * (arcsin . x))

proof

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

end;

A26: for x being Real st x in dom ((ln * arcsin ) `| Z) holds
((ln * arcsin ) `| Z) . x = f . x

proof

let x be Real; :: thesis: ( x in dom ((ln * arcsin ) `| Z) implies ((ln * arcsin ) `| Z) . x = f . x )
assume x in dom ((ln * arcsin ) `| Z) ; :: thesis: ((ln * arcsin ) `| Z) . x = f . x
then A27: x in Z by A25, FDIFF_1:def 8;
then ((ln * arcsin ) `| Z) . x = 1 / ((sqrt (1 - (x ^2 ))) * (arcsin . x)) by A1, A24, FDIFF_7:8
.= f . x by B1, A27 ;
hence ((ln * arcsin ) `| Z) . x = f . x ; :: thesis: verum

end;

dom ((ln * arcsin ) `| Z) = dom f by A1, A25, FDIFF_1:def 8;
then (ln * arcsin ) `| Z = f by A26, PARTFUN1:34;
hence integral f,A = ((ln * arcsin ) . (sup A)) - ((ln * arcsin ) . (inf A)) by A1, A23, A25, INTEGRA5:13; :: thesis: verum