let tfsm1 be non empty Mealy-FSM over IAlph,OAlph; 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; ( 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
; ( 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
; 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; 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; ( 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)
; 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)
; verum