let x, y be Element of REAL ; (((1 + ((- 1) * <i>)) / 2) * (sinh_C /. (x + (y * <i>)))) + (((1 + <i>) / 2) * (sinh_C /. (x + ((- y) * <i>)))) = ((sinh . x) * (cos . y)) + ((cosh . x) * (sin . y))
set shx = sinh . x;
set cy = cos . y;
set chx = cosh . x;
set sy = sin . y;
(((1 + ((- 1) * <i>)) / 2) * (sinh_C /. (x + (y * <i>)))) + (((1 + <i>) / 2) * (sinh_C /. (x + ((- y) * <i>)))) =
(((1 + ((- 1) * <i>)) / 2) * (((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * <i>))) + (((1 + <i>) / 2) * (sinh_C /. (x + ((- y) * <i>))))
by Th46
.=
(((1 + ((- 1) * <i>)) / 2) * (((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * <i>))) + (((1 + <i>) / 2) * (((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * <i>)))
by Th47
.=
(2 * ((((sinh . x) * (cos . y)) + ((cosh . x) * (sin . y))) + (0 * <i>))) / 2
;
hence
(((1 + ((- 1) * <i>)) / 2) * (sinh_C /. (x + (y * <i>)))) + (((1 + <i>) / 2) * (sinh_C /. (x + ((- y) * <i>)))) = ((sinh . x) * (cos . y)) + ((cosh . x) * (sin . y))
; verum