let n be Element of NAT ; :: thesis: exp (((2 * PI) * n) * <i>) = 1
thus exp (((2 * PI) * n) * <i>) = (cos (0 + ((2 * PI) * n))) + ((sin (0 + ((2 * PI) * n))) * <i>) by SIN_COS:25
.= (cos . (0 + ((2 * PI) * n))) + ((sin (0 + ((2 * PI) * n))) * <i>) by SIN_COS:def 19
.= (cos . (0 + ((2 * PI) * n))) + ((sin . (0 + ((2 * PI) * n))) * <i>) by SIN_COS:def 17
.= (cos . (0 + ((2 * PI) * n))) + ((sin . 0) * <i>) by SIN_COS2:10
.= 1 by SIN_COS:30, SIN_COS2:11 ; :: thesis: verum