:: deftheorem defines cosh SIN_COS2:def 4 :
for d being object holds cosh d = cosh . d;