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:28
.= (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