( len ((q,w) -admissible) = (len w) + 1 & (len w) + 1 in Seg ((len w) + 1) ) by Def2, FINSEQ_1:4;
then (len w) + 1 in dom ((q,w) -admissible) by FINSEQ_1:def 3;
then reconsider IT = ((q,w) -admissible) . ((len w) + 1) as Element of fsm by FINSEQ_2:11;
take IT ; :: thesis: q,w -leads_to IT
thus q,w -leads_to IT ; :: thesis: verum