:: deftheorem defines -are_equivalent FSM_1:def 9 :
for IAlph, OAlph being non empty set
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph holds
( tfsm1,tfsm2 -are_equivalent iff for w being FinSequence of IAlph holds ( the InitS of tfsm1,w) -response = ( the InitS of tfsm2,w) -response );