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 lower FinPartState of holds FirstLoc F = il. S,0
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 lower FinPartState of holds FirstLoc F = il. S,0
let F be NAT -defined non empty lower FinPartState of ; :: thesis: FirstLoc F = il. S,0
consider M being non empty Subset of NAT such that
M = { (locnum l,S) where l is Element of NAT : l in dom F } and
A1: FirstLoc F = il. S,(min M) by Def2;
A2: il. S,0 <= il. S,(min M),S by AMISTD_1:28;
FirstLoc F in dom F by Th21;
then il. S,0 in dom F by A1, A2, AMISTD_1:def 20;
then FirstLoc F <= il. S,0 ,S by Th23;
hence FirstLoc F = il. S,0 by A1, A2, AMISTD_1:def 9; :: thesis: verum