let k be Nat; :: thesis:
let IAlph, OAlph be non empty set ; :: thesis:
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis:
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:

now :: thesis:

let qa, qb be Element of tfsm; :: thesis:

hereby :: thesis:

reconsider X = Class ((k -eq_states_EqR tfsm),qb) as Element of k -eq_states_partition tfsm by EQREL_1:def 3;
assume A2: qa,qb -are_equivalent ; :: thesis:
take X = X; :: thesis:
k -equivalent qa,qb by A2;
then [qa,qb] in k -eq_states_EqR tfsm by Def12;
hence ( qa in X & qb in X ) by EQREL_1:19, EQREL_1:20; :: thesis:

end;

given X being Element of k -eq_states_partition tfsm such that A3: qa in X and
A4: qb in X ; :: thesis:
consider qc being object such that
qc in the carrier of tfsm and
A5: X = Class ((k -eq_states_EqR tfsm),qc) by EQREL_1:def 3;
[qb,qc] in k -eq_states_EqR tfsm by A4, A5, EQREL_1:19;
then A6: [qc,qb] in k -eq_states_EqR tfsm by EQREL_1:6;
[qa,qc] in k -eq_states_EqR tfsm by A3, A5, EQREL_1:19;
then A7: [qa,qb] in k -eq_states_EqR tfsm by A6, EQREL_1:7;
then A8: k -equivalent qa,qb by Def12;
thus qa,qb -are_equivalent :: thesis:

proof

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

per cases ;

suppose n <= k ; :: thesis:

hence (qa,w) -response = (qb,w) -response by A8, A10; :: thesis:

end;

suppose n > k ; :: thesis:

then ex m being Element of NAT st
( n = k + m & 1 <= m ) by FINSEQ_4:84;
then n -eq_states_partition tfsm = k -eq_states_partition tfsm by A1, Th29;
then [qa,qb] in n -eq_states_EqR tfsm by A7, FINSEQ_4:86;
then n -equivalent qa,qb by Def12;
hence (qa,w) -response = (qb,w) -response by A10; :: thesis:

end;

end;

end;

end;

hence k -eq_states_partition tfsm is final ; :: thesis: