let IAlph, OAlph be non empty set ; :: thesis: for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM of IAlph,OAlph st tfsm1,tfsm2 -are_equivalent & tfsm2,tfsm3 -are_equivalent holds
tfsm1,tfsm3 -are_equivalent
let tfsm1, tfsm2, tfsm3 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: ( tfsm1,tfsm2 -are_equivalent & tfsm2,tfsm3 -are_equivalent implies tfsm1,tfsm3 -are_equivalent )
assume A1: ( tfsm1,tfsm2 -are_equivalent & tfsm2,tfsm3 -are_equivalent ) ; :: thesis: tfsm1,tfsm3 -are_equivalent
set IS1 = the InitS of tfsm1;
set IS2 = the InitS of tfsm2;
set IS3 = the InitS of tfsm3;
let w1 be FinSequence of IAlph; :: according to FSM_1:def 9 :: thesis: the InitS of tfsm1,w1 -response = the InitS of tfsm3,w1 -response
thus the InitS of tfsm1,w1 -response = the InitS of tfsm2,w1 -response by A1, Def9
.= the InitS of tfsm3,w1 -response by A1, Def9 ; :: thesis: verum