for I being non empty set
for s being Element of I
for S being non empty FSM over I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non zero Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )