let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph
for q1, q2, q3 being State of tfsm st q1,q2 -are_equivalent & q2,q3 -are_equivalent holds
q1,q3 -are_equivalent
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: for q1, q2, q3 being State of tfsm st q1,q2 -are_equivalent & q2,q3 -are_equivalent holds
q1,q3 -are_equivalent
let q1, q2, q3 be State of tfsm; :: thesis: ( q1,q2 -are_equivalent & q2,q3 -are_equivalent implies q1,q3 -are_equivalent )
assume that
A1: q1,q2 -are_equivalent and
A2: q2,q3 -are_equivalent ; :: thesis: q1,q3 -are_equivalent
thus q1,q3 -are_equivalent :: thesis: verum

proof

let w be FinSequence of IAlph; :: according to FSM_1:def 10 :: thesis: (q1,w) -response = (q3,w) -response
(q1,w) -response = (q2,w) -response by A1;
hence (q1,w) -response = (q3,w) -response by A2; :: thesis: verum

end;