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 )
assume a |^ n = 1_ G ; :: thesis: (a ") |^ n = 1_ G
then (a ") |^ n = (1_ G) " by GROUP_1:37
.= 1_ G by GROUP_1:8 ;
hence (a ") |^ n = 1_ G ; :: thesis: verum