let k be Element of NAT ; :: thesis: for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb being State of tfsm st qa,qb -are_equivalent holds
k -equivalent qa,qb
let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb being State of tfsm st qa,qb -are_equivalent holds
k -equivalent qa,qb
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for qa, qb being State of tfsm st qa,qb -are_equivalent holds
k -equivalent qa,qb
let qa, qb be State of tfsm; :: thesis: ( qa,qb -are_equivalent implies k -equivalent qa,qb )
assume A1: qa,qb -are_equivalent ; :: thesis: k -equivalent qa,qb
thus k -equivalent qa,qb :: thesis: verum

proof

let w be FinSequence of IAlph; :: according to FSM_1:def 11 :: thesis: ( len w <= k implies (qa,w) -response = (qb,w) -response )
assume len w <= k ; :: thesis: (qa,w) -response = (qb,w) -response
thus (qa,w) -response = (qb,w) -response by A1, Def10; :: thesis: verum

end;