let p be Real; :: thesis: ( cosh is_differentiable_in p & diff (cosh,p) = sinh . p )
reconsider ff = compreal as PartFunc of REAL,REAL ;
A1: cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) by Lm21;
diff (cosh,p) = diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) by Lm21
.= (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) by Lm19
.= (1 / 2) * ((exp_R . p) - (exp_R . (- p))) by Lm15
.= ((exp_R . p) - (exp_R . (- p))) / 2
.= sinh . p by Def1 ;
hence ( cosh is_differentiable_in p & diff (cosh,p) = sinh . p ) by A1, Lm19; :: thesis: verum