let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of IL,N
for l being Instruction-Location of S holds dom (Start-At l) misses IL
let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated realistic AMI-Struct of IL,N
for l being Instruction-Location of S holds dom (Start-At l) misses IL
let S be non empty IC-Ins-separated realistic AMI-Struct of IL,N; :: thesis: for l being Instruction-Location of S holds dom (Start-At l) misses IL
let l be Instruction-Location of S; :: thesis: dom (Start-At l) misses IL
( dom (Start-At l) = {(IC S)} & not IC S in IL ) by Def21, FUNCOP_1:19;
hence dom (Start-At l) misses IL by ZFMISC_1:56; :: thesis: verum