let x, y be Element of 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 Th44
.= (- (- ((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