theorem Th8: :: FSM_1:8

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
(q1,(w1 ^ w2)) -admissible = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)