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
for k, m being Nat st k + m -equivalent qa,qb holds
k -equivalent qa,qb
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for qa, qb being State of tfsm
for k, m being Nat st k + m -equivalent qa,qb holds
k -equivalent qa,qb
let qa, qb be State of tfsm; :: thesis: for k, m being Nat st k + m -equivalent qa,qb holds
k -equivalent qa,qb
let k, m be Nat; :: thesis: ( k + m -equivalent qa,qb implies k -equivalent qa,qb )
assume A1: k + m -equivalent qa,qb ; :: thesis: k -equivalent qa,qb
let w be FinSequence of IAlph; :: according to FSM_1:def 11 :: thesis: ( len w <= k implies (qa,w) -response = (qb,w) -response )
A2: k <= k + m by NAT_1:11;
assume len w <= k ; :: thesis: (qa,w) -response = (qb,w) -response
then len w <= k + m by A2, XXREAL_0:2;
hence (qa,w) -response = (qb,w) -response by A1; :: thesis: verum