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 q11 being State of tfsm1
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
q11,w -response = q,w -response
let w be FinSequence of IAlph; :: thesis: for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q11 being State of tfsm1
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
q11,w -response = q,w -response
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for q11 being State of tfsm1
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
q11,w -response = q,w -response
let q11 be State of tfsm1; :: thesis: for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
q11,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 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
q11,w -response = q,w -response
let q be State of tfsm; :: thesis: ( tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q implies q11,w -response = q,w -response )
set q1 = q11;
assume that
A1: tfsm = tfsm1 -Mealy_union tfsm2 and
A2: the carrier of tfsm1 misses the carrier of tfsm2 and
A3: q11 = q ; :: thesis: q11,w -response = q,w -response
set ad1 = q11,w -admissible ;
set res = q,w -response ;
set res1 = q11,w -response ;
A4: len (q11,w -response ) = len w by Def6;

A5: now

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

end;

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