let G be Group; :: thesis: for a being Element of G
for n being Nat st (a ") |^ n = 1_ G holds
a |^ n = 1_ G
let a be Element of G; :: thesis: for n being Nat st (a ") |^ n = 1_ G holds
a |^ n = 1_ G
let n be Nat; :: thesis: ( (a ") |^ n = 1_ G implies a |^ n = 1_ G )
(a ") " = a ;
hence ( (a ") |^ n = 1_ G implies a |^ n = 1_ G ) by Th3; :: thesis: verum