let a be Real; :: thesis: for Z being open Subset of REAL
for f3, f, f1, f2 being PartFunc of REAL ,REAL st Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds
( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) )
let Z be open Subset of REAL ; :: thesis: for f3, f, f1, f2 being PartFunc of REAL ,REAL st Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds
( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) )
let f3, f, f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) implies ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) ) )
assume A1: ( Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) ) ; :: thesis: ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) )
then A2: Z c= (dom ((id Z) (#) (arccos * f3))) /\ (dom ((#R (1 / 2)) * f)) by VALUED_1:12;
then A3: Z c= dom ((id Z) (#) (arccos * f3)) by XBOOLE_1:18;
A4: Z c= dom ((#R (1 / 2)) * f) by A2, XBOOLE_1:18;
A5: ( Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 ) ) ) by A1;
then A6: ( (id Z) (#) (arccos * f3) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (arccos * f3)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2 ))))) ) ) by A3, Th26;
A7: ( f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & f . x > 0 ) ) ) by A1;
then A8: ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2 ) - (x #Z 2)) #R (- (1 / 2)))) ) ) by A4, Th27;
A9: for x being Real st x in Z holds
((a ^2 ) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2 ))))

proof

let x be Real; :: thesis: ( x in Z implies ((a ^2 ) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2 )))) )
assume A10: x in Z ; :: thesis: ((a ^2 ) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2 ))))
then A11: a > 0 by A1;
then A12: a ^2 > 0 by SQUARE_1:74;
A13: f3 . x = x / a by A1, A10;
f3 . x > - 1 by A1, A10;
then A14: 1 + (f3 . x) > 1 + (- 1) by XREAL_1:8;
f3 . x < 1 by A1, A10;
then 1 - (f3 . x) > 1 - 1 by XREAL_1:12;
then A15: (1 + (f3 . x)) * (1 - (f3 . x)) > 0 by A14, XREAL_1:131;
1 / (a * (sqrt (1 - ((x / a) ^2 )))) = 1 / ((sqrt (a ^2 )) * (sqrt (1 - ((x / a) ^2 )))) by A11, SQUARE_1:89
.= 1 / (sqrt ((a ^2 ) * (1 - ((x / a) ^2 )))) by A12, A13, A15, SQUARE_1:97
.= (((a ^2 ) * 1) - ((a * (x / a)) ^2 )) #R (- (1 / 2)) by A12, A13, A15, Th3, XREAL_1:131
.= ((a ^2 ) - (((x * a) / a) ^2 )) #R (- (1 / 2)) by XCMPLX_1:75
.= ((a ^2 ) - ((x * (a / a)) ^2 )) #R (- (1 / 2)) by XCMPLX_1:75
.= ((a ^2 ) - ((x * 1) ^2 )) #R (- (1 / 2)) by A11, XCMPLX_1:60
.= ((a ^2 ) - (x #Z 2)) #R (- (1 / 2)) by Th1 ;
hence ((a ^2 ) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2 )))) ; :: thesis: verum

end;

for x being Real st x in Z holds
((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a)

proof

let x be Real; :: thesis: ( x in Z implies ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) )
assume A16: x in Z ; :: thesis: ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a)
then ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = (diff ((id Z) (#) (arccos * f3)),x) - (diff ((#R (1 / 2)) * f),x) by A1, A6, A8, FDIFF_1:27
.= ((((id Z) (#) (arccos * f3)) `| Z) . x) - (diff ((#R (1 / 2)) * f),x) by A6, A16, FDIFF_1:def 8
.= ((((id Z) (#) (arccos * f3)) `| Z) . x) - ((((#R (1 / 2)) * f) `| Z) . x) by A8, A16, FDIFF_1:def 8
.= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2 )))))) - ((((#R (1 / 2)) * f) `| Z) . x) by A3, A5, A16, Th26
.= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2 )))))) - (- (x * (((a ^2 ) - (x #Z 2)) #R (- (1 / 2))))) by A4, A7, A16, Th27
.= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2 )))))) + (x * (((a ^2 ) - (x #Z 2)) #R (- (1 / 2))))
.= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2 )))))) + (x * (1 / (a * (sqrt (1 - ((x / a) ^2 )))))) by A9, A16
.= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2 )))))) + (x / (a * (sqrt (1 - ((x / a) ^2 ))))) by XCMPLX_1:100
.= arccos . (x / a) ;
hence ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ; :: thesis: verum

end;

hence ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) ) by A1, A6, A8, FDIFF_1:27; :: thesis: verum