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