let p be Real; :: 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