:: deftheorem Def1 defines sinh SIN_COS2:def 1 :
for b₁ being Function of REAL,REAL holds
( b₁ = sinh iff for d being Real holds b₁ . d = ((exp_R . d) - (exp_R . (- d))) / 2 );