for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm st qa,qb -are_equivalent holds
for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )