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

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

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

end;

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