let n be non zero Nat; :: thesis: for g1 being Element of (INT.Group n)
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for j being Nat holds (x |^ j) " = x |^ (n - j)
let g1 be Element of (INT.Group n); :: thesis: for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for j being Nat holds (x |^ j) " = x |^ (n - j)
let x be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> implies for j being Nat holds (x |^ j) " = x |^ (n - j) )
assume A1: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: for j being Nat holds (x |^ j) " = x |^ (n - j)
let j be Nat; :: thesis: (x |^ j) " = x |^ (n - j)
A2: (g1 |^ j) " = g1 |^ (n - j)

proof

(g1 |^ (n - j)) * (g1 |^ j) = g1 |^ ((n - j) + j) by GROUP_1:33
.= g1 |^ (card (INT.Group n))
.= 1_ (INT.Group n) by GR_CY_1:9 ;
hence g1 |^ (n - j) = (g1 |^ j) " by GROUP_1:5; :: thesis: verum

end;

x |^ j = <*(g1 |^ j),(1_ (INT.Group 2))*> by A1, Th25;
hence (x |^ j) " = <*(g1 |^ (n - j)),(1_ (INT.Group 2))*> by A2, Th24
.= x |^ (n - j) by A1, Th25 ;
:: thesis: verum