let IAlph, OAlph be non empty set ; :: thesis: for sfsm being non empty finite Moore-FSM of IAlph,OAlph ex tfsm being non empty finite Mealy-FSM of IAlph,OAlph st tfsm is_similar_to sfsm
let sfsm be non empty finite Moore-FSM of IAlph,OAlph; :: thesis: ex tfsm being non empty finite Mealy-FSM of IAlph,OAlph st tfsm is_similar_to sfsm
set S = the carrier of sfsm;
set T = the Tran of sfsm;
set sOF = the OFun of sfsm;
set IS = the InitS of sfsm;
deffunc H₁( Element of the carrier of sfsm, Element of IAlph) -> Element of OAlph = the OFun of sfsm . (the Tran of sfsm . [$1,$2]);
consider tOF being Function of [:the carrier of sfsm,IAlph:],OAlph such that
A1: for q being Element of the carrier of sfsm
for s being Element of IAlph holds tOF . q,s = H₁(q,s) from BINOP_1:sch 4();
take tfsm = Mealy-FSM(# the carrier of sfsm,the Tran of sfsm,tOF,the InitS of sfsm #); :: thesis: tfsm is_similar_to sfsm
let tw be FinSequence of IAlph; :: according to FSM_1:def 8 :: thesis: <*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response ) = the InitS of sfsm,tw -response
set tIS = the InitS of tfsm;
set twa = the InitS of tfsm,tw -admissible ;
set swa = the InitS of sfsm,tw -admissible ;
defpred S₁[ Element of NAT ] means ( $1 in Seg ((len tw) + 1) implies (the InitS of tfsm,tw -admissible ) . $1 = (the InitS of sfsm,tw -admissible ) . $1 );
A2: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: ( i in Seg ((len tw) + 1) implies (the InitS of tfsm,tw -admissible ) . i = (the InitS of sfsm,tw -admissible ) . i ) ; :: thesis: S₁[i + 1]
assume i + 1 in Seg ((len tw) + 1) ; :: thesis: (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1)
then A4: i + 1 <= (len tw) + 1 by FINSEQ_1:3;

per cases ( i = 0 or ( i > 0 & i <= len tw ) ) by A4, XREAL_1:8;

suppose A5: i = 0 ; :: thesis: (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1)

(the InitS of tfsm,tw -admissible ) . 1 = the InitS of tfsm by Def2;
hence (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1) by A5, Def2; :: thesis: verum

end;

suppose A6: ( i > 0 & i <= len tw ) ; :: thesis: (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1)

then A7: i <= (len tw) + 1 by NAT_1:13;
A8: ( 0 + 1 = 1 implies ( 1 <= i & i <= len tw ) ) by A6, NAT_1:13;
then ( ex twi being Element of IAlph ex tqi, tqi1 being Element of tfsm st
( twi = tw . i & tqi = (the InitS of tfsm,tw -admissible ) . i & tqi1 = (the InitS of tfsm,tw -admissible ) . (i + 1) & twi -succ_of tqi = tqi1 ) & ex swi being Element of IAlph ex sqi, sqi1 being Element of sfsm st
( swi = tw . i & sqi = (the InitS of sfsm,tw -admissible ) . i & sqi1 = (the InitS of sfsm,tw -admissible ) . (i + 1) & swi -succ_of sqi = sqi1 ) ) by Def2;
hence (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1) by A3, A8, A7, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

A9: S₁[ 0 ] by FINSEQ_1:3;
A10: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A9, A2);

now

thus len (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) = (len <*(the OFun of sfsm . the InitS of sfsm)*>) + (len (the InitS of tfsm,tw -response )) by FINSEQ_1:35
.= 1 + (len (the InitS of tfsm,tw -response )) by FINSEQ_1:57
.= (len tw) + 1 by Def6 ; :: thesis: ( len (the InitS of sfsm,tw -response ) = (len tw) + 1 & ( for i being Nat st i in dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) holds
(<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b₂ = (the InitS of sfsm,tw -response ) . b₂ ) )
then A11: dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) = Seg ((len tw) + 1) by FINSEQ_1:def 3;
thus len (the InitS of sfsm,tw -response ) = (len tw) + 1 by Def7; :: thesis: for i being Nat st i in dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) holds
(<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b₂ = (the InitS of sfsm,tw -response ) . b₂
let i be Nat; :: thesis: ( i in dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) implies (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b₁ = (the InitS of sfsm,tw -response ) . b₁ )
assume A12: i in dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) ; :: thesis: (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b₁ = (the InitS of sfsm,tw -response ) . b₁
then A13: 1 <= i by A11, FINSEQ_1:3;
A14: i <= (len tw) + 1 by A11, A12, FINSEQ_1:3;

per cases ( i = 1 or 1 < i ) by A13, XXREAL_0:1;

suppose A15: i = 1 ; :: thesis: (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b₁ = (the InitS of sfsm,tw -response ) . b₁

then i in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
then i in dom <*(the OFun of sfsm . the InitS of sfsm)*> by FINSEQ_1:55;
hence (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . i = <*(the OFun of sfsm . the InitS of sfsm)*> . i by FINSEQ_1:def 7
.= the OFun of sfsm . the InitS of sfsm by A15, FINSEQ_1:57
.= (the InitS of sfsm,tw -response ) . i by A15, Th25 ;
:: thesis: verum

end;

suppose 1 < i ; :: thesis: (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b₁ = (the InitS of sfsm,tw -response ) . b₁

then consider j being Element of NAT such that
A16: j = i - 1 and
A17: 1 <= j by INT_1:78;
A18: i = j + 1 by A16;
then A19: j <= len tw by A14, XREAL_1:8;
then consider swj being Element of IAlph, swaj, swai being Element of sfsm such that
A20: ( swj = tw . j & swaj = (the InitS of sfsm,tw -admissible ) . j ) and
A21: ( swai = (the InitS of sfsm,tw -admissible ) . (j + 1) & swj -succ_of swaj = swai ) by A17, Def2;
A22: j in Seg (len tw) by A17, A19, FINSEQ_1:3;
then A23: j in dom tw by FINSEQ_1:def 3;
j <= (len tw) + 1 by A19, NAT_1:12;
then A24: j in Seg ((len tw) + 1) by A17, FINSEQ_1:3;
len (the InitS of tfsm,tw -response ) = len tw by Def6;
then ( len <*(the OFun of sfsm . the InitS of sfsm)*> = 1 & j in dom (the InitS of tfsm,tw -response ) ) by A22, FINSEQ_1:57, FINSEQ_1:def 3;
then (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . i = (the InitS of tfsm,tw -response ) . j by A18, FINSEQ_1:def 7
.= the OFun of tfsm . [((the InitS of tfsm,tw -admissible ) . j),(tw . j)] by A23, Def6
.= tOF . ((the InitS of sfsm,tw -admissible ) . j),(tw . j) by A10, A24
.= the OFun of sfsm . (the Tran of sfsm . swaj,swj) by A1, A20
.= (the InitS of sfsm,tw -response ) . i by A11, A12, A16, A21, Def7 ;
hence (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . i = (the InitS of sfsm,tw -response ) . i ; :: thesis: verum

end;

end;

end;

hence <*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response ) = the InitS of sfsm,tw -response by FINSEQ_2:10; :: thesis: verum