for x being Real st x in dom cos & - x in dom cos holds
cos . (- x) = cos . x by SIN_COS:33;
then ( cos is with_symmetrical_domain & cos is quasi_even ) by Def2, Def3, SIN_COS:27;
hence cos is even ; :: thesis: verum