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 keq = k -eq_states_EqR tfsm;
set k1eq = (k + 1) -eq_states_EqR tfsm;
set kpart = k -eq_states_partition tfsm;
assume A1: k -eq_states_partition tfsm is final ; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume A2: x in (k + 1) -eq_states_EqR tfsm ; :: thesis:
then consider a, b being object such that
A3: x = [a,b] and
A4: a in the carrier of tfsm and
A5: b in the carrier of tfsm by RELSET_1:2;
reconsider b = b as Element of the carrier of tfsm by A5;
reconsider a = a as Element of the carrier of tfsm by A4;
k + 1 -equivalent a,b by A2, A3, Def12;
then k -equivalent a,b by Th26;
hence x in k -eq_states_EqR tfsm by A3, Def12; :: thesis:

end;

assume A6: x in k -eq_states_EqR tfsm ; :: thesis:
then consider a, b being object such that
A7: x = [a,b] and
A8: a in the carrier of tfsm and
A9: b in the carrier of tfsm by RELSET_1:2;
reconsider b = b as Element of the carrier of tfsm by A9;
reconsider a = a as Element of the carrier of tfsm by A8;
reconsider cl = Class ((k -eq_states_EqR tfsm),b) as Element of k -eq_states_partition tfsm by EQREL_1:def 3;
A10: b in cl by EQREL_1:20;
a in cl by A6, A7, EQREL_1:19;
then a,b -are_equivalent by A1, A10;
then k + 1 -equivalent a,b ;
hence x in (k + 1) -eq_states_EqR tfsm by A7, Def12; :: thesis:

end;

hence (k + 1) -eq_states_EqR tfsm = k -eq_states_EqR tfsm by TARSKI:2; :: thesis: