let n be Element of NAT ; :: thesis: exp ((- ((2 * PI ) * n)) * <i> ) = 1
thus exp ((- ((2 * PI ) * n)) * <i> ) = (cos (- ((2 * PI ) * n))) + ((sin (- ((2 * PI ) * n))) * <i> ) by SIN_COS:28
.= (cos ((2 * PI ) * n)) + ((sin (- ((2 * PI ) * n))) * <i> ) by SIN_COS:34
.= (cos (0 + ((2 * PI ) * n))) + ((- (sin ((2 * PI ) * n))) * <i> ) by SIN_COS:34
.= (cos . (0 + ((2 * PI ) * n))) + (- ((sin (0 + ((2 * PI ) * n))) * <i> )) by SIN_COS:def 23
.= (cos . (0 + ((2 * PI ) * n))) + (- ((sin . (0 + ((2 * PI ) * n))) * <i> )) by SIN_COS:def 21
.= (cos . (0 + ((2 * PI ) * n))) + (- ((sin . 0 ) * <i> )) by SIN_COS2:10
.= 1 by SIN_COS:33, SIN_COS2:11 ; :: thesis: verum