let n, k be Element of NAT ; :: thesis: for x being Real st n <> 0 holds
((cos ((x + ((2 * PI ) * k)) / n)) + ((sin ((x + ((2 * PI ) * k)) / n)) * <i> )) |^ n = (cos x) + ((sin x) * <i> )
let x be Real; :: thesis: ( n <> 0 implies ((cos ((x + ((2 * PI ) * k)) / n)) + ((sin ((x + ((2 * PI ) * k)) / n)) * <i> )) |^ n = (cos x) + ((sin x) * <i> ) )
assume A1: n <> 0 ; :: thesis: ((cos ((x + ((2 * PI ) * k)) / n)) + ((sin ((x + ((2 * PI ) * k)) / n)) * <i> )) |^ n = (cos x) + ((sin x) * <i> )
thus ((cos ((x + ((2 * PI ) * k)) / n)) + ((sin ((x + ((2 * PI ) * k)) / n)) * <i> )) |^ n = (cos (n * ((x + ((2 * PI ) * k)) / n))) + ((sin (n * ((x + ((2 * PI ) * k)) / n))) * <i> ) by Th53
.= (cos (x + ((2 * PI ) * k))) + ((sin (n * ((x + ((2 * PI ) * k)) / n))) * <i> ) by A1, XCMPLX_1:88
.= (cos (x + ((2 * PI ) * k))) + ((sin (x + ((2 * PI ) * k))) * <i> ) by A1, XCMPLX_1:88
.= (cos . (x + ((2 * PI ) * k))) + ((sin (x + ((2 * PI ) * k))) * <i> ) by SIN_COS:def 23
.= (cos . (x + ((2 * PI ) * k))) + ((sin . (x + ((2 * PI ) * k))) * <i> ) by SIN_COS:def 21
.= (cos . (x + ((2 * PI ) * k))) + ((sin . x) * <i> ) by SIN_COS2:10
.= (cos . x) + ((sin . x) * <i> ) by SIN_COS2:11
.= (cos . x) + ((sin x) * <i> ) by SIN_COS:def 21
.= (cos x) + ((sin x) * <i> ) by SIN_COS:def 23 ; :: thesis: verum