deffunc H1( Element of NAT ) -> Element of NAT = locnum ($1,S);
set M = { H1(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 { H1(l) where l is Element of NAT : l in dom F } ;
A2: { H1(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 { H1(l) where l is Element of NAT : l in dom F } or k in NAT )
assume k in { H1(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 ;
{ H1(l) where l is Element of NAT : l in dom F } is finite from FRAENKEL:sch 21(A3);
 then reconsider M = { H1(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