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