let IAlph, OAlph be non empty set ; 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; 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; 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; 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; ( 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 that
A1:
q11,w1 -leads_to q12
and
A2:
q21,w1 -leads_to q22
and
A3:
q12,w2 -response <> q22,w2 -response
; q11,(w1 ^ w2) -response <> q21,(w1 ^ w2) -response
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
; contradiction
set r21 = q21,(w1 ^ w2) -response ;
A6:
q21,(w1 ^ w2) -response = (q21,w1 -response ) ^ (q22,w2 -response )
by A2, Th26;
set r11 = q11,(w1 ^ w2) -response ;
A7:
q11,(w1 ^ w2) -response = (q11,w1 -response ) ^ (q12,w2 -response )
by A1, Th26;
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:10;
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; verum