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 l1 being Element of NAT
for F being NAT -defined non empty FinPartState of st l1 in dom F holds
FirstLoc F <= l1,S
let S be non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N; :: thesis: for l1 being Element of NAT
for F being NAT -defined non empty FinPartState of st l1 in dom F holds
FirstLoc F <= l1,S
let l1 be Element of NAT ; :: thesis: for F being NAT -defined non empty FinPartState of st l1 in dom F holds
FirstLoc F <= l1,S
let F be NAT -defined non empty FinPartState of ; :: thesis: ( l1 in dom F implies FirstLoc F <= l1,S )
assume A1: l1 in dom F ; :: thesis: FirstLoc F <= l1,S
consider M being non empty Subset of NAT such that
A2: M = { (locnum w,S) where w is Element of NAT : w in dom F } and
A3: FirstLoc F = il. S,(min M) by Def2;
locnum l1,S in M by A1, A2;
then A4: min M <= locnum l1,S by XXREAL_2:def 7;
locnum (FirstLoc F),S = min M by A3, AMISTD_1:def 13;
hence FirstLoc F <= l1,S by A4, AMISTD_1:29; :: thesis: verum