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

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