let a be Real; :: thesis: for Z being open Subset of REAL
for f, f1, f2, f3 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & 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 f, f1, f2, f3 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & 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 f, f1, f2, f3 be PartFunc of REAL,REAL; :: thesis: ( Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & 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 that
A1: Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) and
A2: ( f = f1 - f2 & f2 = #Z 2 ) and
A3: 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) ) )
A4: Z c= (dom ((id Z) (#) (arccos * f3))) /\ (dom ((#R (1 / 2)) * f)) by A1, VALUED_1:12;
then A5: Z c= dom ((#R (1 / 2)) * f) by XBOOLE_1:18;
A6: for x being Real st x in Z holds
( f1 . x = a ^2 & f . x > 0 ) by A3;
then A7: (#R (1 / 2)) * f is_differentiable_on Z by A2, A5, Th27;
A8: for x being Real st x in Z holds
( f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 ) by A3;
A9: Z c= dom ((id Z) (#) (arccos * f3)) by A4, XBOOLE_1:18;
then A10: (id Z) (#) (arccos * f3) is_differentiable_on Z by A8, Th26;
A11: 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 A12: x in Z ; :: thesis: ((a ^2) - (x #Z 2)) #R (- (1 / 2)) = 1 / (a * (sqrt (1 - ((x / a) ^2))))
then A13: f3 . x = x / a by A3;
f3 . x < 1 by A3, A12;
then A14: 1 - (f3 . x) > 1 - 1 by XREAL_1:10;
f3 . x > - 1 by A3, A12;
then 1 + (f3 . x) > 1 + (- 1) by XREAL_1:6;
then A15: (1 + (f3 . x)) * (1 - (f3 . x)) > 0 by A14, XREAL_1:129;
A16: a > 0 by A3, A12;
then A17: a ^2 > 0 by SQUARE_1:12;
1 / (a * (sqrt (1 - ((x / a) ^2)))) = 1 / ((sqrt (a ^2)) * (sqrt (1 - ((x / a) ^2)))) by A16, SQUARE_1:22
.= 1 / (sqrt ((a ^2) * (1 - ((x / a) ^2)))) by A17, A13, A15, SQUARE_1:29
.= (((a ^2) * 1) - ((a * (x / a)) ^2)) #R (- (1 / 2)) by A17, A13, A15, Th3, XREAL_1:129
.= ((a ^2) - (((x * a) / a) ^2)) #R (- (1 / 2)) by XCMPLX_1:74
.= ((a ^2) - ((x * (a / a)) ^2)) #R (- (1 / 2)) by XCMPLX_1:74
.= ((a ^2) - ((x * 1) ^2)) #R (- (1 / 2)) by A16, 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 A18: 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, A10, A7, FDIFF_1:19
.= ((((id Z) (#) (arccos * f3)) `| Z) . x) - (diff (((#R (1 / 2)) * f),x)) by A10, A18, FDIFF_1:def 7
.= ((((id Z) (#) (arccos * f3)) `| Z) . x) - ((((#R (1 / 2)) * f) `| Z) . x) by A7, A18, FDIFF_1:def 7
.= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2)))))) - ((((#R (1 / 2)) * f) `| Z) . x) by A9, A8, A18, Th26
.= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2)))))) - (- (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2))))) by A2, A5, A6, A18, 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 A11, A18
.= ((arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2)))))) + (x / (a * (sqrt (1 - ((x / a) ^2))))) by XCMPLX_1:99
.= 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, A10, A7, FDIFF_1:19; :: thesis: verum