theorem Th31: :: POLYEQ_3:31

for x being Real
for n being Nat holds ((cos x) + ((sin x) * <i>)) |^ n = (cos (n * x)) + ((sin (n * x)) * <i>)