let n be Element of NAT ; exp ((- ((2 * PI) * n)) * <i>) = 1
thus exp ((- ((2 * PI) * n)) * <i>) =
(cos (- ((2 * PI) * n))) + ((sin (- ((2 * PI) * n))) * <i>)
by SIN_COS:25
.=
(cos ((2 * PI) * n)) + ((sin (- ((2 * PI) * n))) * <i>)
by SIN_COS:31
.=
(cos (0 + ((2 * PI) * n))) + ((- (sin ((2 * PI) * n))) * <i>)
by SIN_COS:31
.=
(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
; verum