let A be symmetrical Subset of REAL; :: thesis: - sin is_odd_on A
A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence - sin is_odd_on A by Th16, Th65; :: thesis: verum