let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph holds 0 -eq_states_partition tfsm = {the carrier of tfsm}
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: 0 -eq_states_partition tfsm = {the carrier of tfsm}
set S = the carrier of tfsm;
set SS = {the carrier of tfsm};
set 0p = 0 -eq_states_partition tfsm;
set 0e = 0 -eq_states_EqR tfsm;

now

let x be set ; :: thesis: ( ( x in 0 -eq_states_partition tfsm implies x in {the carrier of tfsm} ) & ( x in {the carrier of tfsm} implies x in 0 -eq_states_partition tfsm ) )

hereby :: thesis: ( x in {the carrier of tfsm} implies x in 0 -eq_states_partition tfsm )

assume A1: x in 0 -eq_states_partition tfsm ; :: thesis: x in {the carrier of tfsm}
then reconsider x' = x as Subset of the carrier of tfsm ;
consider y being set such that
A2: ( y in the carrier of tfsm & x' = Class (0 -eq_states_EqR tfsm),y ) by A1, EQREL_1:def 5;
reconsider y = y as Element of the carrier of tfsm by A2;
Class (0 -eq_states_EqR tfsm),y = the carrier of tfsm by Th50;
hence x in {the carrier of tfsm} by A2, TARSKI:def 1; :: thesis: verum

end;

assume x in {the carrier of tfsm} ; :: thesis: x in 0 -eq_states_partition tfsm
then A3: x = the carrier of tfsm by TARSKI:def 1;
consider y being Element of the carrier of tfsm;
Class (0 -eq_states_EqR tfsm),y in Class (0 -eq_states_EqR tfsm) by EQREL_1:def 5;
hence x in 0 -eq_states_partition tfsm by A3, Th50; :: thesis: verum

end;

hence 0 -eq_states_partition tfsm = {the carrier of tfsm} by TARSKI:2; :: thesis: verum