let x be Element of REAL ; :: thesis: cosh_C /. x = cosh . x
A1: (exp_R . x) + (exp_R . (- x)) = (cosh . x) * 2

proof

(cosh . x) * 2 = 2 * (((exp_R . x) + (exp_R . (- x))) / 2) by SIN_COS2:def 3
.= ((exp_R . x) + (exp_R . (- x))) / (2 / 2) ;
hence (exp_R . x) + (exp_R . (- x)) = (cosh . x) * 2 ; :: thesis: verum

end;

x in REAL ;
then reconsider z = x as Element of COMPLEX by NUMBERS:11;
cosh_C /. x = cosh_C /. z
.= ((exp (x + (0 * <i> ))) + (exp (- z))) / 2 by Def4
.= ((((exp_R . x) * 1) + (((exp_R . x) * 0 ) * <i> )) + (exp (- z))) / 2 by SIN_COS:33, Th19
.= ((exp_R . x) + (exp ((- x) + (0 * <i> )))) / 2
.= ((exp_R . x) + (((exp_R . (- x)) * 1) + (((exp_R . (- x)) * 0 ) * <i> ))) / 2 by SIN_COS:33, Th19
.= ((cosh . x) * 2) / 2 by A1 ;
hence cosh_C /. x = cosh . x ; :: thesis: verum