theorem Th2: :: SCM_1:2

for i1, i2 being Integer
for il being Element of NAT
for s being b₃ -started State-consisting of <%i1,i2%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 )