let L be non empty non degenerated right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for n being Element of NAT holds not 0. L is_primitive_root_of_degree n
let n be Element of NAT ; :: thesis: not 0. L is_primitive_root_of_degree n
defpred S₁[ Nat] means (0. L) |^ $1 = 0. L;
A1: for j being Nat st 1 <= j & S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( 1 <= j & S₁[j] implies S₁[j + 1] )
assume 1 <= j ; :: thesis: ( not S₁[j] or S₁[j + 1] )
assume S₁[j] ; :: thesis: S₁[j + 1]
(0. L) |^ (j + 1) = ((0. L) |^ j) * (0. L) by GROUP_1:def 7
.= 0. L ;
hence S₁[j + 1] ; :: thesis: verum

end;

A2: S₁[1] by BINOM:8;
A3: for m being Nat st 1 <= m holds
S₁[m] from NAT_1:sch 8(A2, A1);
assume A4: 0. L is_primitive_root_of_degree n ; :: thesis: contradiction
then n <> 0 ;
then 0 + 1 < n + 1 by XREAL_1:8;
then 1 <= n by NAT_1:13;
then (0. L) |^ n <> 1. L by A3;
hence contradiction by A4; :: thesis: verum