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 & k = 0 ) ; :: thesis: contradiction
a = 1_ G by A2, GROUP_1:25;
hence contradiction by A1, GROUP_1:42; :: thesis: verum