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 } ;
set l = the Element of dom F;
reconsider l = the Element of dom F 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 object ; :: 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