for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
for k being Nat st 1 <= k & k <= (len w2) + 1 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -admissible) . k