deffunc H₁( Element of NAT ) -> Element of NAT = locnum $1,S;
set M = { H₁(l) where l is Element of NAT : l in dom F } ;
consider l being Element of dom F;
( l in dom F & dom F c= NAT ) by RELAT_1:def 18;
then reconsider l = l as Element of NAT ;
A1: locnum l,S in { H₁(l) where l is Element of NAT : l in dom F } ;
A2: { H₁(l) where l is Element of NAT : l in dom F } c= NAT

proof

let k be set ; :: according to TARSKI:def 3 :: thesis: ( not k in { H₁(l) where l is Element of NAT : l in dom F } or k in NAT )
assume k in { H₁(l) where l is Element of NAT : l in dom F } ; :: thesis: k in NAT
then ex l being Element of NAT st
( k = locnum l,S & l in dom F ) ;
hence k in NAT ; :: thesis: verum

end;

A3: dom F is finite ;
{ H₁(l) where l is Element of NAT : l in dom F } is finite from FRAENKEL:sch 21(A3);
then reconsider M = { H₁(l) where l is Element of NAT : l in dom F } as non empty finite Subset of NAT by A1, A2;
take il. S,(max M) ; :: thesis: ex M being non empty finite natural-membered set st
( M = { (locnum l,S) where l is Element of NAT : l in dom F } & il. S,(max M) = il. S,(max M) )
take M ; :: thesis: ( M = { (locnum l,S) where l is Element of NAT : l in dom F } & il. S,(max M) = il. S,(max M) )
thus ( M = { (locnum l,S) where l is Element of NAT : l in dom F } & il. S,(max M) = il. S,(max M) ) ; :: thesis: verum