let IAlph, OAlph be non empty set ; :: thesis: for w being FinSequence of IAlph
for sfsm being non empty Moore-FSM of IAlph,OAlph
for qs being State of sfsm holds (qs,w -response ) . 1 = the OFun of sfsm . qs
let w be FinSequence of IAlph; :: thesis: for sfsm being non empty Moore-FSM of IAlph,OAlph
for qs being State of sfsm holds (qs,w -response ) . 1 = the OFun of sfsm . qs
let sfsm be non empty Moore-FSM of IAlph,OAlph; :: thesis: for qs being State of sfsm holds (qs,w -response ) . 1 = the OFun of sfsm . qs
let qs be State of sfsm; :: thesis: (qs,w -response ) . 1 = the OFun of sfsm . qs
1 <= (len w) + 1 by NAT_1:12;
then 1 in Seg ((len w) + 1) by FINSEQ_1:3;
hence (qs,w -response ) . 1 = the OFun of sfsm . ((qs,w -admissible ) . 1) by Def7
.= the OFun of sfsm . qs by Def2 ;
:: thesis: verum