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

- 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