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 ad = (q,w) -admissible ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len ((q21,w) -admissible) implies ((q21,w) -admissible) . $1 = ((q,w) -admissible) . $1 );
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A4: ( 1 <= k & k <= len ((q21,w) -admissible) implies ((q21,w) -admissible) . k = ((q,w) -admissible) . k ) ; :: thesis:
assume that
1 <= k + 1 and
A5: k + 1 <= len ((q21,w) -admissible) ; :: thesis:
A6: ( k = 0 or ( 0 < k & 0 + 1 = 1 ) ) ;

hence ((q21,w) -admissible) . (k + 1) = q21 by Def2
.= ((q,w) -admissible) . (k + 1) by A2, A7, Def2 ;
:: thesis:

end;

k + 1 <= (len w) + 1 by A5, Def2;
then A9: k <= len w by XREAL_1:6;
then consider w9k being Element of IAlph, q9k, q9k1 being Element of tfsm2 such that
A10: ( w9k = w . k & q9k = ((q21,w) -admissible) . k ) and
A11: ( q9k1 = ((q21,w) -admissible) . (k + 1) & w9k -succ_of q9k = q9k1 ) by A8, Def2;
A12: ex wk being Element of IAlph ex qk, qk1 being Element of tfsm st
( wk = w . k & qk = ((q,w) -admissible) . k & qk1 = ((q,w) -admissible) . (k + 1) & wk -succ_of qk = qk1 ) by A8, A9, Def2;
len w <= (len w) + 1 by NAT_1:11;
then A13: k <= (len w) + 1 by A9, XXREAL_0:2;
dom the Tran of tfsm2 = [: the carrier of tfsm2,IAlph:] by FUNCT_2:def 1;
hence ((q21,w) -admissible) . (k + 1) = ( the Tran of tfsm1 +* the Tran of tfsm2) . [q9k,w9k] by A11, FUNCT_4:13
.= ((q,w) -admissible) . (k + 1) by A1, A4, A8, A10, A12, A13, Def2, Def24 ;
:: thesis:

end;