A1: for x being Real st x in dom sin & - x in dom sin holds
sin . (- x) = - (sin . x) by SIN_COS:33;
for x being complex number st x in REAL holds
- x in REAL by XREAL_0:def 1;
then REAL is symmetrical by Def1;
then ( sin is with_symmetrical_domain & sin is quasi_odd ) by A1, Def2, SIN_COS:27, Def6;
hence sin is odd ; :: thesis: verum