let IAlph, OAlph be non empty set ; :: thesis:
let w1, w2 be FinSequence of IAlph; :: thesis:
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph; :: thesis:
let q11, q12 be State of tfsm1; :: thesis:
let q21, q22 be State of tfsm2; :: thesis:
assume that
A1: q11,w1 -leads_to q12 and
A2: q21,w1 -leads_to q22 and
A3: (q12,w2) -response <> (q22,w2) -response ; :: thesis:
set r12 = (q12,w2) -response ;
set r22 = (q22,w2) -response ;
A4: len ((q22,w2) -response) = len w2 by Def6;
set w = w1 ^ w2;
set r1w1 = (q11,w1) -response ;
set r2w1 = (q21,w1) -response ;
assume A5: (q11,(w1 ^ w2)) -response = (q21,(w1 ^ w2)) -response ; :: thesis:
set r21 = (q21,(w1 ^ w2)) -response ;
A6: (q21,(w1 ^ w2)) -response = ((q21,w1) -response) ^ ((q22,w2) -response) by A2, Th11;
set r11 = (q11,(w1 ^ w2)) -response ;
A7: (q11,(w1 ^ w2)) -response = ((q11,w1) -response) ^ ((q12,w2) -response) by A1, Th11;
A8: len ((q11,w1) -response) = len w1 by Def6;
A9: len ((q12,w2) -response) = len w2 by Def6;
then A10: dom w2 = Seg (len ((q12,w2) -response)) by FINSEQ_1:def 3;
then dom w2 = dom ((q12,w2) -response) by FINSEQ_1:def 3;
then consider j being Nat such that
A11: j in dom w2 and
A12: ((q12,w2) -response) . j <> ((q22,w2) -response) . j by A3, A9, A4, FINSEQ_2:9;
A13: len ((q21,w1) -response) = len w1 by Def6;
j in dom ((q12,w2) -response) by A10, A11, FINSEQ_1:def 3;
then A14: ((q11,(w1 ^ w2)) -response) . ((len w1) + j) = ((q12,w2) -response) . j by A8, A7, FINSEQ_1:def 7;
j in dom ((q22,w2) -response) by A9, A4, A10, A11, FINSEQ_1:def 3;
hence contradiction by A5, A13, A12, A6, A14, FINSEQ_1:def 7; :: thesis: