let n be Element of NAT ; :: thesis:
let A be closed-interval Subset of REAL ; :: thesis:
let f1, f be PartFunc of REAL ,REAL ; :: thesis:
let Z be open Subset of REAL ; :: thesis:
assume A1: ( 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))) ) ; :: thesis:
A2: Z = (dom (n (#) ((#Z (n - 1)) * arcsin ))) /\ ((dom ((#R (1 / 2)) * (f1 - (#Z 2)))) \ (((#R (1 / 2)) * (f1 - (#Z 2))) " {0 })) by A1, RFUNCT_1:def 4;
A3: ( Z c= dom (n (#) ((#Z (n - 1)) * arcsin )) & Z c= (dom ((#R (1 / 2)) * (f1 - (#Z 2)))) \ (((#R (1 / 2)) * (f1 - (#Z 2))) " {0 }) ) by XBOOLE_1:18, A2;
A4: Z c= dom ((#Z (n - 1)) * arcsin ) by VALUED_1:def 5, A3;
A5: Z c= dom (((#R (1 / 2)) * (f1 - (#Z 2))) ^ ) by RFUNCT_1:def 8, A3;
dom (((#R (1 / 2)) * (f1 - (#Z 2))) ^ ) c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) by RFUNCT_1:11;
then A6: Z c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) by A5, XBOOLE_1:1;
A7: for x being Real st x in Z holds
(#Z (n - 1)) * arcsin is_differentiable_in x

proof

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then A8: arcsin is_differentiable_in x by A1, FDIFF_1:16, SIN_COS6:84;
consider m being Nat such that
A9: n = m + 1 by A1, NAT_1:6;
set m = n - 1;
thus (#Z (n - 1)) * arcsin is_differentiable_in x by A8, A9, TAYLOR_1:3; :: thesis:

end;

A10: (#Z (n - 1)) * arcsin is_differentiable_on Z by A4, A7, FDIFF_1:16;
A11: n (#) ((#Z (n - 1)) * arcsin ) is_differentiable_on Z by A3, A10, FDIFF_1:28;
set f2 = #Z 2;
A13: for x being Real st x in Z holds
(f1 - (#Z 2)) . x > 0

proof

let x be Real; :: thesis:
assume A14: x in Z ; :: thesis:
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 A15: 0 < (1 + x) * (1 - x) by XREAL_1:131;
A18: for x being Real st x in Z holds
x in dom (f1 - (#Z 2)) by FUNCT_1:21, A6;
(f1 - (#Z 2)) . x = (f1 . x) - ((#Z 2) . x) by A14, A18, 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, A14 ;
hence (f1 - (#Z 2)) . x > 0 by A15; :: thesis:

end;

A22: for x being Real st x in Z holds
( f1 . x = 1 & (f1 - (#Z 2)) . x > 0 ) by A1, A13;
A23: (#R (1 / 2)) * (f1 - (#Z 2)) is_differentiable_on Z by A6, A22, FDIFF_7:22;
A24: for x being Real st x in Z holds
((#R (1 / 2)) * (f1 - (#Z 2))) . x <> 0 by RFUNCT_1:13, A5;
A25: f is_differentiable_on Z by A1, A11, A23, A24, FDIFF_2:21;
f | Z is continuous by A25, FDIFF_1:33;
then A26: f | A is continuous by A1, FCONT_1:17;
A27: ( f is_integrable_on A & f | A is bounded ) by A1, A26, INTEGRA5:10, INTEGRA5:11;
A28: (#Z n) * arcsin is_differentiable_on Z by A1, FDIFF_7:10;
B1: for x being Real st x in Z holds
f . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2 )))

proof

let x be Real; :: thesis:
assume B2: x in Z ; :: thesis:
B3: ( x in dom (f1 - (#Z 2)) & (f1 - (#Z 2)) . x in dom (#R (1 / 2)) ) by FUNCT_1:21, B2, A6;
B4: (f1 - (#Z 2)) . x in right_open_halfline 0 by B3, 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;
((n (#) ((#Z (n - 1)) * arcsin )) / ((#R (1 / 2)) * (f1 - (#Z 2)))) . x = ((n (#) ((#Z (n - 1)) * arcsin )) . x) / (((#R (1 / 2)) * (f1 - (#Z 2))) . x) by RFUNCT_1:def 4, A1, B2
.= (n * (((#Z (n - 1)) * arcsin ) . x)) / (((#R (1 / 2)) * (f1 - (#Z 2))) . x) by VALUED_1:6
.= (n * ((#Z (n - 1)) . (arcsin . x))) / (((#R (1 / 2)) * (f1 - (#Z 2))) . x) by FUNCT_1:22, A4, B2
.= (n * ((arcsin . x) #Z (n - 1))) / (((#R (1 / 2)) * (f1 - (#Z 2))) . x) by TAYLOR_1:def 1
.= (n * ((arcsin . x) #Z (n - 1))) / ((#R (1 / 2)) . ((f1 - (#Z 2)) . x)) by FUNCT_1:22, A6, B2
.= (n * ((arcsin . x) #Z (n - 1))) / (((f1 - (#Z 2)) . x) #R (1 / 2)) by TAYLOR_1:def 4, B4
.= (n * ((arcsin . x) #Z (n - 1))) / (((f1 . x) - ((#Z 2) . x)) #R (1 / 2)) by VALUED_1:13, B3
.= (n * ((arcsin . x) #Z (n - 1))) / (((f1 . x) - (x #Z 2)) #R (1 / 2)) by TAYLOR_1:def 1
.= (n * ((arcsin . x) #Z (n - 1))) / (((f1 . x) - (x ^2 )) #R (1 / 2)) by FDIFF_7:1
.= (n * ((arcsin . x) #Z (n - 1))) / ((1 - (x ^2 )) #R (1 / 2)) by A1, B2
.= (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2 ))) by FDIFF_7:2, B6 ;
hence f . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2 ))) by A1; :: thesis:

end;

A29: for x being Real st x in dom (((#Z n) * arcsin ) `| Z) holds
(((#Z n) * arcsin ) `| Z) . x = f . x

proof

let x be Real; :: thesis:
assume x in dom (((#Z n) * arcsin ) `| Z) ; :: thesis:
then A30: x in Z by A28, FDIFF_1:def 8;
then (((#Z n) * arcsin ) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2 ))) by A1, FDIFF_7:10
.= f . x by B1, A30 ;
hence (((#Z n) * arcsin ) `| Z) . x = f . x ; :: thesis:

end;

dom (((#Z n) * arcsin ) `| Z) = dom f by A1, A28, FDIFF_1:def 8;
then ((#Z n) * arcsin ) `| Z = f by A29, PARTFUN1:34;
hence integral f,A = (((#Z n) * arcsin ) . (sup A)) - (((#Z n) * arcsin ) . (inf A)) by A1, A27, FDIFF_7:10, INTEGRA5:13; :: thesis: