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 Th74; :: thesis: verum
end;
assume (power F_Complex) . (e,n) = x ; :: thesis: e is CRoot of n,x
hence e |^ n = x by Th74; :: according to COMPTRIG:def 2 :: thesis: verum