let IAlph be non empty set ; :: thesis: for fsm being non empty FSM of IAlph
for q being State of fsm holds q, <*> IAlph -leads_to q
let fsm be non empty FSM of IAlph; :: thesis: for q being State of fsm holds q, <*> IAlph -leads_to q
let q be State of fsm; :: thesis: q, <*> IAlph -leads_to q
set eis = <*> IAlph;
A1: <*q*> . ((len (<*> IAlph)) + 1) = <*q*> . (0 + 1)
.= q by FINSEQ_1:57 ;
q,(<*> IAlph) -admissible = <*q*> by Th16;
hence q, <*> IAlph -leads_to q by A1, Def3; :: thesis: verum