( len (q,w -admissible ) = (len w) + 1 & (len w) + 1 in Seg ((len w) + 1) ) by Def2, FINSEQ_1:6;
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:13;
take IT ; :: thesis: q,w -leads_to IT
thus q,w -leads_to IT by Def3; :: thesis: verum