consider q1 being Element of tfsm such that
A1: q1 in qf by FINSEQ_4:87;
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 Nat ;
final_states_partition tfsm = n -eq_states_partition tfsm by A2, Th39;
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 3;
take IT ; :: thesis: ex q being State of tfsm ex n being 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 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