let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM of 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)
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 )
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis: for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM of 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)
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 )
let CRtfsm1, CRtfsm2 be non empty finite reduced connected Mealy-FSM of IAlph,OAlph; :: thesis: ( the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent & 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 CRtfsm1 or not q2 in the carrier of CRtfsm1 or not q1 <> q2 ) )
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
assume A1: ( the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent & 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 CRtfsm1 or not q2 in the carrier of CRtfsm1 or not q1 <> q2 )
consider tfsm1 being non empty finite Mealy-FSM of IAlph,OAlph such that
A2: CRtfsm1, the_reduction_of tfsm1 -are_isomorphic by Th65;
given Q being Element of (the_reduction_of tfsm), q1, q2 being Element of Q such that A3: ( q1 in the carrier of CRtfsm1 & q2 in the carrier of CRtfsm1 & q1 <> q2 ) ; :: thesis: contradiction
set tfsm1r = the_reduction_of tfsm1;
consider Tf being Function of the carrier of CRtfsm1,the carrier of (the_reduction_of tfsm1) such that
A4: ( Tf is bijective & Tf . the InitS of CRtfsm1 = the InitS of (the_reduction_of tfsm1) & ( for q being State of CRtfsm1
for s being Element of IAlph holds
( Tf . (the Tran of CRtfsm1 . q,s) = the Tran of (the_reduction_of tfsm1) . (Tf . q),s & the OFun of CRtfsm1 . q,s = the OFun of (the_reduction_of tfsm1) . (Tf . q),s ) ) ) by A2, Def19;
( Tf is one-to-one & Tf is onto ) by A4;
then A5: ( Tf is one-to-one & rng Tf = the carrier of (the_reduction_of tfsm1) ) by FUNCT_2:def 3;
A6: dom Tf = the carrier of CRtfsm1 by FUNCT_2:def 1;
then A7: ( Tf . q1 in the carrier of (the_reduction_of tfsm1) & Tf . q2 in the carrier of (the_reduction_of tfsm1) & Tf . q1 <> Tf . q2 ) by A3, A5, FUNCT_1:def 5, FUNCT_1:def 8;
reconsider Tq1 = Tf . q1, Tq2 = Tf . q2 as Element of (the_reduction_of tfsm1) by A3, A5, A6, FUNCT_1:def 5;
A8: not Tq1,Tq2 -are_equivalent by A7, Th62;
set rtfsm = the_reduction_of tfsm;
the carrier of tfsm = the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A1, Def24;
then reconsider q1 = q1, q2 = q2 as Element of tfsm by A3, XBOOLE_0:def 3;
A9: final_states_partition tfsm is final by Def15;
A10: 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;
Q <> {} by A10, EQREL_1:def 6;
then A11: q1,q2 -are_equivalent by A9, A10, Def14;
reconsider q1' = q1, q2' = q2 as Element of CRtfsm1 by A3;
not q1',q2' -are_equivalent by A4, A8, Th61;
hence contradiction by A1, A11, Th76; :: thesis: verum