for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph ex Ctfsm being non empty finite connected Mealy-FSM over IAlph,OAlph st
( the Tran of Ctfsm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & the OFun of Ctfsm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of Ctfsm = the InitS of tfsm & tfsm,Ctfsm -are_equivalent )