set FC = F_Complex ;
set cMGFC = the carrier of (MultGroup F_Complex );
set MGFC = MultGroup 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 A1: x in n -roots_of_1 ; :: thesis: not x is being_of_order_0
consider c being Element of F_Complex such that
A2: c = x and
A3: c is CRoot of n, 1_ F_Complex by A1;
A4: 1_ (MultGroup F_Complex ) = 1_ F_Complex by Th20;
(power F_Complex ) . c,n = 1_ F_Complex by A3, COMPLFLD:def 2;
then x |^ n = 1_ (MultGroup F_Complex ) by A2, A4, Th32;
hence not x is being_of_order_0 by GROUP_1:def 11; :: thesis: verum