let IAlph, OAlph be non empty set ; :: thesis: for w1, w2 being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q11, q12 being State of tfsm1
for q21, q22 being State of tfsm2 st q11,w1 -leads_to q12 & q21,w1 -leads_to q22 & q12,w2 -response <> q22,w2 -response holds
q11,(w1 ^ w2) -response <> q21,(w1 ^ w2) -response
let w1, w2 be FinSequence of IAlph; :: thesis: for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q11, q12 being State of tfsm1
for q21, q22 being State of tfsm2 st q11,w1 -leads_to q12 & q21,w1 -leads_to q22 & q12,w2 -response <> q22,w2 -response holds
q11,(w1 ^ w2) -response <> q21,(w1 ^ w2) -response
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for q11, q12 being State of tfsm1
for q21, q22 being State of tfsm2 st q11,w1 -leads_to q12 & q21,w1 -leads_to q22 & q12,w2 -response <> q22,w2 -response holds
q11,(w1 ^ w2) -response <> q21,(w1 ^ w2) -response
let q11, q12 be State of tfsm1; :: thesis: for q21, q22 being State of tfsm2 st q11,w1 -leads_to q12 & q21,w1 -leads_to q22 & q12,w2 -response <> q22,w2 -response holds
q11,(w1 ^ w2) -response <> q21,(w1 ^ w2) -response
let q21, q22 be State of tfsm2; :: thesis: ( q11,w1 -leads_to q12 & q21,w1 -leads_to q22 & q12,w2 -response <> q22,w2 -response implies q11,(w1 ^ w2) -response <> q21,(w1 ^ w2) -response )
assume A1: ( q11,w1 -leads_to q12 & q21,w1 -leads_to q22 & q12,w2 -response <> q22,w2 -response ) ; :: thesis: q11,(w1 ^ w2) -response <> q21,(w1 ^ w2) -response
assume A2: q11,(w1 ^ w2) -response = q21,(w1 ^ w2) -response ; :: thesis: contradiction
set r12 = q12,w2 -response ;
set r22 = q22,w2 -response ;
set r1w1 = q11,w1 -response ;
set r2w1 = q21,w1 -response ;
set w = w1 ^ w2;
set r11 = q11,(w1 ^ w2) -response ;
set r21 = q21,(w1 ^ w2) -response ;
A3: ( len (q21,w1 -response ) = len w1 & len (q11,w1 -response ) = len w1 ) by Def6;
A4: ( len (q12,w2 -response ) = len w2 & len (q22,w2 -response ) = len w2 ) by Def6;
then X: 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
A5: ( j in dom w2 & (q12,w2 -response ) . j <> (q22,w2 -response ) . j ) by A1, A4, FINSEQ_2:10;
A6: ( j in dom (q12,w2 -response ) & j in dom (q22,w2 -response ) ) by A4, A5, X, FINSEQ_1:def 3;
( q11,(w1 ^ w2) -response = (q11,w1 -response ) ^ (q12,w2 -response ) & q21,(w1 ^ w2) -response = (q21,w1 -response ) ^ (q22,w2 -response ) ) by A1, Th26;
then ( (q11,(w1 ^ w2) -response ) . ((len w1) + j) = (q12,w2 -response ) . j & (q21,(w1 ^ w2) -response ) . ((len w1) + j) = (q22,w2 -response ) . j ) by A3, A6, FINSEQ_1:def 7;
hence contradiction by A2, A5; :: thesis: verum