let x be Real; for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds
( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) )
let f be PartFunc of REAL,REAL; ( f is_differentiable_in x & f . x > - 1 & f . x < 1 implies ( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) ) )
assume that
A1:
f is_differentiable_in x
and
A2:
( f . x > - 1 & f . x < 1 )
; ( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) )
f . x in ].(- 1),1.[
by A2;
then A3:
arcsin is_differentiable_in f . x
by FDIFF_1:9, SIN_COS6:83;
then diff ((arcsin * f),x) =
(diff (arcsin,(f . x))) * (diff (f,x))
by A1, FDIFF_2:13
.=
(diff (f,x)) * (1 / (sqrt (1 - ((f . x) ^2))))
by A2, SIN_COS6:83
.=
(diff (f,x)) / (sqrt (1 - ((f . x) ^2)))
by XCMPLX_1:99
;
hence
( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) )
by A1, A3, FDIFF_2:13; verum