let G be strict Group; :: thesis: for b being Element of G holds
( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds
n = 0 )
let b be Element of G; :: thesis: ( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds
n = 0 )
thus ( b is being_of_order_0 implies for n being Integer st b |^ n = 1_ G holds
n = 0 ) :: thesis: ( ( for n being Integer st b |^ n = 1_ G holds
n = 0 ) implies b is being_of_order_0 )

proof

assume A1: b is being_of_order_0 ; :: thesis: for n being Integer st b |^ n = 1_ G holds
n = 0
A2: for m being Element of NAT st b |^ (- m) = 1_ G holds
m = 0

proof

let m be Element of NAT ; :: thesis: ( b |^ (- m) = 1_ G implies m = 0 )
assume A3: b |^ (- m) = 1_ G ; :: thesis: m = 0
b |^ (- m) = (b |^ m) " by GROUP_1:70;
then A4: (b " ) |^ m = 1_ G by A3, GROUP_1:72;
b " is being_of_order_0 by A1, Th12;
hence m = 0 by A4, GROUP_1:def 11; :: thesis: verum

end;

for n being Integer st b |^ n = 1_ G holds
n = 0

proof

let n be Integer; :: thesis: ( b |^ n = 1_ G implies n = 0 )
assume A5: b |^ n = 1_ G ; :: thesis: n = 0
consider k being Element of NAT such that
A6: ( n = k or n = - k ) by INT_1:8;

per cases ( n = k or n = - k ) by A6;

suppose n = k ; :: thesis: n = 0

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

end;

suppose A7: n = - k ; :: thesis: n = 0

then k = 0 by A2, A5;
hence n = 0 by A7; :: thesis: verum

end;

end;

end;

hence for n being Integer st b |^ n = 1_ G holds
n = 0 ; :: thesis: verum

end;

assume for n being Integer st b |^ n = 1_ G holds
n = 0 ; :: thesis: b is being_of_order_0
then for n being Nat st b |^ n = 1_ G holds
n = 0 ;
hence b is being_of_order_0 by GROUP_1:def 11; :: thesis: verum