set s = the State-consisting of D;
set s1 = the State-consisting of D +* (Start-At (il,SCM));
for k being Element of NAT st k < len D holds
( the State-consisting of D +* (Start-At (il,SCM))) . (dl. k) = D . k

proof

let k be Element of NAT ; :: thesis: ( k < len D implies ( the State-consisting of D +* (Start-At (il,SCM))) . (dl. k) = D . k )
assume A1: k < len D ; :: thesis: ( the State-consisting of D +* (Start-At (il,SCM))) . (dl. k) = D . k
A2: dom (Start-At (il,SCM)) = {(IC )} by FUNCOP_1:13;
dl. k <> IC by AMI_3:13;
then not dl. k in dom (Start-At (il,SCM)) by A2, TARSKI:def 1;
hence ( the State-consisting of D +* (Start-At (il,SCM))) . (dl. k) = the State-consisting of D . (dl. k) by FUNCT_4:11
.= D . k by A1, Def1 ;
:: thesis: verum

end;

then reconsider s1 = the State-consisting of D +* (Start-At (il,SCM)) as State-consisting of D by Def1;
take s1 ; :: thesis: s1 is il -started
thus IC s1 = il by MEMSTR_0:16; :: according to MEMSTR_0:def 12 :: thesis: verum