let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over 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 over 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 :: thesis: for z being object holds
( ( 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) ) )

let z be object ; :: 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 Th25;
then [z,q] in 0 -eq_states_EqR tfsm by Def12;
hence z in Class ((0 -eq_states_EqR tfsm),q) by EQREL_1:19; :: thesis: verum

end;

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