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 )

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 10; :: thesis: verum

( 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
for n being Integer st b |^ n = 1_ G holds
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 Nat st b |^ (- m) = 1_ G holds

m = 0

n = 0

n = 0 ; :: thesis: verum

end;n = 0

A2: for m being Nat st b |^ (- m) = 1_ G holds

m = 0

proof

for n being Integer st b |^ n = 1_ G holds
let m be 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:36;

then A4: (b ") |^ m = 1_ G by A3, GROUP_1:37;

b " is being_of_order_0 by A1, Th12;

hence m = 0 by A4, GROUP_1:def 10; :: thesis: verum

end;assume A3: b |^ (- m) = 1_ G ; :: thesis: m = 0

b |^ (- m) = (b |^ m) " by GROUP_1:36;

then A4: (b ") |^ m = 1_ G by A3, GROUP_1:37;

b " is being_of_order_0 by A1, Th12;

hence m = 0 by A4, GROUP_1:def 10; :: thesis: verum

n = 0

proof

hence
for n being Integer st b |^ n = 1_ G holds
let n be Integer; :: thesis: ( b |^ n = 1_ G implies n = 0 )

assume A5: b |^ n = 1_ G ; :: thesis: n = 0

consider k being Nat such that

A6: ( n = k or n = - k ) by INT_1:2;

end;assume A5: b |^ n = 1_ G ; :: thesis: n = 0

consider k being Nat such that

A6: ( n = k or n = - k ) by INT_1:2;

n = 0 ; :: thesis: verum

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 10; :: thesis: verum