theorem Th14: :: AMI_8:14

for n being Nat
for i1, i2, i3 being Integer
for s being b₁ -started State-consisting of <%i1,i2,i3%> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 )