let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b₁ -valued non empty finite Function holds LastLoc F in dom F
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for F being NAT -defined the InstructionsF of T -valued non empty finite Function holds LastLoc F in dom F
let F be NAT -defined the InstructionsF of T -valued non empty finite Function; :: thesis: LastLoc F in dom F
consider M being non empty finite natural-membered set such that
A1: M = { (locnum (l,T)) where l is Element of NAT : l in dom F } and
A2: LastLoc F = il. (T,(max M)) by Def11;
max M in M by XXREAL_2:def 8;
then ex l being Element of NAT st
( max M = locnum (l,T) & l in dom F ) by A1;
hence LastLoc F in dom F by A2, Def5; :: thesis: verum