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 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 Nat st y = a |^ n

proof

let y be set ; :: thesis: ( y in rng F implies ex n being Nat st y = a |^ n )
assume y in rng F ; :: thesis: ex n being Nat st y = a |^ n
then consider x being object such that
A5: x in dom F and
A6: F . x = y by FUNCT_1:def 3;
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;

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

proof

let y be object ; :: 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 Nat st y = a |^ n by A4;
hence y in the carrier of G ; :: thesis: verum

end;

then rng F c= the carrier of G ;
then reconsider F9 = F as Function of (Seg ((card G) + 1)), the carrier of G by A3, FUNCT_2:def 1, RELSET_1:4;
A7: card G < (card G) + 1 by XREAL_1:29;
( card (Segm (card G)) = card the carrier of G & card (Seg ((card G) + 1)) = card (Segm ((card G) + 1)) ) by FINSEQ_1:55;
then card the carrier of G in card (Seg ((card G) + 1)) by A7, NAT_1:41;
then consider x, y being object such that
A8: x in Seg ((card G) + 1) and
A9: y in Seg ((card G) + 1) and
A10: x <> y and
A11: F9 . x = F9 . y by FINSEQ_4:65;
reconsider p = x, n = y as Element of NAT by A8, A9;

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

suppose A12: n > p ; :: thesis: ex n being Nat st
( n <> 0 & a |^ n = 1_ G )

then reconsider t = n - p as Element of NAT by INT_1:5;
take t ; :: thesis: ( t <> 0 & a |^ t = 1_ G )
F9 . p = a |^ p by A2, A3, A8;
then a |^ n = a |^ p by A2, A3, A9, A11;
then a |^ (n + (- p)) = (a |^ p) * (a |^ (- p)) by GROUP_1:33;
then a |^ t = a |^ (p + (- p)) by GROUP_1:33;
hence ( t <> 0 & a |^ t = 1_ G ) by A12, GROUP_1:25; :: thesis: verum

end;

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

then reconsider t = p - n as Element of NAT by INT_1:5;
take t ; :: thesis: ( t <> 0 & a |^ t = 1_ G )
F9 . p = a |^ p by A2, A3, A8;
then a |^ n = a |^ p by A2, A3, A9, A11;
then a |^ (p + (- n)) = (a |^ n) * (a |^ (- n)) by GROUP_1:33;
then a |^ t = a |^ (n + (- n)) by GROUP_1:33;
hence ( t <> 0 & a |^ t = 1_ G ) by A13, GROUP_1:25; :: thesis: verum

end;

end;

end;

hence not a is being_of_order_0 ; :: thesis: verum