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, FINSEQ_4:85; :: 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:13; :: 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:13
.= 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:13 ; :: 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:13
.= 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