for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for q being State of tfsm holds Class ((0 -eq_states_EqR tfsm),q) = the carrier of tfsm