let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for m being Element of NAT
for x being Element of L st x is_primitive_root_of_degree m holds
x " is_primitive_root_of_degree m
let m be Element of NAT ; :: thesis: for x being Element of L st x is_primitive_root_of_degree m holds
x " is_primitive_root_of_degree m
let x be Element of L; :: thesis: ( x is_primitive_root_of_degree m implies x " is_primitive_root_of_degree m )
assume A1: x is_primitive_root_of_degree m ; :: thesis: x " is_primitive_root_of_degree m
then A2: m <> 0 by Def6;
A3: x <> 0. L by A1, Th30;
x |^ m = 1. L by A1, Def6;
then A4: (x " ) |^ m = 1. L by A3, Lm10;
for i being Element of NAT st 0 < i & i < m holds
(x " ) |^ i <> 1. L

proof

let i be Element of NAT ; :: thesis: ( 0 < i & i < m implies (x " ) |^ i <> 1. L )
assume ( 0 < i & i < m ) ; :: thesis: (x " ) |^ i <> 1. L
then x |^ i <> 1. L by A1, Def6;
hence (x " ) |^ i <> 1. L by A3, Lm11; :: thesis: verum

end;

hence x " is_primitive_root_of_degree m by A2, A4, Def6; :: thesis: verum