theorem Th8: :: UNIROOTS:8

for n being Element of NAT holds 1_ F_Complex = (power F_Complex) . ((1_ F_Complex),n)