let IAlph, OAlph be non empty set ; :: thesis: for sfsm being non empty finite Moore-FSM over IAlph,OAlph ex tfsm being non empty finite Mealy-FSM over IAlph,OAlph st tfsm is_similar_to sfsm
let sfsm be non empty finite Moore-FSM over IAlph,OAlph; :: thesis: ex tfsm being non empty finite Mealy-FSM over 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₁[ 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 Nat st S₁[i] holds
S₁[i + 1]

proof

let i be 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:1;

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

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:1; :: thesis: verum

end;

end;

end;

A9: S₁[ 0 ] by FINSEQ_1:1;
A10: for i being Nat holds S₁[i] from NAT_1:sch 2(A9, A2);

now :: thesis: ( len (<*( the OFun of sfsm . the InitS of sfsm)*> ^ (( the InitS of tfsm,tw) -response)) = (len tw) + 1 & 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)) . i = (( the InitS of sfsm,tw) -response) . i ) )

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:22
.= 1 + (len (( the InitS of tfsm,tw) -response)) by FINSEQ_1:40
.= (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:1;
A14: i <= (len tw) + 1 by A11, A12, FINSEQ_1:1;

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:2, TARSKI:def 1;
then i in dom <*( the OFun of sfsm . the InitS of sfsm)*> by FINSEQ_1:38;
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
.= (( the InitS of sfsm,tw) -response) . i by A15, Th10 ;
:: 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:51;
A18: i = j + 1 by A16;
then A19: j <= len tw by A14, XREAL_1:6;
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:1;
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:1;
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:40, 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:9; :: thesis: verum