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
proof
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;
hence b " is being_of_order_0 by GROUP_1:def 10; :: thesis: verum