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