let IAlph, OAlph be non empty set ; :: thesis: for w being FinSequence of IAlph
for sfsm being non empty Moore-FSM over 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 over 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 over 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:1;
hence ((qs,w) -response) . 1 = the OFun of sfsm . (((qs,w) -admissible) . 1) by Def7
.= the OFun of sfsm . qs by Def2 ;
:: thesis: verum