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 A4: ( q1 in qf & 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 )
given q2 being Element of tfsm, n2 being Element of NAT such that A5: ( q2 in qf & n2 + 1 = card the carrier of tfsm & it2 = Class (n2 -eq_states_EqR tfsm),(the Tran of tfsm . [q2,s]) ) ; :: thesis: it1 = it2
set m = n1 + 1;
A6: 1 <= n1 + 1 by INT_1:19;
A7: n1 = (n1 + 1) - 1 ;
set q1' = the Tran of tfsm . [q1,s];
set q2' = the Tran of tfsm . [q2,s];
final_states_partition tfsm is final by Def15;
then q1,q2 -are_equivalent by A4, 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 A6, 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, A5, EQREL_1:44; :: thesis: verum