let x be Real; :: thesis: cosh_C /. x = cosh . x
A1: (cosh . x) * 2 = 2 * (((exp_R . x) + (exp_R . (- x))) / 2) by SIN_COS2:def 3
.= ((exp_R . x) + (exp_R . (- x))) / (2 / 2) ;
x in REAL by XREAL_0:def 1;
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 Th19, SIN_COS:30
.= ((exp_R . x) + (exp ((- x) + (0 * <i>)))) / 2
.= ((exp_R . x) + (((exp_R . (- x)) * 1) + (((exp_R . (- x)) * 0) * <i>))) / 2 by Th19, SIN_COS:30
.= ((cosh . x) * 2) / 2 by A1 ;
hence cosh_C /. x = cosh . x ; :: thesis: verum