let G be finite Group; :: thesis: for a being Element of G holds not a is being_of_order_0
let a be Element of G; :: thesis: not a is being_of_order_0
ex n being Element of NAT st
( n <> 0 & a |^ n = 1_ G )

proof

deffunc H₁( Nat) -> Element of the carrier of G = a |^ $1;
consider F being FinSequence such that
A1: len F = (card G) + 1 and
A2: for p being Nat st p in dom F holds
F . p = H₁(p) from FINSEQ_1:sch 2();
A3: dom F = Seg ((card G) + 1) by A1, FINSEQ_1:def 3;
A4: for y being set st y in rng F holds
ex n being Element of NAT st y = a |^ n

proof

let y be set ; :: thesis: ( y in rng F implies ex n being Element of NAT st y = a |^ n )
assume y in rng F ; :: thesis: ex n being Element of NAT st y = a |^ n
then consider x being set such that
A5: x in dom F and
A6: F . x = y by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A5;
take n ; :: thesis: y = a |^ n
thus y = a |^ n by A2, A5, A6; :: thesis: verum

end;

rng F c= the carrier of G

proof

for x being set st x in rng F holds
x in the carrier of G

proof

let y be set ; :: thesis: ( y in rng F implies y in the carrier of G )
assume y in rng F ; :: thesis: y in the carrier of G
then ex n being Element of NAT st y = a |^ n by A4;
hence y in the carrier of G ; :: thesis: verum

end;

hence rng F c= the carrier of G by TARSKI:def 3; :: thesis: verum

end;

then reconsider F' = F as Function of (Seg ((card G) + 1)),the carrier of G by A3, FUNCT_2:def 1, RELSET_1:11;
A7: card (card G) = card the carrier of G ;
A8: card (Seg ((card G) + 1)) = card ((card G) + 1) by FINSEQ_1:76;
card G < (card G) + 1 by XREAL_1:31;
then card the carrier of G in card (Seg ((card G) + 1)) by A7, A8, NAT_1:42;
then consider x, y being set such that
A9: x in Seg ((card G) + 1) and
A10: y in Seg ((card G) + 1) and
A11: x <> y and
A12: F' . x = F' . y by FINSEQ_4:80;
reconsider p = x, n = y as Element of NAT by A9, A10;

per cases ( n > p or p > n ) by A11, XXREAL_0:1;

suppose A13: n > p ; :: thesis: ex n being Element of NAT st
( n <> 0 & a |^ n = 1_ G )

then reconsider t = n - p as Element of NAT by INT_1:18;
take t ; :: thesis: ( t <> 0 & a |^ t = 1_ G )
F' . p = a |^ p by A2, A3, A9;
then a |^ n = a |^ p by A2, A3, A10, A12;
then a |^ (n + (- p)) = (a |^ p) * (a |^ (- p)) by GROUP_1:63;
then a |^ t = a |^ (p + (- p)) by GROUP_1:63;
hence ( t <> 0 & a |^ t = 1_ G ) by A13, GROUP_1:43; :: thesis: verum

end;

suppose A14: p > n ; :: thesis: ex n being Element of NAT st
( n <> 0 & a |^ n = 1_ G )

then reconsider t = p - n as Element of NAT by INT_1:18;
take t ; :: thesis: ( t <> 0 & a |^ t = 1_ G )
F' . p = a |^ p by A2, A3, A9;
then a |^ n = a |^ p by A2, A3, A10, A12;
then a |^ (p + (- n)) = (a |^ n) * (a |^ (- n)) by GROUP_1:63;
then a |^ t = a |^ (n + (- n)) by GROUP_1:63;
hence ( t <> 0 & a |^ t = 1_ G ) by A14, GROUP_1:43; :: thesis: verum

end;

end;

end;

hence not a is being_of_order_0 by GROUP_1:def 11; :: thesis: verum