deffunc H₁( Element of G) -> Element of NAT = ord G;
GG: the carrier of G is finite ;
set A = { H₁(g) where g is Element of G : g in the carrier of G } ;
T1: { H₁(g) where g is Element of G : g in the carrier of G } = Ordset G

proof

Y1: { H₁(g) where g is Element of G : g in the carrier of G } c= Ordset G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(g) where g is Element of G : g in the carrier of G } or x in Ordset G )
assume x in { H₁(g) where g is Element of G : g in the carrier of G } ; :: thesis: x in Ordset G
then consider g being Element of G such that
Y2: ( x = H₁(g) & g in the carrier of G ) ;
thus x in Ordset G by Y2; :: thesis: verum

end;

Ordset G c= { H₁(g) where g is Element of G : g in the carrier of G }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ordset G or x in { H₁(g) where g is Element of G : g in the carrier of G } )
assume x in Ordset G ; :: thesis: x in { H₁(g) where g is Element of G : g in the carrier of G }
then consider g being Element of G such that
Y2: x = H₁(g) ;
thus x in { H₁(g) where g is Element of G : g in the carrier of G } by Y2; :: thesis: verum

end;

hence { H₁(g) where g is Element of G : g in the carrier of G } = Ordset G by Y1, XBOOLE_0:def 10; :: thesis: verum

end;

P1: { H₁(g) where g is Element of G : g in the carrier of G } is finite from FRAENKEL:sch 21(GG);
ord (1_ G) in { H₁(g) where g is Element of G : g in the carrier of G } ;
hence ( Ordset G is finite & not Ordset G is empty ) by P1, T1; :: thesis: verum