:: deftheorem defines -eq_states_partition FSM_1:def 13 :
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for i being Nat holds i -eq_states_partition tfsm = Class (i -eq_states_EqR tfsm);