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

- 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