for I, O being non empty set
for s being Element of I
for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M 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
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) )