let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of IL,N
for s being State of S
for iloc being Instruction-Location of S holds IC (s +* (Start-At iloc)) = iloc
let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of IL,N
for s being State of S
for iloc being Instruction-Location of S holds IC (s +* (Start-At iloc)) = iloc
let S be non empty IC-Ins-separated AMI-Struct of IL,N; :: thesis: for s being State of S
for iloc being Instruction-Location of S holds IC (s +* (Start-At iloc)) = iloc
let s be State of S; :: thesis: for iloc being Instruction-Location of S holds IC (s +* (Start-At iloc)) = iloc
let iloc be Instruction-Location of S; :: thesis: IC (s +* (Start-At iloc)) = iloc
A1: ( dom (Start-At iloc) = {(IC S)} & IC S in {(IC S)} ) by FUNCOP_1:19, TARSKI:def 1;
then IC S in (dom s) \/ {(IC S)} by XBOOLE_0:def 3;
hence IC (s +* (Start-At iloc)) = (Start-At iloc) . (IC S) by A1, FUNCT_4:def 1
.= iloc by FUNCOP_1:87 ;
:: thesis: verum