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