let G be strict Group; :: thesis: for b being Element of G st b is being_of_order_0 holds

b " is being_of_order_0

let b be Element of G; :: thesis: ( b is being_of_order_0 implies b " is being_of_order_0 )

assume A1: b is being_of_order_0 ; :: thesis: b " is being_of_order_0

for n being Nat st (b ") |^ n = 1_ G holds

n = 0

b " is being_of_order_0

let b be Element of G; :: thesis: ( b is being_of_order_0 implies b " is being_of_order_0 )

assume A1: b is being_of_order_0 ; :: thesis: b " is being_of_order_0

for n being Nat st (b ") |^ n = 1_ G holds

n = 0

proof

hence
b " is being_of_order_0
by GROUP_1:def 10; :: thesis: verum
let n be Nat; :: thesis: ( (b ") |^ n = 1_ G implies n = 0 )

assume (b ") |^ n = 1_ G ; :: thesis: n = 0

then (b |^ n) " = 1_ G by GROUP_1:37;

then (b |^ n) " = (1_ G) " by GROUP_1:8;

then b |^ n = 1_ G by GROUP_1:9;

hence n = 0 by A1, GROUP_1:def 10; :: thesis: verum

end;assume (b ") |^ n = 1_ G ; :: thesis: n = 0

then (b |^ n) " = 1_ G by GROUP_1:37;

then (b |^ n) " = (1_ G) " by GROUP_1:8;

then b |^ n = 1_ G by GROUP_1:9;

hence n = 0 by A1, GROUP_1:def 10; :: thesis: verum