for IAlph, OAlph being non empty set
for w1, w2 being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM over 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