let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph holds 0 -eq_states_partition tfsm = { the carrier of tfsm}
let tfsm be non empty Mealy-FSM over 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 :: thesis: for x being object holds
( ( 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 ) )

set y = the Element of the carrier of tfsm;
let x be object ; :: 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 x9 = x as Subset of the carrier of tfsm ;
consider y being object such that
A2: y in the carrier of tfsm and
A3: x9 = Class ((0 -eq_states_EqR tfsm),y) by A1, EQREL_1:def 3;
reconsider y = y as Element of the carrier of tfsm by A2;
Class ((0 -eq_states_EqR tfsm),y) = the carrier of tfsm by Th33;
hence x in { the carrier of tfsm} by A3, TARSKI:def 1; :: thesis: verum

end;

assume x in { the carrier of tfsm} ; :: thesis: x in 0 -eq_states_partition tfsm
then A4: x = the carrier of tfsm by TARSKI:def 1;
Class ((0 -eq_states_EqR tfsm), the Element of the carrier of tfsm) in Class (0 -eq_states_EqR tfsm) by EQREL_1:def 3;
hence x in 0 -eq_states_partition tfsm by A4, Th33; :: thesis: verum

end;

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