let IAlph, OAlph be non empty set ; :: thesis: 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 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 CRtfsm2 or not q2 in the carrier of CRtfsm2 or not q1 <> q2 )
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph st 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 CRtfsm2 or not q2 in the carrier of CRtfsm2 or not q1 <> q2 )
let CRtfsm1, CRtfsm2 be non empty finite reduced connected Mealy-FSM over IAlph,OAlph; :: thesis: ( tfsm = CRtfsm1 -Mealy_union CRtfsm2 implies for Q being State of (the_reduction_of tfsm)
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm2 or not q2 in the carrier of CRtfsm2 or not q1 <> q2 ) )
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
set rtfsm = the_reduction_of tfsm;
consider tfsm2 being non empty finite Mealy-FSM over IAlph,OAlph such that
A1: CRtfsm2, the_reduction_of tfsm2 -are_isomorphic by Th47;
set tfsm2r = the_reduction_of tfsm2;
consider Tf being Function of the carrier of CRtfsm2, the carrier of (the_reduction_of tfsm2) such that
A2: Tf is bijective and
Tf . the InitS of CRtfsm2 = the InitS of (the_reduction_of tfsm2) and
A3: for q being State of CRtfsm2
for s being Element of IAlph holds
( Tf . ( the Tran of CRtfsm2 . (q,s)) = the Tran of (the_reduction_of tfsm2) . ((Tf . q),s) & the OFun of CRtfsm2 . (q,s) = the OFun of (the_reduction_of tfsm2) . ((Tf . q),s) ) by A1;
assume A4: tfsm = CRtfsm1 -Mealy_union CRtfsm2 ; :: thesis: for Q being State of (the_reduction_of tfsm)
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm2 or not q2 in the carrier of CRtfsm2 or not q1 <> q2 )
then A5: the carrier of tfsm = the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by Def24;
given Q being Element of (the_reduction_of tfsm), q1, q2 being Element of Q such that A6: q1 in the carrier of CRtfsm2 and
A7: q2 in the carrier of CRtfsm2 and
A8: q1 <> q2 ; :: thesis: contradiction
A9: dom Tf = the carrier of CRtfsm2 by FUNCT_2:def 1;
then A10: Tf . q1 <> Tf . q2 by A6, A7, A8, A2, FUNCT_1:def 4;
rng Tf = the carrier of (the_reduction_of tfsm2) by A2, FUNCT_2:def 3;
then reconsider Tq1 = Tf . q1, Tq2 = Tf . q2 as Element of (the_reduction_of tfsm2) by A6, A7, A9, FUNCT_1:def 3;
reconsider q2 = q2 as Element of tfsm by A7, A5, XBOOLE_0:def 3;
reconsider q29 = q2 as Element of CRtfsm2 by A7;
reconsider q1 = q1 as Element of tfsm by A6, A5, XBOOLE_0:def 3;
reconsider q19 = q1 as Element of CRtfsm2 by A6;
not Tq1,Tq2 -are_equivalent by A10, Th45;
then A11: not q19,q29 -are_equivalent by A3, Th44;
A12: the carrier of (the_reduction_of tfsm) = final_states_partition tfsm by Def18;
then reconsider Q = Q as Subset of tfsm by TARSKI:def 3;
A13: final_states_partition tfsm is final by Def15;
q1,q2 -are_equivalent by A13, A12;
hence contradiction by A4, A11, Th58; :: thesis: verum