let x be Real; :: thesis: cosh . (2 * x) = 1 + (2 * ((sinh . x) ^2))
2 * ((sinh . x) ^2) = 2 * ((1 / 2) * ((cosh . (2 * x)) - 1)) by SIN_COS2:18;
hence cosh . (2 * x) = 1 + (2 * ((sinh . x) ^2)) ; :: thesis: verum