let IAlph, OAlph be non empty set ; :: thesis:
let tfsm1, tfsm2 be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis:
set Stfsm1 = the carrier of tfsm1;
set Tr1 = the Tran of tfsm1;
set Of1 = the OFun of tfsm1;
set Stfsm2 = the carrier of tfsm2;
set Tr2 = the Tran of tfsm2;
set Of2 = the OFun of tfsm2;
set Sfsm1 = [:{0 },the carrier of tfsm1:];
set Sfsm2 = [:{1},the carrier of tfsm2:];
deffunc H₁( Element of [:{0 },the carrier of tfsm1:], Element of IAlph) -> Element of [:{0 },the carrier of tfsm1:] = [($1 `1 ),(the Tran of tfsm1 . [($1 `2 ),$2])];
consider T1 being Function of [:[:{0 },the carrier of tfsm1:],IAlph:],[:{0 },the carrier of tfsm1:] such that
A1: for q being Element of [:{0 },the carrier of tfsm1:]
for s being Element of IAlph holds T1 . q,s = H₁(q,s) from BINOP_1:sch 4();
deffunc H₂( Element of [:{0 },the carrier of tfsm1:], Element of IAlph) -> Element of OAlph = the OFun of tfsm1 . [($1 `2 ),$2];
consider O1 being Function of [:[:{0 },the carrier of tfsm1:],IAlph:],OAlph such that
A2: for q being Element of [:{0 },the carrier of tfsm1:]
for s being Element of IAlph holds O1 . q,s = H₂(q,s) from BINOP_1:sch 4();
deffunc H₃( Element of [:{1},the carrier of tfsm2:], Element of IAlph) -> Element of [:{1},the carrier of tfsm2:] = [($1 `1 ),(the Tran of tfsm2 . [($1 `2 ),$2])];
consider T2 being Function of [:[:{1},the carrier of tfsm2:],IAlph:],[:{1},the carrier of tfsm2:] such that
A3: for q being Element of [:{1},the carrier of tfsm2:]
for s being Element of IAlph holds T2 . q,s = H₃(q,s) from BINOP_1:sch 4();
deffunc H₄( Element of [:{1},the carrier of tfsm2:], Element of IAlph) -> Element of OAlph = the OFun of tfsm2 . [($1 `2 ),$2];
consider O2 being Function of [:[:{1},the carrier of tfsm2:],IAlph:],OAlph such that
A4: for q being Element of [:{1},the carrier of tfsm2:]
for s being Element of IAlph holds O2 . q,s = H₄(q,s) from BINOP_1:sch 4();
set z = 0 ;
set zz = 1;
set A = {0 };
set B = {1};
set sSfsm1 = [:{0 },the carrier of tfsm1:];
reconsider sT1 = T1 as Function of [:[:{0 },the carrier of tfsm1:],IAlph:],[:{0 },the carrier of tfsm1:] ;
reconsider sO1 = O1 as Function of [:[:{0 },the carrier of tfsm1:],IAlph:],OAlph ;
reconsider I1 = [0 ,the InitS of tfsm1] as Element of [:{0 },the carrier of tfsm1:] by ZFMISC_1:128;
set sI1 = I1;
take fsm1 = Mealy-FSM(# [:{0 },the carrier of tfsm1:],sT1,sO1,I1 #); :: thesis:
reconsider sSfsm2 = [:{1},the carrier of tfsm2:] as non empty finite set ;
reconsider sT2 = T2 as Function of [:sSfsm2,IAlph:],sSfsm2 ;
reconsider sO2 = O2 as Function of [:sSfsm2,IAlph:],OAlph ;
reconsider I2 = [1,the InitS of tfsm2] as Element of [:{1},the carrier of tfsm2:] by ZFMISC_1:128;
reconsider sI2 = I2 as Element of sSfsm2 ;
take fsm2 = Mealy-FSM(# sSfsm2,sT2,sO2,sI2 #); :: thesis:
A5: {0 } misses {1} by ZFMISC_1:17;
[:{0 },the carrier of tfsm1:] /\ [:{1},the carrier of tfsm2:] = [:({0 } /\ {1}),(the carrier of tfsm1 /\ the carrier of tfsm2):] by ZFMISC_1:123
.= [:{} ,(the carrier of tfsm1 /\ the carrier of tfsm2):] by A5, XBOOLE_0:def 7
.= {} by ZFMISC_1:113 ;
hence the carrier of fsm1 /\ the carrier of fsm2 = {} ; :: according to XBOOLE_0:def 7 :: thesis:
thus fsm1,tfsm1 -are_isomorphic :: thesis:

proof

deffunc H₅( set ) -> set = $1 `2 ;
consider Tf1 being Function such that
A6: ( dom Tf1 = the carrier of fsm1 & ( for q being set st q in the carrier of fsm1 holds
Tf1 . q = H₅(q) ) ) from FUNCT_1:sch 3();
A7: rng Tf1 = the carrier of tfsm1

proof

assume A8: not rng Tf1 = the carrier of tfsm1 ; :: thesis:

per cases by A8, XBOOLE_0:def 10;

suppose not rng Tf1 c= the carrier of tfsm1 ; :: thesis:

then consider q being set such that
A9: ( q in rng Tf1 & not q in the carrier of tfsm1 ) by TARSKI:def 3;
consider x being set such that
A10: ( x in dom Tf1 & q = Tf1 . x ) by A9, FUNCT_1:def 5;
reconsider x2 = x `2 as Element of the carrier of tfsm1 by A6, A10, MCART_1:10;
x2 in the carrier of tfsm1 ;
hence contradiction by A6, A9, A10; :: thesis:

end;

suppose not the carrier of tfsm1 c= rng Tf1 ; :: thesis:

then consider x being set such that
A11: ( x in the carrier of tfsm1 & not x in rng Tf1 ) by TARSKI:def 3;
0 in {0 } by TARSKI:def 1;
then A12: [0 ,x] in [:{0 },the carrier of tfsm1:] by A11, ZFMISC_1:106;
then A13: Tf1 . [0 ,x] in rng Tf1 by A6, FUNCT_1:def 5;
Tf1 . [0 ,x] = [0 ,x] `2 by A6, A12;
hence contradiction by A11, A13, MCART_1:7; :: thesis:

end;

then reconsider Tf1s = Tf1 as Function of the carrier of fsm1,the carrier of tfsm1 by A6, FUNCT_2:3;
take Tf1s ; :: according to FSM_1:def 19 :: thesis:

now

let x1, x2 be set ; :: thesis:
assume A14: ( x1 in dom Tf1 & x2 in dom Tf1 & Tf1 . x1 = Tf1 . x2 ) ; :: thesis:
then A15: ( x1 = [(x1 `1 ),(x1 `2 )] & x2 = [(x2 `1 ),(x2 `2 )] ) by A6, MCART_1:23;
A16: ( Tf1 . x1 = x1 `2 & Tf1 . x2 = x2 `2 ) by A6, A14;
A17: x1 `1 in {0 } by A6, A14, MCART_1:10;
x2 `1 in {0 } by A6, A14, MCART_1:10;
then ( x1 `1 = 0 & x2 `1 = 0 ) by A17, TARSKI:def 1;
hence x1 = x2 by A14, A15, A16; :: thesis:

end;

then ( Tf1s is one-to-one & Tf1s is onto ) by A7, FUNCT_1:def 8, FUNCT_2:def 3;
hence Tf1s is bijective ; :: thesis:
thus Tf1s . the InitS of fsm1 = I1 `2 by A6
.= the InitS of tfsm1 by MCART_1:7 ; :: thesis:

now

let q be State of fsm1; :: thesis:
let s be Element of IAlph; :: thesis:
A18: ( q `1 in {0 } & q `2 in the carrier of tfsm1 ) by MCART_1:10;
reconsider q1 = q `2 as Element of the carrier of tfsm1 by MCART_1:10;
reconsider Tq1 = the Tran of tfsm1 . [q1,s] as Element of the carrier of tfsm1 ;
A19: [(q `1 ),Tq1] in [:{0 },the carrier of tfsm1:] by A18, ZFMISC_1:106;
thus Tf1s . (the Tran of fsm1 . q,s) = Tf1s . (q `1 ),(the Tran of tfsm1 . (q `2 ),s) by A1
.= [(q `1 ),(the Tran of tfsm1 . [(q `2 ),s])] `2 by A6, A19
.= the Tran of tfsm1 . [(q `2 ),s] by MCART_1:7
.= the Tran of tfsm1 . [(Tf1s . q),s] by A6 ; :: thesis:
thus the OFun of fsm1 . q,s = the OFun of tfsm1 . (q `2 ),s by A2
.= the OFun of tfsm1 . (Tf1s . q),s by A6 ; :: thesis:

end;

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

end;

deffunc H₅( set ) -> set = $1 `2 ;
consider Tf1 being Function such that
A20: ( dom Tf1 = the carrier of fsm2 & ( for q being set st q in the carrier of fsm2 holds
Tf1 . q = H₅(q) ) ) from FUNCT_1:sch 3();
A21: rng Tf1 = the carrier of tfsm2

proof

assume A22: not rng Tf1 = the carrier of tfsm2 ; :: thesis:

per cases by A22, XBOOLE_0:def 10;

suppose not rng Tf1 c= the carrier of tfsm2 ; :: thesis:

then consider q being set such that
A23: ( q in rng Tf1 & not q in the carrier of tfsm2 ) by TARSKI:def 3;
consider x being set such that
A24: ( x in dom Tf1 & q = Tf1 . x ) by A23, FUNCT_1:def 5;
reconsider x2 = x `2 as Element of the carrier of tfsm2 by A20, A24, MCART_1:10;
x2 in the carrier of tfsm2 ;
hence contradiction by A20, A23, A24; :: thesis:

end;

suppose not the carrier of tfsm2 c= rng Tf1 ; :: thesis:

then consider x being set such that
A25: ( x in the carrier of tfsm2 & not x in rng Tf1 ) by TARSKI:def 3;
1 in {1} by TARSKI:def 1;
then A26: [1,x] in sSfsm2 by A25, ZFMISC_1:106;
then A27: Tf1 . [1,x] in rng Tf1 by A20, FUNCT_1:def 5;
Tf1 . [1,x] = [1,x] `2 by A20, A26;
hence contradiction by A25, A27, MCART_1:7; :: thesis:

end;

then reconsider Tf1s = Tf1 as Function of the carrier of fsm2,the carrier of tfsm2 by A20, FUNCT_2:3;
take Tf1s ; :: according to FSM_1:def 19 :: thesis:

now

let x1, x2 be set ; :: thesis:
assume A28: ( x1 in dom Tf1 & x2 in dom Tf1 & Tf1 . x1 = Tf1 . x2 ) ; :: thesis:
then A29: ( x1 = [(x1 `1 ),(x1 `2 )] & x2 = [(x2 `1 ),(x2 `2 )] ) by A20, MCART_1:23;
A30: ( Tf1 . x1 = x1 `2 & Tf1 . x2 = x2 `2 ) by A20, A28;
A31: x1 `1 in {1} by A20, A28, MCART_1:10;
x2 `1 in {1} by A20, A28, MCART_1:10;
then ( x1 `1 = 1 & x2 `1 = 1 ) by A31, TARSKI:def 1;
hence x1 = x2 by A28, A29, A30; :: thesis:

end;

then ( Tf1s is one-to-one & Tf1s is onto ) by A21, FUNCT_1:def 8, FUNCT_2:def 3;
hence Tf1s is bijective ; :: thesis:
thus Tf1s . the InitS of fsm2 = sI2 `2 by A20
.= the InitS of tfsm2 by MCART_1:7 ; :: thesis:

now

let q be State of fsm2; :: thesis:
let s be Element of IAlph; :: thesis:
A32: ( q `1 in {1} & q `2 in the carrier of tfsm2 ) by MCART_1:10;
reconsider q1 = q `2 as Element of the carrier of tfsm2 by MCART_1:10;
set Tq1 = the Tran of tfsm2 . [q1,s];
A33: [(q `1 ),(the Tran of tfsm2 . [q1,s])] in [:{1},the carrier of tfsm2:] by A32, ZFMISC_1:106;
thus Tf1s . (the Tran of fsm2 . q,s) = Tf1s . (q `1 ),(the Tran of tfsm2 . (q `2 ),s) by A3
.= [(q `1 ),(the Tran of tfsm2 . [(q `2 ),s])] `2 by A20, A33
.= the Tran of tfsm2 . [(q `2 ),s] by MCART_1:7
.= the Tran of tfsm2 . [(Tf1s . q),s] by A20 ; :: thesis:
thus the OFun of fsm2 . q,s = the OFun of tfsm2 . (q `2 ),s by A4
.= the OFun of tfsm2 . [(Tf1s . q),s] by A20 ; :: thesis:

end;

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