for x being Complex st x in REAL holds
- x in REAL by XREAL_0:def 1;
then A1: REAL is symmetrical ;
( ( for x being Real st x in dom cosh & - x in dom cosh holds
cosh . (- x) = cosh . x ) & dom cosh = REAL ) by FUNCT_2:def 1, SIN_COS2:19;
then ( cosh is with_symmetrical_domain & cosh is quasi_even ) by A1;
hence cosh is even ; :: thesis: verum