theorem Th53: :: COMPTRIG:53

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