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 is final holds
(k + 1) -eq_states_EqR tfsm = k -eq_states_EqR tfsm
let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph st k -eq_states_partition tfsm is final holds
(k + 1) -eq_states_EqR tfsm = k -eq_states_EqR tfsm
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: ( k -eq_states_partition tfsm is final implies (k + 1) -eq_states_EqR tfsm = k -eq_states_EqR tfsm )
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: (k + 1) -eq_states_EqR tfsm = k -eq_states_EqR tfsm

now

let x be set ; :: thesis: ( ( x in (k + 1) -eq_states_EqR tfsm implies x in k -eq_states_EqR tfsm ) & ( x in k -eq_states_EqR tfsm implies x in (k + 1) -eq_states_EqR tfsm ) )

hereby :: thesis: ( x in k -eq_states_EqR tfsm implies x in (k + 1) -eq_states_EqR tfsm )

assume A2: x in (k + 1) -eq_states_EqR tfsm ; :: thesis: x in k -eq_states_EqR tfsm
then consider a, b being set 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 Th43;
hence x in k -eq_states_EqR tfsm by A3, Def12; :: thesis: verum

end;

assume A6: x in k -eq_states_EqR tfsm ; :: thesis: x in (k + 1) -eq_states_EqR tfsm
then consider a, b being set 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, Def14;
then k + 1 -equivalent a,b by Th41;
hence x in (k + 1) -eq_states_EqR tfsm by A7, Def12; :: thesis: verum

end;

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