let x, y be Real; :: thesis: sinh_C /. (x + (y * <i>)) = ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * <i>)
sinh_C /. (x + (y * <i>)) = sinh_C /. ((y + ((- x) * <i>)) * <i>)
.= <i> * (sin_C /. (y + ((- x) * <i>))) by Th17
.= <i> * (((sin . y) * (cosh . x)) + ((- ((cos . y) * (sinh . x))) * <i>)) by Th43
.= (- (- ((sinh . x) * (cos . y)))) + (((cosh . x) * (sin . y)) * <i>) ;
hence sinh_C /. (x + (y * <i>)) = ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * <i>) ; :: thesis: verum