let it1, it2 be Element of fsm; :: thesis: ( q,w -leads_to it1 & q,w -leads_to it2 implies it1 = it2 )
assume ( q,w -leads_to it1 & q,w -leads_to it2 ) ; :: thesis: it1 = it2
then ( (q,w -admissible ) . ((len w) + 1) = it1 & (q,w -admissible ) . ((len w) + 1) = it2 ) by Def3;
hence it1 = it2 ; :: thesis: verum