for x being Complex st x in REAL holds
- x in REAL by XREAL_0:def 1;
then A1: REAL is symmetrical ;
( ( for x being Real st x in dom sinh & - x in dom sinh holds
sinh . (- x) = - (sinh . x) ) & dom sinh = REAL ) by FUNCT_2:def 1, SIN_COS2:19;
then ( sinh is with_symmetrical_domain & sinh is quasi_odd ) by A1;
hence sinh is odd ; :: thesis: verum