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 Lm18;
diff sinh ,p = diff ((1 / 2) (#) (exp_R - (exp_R * compreal ))),p by Lm18
.= (1 / 2) * (diff (exp_R - (exp_R * compreal )),p) by Lm16
.= (1 / 2) * ((exp_R . p) + (exp_R . (- p))) by Lm15
.= ((exp_R . p) + (exp_R . (- p))) / 2
.= cosh . p by Def3 ;
hence ( sinh is_differentiable_in p & diff sinh ,p = cosh . p ) by A1, Lm16; :: thesis: verum