theorem :: FUNCT_8:71

for A being symmetrical Subset of COMPLEX st A c= dom cot holds
cot is_odd_on A