let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for cTran being Function of [:(accessibleStates tfsm),IAlph:], accessibleStates tfsm
for cOFun being Function of [:(accessibleStates tfsm),IAlph:],OAlph
for cInitS being Element of accessibleStates tfsm st cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis: for cTran being Function of [:(accessibleStates tfsm),IAlph:], accessibleStates tfsm
for cOFun being Function of [:(accessibleStates tfsm),IAlph:],OAlph
for cInitS being Element of accessibleStates tfsm st cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
set M = tfsm;
let cTran be Function of [:(accessibleStates tfsm),IAlph:], accessibleStates tfsm; :: thesis: for cOFun being Function of [:(accessibleStates tfsm),IAlph:],OAlph
for cInitS being Element of accessibleStates tfsm st cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
let cOFun be Function of [:(accessibleStates tfsm),IAlph:],OAlph; :: thesis: for cInitS being Element of accessibleStates tfsm st cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
let cInitS be Element of accessibleStates tfsm; :: thesis: ( cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm implies tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent )
assume that
A1: cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] and
A2: cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] and
A3: cInitS = the InitS of tfsm ; :: thesis: tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
set cm = Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #);
let w be FinSequence of IAlph; :: according to FSM_1:def 9 :: thesis: the InitS of tfsm,w -response = the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -response
set ma = the InitS of tfsm,w -admissible ;
set cma = the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ;

A4: now

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 X: dom (the InitS of tfsm,w -admissible ) = Seg ((len w) + 1) by FINSEQ_1:def 3;
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 );
A5: S₁[ 0 ] by X, FINSEQ_1:3;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A7: ( 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]
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 ( 1 <= j + 1 & j + 1 <= (len w) + 1 ) by X, FINSEQ_1:3;
then A8: ( j <= len w & j < (len w) + 1 ) by NAT_1:13, XREAL_1:8;
A9: ( 0 = j or ( 0 < j & 0 + 1 = 1 ) ) ;

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

suppose A10: 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 A3, A10, Def2 ;
:: thesis: verum

end;

suppose A11: 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 consider mwj being Element of IAlph, mqj, mqj1 being State of tfsm such that
A12: ( 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 ) by A8, Def2;
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 A8, A11, 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 A1, A7, A8, A11, A12, X, FINSEQ_1:3, FUNCT_1:72; :: thesis: verum

end;

end;

end;

thus for j being Nat holds S₁[j] from NAT_1:sch 2(A5, A6); :: thesis: verum

end;

then A13: the InitS of tfsm,w -admissible = the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible by FINSEQ_2:10;
set mr = the InitS of tfsm,w -response ;
set cmr = the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -response ;

now

thus ( len (the InitS of tfsm,w -response ) = len w & len (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),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 Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -response ) . j
then X: 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 Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -response ) . j )
assume A14: j in dom (the InitS of tfsm,w -response ) ; :: thesis: (the InitS of tfsm,w -response ) . j = (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -response ) . j
then A15: j in dom w by X, FINSEQ_1:def 3;
A16: j in Seg ((len w) + 1) by A14, X, FINSEQ_2:9;
then j in dom (the InitS of tfsm,w -admissible ) by A4, FINSEQ_1:def 3;
then A17: ( (the InitS of tfsm,w -admissible ) . j in the carrier of tfsm & w . j in IAlph ) by A15, FINSEQ_2:13;
j in dom (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) by A4, A16, FINSEQ_1:def 3;
then (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . j in accessibleStates tfsm by FINSEQ_2:13;
then A18: [((the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . j),(w . j)] in [:(accessibleStates tfsm),IAlph:] by A17, ZFMISC_1:106;
thus (the InitS of tfsm,w -response ) . j = the OFun of tfsm . [((the InitS of tfsm,w -admissible ) . j),(w . j)] by A15, Def6
.= cOFun . [((the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ) . j),(w . j)] by A2, A13, A18, FUNCT_1:72
.= (the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -response ) . j by A15, Def6 ; :: thesis: verum

end;

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