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

take s1 ; :: thesis: s1 is il -started

thus IC s1 = il by MEMSTR_0:16; :: according to MEMSTR_0:def 12 :: thesis: verum

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

then reconsider s1 = the State-consisting of D +* (Start-At (il,SCM)) as State-consisting of D by Def1;
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;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

take s1 ; :: thesis: s1 is il -started

thus IC s1 = il by MEMSTR_0:16; :: according to MEMSTR_0:def 12 :: thesis: verum