let e be Element of F_Complex ; :: thesis: ( e is CRoot of n,x iff (power F_Complex ) . e,n = x )
thus ( e is CRoot of n,x implies (power F_Complex ) . e,n = x ) :: thesis: ( (power F_Complex ) . e,n = x implies e is CRoot of n,x )

proof

assume e is CRoot of n,x ; :: thesis: (power F_Complex ) . e,n = x
then e |^ n = x by COMPTRIG:def 2;
hence (power F_Complex ) . e,n = x by Th112; :: thesis: verum

end;

assume (power F_Complex ) . e,n = x ; :: thesis: e is CRoot of n,x
hence e |^ n = x by Th112; :: according to COMPTRIG:def 2 :: thesis: verum