let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph
for q being State of tfsm holds Class (0 -eq_states_EqR tfsm),q = the carrier of tfsm
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for q being State of tfsm holds Class (0 -eq_states_EqR tfsm),q = the carrier of tfsm
let q be State of tfsm; :: thesis: Class (0 -eq_states_EqR tfsm),q = the carrier of tfsm
set 0e = 0 -eq_states_EqR tfsm;
set S = the carrier of tfsm;

now

let z be set ; :: thesis: ( ( z in Class (0 -eq_states_EqR tfsm),q implies z in the carrier of tfsm ) & ( z in the carrier of tfsm implies z in Class (0 -eq_states_EqR tfsm),q ) )
thus ( z in Class (0 -eq_states_EqR tfsm),q implies z in the carrier of tfsm ) ; :: thesis: ( z in the carrier of tfsm implies z in Class (0 -eq_states_EqR tfsm),q )
assume z in the carrier of tfsm ; :: thesis: z in Class (0 -eq_states_EqR tfsm),q
then reconsider z9 = z as Element of the carrier of tfsm ;
0 -equivalent z9,q by Th42;
then [z,q] in 0 -eq_states_EqR tfsm by Def12;
hence z in Class (0 -eq_states_EqR tfsm),q by EQREL_1:27; :: thesis: verum

end;

hence Class (0 -eq_states_EqR tfsm),q = the carrier of tfsm by TARSKI:2; :: thesis: verum