let A be symmetrical Subset of REAL; :: thesis: cos " is_even_on A
A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence cos " is_even_on A by Th19, Th66; :: thesis: verum