deffunc H₁( Instruction-Location of S) -> Element of NAT = locnum $1;
reconsider F = F as NAT -defined non empty FinPartState of S by A1, A2;
set M = { H₁(l) where l is Instruction-Location of S : l in dom F } ;
A3: dom F is finite ;
A4: { H₁(l) where l is Instruction-Location of S : l in dom F } is finite from AMI_1:sch 1(A3);
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;
A5: 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 A4, A5;
take il. S,(min M) ; :: thesis: ex M being non empty Subset of NAT st
( M = { (locnum l) where l is Instruction-Location of S : l in dom F } & il. S,(min M) = il. S,(min M) )
take M ; :: thesis: ( M = { (locnum l) where l is Instruction-Location of S : l in dom F } & il. S,(min M) = il. S,(min M) )
thus ( M = { (locnum l) where l is Instruction-Location of S : l in dom F } & il. S,(min M) = il. S,(min M) ) ; :: thesis: verum