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