let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of 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 of 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, Def10;
hence q1,w -response = q3,w -response by A2, Def10; :: thesis: verum

end;