let IAlph, OAlph be non empty set ; for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM over 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 over IAlph,OAlph; ( 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
; 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;
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;
take Tf = Tf2 * Tf1; FSM_1:def 19 ( 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; ( 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; 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 for q being Element of tfsm1
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 q be
Element of
tfsm1;
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;
( 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
;
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
;
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) )
; verum