let x, y be Element of REAL ; :: thesis: exp (x + (y * <i> )) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * <i> )
exp (x + (y * <i> )) = (exp_R x) * ((cos y) + ((sin y) * <i> )) by Lm4
.= (((exp_R x) * (cos y)) - (0 * (sin y))) + ((((exp_R x) * (sin y)) + ((cos y) * 0 )) * <i> )
.= ((exp_R x) * (cos . y)) + (((exp_R x) * (sin y)) * <i> ) by SIN_COS:def 23
.= ((exp_R . x) * (cos . y)) + (((exp_R x) * (sin y)) * <i> ) by SIN_COS:def 27
.= ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin y)) * <i> ) by SIN_COS:def 27 ;
hence exp (x + (y * <i> )) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * <i> ) by SIN_COS:def 21; :: thesis: verum