:: deftheorem Def2 defines CRoot COMPTRIG:def 2 :
for x being Complex
for n being non zero Nat
for b₃ being Complex holds
( b₃ is CRoot of n,x iff b₃ |^ n = x );