let OAlph, IAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM of IAlph,OAlph ex Ctfsm being non empty finite connected Mealy-FSM of IAlph,OAlph st
( the Tran of Ctfsm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & the OFun of Ctfsm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of Ctfsm = the InitS of tfsm & tfsm,Ctfsm -are_equivalent )
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis: ex Ctfsm being non empty finite connected Mealy-FSM of IAlph,OAlph st
( the Tran of Ctfsm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & the OFun of Ctfsm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of Ctfsm = the InitS of tfsm & tfsm,Ctfsm -are_equivalent )
set M = tfsm;
set I = the InitS of tfsm;
accessibleStates tfsm c= the carrier of tfsm by Th67;
then [:(accessibleStates tfsm),IAlph:] c= [:the carrier of tfsm,IAlph:] by ZFMISC_1:119;
then reconsider cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] as Function of [:(accessibleStates tfsm),IAlph:],OAlph by FUNCT_2:38;
the InitS of tfsm, <*> IAlph -leads_to the InitS of tfsm by Th17;
then the InitS of tfsm is accessible by Def21;
then reconsider cInitS = the InitS of tfsm as Element of accessibleStates tfsm by Th67;
reconsider cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] as Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm) by Th68;
set cm = Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #);

A1: now

let w be FinSequence of IAlph; :: thesis: the InitS of tfsm,w -admissible = the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible
set ma = the InitS of tfsm,w -admissible ;
set cma = the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ;

now

defpred S₁[ Nat] means ( $1 in dom (the InitS of tfsm,w -admissible ) implies (the InitS of tfsm,w -admissible ) . $1 = (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . $1 );
thus ( len (the InitS of tfsm,w -admissible ) = (len w) + 1 & len (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) = (len w) + 1 ) by Def2; :: thesis: for j being Nat holds S₁[j]
then A2: dom (the InitS of tfsm,w -admissible ) = Seg ((len w) + 1) by FINSEQ_1:def 3;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A4: ( j in dom (the InitS of tfsm,w -admissible ) implies (the InitS of tfsm,w -admissible ) . j = (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . j ) ; :: thesis: S₁[j + 1]
A5: ( 0 = j or ( 0 < j & 0 + 1 = 1 ) ) ;
assume j + 1 in dom (the InitS of tfsm,w -admissible ) ; :: thesis: (the InitS of tfsm,w -admissible ) . (j + 1) = (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . (j + 1)
then A6: j + 1 <= (len w) + 1 by A2, FINSEQ_1:3;
then A7: j <= len w by XREAL_1:8;
A8: j < (len w) + 1 by A6, NAT_1:13;

per cases ( 0 = j or 1 <= j ) by A5, NAT_1:13;

suppose A9: 0 = j ; :: thesis: (the InitS of tfsm,w -admissible ) . (j + 1) = (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . (j + 1)

hence (the InitS of tfsm,w -admissible ) . (j + 1) = the InitS of tfsm by Def2
.= (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . (j + 1) by A9, Def2 ;
:: thesis: verum

end;

suppose A10: 1 <= j ; :: thesis: (the InitS of tfsm,w -admissible ) . (j + 1) = (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . (j + 1)

then ( ex mwj being Element of IAlph ex mqj, mqj1 being State of tfsm st
( mwj = w . j & mqj = (the InitS of tfsm,w -admissible ) . j & mqj1 = (the InitS of tfsm,w -admissible ) . (j + 1) & mwj -succ_of mqj = mqj1 ) & ex cmwj being Element of IAlph ex cmqj, cmqj1 being State of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) st
( cmwj = w . j & cmqj = (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . j & cmqj1 = (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . (j + 1) & cmwj -succ_of cmqj = cmqj1 ) ) by A7, Def2;
hence (the InitS of tfsm,w -admissible ) . (j + 1) = (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . (j + 1) by A2, A4, A8, A10, FINSEQ_1:3, FUNCT_1:72; :: thesis: verum

end;

end;

end;

A11: S₁[ 0 ] by A2, FINSEQ_1:3;
thus for j being Nat holds S₁[j] from NAT_1:sch 2(A11, A3); :: thesis: verum

end;

hence the InitS of tfsm,w -admissible = the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible by FINSEQ_2:10; :: thesis: verum

end;

now

let q be State of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #); :: thesis: q is accessible
( q in accessibleStates tfsm & accessibleStates tfsm c= the carrier of tfsm ) by Th67;
then reconsider q9 = q as State of tfsm ;
q9 is accessible by Th67;
then consider w being FinSequence of IAlph such that
A12: the InitS of tfsm,w -leads_to q9 by Def21;
(the InitS of tfsm,w -admissible ) . ((len w) + 1) = q9 by A12, Def3;
then (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . ((len w) + 1) = q by A1;
then the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -leads_to q by Def3;
hence q is accessible by Def21; :: thesis: verum

end;

then reconsider cm = Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) as non empty finite connected Mealy-FSM of IAlph,OAlph by Def22;
take cm ; :: thesis: ( the Tran of cm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & the OFun of cm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of cm = the InitS of tfsm & tfsm,cm -are_equivalent )
thus the Tran of cm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] ; :: thesis: ( the OFun of cm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of cm = the InitS of tfsm & tfsm,cm -are_equivalent )
thus the OFun of cm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] ; :: thesis: ( the InitS of cm = the InitS of tfsm & tfsm,cm -are_equivalent )
thus the InitS of cm = the InitS of tfsm ; :: thesis: tfsm,cm -are_equivalent
let w be FinSequence of IAlph; :: according to FSM_1:def 9 :: thesis: the InitS of tfsm,w -response = the InitS of cm,w -response
set ma = the InitS of tfsm,w -admissible ;
set cma = the InitS of cm,w -admissible ;
set mr = the InitS of tfsm,w -response ;
set cmr = the InitS of cm,w -response ;
A13: len (the InitS of cm,w -admissible ) = (len w) + 1 by Def2;

now

thus ( len (the InitS of tfsm,w -response ) = len w & len (the InitS of cm,w -response ) = len w ) by Def6; :: thesis: for j being Nat st j in dom (the InitS of tfsm,w -response ) holds
(the InitS of tfsm,w -response ) . j = (the InitS of cm,w -response ) . j
then A14: dom (the InitS of tfsm,w -response ) = Seg (len w) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in dom (the InitS of tfsm,w -response ) implies (the InitS of tfsm,w -response ) . j = (the InitS of cm,w -response ) . j )
assume A15: j in dom (the InitS of tfsm,w -response ) ; :: thesis: (the InitS of tfsm,w -response ) . j = (the InitS of cm,w -response ) . j
then A16: j in dom w by A14, FINSEQ_1:def 3;
j in Seg ((len w) + 1) by A14, A15, FINSEQ_2:9;
then j in dom (the InitS of cm,w -admissible ) by A13, FINSEQ_1:def 3;
then A17: (the InitS of cm,w -admissible ) . j in accessibleStates tfsm by FINSEQ_2:13;
w . j in IAlph by A16, FINSEQ_2:13;
then A18: [((the InitS of cm,w -admissible ) . j),(w . j)] in [:(accessibleStates tfsm),IAlph:] by A17, ZFMISC_1:106;
A19: [((the InitS of tfsm,w -admissible ) . j),(w . j)] = [((the InitS of cm,w -admissible ) . j),(w . j)] by A1;
thus (the InitS of tfsm,w -response ) . j = the OFun of tfsm . [((the InitS of tfsm,w -admissible ) . j),(w . j)] by A16, Def6
.= cOFun . [((the InitS of cm,w -admissible ) . j),(w . j)] by A19, A18, FUNCT_1:72
.= (the InitS of cm,w -response ) . j by A16, Def6 ; :: thesis: verum

end;

hence the InitS of tfsm,w -response = the InitS of cm,w -response by FINSEQ_2:10; :: thesis: verum