for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph st k -eq_states_partition tfsm is final holds
(k + 1) -eq_states_EqR tfsm = k -eq_states_EqR tfsm