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 and
A2: Tf . the InitS of tfsm1 = the InitS of tfsm2 and
A3: 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:
A4: dom Tf = the carrier of tfsm1 by FUNCT_2:def 1;
then A5: rng (Tf " ) = the carrier of tfsm1 by A1, FUNCT_1:55;
A6: rng Tf = the carrier of tfsm2 by A1, FUNCT_2:def 3;
then the carrier of tfsm2 = dom (Tf " ) by A1, FUNCT_1:55;
then reconsider Tf' = Tf " as Function of the carrier of tfsm2,the carrier of tfsm1 by A5, FUNCT_2:3;
take Tf' ; :: thesis:
Tf' is onto by A5, FUNCT_2:def 3;
hence Tf' is bijective by A1; :: thesis:
thus the InitS of tfsm1 = Tf' . the InitS of tfsm2 by A1, A2, A4, FUNCT_1:56; :: thesis:

let q be Element of tfsm2; :: thesis:
let s be Element of IAlph; :: thesis:
A7: q = Tf . (Tf' . q) by A1, A6, FUNCT_1:57;
thus the Tran of tfsm1 . [(Tf' . q),s] = Tf' . (Tf . (the Tran of tfsm1 . (Tf' . q),s)) by A1, A4, FUNCT_1:56
.= Tf' . (the Tran of tfsm2 . q,s) by A3, A7 ; :: thesis:
thus the OFun of tfsm1 . (Tf' . q),s = the OFun of tfsm2 . q,s by A3, 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: