let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined non empty FinPartState of T holds LastLoc F in dom F
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being NAT -defined non empty FinPartState of T holds LastLoc F in dom F
let F be NAT -defined non empty FinPartState of T; :: thesis: LastLoc F in dom F
consider M being non empty finite natural-membered set such that
A1: M = { (locnum l) where l is Instruction-Location of T : l in dom F } and
A2: LastLoc F = il. T,(max M) by Def21;
max M in M by XXREAL_2:def 8;
then ex l being Instruction-Location of T st
( max M = locnum l & l in dom F ) by A1;
hence LastLoc F in dom F by A2, Def13; :: thesis: verum