let IAlph be non empty set ; :: thesis: for fsm being non empty FSM over IAlph
for q being State of fsm holds (q,(<*> IAlph)) -admissible = <*q*>
let fsm be non empty FSM over IAlph; :: thesis: for q being State of fsm holds (q,(<*> IAlph)) -admissible = <*q*>
let q be State of fsm; :: thesis: (q,(<*> IAlph)) -admissible = <*q*>
set eis = <*> IAlph;
A1: for i being Nat st 1 <= i & i <= len (<*> IAlph) holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = (<*> IAlph) . i & qi = <*q*> . i & qi1 = <*q*> . (i + 1) & wi -succ_of qi = qi1 ) ;
( len <*q*> = (len (<*> IAlph)) + 1 & <*q*> . 1 = q ) by FINSEQ_1:40;
hence (q,(<*> IAlph)) -admissible = <*q*> by A1, Def2; :: thesis: verum