let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph; :: thesis:
given Tf being Function of the carrier of tfsm1,the carrier of tfsm2 such that A1: ( Tf is bijective & Tf . the InitS of tfsm1 = the InitS of tfsm2 & ( for q being Element of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm2 . (Tf . q),s & the OFun of tfsm1 . q,s = the OFun of tfsm2 . (Tf . q),s ) ) ) ; :: thesis:
A2: ( Tf is one-to-one & Tf is onto ) by A1;
then A3: rng Tf = the carrier of tfsm2 by FUNCT_2:def 3;
then A4: the carrier of tfsm2 = dom (Tf " ) by A2, FUNCT_1:55;
A5: dom Tf = the carrier of tfsm1 by FUNCT_2:def 1;
then A6: rng (Tf " ) = the carrier of tfsm1 by A2, FUNCT_1:55;
then reconsider Tf' = Tf " as Function of the carrier of tfsm2,the carrier of tfsm1 by A4, FUNCT_2:3;
take Tf' ; :: thesis:
( Tf' is one-to-one & Tf' is onto ) by A2, A6, FUNCT_2:def 3;
hence Tf' is bijective ; :: thesis:
thus the InitS of tfsm1 = Tf' . the InitS of tfsm2 by A1, A5, FUNCT_1:56; :: thesis:

let q be Element of tfsm2; :: thesis:
let s be Element of IAlph; :: thesis:
A7: q = Tf . (Tf' . q) by A2, A3, FUNCT_1:57;
thus the Tran of tfsm1 . [(Tf' . q),s] = Tf' . (Tf . (the Tran of tfsm1 . (Tf' . q),s)) by A2, A5, FUNCT_1:56
.= Tf' . (the Tran of tfsm2 . q,s) by A1, A7 ; :: thesis:
thus the OFun of tfsm1 . (Tf' . q),s = the OFun of tfsm2 . q,s by A1, A7; :: thesis:

end;

hence for q11 being State of tfsm2
for s being Element of IAlph holds
( Tf' . (the Tran of tfsm2 . q11,s) = the Tran of tfsm1 . (Tf' . q11),s & the OFun of tfsm2 . q11,s = the OFun of tfsm1 . (Tf' . q11),s ) ; :: thesis: