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

proof

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

end;

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