theorem Th32: :: FSM_1:32

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds
( k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm or card (k -eq_states_partition tfsm) < card ((k + 1) -eq_states_partition tfsm) )