:: deftheorem Def2 defines CRoot COMPLFLD:def 2 :
for x being Element of F_Complex
for n being non zero Element of NAT
for b₃ being Element of F_Complex holds
( b₃ is CRoot of n,x iff (power F_Complex) . (b₃,n) = x );