for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph st (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm holds
for i being Nat st i <= k holds
(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm