let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for F being NAT -defined non empty FinPartState of holds FirstLoc F in dom F
let S be non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N; :: thesis: for F being NAT -defined non empty FinPartState of holds FirstLoc F in dom F
let F be NAT -defined non empty FinPartState of ; :: thesis: FirstLoc F in dom F
consider M being non empty Subset of NAT such that
A1: M = { (locnum l,S) where l is Element of NAT : l in dom F } and
A2: FirstLoc F = il. S,(min M) by Def2;
min M in M by XXREAL_2:def 7;
then ex l being Element of NAT st
( min M = locnum l,S & l in dom F ) by A1;
hence FirstLoc F in dom F by A2, AMISTD_1:def 13; :: thesis: verum