let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa being State of tfsm
for k being Nat holds k -equivalent qa,qa
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for qa being State of tfsm
for k being Nat holds k -equivalent qa,qa
let qa be State of tfsm; :: thesis: for k being Nat holds k -equivalent qa,qa
let k be Nat; :: thesis: k -equivalent qa,qa
let w be FinSequence of IAlph; :: according to FSM_1:def 11 :: thesis: ( len w <= k implies qa,w -response = qa,w -response )
assume len w <= k ; :: thesis: qa,w -response = qa,w -response
thus qa,w -response = qa,w -response ; :: thesis: verum