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