let A be symmetrical Subset of REAL; :: thesis: sin ^2 is_even_on A
( A is symmetrical Subset of COMPLEX & sin is_odd_on A ) by Th65, NUMBERS:11, XBOOLE_1:1;
hence sin ^2 is_even_on A by Th22; :: thesis: verum