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 A1: ( tfsm1,tfsm2 -are_isomorphic & tfsm2,tfsm3 -are_isomorphic ) ; :: thesis: tfsm1,tfsm3 -are_isomorphic
then consider Tf1 being Function of the carrier of tfsm1,the carrier of tfsm2 such that
A2: ( Tf1 is bijective & Tf1 . the InitS of tfsm1 = the InitS of tfsm2 & ( 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 Def19;
consider Tf2 being Function of the carrier of tfsm2,the carrier of tfsm3 such that
A3: ( Tf2 is bijective & Tf2 . the InitS of tfsm2 = the InitS of tfsm3 & ( 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 A1, 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 A2, A3, 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 ) ) )
A4: dom Tf1 = the carrier of tfsm1 by FUNCT_2:def 1;
hence Tf . the InitS of tfsm1 = the InitS of tfsm3 by A2, A3, 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 A4, FUNCT_1:23
.= Tf2 . (the Tran of tfsm2 . (Tf1 . q),s1) by A3
.= Tf2 . (Tf1 . (the Tran of tfsm1 . q,s1)) by A2
.= Tf . (the Tran of tfsm1 . q,s1) by A4, 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 A4, FUNCT_1:23
.= the OFun of tfsm2 . (Tf1 . q),s1 by A3
.= the OFun of tfsm1 . q,s1 by A2 ; :: 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