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

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