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
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 cm = Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #);
set ma = the InitS of tfsm,w -admissible ;
set cma = the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -admissible ;
set mr = the InitS of tfsm,w -response ;
set cmr = the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -response ;

A4: 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 A5: dom (the InitS of tfsm,w -admissible ) = Seg ((len w) + 1) by FINSEQ_1:def 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]
A8: ( 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 A9: j + 1 <= (len w) + 1 by A5, FINSEQ_1:3;
then A10: j <= len w by XREAL_1:8;
A11: j < (len w) + 1 by A9, NAT_1:13;

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

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

end;

suppose A13: 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 A10, 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, A5, A7, A11, A13, FINSEQ_1:3, FUNCT_1:72; :: thesis: verum

end;

end;

end;

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

end;

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

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