let it1, it2 be Element of final_states_partition tfsm; :: thesis: ( ex q being State of tfsm ex n being 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 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 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 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];
given q2 being Element of tfsm, n2 being 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];
set m = n1 + 1;
A7: ( 1 <= n1 + 1 & n1 = (n1 + 1) - 1 ) by NAT_1:11;
final_states_partition tfsm is final by Def15;
then q1,q2 -are_equivalent by A3, A5;
then n1 + 1 -equivalent q1,q2 ;
then n1 -equivalent the Tran of tfsm . [q1,s], the Tran of tfsm . [q2,s] by A7, Th27;
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:35; :: thesis: verum