let p, r be Real; :: thesis: sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))
sinh . (p - r) = sinh . (p + (- r))
.= ((sinh . p) * (cosh . (- r))) + ((cosh . p) * (sinh . (- r))) by Lm3
.= ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . (- r))) by Th19
.= ((sinh . p) * (cosh . r)) + ((cosh . p) * (- (sinh . r))) by Th19
.= ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ;
hence sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ; :: thesis: verum