let IAlph be non empty set ; :: thesis: for fsm being non empty FSM of IAlph
for q being State of fsm holds q,(<*> IAlph) -admissible = <*q*>
let fsm be non empty FSM of 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: len <*q*> = (len (<*> IAlph)) + 1 by FINSEQ_1:57;
A2: <*q*> . 1 = q by FINSEQ_1:57;
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 ) ;
hence q,(<*> IAlph) -admissible = <*q*> by A1, A2, Def2; :: thesis: verum