let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm holds 0 -equivalent qa,qb
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for qa, qb being State of tfsm holds 0 -equivalent qa,qb
let qa, qb be State of tfsm; :: thesis: 0 -equivalent qa,qb
let w be FinSequence of IAlph; :: according to FSM_1:def 11 :: thesis: ( len w <= 0 implies (qa,w) -response = (qb,w) -response )
assume len w <= 0 ; :: thesis: (qa,w) -response = (qb,w) -response
then A1: w = <*> IAlph ;
hence (qa,w) -response = <*> OAlph by Th9
.= (qb,w) -response by A1, Th9 ;
:: thesis: verum