let IAlph be non empty set ; :: thesis: for fsm being non empty FSM of IAlph
for w being FinSequence of IAlph
for q, q9 being State of fsm holds
( (q,w -admissible ) . (len (q,w -admissible )) = q9 iff q,w -leads_to q9 )
let fsm be non empty FSM of IAlph; :: thesis: for w being FinSequence of IAlph
for q, q9 being State of fsm holds
( (q,w -admissible ) . (len (q,w -admissible )) = q9 iff q,w -leads_to q9 )
let w be FinSequence of IAlph; :: thesis: for q, q9 being State of fsm holds
( (q,w -admissible ) . (len (q,w -admissible )) = q9 iff q,w -leads_to q9 )
let q, q9 be State of fsm; :: thesis: ( (q,w -admissible ) . (len (q,w -admissible )) = q9 iff q,w -leads_to q9 )

hereby :: thesis: ( q,w -leads_to q9 implies (q,w -admissible ) . (len (q,w -admissible )) = q9 )

set qs = q,w -admissible ;
assume A1: (q,w -admissible ) . (len (q,w -admissible )) = q9 ; :: thesis: q,w -leads_to q9
len (q,w -admissible ) = (len w) + 1 by Def2;
hence q,w -leads_to q9 by A1, Def3; :: thesis: verum

end;

assume q,w -leads_to q9 ; :: thesis: (q,w -admissible ) . (len (q,w -admissible )) = q9
then (q,w -admissible ) . ((len w) + 1) = q9 by Def3;
hence (q,w -admissible ) . (len (q,w -admissible )) = q9 by Def2; :: thesis: verum