deffunc H₁( Instruction-Location of S) -> Element of NAT = locnum $1;
set M = { H₁(l) where l is Instruction-Location of S : l in dom F } ;
A1: dom F is finite ;
A2: { H₁(l) where l is Instruction-Location of S : l in dom F } is finite from AMI_1:sch 1(A1);
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 Instruction-Location of S by AMI_1:def 4;
A3: locnum l in { H₁(l) where l is Instruction-Location of S : l in dom F } ;
{ H₁(l) where l is Instruction-Location of S : 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 Instruction-Location of S : l in dom F } or k in NAT )
assume k in { H₁(l) where l is Instruction-Location of S : l in dom F } ; :: thesis: k in NAT
then ex l being Instruction-Location of S st
( k = locnum l & l in dom F ) ;
hence k in NAT ; :: thesis: verum

end;

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