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 = (k + 1) -eq_states_partition tfsm holds
for m being Nat holds (k + m) -eq_states_partition tfsm = k -eq_states_partition tfsm by Th29;