for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm = CRtfsm1 -Mealy_union CRtfsm2 holds
for Q being State of (the_reduction_of tfsm)
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm1 or not q2 in the carrier of CRtfsm1 or not q1 <> q2 )