theorem Th71: :: SIN_COS7:71

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