let IAlph, OAlph be non empty set ; :: thesis:
deffunc H₁( object ) -> object = $1 `2 ;
set z = 0 ;
set zz = 1;
set A = {0};
set B = {1};
let tfsm1, tfsm2 be non empty finite Mealy-FSM over 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();
reconsider I2 = [1, the InitS of tfsm2] as Element of [:{1}, the carrier of tfsm2:] by ZFMISC_1:105;
reconsider sSfsm2 = [:{1}, the carrier of tfsm2:] as non empty finite set ;
reconsider I1 = [0, the InitS of tfsm1] as Element of [:{0}, the carrier of tfsm1:] by ZFMISC_1:105;
set sSfsm1 = [:{0}, the carrier of tfsm1:];
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();
reconsider sI2 = I2 as Element of sSfsm2 ;
set sI1 = I1;
reconsider sO1 = O1 as Function of [:[:{0}, the carrier of tfsm1:],IAlph:],OAlph ;
reconsider sT1 = T1 as Function of [:[:{0}, the carrier of tfsm1:],IAlph:],[:{0}, the carrier of tfsm1:] ;
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();
reconsider sT2 = T2 as Function of [:sSfsm2,IAlph:],sSfsm2 ;
take fsm1 = Mealy-FSM(# [:{0}, the carrier of tfsm1:],sT1,sO1,I1 #); :: thesis:
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();
A5: {0} misses {1} by ZFMISC_1:11;
reconsider sO2 = O2 as Function of [:sSfsm2,IAlph:],OAlph ;
take fsm2 = Mealy-FSM(# sSfsm2,sT2,sO2,sI2 #); :: thesis:
[:{0}, the carrier of tfsm1:] /\ [:{1}, the carrier of tfsm2:] = [:({0} /\ {1}),( the carrier of tfsm1 /\ the carrier of tfsm2):] by ZFMISC_1:100
.= [:{},( the carrier of tfsm1 /\ the carrier of tfsm2):] by A5
.= {} by ZFMISC_1:90 ;
hence the carrier of fsm1 /\ the carrier of fsm2 = {} ; :: according to XBOOLE_0:def 7 :: thesis:
thus fsm1,tfsm1 -are_isomorphic :: thesis:

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

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

per cases by A8;

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

then consider q being object such that
A9: q in rng Tf1 and
A10: not q in the carrier of tfsm1 ;
consider x being object such that
A11: x in dom Tf1 and
A12: q = Tf1 . x by A9, FUNCT_1:def 3;
reconsider x2 = x `2 as Element of the carrier of tfsm1 by A6, A11, MCART_1:10;
x2 in the carrier of tfsm1 ;
hence contradiction by A6, A10, A11, A12; :: thesis:

end;

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

then consider x being object such that
A13: x in the carrier of tfsm1 and
A14: not x in rng Tf1 ;
0 in {0} by TARSKI:def 1;
then [0,x] in [:{0}, the carrier of tfsm1:] by A13, ZFMISC_1:87;
then ( Tf1 . [0,x] in rng Tf1 & Tf1 . [0,x] = [0,x] `2 ) by A6, FUNCT_1:def 3;
hence contradiction by A14; :: thesis:

end;

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

now :: thesis:

let x1, x2 be object ; :: thesis:
assume that
A15: x1 in dom Tf1 and
A16: x2 in dom Tf1 and
A17: Tf1 . x1 = Tf1 . x2 ; :: thesis:
A18: ( Tf1 . x1 = x1 `2 & Tf1 . x2 = x2 `2 ) by A6, A15, A16;
x1 `1 in {0} by A6, A15, MCART_1:10;
then A19: x1 `1 = 0 by TARSKI:def 1;
A20: x2 `1 in {0} by A6, A16, MCART_1:10;
( x1 = [(x1 `1),(x1 `2)] & x2 = [(x2 `1),(x2 `2)] ) by A6, A15, A16, MCART_1:21;
hence x1 = x2 by A17, A18, A20, A19, TARSKI:def 1; :: thesis:

end;

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

now :: thesis:

let q be State of fsm1; :: thesis:
let s be Element of IAlph; :: thesis:
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 ;
q `1 in {0} by MCART_1:10;
then A21: [(q `1),Tq1] in [:{0}, the carrier of tfsm1:] by ZFMISC_1:87;
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, A21
.= the Tran of tfsm1 . [(q `2),s]
.= 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;

consider Tf1 being Function such that
A22: ( dom Tf1 = the carrier of fsm2 & ( for q being object st q in the carrier of fsm2 holds
Tf1 . q = H₁(q) ) ) from FUNCT_1:sch 3();
A23: rng Tf1 = the carrier of tfsm2

proof

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

per cases by A24;

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

then consider q being object such that
A25: q in rng Tf1 and
A26: not q in the carrier of tfsm2 ;
consider x being object such that
A27: x in dom Tf1 and
A28: q = Tf1 . x by A25, FUNCT_1:def 3;
reconsider x2 = x `2 as Element of the carrier of tfsm2 by A22, A27, MCART_1:10;
x2 in the carrier of tfsm2 ;
hence contradiction by A22, A26, A27, A28; :: thesis:

end;

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

then consider x being object such that
A29: x in the carrier of tfsm2 and
A30: not x in rng Tf1 ;
1 in {1} by TARSKI:def 1;
then [1,x] in sSfsm2 by A29, ZFMISC_1:87;
then ( Tf1 . [1,x] in rng Tf1 & Tf1 . [1,x] = [1,x] `2 ) by A22, FUNCT_1:def 3;
hence contradiction by A30; :: thesis:

end;

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

now :: thesis:

let x1, x2 be object ; :: thesis:
assume that
A31: x1 in dom Tf1 and
A32: x2 in dom Tf1 and
A33: Tf1 . x1 = Tf1 . x2 ; :: thesis:
A34: ( Tf1 . x1 = x1 `2 & Tf1 . x2 = x2 `2 ) by A22, A31, A32;
x1 `1 in {1} by A22, A31, MCART_1:10;
then A35: x1 `1 = 1 by TARSKI:def 1;
A36: x2 `1 in {1} by A22, A32, MCART_1:10;
( x1 = [(x1 `1),(x1 `2)] & x2 = [(x2 `1),(x2 `2)] ) by A22, A31, A32, MCART_1:21;
hence x1 = x2 by A33, A34, A36, A35, TARSKI:def 1; :: thesis:

end;

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

now :: thesis:

let q be State of fsm2; :: thesis:
let s be Element of IAlph; :: thesis:
reconsider q1 = q `2 as Element of the carrier of tfsm2 by MCART_1:10;
set Tq1 = the Tran of tfsm2 . [q1,s];
q `1 in {1} by MCART_1:10;
then A37: [(q `1),( the Tran of tfsm2 . [q1,s])] in [:{1}, the carrier of tfsm2:] by ZFMISC_1:87;
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 A22, A37
.= the Tran of tfsm2 . [(q `2),s]
.= the Tran of tfsm2 . [(Tf1s . q),s] by A22 ; :: 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 A22 ; :: 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: