deffunc H1( Element of G) -> Element of NAT = ord G;
GG: the carrier of G is finite ;
set A = { H1(g) where g is Element of G : g in the carrier of G } ;
T1: { H1(g) where g is Element of G : g in the carrier of G } = Ordset G
proof
Y1: { H1(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 { H1(g) where g is Element of G : g in the carrier of G } or x in Ordset G )
assume x in { H1(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 = H1(g) & g in the carrier of G ) ;
thus x in Ordset G by Y2; :: thesis: verum
end;
Ordset G c= { H1(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 { H1(g) where g is Element of G : g in the carrier of G } )
assume x in Ordset G ; :: thesis: x in { H1(g) where g is Element of G : g in the carrier of G }
then consider g being Element of G such that
Y2: x = H1(g) ;
thus x in { H1(g) where g is Element of G : g in the carrier of G } by Y2; :: thesis: verum
end;
hence { H1(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: { H1(g) where g is Element of G : g in the carrier of G } is finite from FRAENKEL:sch 21(GG);
 ord (1_ G) in { H1(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