consider q1 being Element of tfsm such that
A1: q1 in qf by Th11;
set q9 = the Tran of tfsm . [q1,s];
set m = card the carrier of tfsm;
consider n being Nat such that
A2: card the carrier of tfsm = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
final_states_partition tfsm = n -eq_states_partition tfsm by A2, Th56;
then reconsider IT = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q1,s]) as Element of final_states_partition tfsm by EQREL_1:def 5;
take IT ; :: thesis: ex q being State of tfsm ex n being Element of NAT st
( q in qf & n + 1 = card the carrier of tfsm & IT = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q,s]) )
thus ex q being State of tfsm ex n being Element of NAT st
( q in qf & n + 1 = card the carrier of tfsm & IT = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q,s]) ) by A2, A1; :: thesis: verum