let A be symmetrical Subset of REAL ; :: thesis: cos ^2 is_even_on A
a: A is symmetrical Subset of COMPLEX by XBOOLE_1:1, NUMBERS:11;
cos is_even_on A by Th55;
hence cos ^2 is_even_on A by an0, a; :: thesis: verum