theorem Th61: :: FSM_1:61

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 & CRtfsm1,CRtfsm2 -are_equivalent & tfsm = CRtfsm1 -Mealy_union CRtfsm2 holds
for Q being State of (the_reduction_of tfsm) ex q1, q2 being Element of Q st
( q1 in the carrier of CRtfsm1 & q2 in the carrier of CRtfsm2 & ( for q being Element of Q holds
( q = q1 or q = q2 ) ) )