theorem Th11: :: SIN_COS8:11

for y, z being Real holds
( (sinh y) * (sinh z) = (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) & (sinh y) * (cosh z) = (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) & (cosh y) * (sinh z) = (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) & (cosh y) * (cosh z) = (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) )