deffunc H_{1}( Element of G) -> Element of NAT = ord G;

GG: the carrier of G is finite ;

set A = { H_{1}(g) where g is Element of G : g in the carrier of G } ;

T1: { H_{1}(g) where g is Element of G : g in the carrier of G } = Ordset G
_{1}(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_{1}(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

GG: the carrier of G is finite ;

set A = { H

T1: { H

proof

P1:
{ H
Y1:
{ H_{1}(g) where g is Element of G : g in the carrier of G } c= Ordset G
_{1}(g) where g is Element of G : g in the carrier of G }
_{1}(g) where g is Element of G : g in the carrier of G } = Ordset G
by Y1, XBOOLE_0:def 10; :: thesis: verum

end;proof

Ordset G c= { H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H_{1}(g) where g is Element of G : g in the carrier of G } or x in Ordset G )

assume x in { H_{1}(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_{1}(g) & g in the carrier of G )
;

thus x in Ordset G by Y2; :: thesis: verum

end;assume x in { H

then consider g being Element of G such that

Y2: ( x = H

thus x in Ordset G by Y2; :: thesis: verum

proof

hence
{ H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ordset G or x in { H_{1}(g) where g is Element of G : g in the carrier of G } )

assume x in Ordset G ; :: thesis: x in { H_{1}(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_{1}(g)
;

thus x in { H_{1}(g) where g is Element of G : g in the carrier of G }
by Y2; :: thesis: verum

end;assume x in Ordset G ; :: thesis: x in { H

then consider g being Element of G such that

Y2: x = H

thus x in { H

ord (1_ G) in { H

hence ( Ordset G is finite & not Ordset G is empty ) by P1, T1; :: thesis: verum