reconsider n = card the carrier of tfsm as Nat ;
consider m being Nat such that
A1: n = m + 1 by NAT_1:6;
reconsider m = m as Nat ;
take m -eq_states_partition tfsm ; :: thesis: m -eq_states_partition tfsm is final
m -eq_states_partition tfsm = (m + 1) -eq_states_partition tfsm by A1, Th35;
hence m -eq_states_partition tfsm is final by Th37; :: thesis: verum