for x being Real st x in dom cos & - x in dom cos holds
cos . (- x) = cos . x by SIN_COS:30;
then ( cos is with_symmetrical_domain & cos is quasi_even ) by SIN_COS:24;
hence cos is even ; :: thesis: verum