let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qt being State of tfsm holds qt,(<*> IAlph) -response = <*> OAlph
let tfsm be non empty Mealy-FSM of 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