theorem :: FUNCT_8:80

for A being symmetrical Subset of REAL holds cos ^2 is_even_on A