( ((AffineMap (1,0)) (#) cosh) - sinh is_differentiable_on REAL & ( for x being Real holds ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = x * (sinh . x) ) )