let a, b be Real; for A being non empty closed_interval Subset of REAL
for f, f1, f2 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 = (a * x) + b & f2 . x = 1 ) ) & Z = dom f & f = (a (#) arccos) - (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) holds
integral (f,A) = ((f1 (#) arccos) . (upper_bound A)) - ((f1 (#) arccos) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; for f, f1, f2 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 = (a * x) + b & f2 . x = 1 ) ) & Z = dom f & f = (a (#) arccos) - (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) holds
integral (f,A) = ((f1 (#) arccos) . (upper_bound A)) - ((f1 (#) arccos) . (lower_bound A))
let f, f1, f2 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 = (a * x) + b & f2 . x = 1 ) ) & Z = dom f & f = (a (#) arccos) - (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) holds
integral (f,A) = ((f1 (#) arccos) . (upper_bound A)) - ((f1 (#) arccos) . (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 = (a * x) + b & f2 . x = 1 ) ) & Z = dom f & f = (a (#) arccos) - (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) implies integral (f,A) = ((f1 (#) arccos) . (upper_bound A)) - ((f1 (#) arccos) . (lower_bound A)) )
assume A1:
( A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = (a * x) + b & f2 . x = 1 ) ) & Z = dom f & f = (a (#) arccos) - (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) )
; integral (f,A) = ((f1 (#) arccos) . (upper_bound A)) - ((f1 (#) arccos) . (lower_bound A))
then
Z = (dom (a (#) arccos)) /\ (dom (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))))
by VALUED_1:12;
then A2:
( Z c= dom (a (#) arccos) & Z c= dom (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) )
by XBOOLE_1:18;
then A3:
Z c= dom arccos
by VALUED_1:def 5;
Z c= (dom f1) /\ ((dom ((#R (1 / 2)) * (f2 - (#Z 2)))) \ (((#R (1 / 2)) * (f2 - (#Z 2))) " {0}))
by A2, RFUNCT_1:def 1;
then A4:
( Z c= dom f1 & Z c= (dom ((#R (1 / 2)) * (f2 - (#Z 2)))) \ (((#R (1 / 2)) * (f2 - (#Z 2))) " {0}) )
by XBOOLE_1:18;
then
Z c= (dom f1) /\ (dom arccos)
by A3, XBOOLE_1:19;
then A5:
Z c= dom (f1 (#) arccos)
by VALUED_1:def 4;
A6:
Z c= dom (((#R (1 / 2)) * (f2 - (#Z 2))) ^)
by A4, RFUNCT_1:def 2;
dom (((#R (1 / 2)) * (f2 - (#Z 2))) ^) c= dom ((#R (1 / 2)) * (f2 - (#Z 2)))
by RFUNCT_1:1;
then A7:
Z c= dom ((#R (1 / 2)) * (f2 - (#Z 2)))
by A6;
A8:
arccos is_differentiable_on Z
by A1, FDIFF_1:26, SIN_COS6:106;
then A9:
a (#) arccos is_differentiable_on Z
by A2, FDIFF_1:20;
A10:
for x being Real st x in Z holds
f1 . x = (a * x) + b
by A1;
then A11:
f1 is_differentiable_on Z
by A4, FDIFF_1:23;
set f3 = #Z 2;
for x being Real st x in Z holds
(f2 - (#Z 2)) . x > 0
then
for x being Real st x in Z holds
( f2 . x = 1 & (f2 - (#Z 2)) . x > 0 )
by A1;
then A14:
(#R (1 / 2)) * (f2 - (#Z 2)) is_differentiable_on Z
by A7, FDIFF_7:22;
for x being Real st x in Z holds
((#R (1 / 2)) * (f2 - (#Z 2))) . x <> 0
by A6, RFUNCT_1:3;
then
f1 / ((#R (1 / 2)) * (f2 - (#Z 2))) is_differentiable_on Z
by A11, A14, FDIFF_2:21;
then
f is_differentiable_on Z
by A1, A9, FDIFF_1:19;
then
f | Z is continuous
by FDIFF_1:25;
then
f | A is continuous
by A1, FCONT_1:16;
then A15:
( f is_integrable_on A & f | A is bounded )
by A1, INTEGRA5:10, INTEGRA5:11;
A16:
f1 (#) arccos is_differentiable_on Z
by A5, A8, A11, FDIFF_1:21;
A17:
for x being Real st x in Z holds
f . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2))))
proof
let x be
Real;
( x in Z implies f . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) )
assume A18:
x in Z
;
f . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2))))
then A19:
(
x in dom (f2 - (#Z 2)) &
(f2 - (#Z 2)) . x in dom (#R (1 / 2)) )
by A7, FUNCT_1:11;
then A20:
(f2 - (#Z 2)) . x in right_open_halfline 0
by TAYLOR_1:def 4;
(
- 1
< x &
x < 1 )
by A1, A18, XXREAL_1:4;
then
(
0 < 1
+ x &
0 < 1
- x )
by XREAL_1:50, XREAL_1:148;
then A21:
0 < (1 + x) * (1 - x)
by XREAL_1:129;
((a (#) arccos) - (f1 / ((#R (1 / 2)) * (f2 - (#Z 2))))) . x =
((a (#) arccos) . x) - ((f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) . x)
by A1, A18, VALUED_1:13
.=
(a * (arccos . x)) - ((f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) . x)
by VALUED_1:6
.=
(a * (arccos . x)) - ((f1 . x) / (((#R (1 / 2)) * (f2 - (#Z 2))) . x))
by A2, A18, RFUNCT_1:def 1
.=
(a * (arccos . x)) - (((a * x) + b) / (((#R (1 / 2)) * (f2 - (#Z 2))) . x))
by A1, A18
.=
(a * (arccos . x)) - (((a * x) + b) / ((#R (1 / 2)) . ((f2 - (#Z 2)) . x)))
by A7, A18, FUNCT_1:12
.=
(a * (arccos . x)) - (((a * x) + b) / (((f2 - (#Z 2)) . x) #R (1 / 2)))
by A20, TAYLOR_1:def 4
.=
(a * (arccos . x)) - (((a * x) + b) / (((f2 . x) - ((#Z 2) . x)) #R (1 / 2)))
by A19, VALUED_1:13
.=
(a * (arccos . x)) - (((a * x) + b) / (((f2 . x) - (x #Z 2)) #R (1 / 2)))
by TAYLOR_1:def 1
.=
(a * (arccos . x)) - (((a * x) + b) / (((f2 . x) - (x ^2)) #R (1 / 2)))
by FDIFF_7:1
.=
(a * (arccos . x)) - (((a * x) + b) / ((1 - (x ^2)) #R (1 / 2)))
by A1, A18
.=
(a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2))))
by A21, FDIFF_7:2
;
hence
f . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2))))
by A1;
verum
end;
A22:
for x being Element of REAL st x in dom ((f1 (#) arccos) `| Z) holds
((f1 (#) arccos) `| Z) . x = f . x
dom ((f1 (#) arccos) `| Z) = dom f
by A1, A16, FDIFF_1:def 7;
then
(f1 (#) arccos) `| Z = f
by A22, PARTFUN1:5;
hence
integral (f,A) = ((f1 (#) arccos) . (upper_bound A)) - ((f1 (#) arccos) . (lower_bound A))
by A1, A15, A16, INTEGRA5:13; verum