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