theorem :: FUNCT_8:76

for A being symmetrical Subset of REAL holds cos " is_even_on A