for x being complex number st x in REAL holds
- x in REAL by XREAL_0:def 1;
then A1: REAL is symmetrical by Def1;
( ( 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, Def2, Def6;
hence sinh is odd ; :: thesis: verum