set m = card the carrier of tfsm;
consider n being Nat such that
A1: card the carrier of tfsm = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
consider q1 being Element of tfsm such that
A2: q1 in qf by Th11;
A3: final_states_partition tfsm = n -eq_states_partition tfsm by A1, Th56;
set q' = the Tran of tfsm . [q1,s];
reconsider IT = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q1,s]) as Element of final_states_partition tfsm by A3, 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 A1, A2; :: thesis: verum