let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qt being State of tfsm holds (qt,(<*> IAlph)) -response = <*> OAlph
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for qt being State of tfsm holds (qt,(<*> IAlph)) -response = <*> OAlph
let qt be State of tfsm; :: thesis: (qt,(<*> IAlph)) -response = <*> OAlph
len ((qt,(<*> IAlph)) -response) = len (<*> IAlph) by Def6
.= 0 ;
hence (qt,(<*> IAlph)) -response = <*> OAlph ; :: thesis: verum