let tfsm1 be non empty Mealy-FSM over 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 ; :: 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]
.= the Tran of tfsm1 . ((Tf . q),s) ; :: 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) ; :: thesis: verum