theorem Th70: :: SIN_COS7:70

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