let IAlph, OAlph be non empty set ; :: thesis: for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q21 being State of tfsm2
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & q21 = q holds
q21,w -response = q,w -response
let w be FinSequence of IAlph; :: thesis: for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q21 being State of tfsm2
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & q21 = q holds
q21,w -response = q,w -response
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for q21 being State of tfsm2
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & q21 = q holds
q21,w -response = q,w -response
let q21 be State of tfsm2; :: thesis: for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & q21 = q holds
q21,w -response = q,w -response
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis: for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & q21 = q holds
q21,w -response = q,w -response
let q be State of tfsm; :: thesis: ( tfsm = tfsm1 -Mealy_union tfsm2 & q21 = q implies q21,w -response = q,w -response )
set q9 = q21;
assume that
A1: tfsm = tfsm1 -Mealy_union tfsm2 and
A2: q21 = q ; :: thesis: q21,w -response = q,w -response
set ad9 = q21,w -admissible ;
set res = q,w -response ;
set res9 = q21,w -response ;
A3: len (q21,w -response ) = len w by Def6;

A4: now

let k be Nat; :: thesis: ( 1 <= k & k <= len (q21,w -response ) implies (q21,w -response ) . k = (q,w -response ) . k )
assume ( 1 <= k & k <= len (q21,w -response ) ) ; :: thesis: (q21,w -response ) . k = (q,w -response ) . k
then A5: k in Seg (len w) by A3, FINSEQ_1:3;
then A6: k in dom w by FINSEQ_1:def 3;
k in Seg ((len w) + 1) by A5, FINSEQ_2:9;
then k in Seg (len (q21,w -admissible )) by Def2;
then k in dom (q21,w -admissible ) by FINSEQ_1:def 3;
then A7: (q21,w -admissible ) . k in the carrier of tfsm2 by FINSEQ_2:13;
( dom the OFun of tfsm2 = [:the carrier of tfsm2,IAlph:] & w . k in IAlph ) by A6, FINSEQ_2:13, FUNCT_2:def 1;
then A8: [((q21,w -admissible ) . k),(w . k)] in dom the OFun of tfsm2 by A7, ZFMISC_1:106;
(q21,w -response ) . k = the OFun of tfsm2 . [((q21,w -admissible ) . k),(w . k)] by A6, Def6
.= (the OFun of tfsm1 +* the OFun of tfsm2) . [((q21,w -admissible ) . k),(w . k)] by A8, FUNCT_4:14
.= (the OFun of tfsm1 +* the OFun of tfsm2) . [((q,w -admissible ) . k),(w . k)] by A1, A2, Th73
.= the OFun of tfsm . [((q,w -admissible ) . k),(w . k)] by A1, Def24
.= (q,w -response ) . k by A6, Def6 ;
hence (q21,w -response ) . k = (q,w -response ) . k ; :: thesis: verum

end;

len (q21,w -response ) = len w by Def6
.= len (q,w -response ) by Def6 ;
hence q21,w -response = q,w -response by A4, FINSEQ_1:18; :: thesis: verum