the carrier of (the_reduction_of tfsm) = final_states_partition tfsm by Def18;
hence ( not the_reduction_of tfsm is empty & the_reduction_of tfsm is finite ) ; :: thesis: verum