let IAlph, OAlph be non empty set ; for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM over 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 over IAlph,OAlph; ( tfsm1,tfsm2 -are_equivalent & tfsm2,tfsm3 -are_equivalent implies tfsm1,tfsm3 -are_equivalent )
assume that
A1:
tfsm1,tfsm2 -are_equivalent
and
A2:
tfsm2,tfsm3 -are_equivalent
; tfsm1,tfsm3 -are_equivalent
let w1 be FinSequence of IAlph; FSM_1:def 9 ( the InitS of tfsm1,w1) -response = ( the InitS of tfsm3,w1) -response
set IS3 = the InitS of tfsm3;
set IS1 = the InitS of tfsm1;
set IS2 = the InitS of tfsm2;
thus ( the InitS of tfsm1,w1) -response =
( the InitS of tfsm2,w1) -response
by A1
.=
( the InitS of tfsm3,w1) -response
by A2
; verum