let tfsm1 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: ex Tf being Function of the carrier of tfsm1,the carrier of tfsm1 st
( Tf is bijective & Tf . the InitS of tfsm1 = the InitS of tfsm1 & ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm1 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm1 . (Tf . q11),s ) ) )
take Tf = id the carrier of tfsm1; :: thesis: ( Tf is bijective & Tf . the InitS of tfsm1 = the InitS of tfsm1 & ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm1 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm1 . (Tf . q11),s ) ) )
thus Tf is bijective ; :: thesis: ( Tf . the InitS of tfsm1 = the InitS of tfsm1 & ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm1 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm1 . (Tf . q11),s ) ) )
thus Tf . the InitS of tfsm1 = the InitS of tfsm1 by FUNCT_1:34; :: thesis: for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm1 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm1 . (Tf . q11),s )
let q be Element of tfsm1; :: thesis: for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm1 . (Tf . q),s & the OFun of tfsm1 . q,s = the OFun of tfsm1 . (Tf . q),s )
let s be Element of IAlph; :: thesis: ( Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm1 . (Tf . q),s & the OFun of tfsm1 . q,s = the OFun of tfsm1 . (Tf . q),s )
thus Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm1 . [q,s] by FUNCT_1:34
.= the Tran of tfsm1 . (Tf . q),s by FUNCT_1:34 ; :: thesis: the OFun of tfsm1 . q,s = the OFun of tfsm1 . (Tf . q),s
thus the OFun of tfsm1 . q,s = the OFun of tfsm1 . (Tf . q),s by FUNCT_1:34; :: thesis: verum