let x be Element of REAL ; :: thesis: sinh_C /. x = sinh . x
A2: (exp_R . x) - (exp_R . (- x)) = (sinh . x) * 2

proof

(sinh . x) * 2 = 2 * (((exp_R . x) - (exp_R . (- x))) / 2) by SIN_COS2:def 1
.= ((exp_R . x) - (exp_R . (- x))) / (2 / 2) ;
hence (exp_R . x) - (exp_R . (- x)) = (sinh . x) * 2 ; :: thesis: verum

end;

x in REAL ;
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 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
.= ((sinh . x) * 2) / 2 by A2 ;
hence sinh_C /. x = sinh . x ; :: thesis: verum