let IAlph be non empty set ; :: thesis: for fsm being non empty FSM over IAlph
for q being State of fsm holds q, <*> IAlph -leads_to q
let fsm be non empty FSM over 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:40 ;
(q,(<*> IAlph)) -admissible = <*q*> by Th1;
hence q, <*> IAlph -leads_to q by A1; :: thesis: verum