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 )
assume A1: k -eq_states_partition tfsm is final ; :: thesis: (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;

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] & a in the carrier of tfsm & b in the carrier of tfsm ) by RELSET_1:6;
reconsider a = a as Element of the carrier of tfsm by A3;
reconsider b = b as Element of the carrier of tfsm by A3;
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 A4: x in k -eq_states_EqR tfsm ; :: thesis: x in (k + 1) -eq_states_EqR tfsm
then consider a, b being set such that
A5: ( x = [a,b] & a in the carrier of tfsm & b in the carrier of tfsm ) by RELSET_1:6;
reconsider a = a as Element of the carrier of tfsm by A5;
reconsider b = b as Element of the carrier of tfsm by A5;
reconsider cl = Class (k -eq_states_EqR tfsm),b as Element of k -eq_states_partition tfsm by EQREL_1:def 5;
( a in cl & b in cl ) by A4, A5, EQREL_1:27, EQREL_1:28;
then a,b -are_equivalent by A1, Def14;
then k + 1 -equivalent a,b by Th41;
hence x in (k + 1) -eq_states_EqR tfsm by A5, Def12; :: thesis: verum

end;

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