let x, y be Element of 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