:: deftheorem Def16 defines -succ_class FSM_1:def 16 :
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for qf being Element of final_states_partition tfsm
for s being Element of IAlph
for b₆ being Element of final_states_partition tfsm holds
( b₆ = (s,qf) -succ_class iff ex q being State of tfsm ex n being Nat st
( q in qf & n + 1 = card the carrier of tfsm & b₆ = Class ((n -eq_states_EqR tfsm),( the Tran of tfsm . [q,s])) ) );