let IAlph, OAlph be non empty set ; :: thesis: for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM of IAlph,OAlph st tfsm1,tfsm2 -are_isomorphic & tfsm2,tfsm3 -are_isomorphic holds
tfsm1,tfsm3 -are_isomorphic
let tfsm1, tfsm2, tfsm3 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: ( tfsm1,tfsm2 -are_isomorphic & tfsm2,tfsm3 -are_isomorphic implies tfsm1,tfsm3 -are_isomorphic )
assume that
A1: tfsm1,tfsm2 -are_isomorphic and
A2: tfsm2,tfsm3 -are_isomorphic ; :: thesis: tfsm1,tfsm3 -are_isomorphic
consider Tf1 being Function of the carrier of tfsm1,the carrier of tfsm2 such that
A3: Tf1 is bijective and
A4: Tf1 . the InitS of tfsm1 = the InitS of tfsm2 and
A5: for q being Element of tfsm1
for s1 being Element of IAlph holds
( Tf1 . (the Tran of tfsm1 . q,s1) = the Tran of tfsm2 . (Tf1 . q),s1 & the OFun of tfsm1 . q,s1 = the OFun of tfsm2 . (Tf1 . q),s1 ) by A1, Def19;
consider Tf2 being Function of the carrier of tfsm2,the carrier of tfsm3 such that
A6: Tf2 is bijective and
A7: Tf2 . the InitS of tfsm2 = the InitS of tfsm3 and
A8: for q being Element of tfsm2
for s1 being Element of IAlph holds
( Tf2 . (the Tran of tfsm2 . q,s1) = the Tran of tfsm3 . (Tf2 . q),s1 & the OFun of tfsm2 . q,s1 = the OFun of tfsm3 . (Tf2 . q),s1 ) by A2, Def19;
take Tf = Tf2 * Tf1; :: according to FSM_1:def 19 :: thesis: ( Tf is bijective & Tf . the InitS of tfsm1 = the InitS of tfsm3 & ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm3 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm3 . (Tf . q11),s ) ) )
thus Tf is bijective by A3, A6, Th7; :: thesis: ( Tf . the InitS of tfsm1 = the InitS of tfsm3 & ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm3 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm3 . (Tf . q11),s ) ) )
A9: dom Tf1 = the carrier of tfsm1 by FUNCT_2:def 1;
hence Tf . the InitS of tfsm1 = the InitS of tfsm3 by A4, A7, FUNCT_1:23; :: thesis: for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm3 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm3 . (Tf . q11),s )

now

let q be Element of tfsm1; :: thesis: for s1 being Element of IAlph holds
( the Tran of tfsm3 . [(Tf . q),s1] = Tf . (the Tran of tfsm1 . q,s1) & the OFun of tfsm3 . [(Tf . q),s1] = the OFun of tfsm1 . q,s1 )
let s1 be Element of IAlph; :: thesis: ( the Tran of tfsm3 . [(Tf . q),s1] = Tf . (the Tran of tfsm1 . q,s1) & the OFun of tfsm3 . [(Tf . q),s1] = the OFun of tfsm1 . q,s1 )
thus the Tran of tfsm3 . [(Tf . q),s1] = the Tran of tfsm3 . (Tf2 . (Tf1 . q)),s1 by A9, FUNCT_1:23
.= Tf2 . (the Tran of tfsm2 . (Tf1 . q),s1) by A8
.= Tf2 . (Tf1 . (the Tran of tfsm1 . q,s1)) by A5
.= Tf . (the Tran of tfsm1 . q,s1) by A9, FUNCT_1:23 ; :: thesis: the OFun of tfsm3 . [(Tf . q),s1] = the OFun of tfsm1 . q,s1
thus the OFun of tfsm3 . [(Tf . q),s1] = the OFun of tfsm3 . (Tf2 . (Tf1 . q)),s1 by A9, FUNCT_1:23
.= the OFun of tfsm2 . (Tf1 . q),s1 by A8
.= the OFun of tfsm1 . q,s1 by A5 ; :: thesis: verum

end;

hence for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm3 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm3 . (Tf . q11),s ) ; :: thesis: verum