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