theorem Th18: :: FSM_1:18

for IAlph, OAlph being non empty set
for s being Element of IAlph
for w being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qa9 being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
(qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)