set MGFC = MultGroup F_Complex ;
set cMGFC = the carrier of (MultGroup F_Complex );
set FC = F_Complex ;
let n be non empty Element of NAT ; :: thesis: for x being Element of (MultGroup F_Complex ) st x in n -roots_of_1 holds
not x is being_of_order_0
let x be Element of the carrier of (MultGroup F_Complex ); :: thesis: ( x in n -roots_of_1 implies not x is being_of_order_0 )
assume x in n -roots_of_1 ; :: thesis: not x is being_of_order_0
then consider c being Element of F_Complex such that
A1: c = x and
A2: c is CRoot of n, 1_ F_Complex ;
A3: 1_ (MultGroup F_Complex ) = 1_ F_Complex by Th20;
(power F_Complex ) . c,n = 1_ F_Complex by A2, COMPLFLD:def 2;
then x |^ n = 1_ (MultGroup F_Complex ) by A1, A3, Th32;
hence not x is being_of_order_0 by GROUP_1:def 11; :: thesis: verum