reconsider n = card the carrier of tfsm as Element of NAT ;
consider m being Nat such that
A1: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
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, Th52;
hence m -eq_states_partition tfsm is final by Th54; :: thesis: verum