let n be Element of NAT ; for A being non empty closed_interval Subset of REAL
for f, f1 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
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))) holds
integral (f,A) = (((#Z n) * arcsin) . (upper_bound A)) - (((#Z n) * arcsin) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; for f, f1 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
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))) holds
integral (f,A) = (((#Z n) * arcsin) . (upper_bound A)) - (((#Z n) * arcsin) . (lower_bound A))
let f, f1 be 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
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))) holds
integral (f,A) = (((#Z n) * arcsin) . (upper_bound A)) - (((#Z n) * arcsin) . (lower_bound A))
let Z be open Subset of REAL; ( 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))) implies integral (f,A) = (((#Z n) * arcsin) . (upper_bound A)) - (((#Z n) * arcsin) . (lower_bound A)) )
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))) )
; integral (f,A) = (((#Z n) * arcsin) . (upper_bound A)) - (((#Z n) * arcsin) . (lower_bound A))
then
Z = (dom (n (#) ((#Z (n - 1)) * arcsin))) /\ ((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)) * arcsin)) & 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)) * arcsin)
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)) * arcsin is_differentiable_in x
then
(#Z (n - 1)) * arcsin is_differentiable_on Z
by A3, FDIFF_1:9;
then A8:
n (#) ((#Z (n - 1)) * arcsin) 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
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) * arcsin is_differentiable_on Z
by A1, FDIFF_7:10;
A14:
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;
( x in Z implies f . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) )
assume A15:
x in Z
;
f . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))
then A16:
(
x in dom (f1 - (#Z 2)) &
(f1 - (#Z 2)) . x in dom (#R (1 / 2)) )
by A5, FUNCT_1:11;
then A17:
(f1 - (#Z 2)) . x in right_open_halfline 0
by TAYLOR_1:def 4;
(
- 1
< x &
x < 1 )
by A1, A15, XXREAL_1:4;
then
(
0 < 1
+ x &
0 < 1
- x )
by XREAL_1:50, XREAL_1:148;
then A18:
0 < (1 + x) * (1 - x)
by XREAL_1:129;
((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 A1, A15, RFUNCT_1:def 1
.=
(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 A3, A15, FUNCT_1:12
.=
(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 A5, A15, FUNCT_1:12
.=
(n * ((arcsin . x) #Z (n - 1))) / (((f1 - (#Z 2)) . x) #R (1 / 2))
by A17, TAYLOR_1:def 4
.=
(n * ((arcsin . x) #Z (n - 1))) / (((f1 . x) - ((#Z 2) . x)) #R (1 / 2))
by A16, VALUED_1:13
.=
(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, A15
.=
(n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))
by A18, FDIFF_7:2
;
hence
f . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))
by A1;
verum
end;
A19:
for x being Element of REAL st x in dom (((#Z n) * arcsin) `| Z) holds
(((#Z n) * arcsin) `| Z) . x = f . x
dom (((#Z n) * arcsin) `| Z) = dom f
by A1, A13, FDIFF_1:def 7;
then
((#Z n) * arcsin) `| Z = f
by A19, PARTFUN1:5;
hence
integral (f,A) = (((#Z n) * arcsin) . (upper_bound A)) - (((#Z n) * arcsin) . (lower_bound A))
by A1, A12, FDIFF_7:10, INTEGRA5:13; verum