let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for l being Instruction-Location of S holds IC (Start-At l) = l
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for l being Instruction-Location of S holds IC (Start-At l) = l
let l be Instruction-Location of S; :: thesis: IC (Start-At l) = l
IC S in dom (Start-At l) by Th17;
hence IC (Start-At l) = (Start-At l) . (IC S) by AMI_1:def 43
.= l by FUNCOP_1:87 ;
:: thesis: verum