:: deftheorem Def1 defines State-consisting SCM_1:def 1 :
for D being XFinSequence of INT
for b₂ being State of SCM holds
( b₂ is State-consisting of D iff for k being Element of NAT st k < len D holds
b₂ . (dl. k) = D . k );