let a, b be Real; for A being closed-interval Subset of REAL
for f1, f2, 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
( 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 closed-interval Subset of REAL; for f1, f2, 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
( 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 f1, f2, f 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 A3:
( Z c= dom (a (#) arccos) & Z c= dom (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) )
by XBOOLE_1:18;
then A4:
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 A3, RFUNCT_1:def 4;
then A6:
( 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 XBOOLE_1:19, A4;
then A8:
Z c= dom (f1 (#) arccos)
by VALUED_1:def 4;
A9:
Z c= dom (((#R (1 / 2)) * (f2 - (#Z 2))) ^)
by RFUNCT_1:def 8, A6;
dom (((#R (1 / 2)) * (f2 - (#Z 2))) ^) c= dom ((#R (1 / 2)) * (f2 - (#Z 2)))
by RFUNCT_1:11;
then A10:
Z c= dom ((#R (1 / 2)) * (f2 - (#Z 2)))
by XBOOLE_1:1, A9;
A11:
arccos is_differentiable_on Z
by A1, FDIFF_1:34, SIN_COS6:108;
then A12:
a (#) arccos is_differentiable_on Z
by A3, FDIFF_1:28;
A13:
for x being Real st x in Z holds
f1 . x = (a * x) + b
by A1;
then A14:
f1 is_differentiable_on Z
by A6, FDIFF_1:31;
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 A25:
(#R (1 / 2)) * (f2 - (#Z 2)) is_differentiable_on Z
by A10, FDIFF_7:22;
for x being Real st x in Z holds
((#R (1 / 2)) * (f2 - (#Z 2))) . x <> 0
by RFUNCT_1:13, A9;
then
f1 / ((#R (1 / 2)) * (f2 - (#Z 2))) is_differentiable_on Z
by A14, A25, FDIFF_2:21;
then
f is_differentiable_on Z
by A1, A12, FDIFF_1:27;
then
f | Z is continuous
by FDIFF_1:33;
then
f | A is continuous
by A1, FCONT_1:17;
then A30:
( f is_integrable_on A & f | A is bounded )
by A1, INTEGRA5:10, INTEGRA5:11;
A31:
f1 (#) arccos is_differentiable_on Z
by A8, A11, A14, FDIFF_1:29;
B1:
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 B2:
x in Z
;
f . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2))))
then B3:
(
x in dom (f2 - (#Z 2)) &
(f2 - (#Z 2)) . x in dom (#R (1 / 2)) )
by FUNCT_1:21, A10;
then B4:
(f2 - (#Z 2)) . x in right_open_halfline 0
by 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;
((a (#) arccos) - (f1 / ((#R (1 / 2)) * (f2 - (#Z 2))))) . x =
((a (#) arccos) . x) - ((f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) . x)
by VALUED_1:13, A1, B2
.=
(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 RFUNCT_1:def 4, A3, B2
.=
(a * (arccos . x)) - (((a * x) + b) / (((#R (1 / 2)) * (f2 - (#Z 2))) . x))
by A1, B2
.=
(a * (arccos . x)) - (((a * x) + b) / ((#R (1 / 2)) . ((f2 - (#Z 2)) . x)))
by A10, FUNCT_1:22, B2
.=
(a * (arccos . x)) - (((a * x) + b) / (((f2 - (#Z 2)) . x) #R (1 / 2)))
by TAYLOR_1:def 4, B4
.=
(a * (arccos . x)) - (((a * x) + b) / (((f2 . x) - ((#Z 2) . x)) #R (1 / 2)))
by VALUED_1:13, B3
.=
(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, B2
.=
(a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2))))
by FDIFF_7:2, B6
;
hence
f . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2))))
by A1;
verum
end;
A32:
for x being Real st x in dom ((f1 (#) arccos) `| Z) holds
((f1 (#) arccos) `| Z) . x = f . x
dom ((f1 (#) arccos) `| Z) = dom f
by A1, A31, FDIFF_1:def 8;
then
(f1 (#) arccos) `| Z = f
by A32, PARTFUN1:34;
hence
integral (f,A) = ((f1 (#) arccos) . (upper_bound A)) - ((f1 (#) arccos) . (lower_bound A))
by A1, A30, A31, INTEGRA5:13; verum