let tfsm1, tfsm2 be non empty Mealy-FSM over 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:33;
A6: rng Tf = the carrier of tfsm2 by A1, FUNCT_2:def 3;
then the carrier of tfsm2 = dom (Tf ") by A1, FUNCT_1:33;
then reconsider Tf9 = Tf " as Function of the carrier of tfsm2, the carrier of tfsm1 by A5, FUNCT_2:1;
take Tf9 ; :: thesis:
Tf9 is onto by A5, FUNCT_2:def 3;
hence Tf9 is bijective by A1; :: thesis:
thus the InitS of tfsm1 = Tf9 . the InitS of tfsm2 by A1, A2, A4, FUNCT_1:34; :: thesis:

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