let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis:
let m be Element of NAT ; :: thesis:
let x be Element of L; :: thesis:
assume A1: x is_primitive_root_of_degree m ; :: thesis:
then A2: x <> 0. L by Th30;
let i, j be Nat; :: thesis:
assume that
A3: 1 <= i and
A4: i <= m and
A5: 1 <= j and
A6: j <= m and
A7: i <> j ; :: thesis:

suppose A8: i > j ; :: thesis:

then reconsider k = i - j as Element of NAT by INT_1:18;
k <= i - 1 by A5, XREAL_1:15;
then k + 1 <= (i - 1) + 1 by XREAL_1:8;
then k < i by NAT_1:13;
then A9: k < m by A4, XXREAL_0:2;
i - j > j - j by A8, XREAL_1:16;
then x |^ k <> 1. L by A1, A9, Def6;
hence pow x,(i - j) <> 1. L by Def3; :: thesis:

end;

suppose i <= j ; :: thesis:

then A10: i < j by A7, XXREAL_0:1;
then A11: j - i > i - i by XREAL_1:16;
A12: i - j < j - j by A10, XREAL_1:16;
then A13: abs (i - j) = - (i - j) by ABSVALUE:def 1;
then reconsider k = - (i - j) as Element of NAT ;
j - i <= j - 1 by A3, XREAL_1:15;
then k + 1 <= (j - 1) + 1 by XREAL_1:8;
then k < j by NAT_1:13;
then A14: k < m by A6, XXREAL_0:2;
A15: x |^ k <> 0. L by A2, Th1;

assume (x |^ k) " = 1. L ; :: thesis:
then 1. L = (x |^ k) * (1. L) by A15, VECTSP_1:def 22
.= x |^ k by VECTSP_1:def 13 ;
hence contradiction by A1, A11, A14, Def6; :: thesis:

end;

hence pow x,(i - j) <> 1. L by A12, A13, Def3; :: thesis:

end;

end;