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 q21 be State of tfsm2; :: thesis:
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis:
let q be State of tfsm; :: thesis:
set q9 = q21;
assume that
A1: tfsm = tfsm1 -Mealy_union tfsm2 and
A2: q21 = q ; :: thesis:
set ad9 = (q21,w) -admissible ;
set res = (q,w) -response ;
set res9 = (q21,w) -response ;
A3: len ((q21,w) -response) = len w by Def6;

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

end;