let G be Group; :: thesis: for a, b being Element of G
for k being Element of NAT st ord a > 1 & a = b |^ k holds
k <> 0
let a, b be Element of G; :: thesis: for k being Element of NAT st ord a > 1 & a = b |^ k holds
k <> 0
let k be Element of NAT ; :: thesis: ( ord a > 1 & a = b |^ k implies k <> 0 )
assume that
A1: ord a > 1 and
A2: a = b |^ k and
A3: k = 0 ; :: thesis: contradiction
a = 1_ G by A2, A3, GROUP_1:43;
hence contradiction by A1, GROUP_1:84; :: thesis: verum