theorem :: SCM_1:13

for i1, i2, i3, i4 being Integer
for s being State of SCM st s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds
s is State-consisting of <%i1,i2,i3,i4%>