for x being Complex st x in REAL holds
- x in REAL by XREAL_0:def 1;
then ( ( for x being Real st x in dom sin & - x in dom sin holds
sin . (- x) = - (sin . x) ) & REAL is symmetrical ) by SIN_COS:30;
then ( sin is with_symmetrical_domain & sin is quasi_odd ) by SIN_COS:24;
hence sin is odd ; :: thesis: verum