:: deftheorem Def15 defines final_states_partition FSM_1:def 15 :
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for b₄ being a_partition of the carrier of tfsm holds
( b₄ = final_states_partition tfsm iff b₄ is final );