let it1, it2 be Element of final_states_partition tfsm; :: thesis: ( ex q being State of tfsm ex n being Element of NAT st
( q in qf & n + 1 = card the carrier of tfsm & it1 = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q,s]) ) & ex q being State of tfsm ex n being Element of NAT st
( q in qf & n + 1 = card the carrier of tfsm & it2 = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q,s]) ) implies it1 = it2 )
given q1 being Element of tfsm, n1 being Element of NAT such that A3: q1 in qf and
A4: ( n1 + 1 = card the carrier of tfsm & it1 = Class (n1 -eq_states_EqR tfsm),(the Tran of tfsm . [q1,s]) ) ; :: thesis: ( for q being State of tfsm
for n being Element of NAT holds
( not q in qf or not n + 1 = card the carrier of tfsm or not it2 = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q,s]) ) or it1 = it2 )
set q19 = the Tran of tfsm . [q1,s];
set m = n1 + 1;
given q2 being Element of tfsm, n2 being Element of NAT such that A5: q2 in qf and
A6: ( n2 + 1 = card the carrier of tfsm & it2 = Class (n2 -eq_states_EqR tfsm),(the Tran of tfsm . [q2,s]) ) ; :: thesis: it1 = it2
set q29 = the Tran of tfsm . [q2,s];
A7: ( 1 <= n1 + 1 & n1 = (n1 + 1) - 1 ) by INT_1:19;
final_states_partition tfsm is final by Def15;
then q1,q2 -are_equivalent by A3, A5, Def14;
then n1 + 1 -equivalent q1,q2 by Th41;
then n1 -equivalent the Tran of tfsm . [q1,s],the Tran of tfsm . [q2,s] by A7, Th44;
then [(the Tran of tfsm . [q1,s]),(the Tran of tfsm . [q2,s])] in n1 -eq_states_EqR tfsm by Def12;
hence it1 = it2 by A4, A6, EQREL_1:44; :: thesis: verum