for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty reduced connected Mealy-FSM over IAlph,OAlph
for q1u, q2u being State of tfsm
for crq21, crq22 being State of CRtfsm2 st crq21 = q1u & crq22 = q2u & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq21,crq22 -are_equivalent holds
not q1u,q2u -are_equivalent