for n being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph st n + 1 = card the carrier of tfsm holds
final_states_partition tfsm = n -eq_states_partition tfsm