theorem Th11: :: INTEGR11:11

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