let x be Real; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: ( 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:16, SIN_COS6:84;
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:84
.= (diff f,x) / (sqrt (1 - ((f . x) ^2 ))) by XCMPLX_1:100 ;
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; :: thesis: verum