theorem Th69: :: SIN_COS7:69

for x being Real holds cosh . (2 * x) = 1 + (2 * ((sinh . x) ^2))