let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for p being FinPartState of S
for l being Element of IL st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for p being FinPartState of S
for l being Element of IL st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N; :: thesis: for p being FinPartState of S
for l being Element of IL st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let p be FinPartState of S; :: thesis: for l being Element of IL st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let l be Element of IL; :: thesis: ( p starts_at l implies for s being State of S st p c= s holds
s starts_at l )
assume A1: ( IC S in dom p & IC p = l ) ; :: according to AMI_1:def 44 :: thesis: for s being State of S st p c= s holds
s starts_at l
let s be State of S; :: thesis: ( p c= s implies s starts_at l )
assume A2: p c= s ; :: thesis: s starts_at l
thus IC s = p . (IC S) by A1, A2, GRFUNC_1:8
.= l by A1, Def43 ; :: according to AMI_1:def 41 :: thesis: verum