let p be real number ; :: thesis: ( sinh is_differentiable_in p & diff sinh ,p = cosh . p )
set ff = compreal ;
A1: sinh = (1 / 2) (#) (exp_R - (exp_R * compreal )) by Lm19;
diff sinh ,p = diff ((1 / 2) (#) (exp_R - (exp_R * compreal ))),p by Lm19
.= (1 / 2) * (diff (exp_R - (exp_R * compreal )),p) by Lm17
.= (1 / 2) * ((exp_R . p) + (exp_R . (- p))) by Lm16
.= ((exp_R . p) + (exp_R . (- p))) / 2
.= cosh . p by Def3 ;
hence ( sinh is_differentiable_in p & diff sinh ,p = cosh . p ) by A1, Lm17; :: thesis: verum