let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb, qc being State of tfsm
for k being Nat st k -equivalent qa,qb & k -equivalent qb,qc holds
k -equivalent qa,qc
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for qa, qb, qc being State of tfsm
for k being Nat st k -equivalent qa,qb & k -equivalent qb,qc holds
k -equivalent qa,qc
let qa, qb, qc be State of tfsm; :: thesis: for k being Nat st k -equivalent qa,qb & k -equivalent qb,qc holds
k -equivalent qa,qc
let k be Nat; :: thesis: ( k -equivalent qa,qb & k -equivalent qb,qc implies k -equivalent qa,qc )
assume that
A1: k -equivalent qa,qb and
A2: k -equivalent qb,qc ; :: thesis: k -equivalent qa,qc
thus k -equivalent qa,qc :: thesis: verum

proof

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

end;