theorem Th9: :: FSM_1:9

for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qt being State of tfsm holds (qt,(<*> IAlph)) -response = <*> OAlph