let k be Element of NAT ; :: thesis: for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph st k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm holds
k -eq_states_partition tfsm is final
let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph st k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm holds
k -eq_states_partition tfsm is final
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: ( k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm implies k -eq_states_partition tfsm is final )
set S = the carrier of tfsm;
set kpart = k -eq_states_partition tfsm;
set k1part = (k + 1) -eq_states_partition tfsm;
set keq = k -eq_states_EqR tfsm;
assume A1: k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm ; :: thesis: k -eq_states_partition tfsm is final

now

let qa, qb be Element of tfsm; :: thesis: ( ( qa,qb -are_equivalent implies ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X ) ) & ( ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X ) implies qa,qb -are_equivalent ) )

hereby :: thesis: ( ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X ) implies qa,qb -are_equivalent )

assume qa,qb -are_equivalent ; :: thesis: ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X )
then k -equivalent qa,qb by Th41;
then A2: [qa,qb] in k -eq_states_EqR tfsm by Def12;
reconsider X = Class (k -eq_states_EqR tfsm),qb as Element of k -eq_states_partition tfsm by EQREL_1:def 5;
take X = X; :: thesis: ( qa in X & qb in X )
thus ( qa in X & qb in X ) by A2, EQREL_1:27, EQREL_1:28; :: thesis: verum

end;

given X being Element of k -eq_states_partition tfsm such that A3: ( qa in X & qb in X ) ; :: thesis: qa,qb -are_equivalent
consider qc being set such that
A4: ( qc in the carrier of tfsm & X = Class (k -eq_states_EqR tfsm),qc ) by EQREL_1:def 5;
[qb,qc] in k -eq_states_EqR tfsm by A3, A4, EQREL_1:27;
then A5: [qc,qb] in k -eq_states_EqR tfsm by EQREL_1:12;
[qa,qc] in k -eq_states_EqR tfsm by A3, A4, EQREL_1:27;
then A6: [qa,qb] in k -eq_states_EqR tfsm by A5, EQREL_1:13;
then A7: k -equivalent qa,qb by Def12;
thus qa,qb -are_equivalent :: thesis: verum

proof

let w be FinSequence of IAlph; :: according to FSM_1:def 10 :: thesis: qa,w -response = qb,w -response
consider n being Nat such that
A8: dom w = Seg n by FINSEQ_1:def 2;
n in NAT by ORDINAL1:def 13;
then A9: n = len w by A8, FINSEQ_1:def 3;

per cases ( n <= k or n > k ) ;

suppose n <= k ; :: thesis: qa,w -response = qb,w -response

hence qa,w -response = qb,w -response by A7, A9, Def11; :: thesis: verum

end;

suppose n > k ; :: thesis: qa,w -response = qb,w -response

then consider m being Element of NAT such that
A10: ( n = k + m & 1 <= m ) by Th1;
n -eq_states_partition tfsm = k -eq_states_partition tfsm by A1, A10, Th46;
then [qa,qb] in n -eq_states_EqR tfsm by A6, Th8;
then n -equivalent qa,qb by Def12;
hence qa,w -response = qb,w -response by A9, Def11; :: thesis: verum

end;

end;

end;

end;

hence k -eq_states_partition tfsm is final by Def14; :: thesis: verum