theorem :: FUNCT_8:68

for A being symmetrical Subset of REAL holds cosh is_even_on A