theorem Th27: :: FSM_1:27

for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm
for k being Nat st 1 <= k holds
( k -equivalent qa,qb iff ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] ) ) )