let n be Element of NAT ; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let f, f1 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 c= dom ((#Z n) * arccos) & Z = dom f & 1 < n & f = (n (#) ((#Z (n - 1)) * arccos)) / ((#R (1 / 2)) * (f1 - (#Z 2))) ) ; :: thesis:
then Z = (dom (n (#) ((#Z (n - 1)) * arccos))) /\ ((dom ((#R (1 / 2)) * (f1 - (#Z 2)))) \ (((#R (1 / 2)) * (f1 - (#Z 2))) " {0})) by RFUNCT_1:def 1;
then A2: ( Z c= dom (n (#) ((#Z (n - 1)) * arccos)) & Z c= (dom ((#R (1 / 2)) * (f1 - (#Z 2)))) \ (((#R (1 / 2)) * (f1 - (#Z 2))) " {0}) ) by XBOOLE_1:18;
then A3: Z c= dom ((#Z (n - 1)) * arccos) by VALUED_1:def 5;
A4: Z c= dom (((#R (1 / 2)) * (f1 - (#Z 2))) ^) by A2, RFUNCT_1:def 2;
dom (((#R (1 / 2)) * (f1 - (#Z 2))) ^) c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) by RFUNCT_1:1;
then A5: Z c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) by A4;
for x being Real st x in Z holds
(#Z (n - 1)) * arccos is_differentiable_in x

proof

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then A6: arccos is_differentiable_in x by A1, FDIFF_1:9, SIN_COS6:106;
consider m being Nat such that
A7: n = m + 1 by A1, NAT_1:6;
thus (#Z (n - 1)) * arccos is_differentiable_in x by A6, A7, TAYLOR_1:3; :: thesis:

end;

then (#Z (n - 1)) * arccos is_differentiable_on Z by A3, FDIFF_1:9;
then A8: n (#) ((#Z (n - 1)) * arccos) is_differentiable_on Z by A2, FDIFF_1:20;
set f2 = #Z 2;
for x being Real st x in Z holds
(f1 - (#Z 2)) . x > 0

proof

let x be Real; :: thesis:
assume A9: x in Z ; :: thesis:
then ( - 1 < x & x < 1 ) by A1, XXREAL_1:4;
then ( 0 < 1 + x & 0 < 1 - x ) by XREAL_1:50, XREAL_1:148;
then A10: 0 < (1 + x) * (1 - x) by XREAL_1:129;
for x being Real st x in Z holds
x in dom (f1 - (#Z 2)) by A5, FUNCT_1:11;
then (f1 - (#Z 2)) . x = (f1 . x) - ((#Z 2) . x) by A9, 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:35
.= (f1 . x) - (x * x) by PREPOWER:35
.= 1 - (x * x) by A1, A9 ;
hence (f1 - (#Z 2)) . x > 0 by A10; :: thesis:

end;

then for x being Real st x in Z holds
( f1 . x = 1 & (f1 - (#Z 2)) . x > 0 ) by A1;
then A11: (#R (1 / 2)) * (f1 - (#Z 2)) is_differentiable_on Z by A5, FDIFF_7:22;
for x being Real st x in Z holds
((#R (1 / 2)) * (f1 - (#Z 2))) . x <> 0 by A4, RFUNCT_1:3;
then f is_differentiable_on Z by A1, A8, A11, FDIFF_2:21;
then f | Z is continuous by FDIFF_1:25;
then f | A is continuous by A1, FCONT_1:16;
then A12: ( f is_integrable_on A & f | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A13: (#Z n) * arccos is_differentiable_on Z by A1, FDIFF_7:11;
A14: Z c= dom (- ((#Z n) * arccos)) by A1, VALUED_1:8;
then A15: (- 1) (#) ((#Z n) * arccos) is_differentiable_on Z by A13, FDIFF_1:20;
A16: for x being Real st x in Z holds
f . x = (n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))

proof

let x be Real; :: thesis:
assume A17: x in Z ; :: thesis:
then A18: ( x in dom (f1 - (#Z 2)) & (f1 - (#Z 2)) . x in dom (#R (1 / 2)) ) by A5, FUNCT_1:11;
then A19: (f1 - (#Z 2)) . x in right_open_halfline 0 by TAYLOR_1:def 4;
( - 1 < x & x < 1 ) by A1, A17, XXREAL_1:4;
then ( 0 < 1 + x & 0 < 1 - x ) by XREAL_1:50, XREAL_1:148;
then A20: 0 < (1 + x) * (1 - x) by XREAL_1:129;
((n (#) ((#Z (n - 1)) * arccos)) / ((#R (1 / 2)) * (f1 - (#Z 2)))) . x = ((n (#) ((#Z (n - 1)) * arccos)) . x) / (((#R (1 / 2)) * (f1 - (#Z 2))) . x) by A1, A17, RFUNCT_1:def 1
.= (n * (((#Z (n - 1)) * arccos) . x)) / (((#R (1 / 2)) * (f1 - (#Z 2))) . x) by VALUED_1:6
.= (n * ((#Z (n - 1)) . (arccos . x))) / (((#R (1 / 2)) * (f1 - (#Z 2))) . x) by A3, A17, FUNCT_1:12
.= (n * ((arccos . x) #Z (n - 1))) / (((#R (1 / 2)) * (f1 - (#Z 2))) . x) by TAYLOR_1:def 1
.= (n * ((arccos . x) #Z (n - 1))) / ((#R (1 / 2)) . ((f1 - (#Z 2)) . x)) by A5, A17, FUNCT_1:12
.= (n * ((arccos . x) #Z (n - 1))) / (((f1 - (#Z 2)) . x) #R (1 / 2)) by A19, TAYLOR_1:def 4
.= (n * ((arccos . x) #Z (n - 1))) / (((f1 . x) - ((#Z 2) . x)) #R (1 / 2)) by A18, VALUED_1:13
.= (n * ((arccos . x) #Z (n - 1))) / (((f1 . x) - (x #Z 2)) #R (1 / 2)) by TAYLOR_1:def 1
.= (n * ((arccos . x) #Z (n - 1))) / (((f1 . x) - (x ^2)) #R (1 / 2)) by FDIFF_7:1
.= (n * ((arccos . x) #Z (n - 1))) / ((1 - (x ^2)) #R (1 / 2)) by A1, A17
.= (n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) by A20, FDIFF_7:2 ;
hence f . x = (n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) by A1; :: thesis:

end;

A21: for x being Real st x in Z holds
((- ((#Z n) * arccos)) `| Z) . x = (n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))

proof

let x be Real; :: thesis:
assume A22: x in Z ; :: thesis:
then A23: ( - 1 < x & x < 1 ) by A1, XXREAL_1:4;
A24: arccos is_differentiable_in x by A1, A22, FDIFF_1:9, SIN_COS6:106;
A25: (#Z n) * arccos is_differentiable_in x by A13, A22, FDIFF_1:9;
((- ((#Z n) * arccos)) `| Z) . x = diff ((- ((#Z n) * arccos)),x) by A15, A22, FDIFF_1:def 7
.= (- 1) * (diff (((#Z n) * arccos),x)) by A25, FDIFF_1:15
.= (- 1) * ((n * ((arccos . x) #Z (n - 1))) * (diff (arccos,x))) by A24, TAYLOR_1:3
.= (- 1) * ((n * ((arccos . x) #Z (n - 1))) * (- (1 / (sqrt (1 - (x ^2)))))) by A23, SIN_COS6:106
.= (n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ;
hence ((- ((#Z n) * arccos)) `| Z) . x = (n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ; :: thesis:

end;

A26: for x being Element of REAL st x in dom ((- ((#Z n) * arccos)) `| Z) holds
((- ((#Z n) * arccos)) `| Z) . x = f . x

proof

let x be Element of REAL ; :: thesis:
assume x in dom ((- ((#Z n) * arccos)) `| Z) ; :: thesis:
then A27: x in Z by A15, FDIFF_1:def 7;
then ((- ((#Z n) * arccos)) `| Z) . x = (n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) by A21
.= f . x by A16, A27 ;
hence ((- ((#Z n) * arccos)) `| Z) . x = f . x ; :: thesis:

end;

dom ((- ((#Z n) * arccos)) `| Z) = dom f by A1, A15, FDIFF_1:def 7;
then (- ((#Z n) * arccos)) `| Z = f by A26, PARTFUN1:5;
hence integral (f,A) = ((- ((#Z n) * arccos)) . (upper_bound A)) - ((- ((#Z n) * arccos)) . (lower_bound A)) by A1, A12, A13, A14, FDIFF_1:20, INTEGRA5:13; :: thesis: