theorem :: FUNCT_8:75
for A being symmetrical Subset of REAL holds sin " is_odd_on A