let x, y be Real; :: thesis: cos_C /. (x + (y * <i>)) = ((cos . x) * (cosh . y)) + ((- ((sin . x) * (sinh . y))) * <i>)
cos_C /. (x + (y * <i>)) = ((cos_C /. x) * (cos_C /. (<i> * y))) - ((sin_C /. x) * (sin_C /. (<i> * y))) by Th6
.= ((cos_C /. x) * (cos_C /. (<i> * y))) - ((sin_C /. x) * ((sinh_C /. y) * <i>)) by Th15
.= ((cos_C /. x) * (cosh_C /. y)) - ((sin_C /. x) * ((sinh_C /. y) * <i>)) by Th16
.= ((cos_C /. x) * (cosh_C /. y)) - ((sin . x) * ((sinh_C /. y) * <i>)) by Th38
.= ((cos . x) * (cosh_C /. y)) - ((sin . x) * ((sinh_C /. y) * <i>)) by Th39
.= ((cos . x) * (cosh_C /. y)) - ((sin . x) * ((sinh . y) * <i>)) by Th40
.= ((cos . x) * (cosh . y)) - (((sin . x) * (sinh . y)) * <i>) by Th41
.= ((cos . x) * (cosh . y)) + ((- ((sin . x) * (sinh . y))) * <i>) ;
hence cos_C /. (x + (y * <i>)) = ((cos . x) * (cosh . y)) + ((- ((sin . x) * (sinh . y))) * <i>) ; :: thesis: verum