let x be Real; :: thesis: sinh_C /. x = sinh . x
A1: (sinh . x) * 2 = 2 * (((exp_R . x) - (exp_R . (- x))) / 2) by SIN_COS2:def 1
.= ((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;
sinh_C /. x = sinh_C /. z
.= ((exp (x + (0 * <i>))) - (exp (- z))) / 2 by Def3
.= ((((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
.= ((sinh . x) * 2) / 2 by A1 ;
hence sinh_C /. x = sinh . x ; :: thesis: verum