theorem Th19: :: FSM_1:19

for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm holds
( qa,qb -are_equivalent iff for s being Element of IAlph holds
( the OFun of tfsm . [qa,s] = the OFun of tfsm . [qb,s] & the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] -are_equivalent ) )