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

- 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