let IAlph, OAlph be non empty set ; :: thesis:
let w be FinSequence of IAlph; :: thesis:
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph; :: thesis:
let q11 be State of tfsm1; :: thesis:
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis:
let q be State of tfsm; :: thesis:
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:
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 :: thesis:

let k be Nat; :: thesis:
A6: [: the carrier of tfsm1,IAlph:] misses [: the carrier of tfsm2,IAlph:] by A2, ZFMISC_1:104;
assume ( 1 <= k & k <= len ((q11,w) -response) ) ; :: thesis:
then A7: k in Seg (len w) by A4, FINSEQ_1:1;
then A8: k in dom w by FINSEQ_1:def 3;
k in Seg ((len w) + 1) by A7, FINSEQ_2:8;
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:11;
w . k in IAlph by A8, FINSEQ_2:11;
then [(((q11,w) -admissible) . k),(w . k)] in [: the carrier of tfsm1,IAlph:] by A9, ZFMISC_1:87;
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:11
.= ( the OFun of tfsm1 +* the OFun of tfsm2) . [(((q,w) -admissible) . k),(w . k)] by A1, A2, A3, Th52
.= 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:

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:14; :: thesis: