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 SS = { the carrier of tfsm};
set 0p = 0 -eq_states_partition tfsm;
set 0e = 0 -eq_states_EqR tfsm;

set y = the Element of the carrier of tfsm;
let x be object ; :: thesis:

assume A1: x in 0 -eq_states_partition tfsm ; :: thesis:
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:

end;

end;