for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w being FinSequence of IAlph
for q, q9 being State of fsm holds
( ((q,w) -admissible) . (len ((q,w) -admissible)) = q9 iff q,w -leads_to q9 ) by Def2;