let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for Rtfsm1, Rtfsm2 being non empty reduced Mealy-FSM over IAlph,OAlph st tfsm = Rtfsm1 -Mealy_union Rtfsm2 & the carrier of Rtfsm1 misses the carrier of Rtfsm2 & Rtfsm1,Rtfsm2 -are_equivalent holds
ex Q being State of (the_reduction_of tfsm) st
( the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q & Q = the InitS of (the_reduction_of tfsm) )
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: for Rtfsm1, Rtfsm2 being non empty reduced Mealy-FSM over IAlph,OAlph st tfsm = Rtfsm1 -Mealy_union Rtfsm2 & the carrier of Rtfsm1 misses the carrier of Rtfsm2 & Rtfsm1,Rtfsm2 -are_equivalent holds
ex Q being State of (the_reduction_of tfsm) st
( the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q & Q = the InitS of (the_reduction_of tfsm) )
let Rtfsm1, Rtfsm2 be non empty reduced Mealy-FSM over IAlph,OAlph; :: thesis: ( tfsm = Rtfsm1 -Mealy_union Rtfsm2 & the carrier of Rtfsm1 misses the carrier of Rtfsm2 & Rtfsm1,Rtfsm2 -are_equivalent implies ex Q being State of (the_reduction_of tfsm) st
( the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q & Q = the InitS of (the_reduction_of tfsm) ) )
set rtfsm1 = Rtfsm1;
set rtfsm2 = Rtfsm2;
assume that
A1: tfsm = Rtfsm1 -Mealy_union Rtfsm2 and
A2: the carrier of Rtfsm1 misses the carrier of Rtfsm2 and
A3: Rtfsm1,Rtfsm2 -are_equivalent ; :: thesis: ex Q being State of (the_reduction_of tfsm) st
( the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q & Q = the InitS of (the_reduction_of tfsm) )
set Srtfsm2 = the carrier of Rtfsm2;
set Stfsm = the carrier of tfsm;
set Srtfsm1 = the carrier of Rtfsm1;
the carrier of tfsm = the carrier of Rtfsm1 \/ the carrier of Rtfsm2 by A1, Def24;
then reconsider IS2 = the InitS of Rtfsm2 as Element of the carrier of tfsm by XBOOLE_0:def 3;
reconsider IS1 = the InitS of Rtfsm1 as Element of the carrier of tfsm by A1, Def24;

now :: thesis: for w being FinSequence of IAlph holds (IS1,w) -response = (IS2,w) -response

let w be FinSequence of IAlph; :: thesis: (IS1,w) -response = (IS2,w) -response
( the InitS of Rtfsm1,w) -response = ( the InitS of Rtfsm2,w) -response by A3;
hence (IS1,w) -response = ( the InitS of Rtfsm2,w) -response by A1, A2, Th53
.= (IS2,w) -response by A1, Th55 ;
:: thesis: verum

end;

then A4: IS1,IS2 -are_equivalent ;
set RUN = the_reduction_of tfsm;
the InitS of tfsm = the InitS of Rtfsm1 by A1, Def24;
then A5: the InitS of Rtfsm1 in the InitS of (the_reduction_of tfsm) by Def18;
set SRUN = the carrier of (the_reduction_of tfsm);
A6: the carrier of (the_reduction_of tfsm) = final_states_partition tfsm by Def18;
final_states_partition tfsm is final by Def15;
then consider X being Element of the carrier of (the_reduction_of tfsm) such that
A7: IS1 in X and
A8: IS2 in X by A6, A4;
take X ; :: thesis: ( the InitS of Rtfsm1 in X & the InitS of Rtfsm2 in X & X = the InitS of (the_reduction_of tfsm) )
thus ( the InitS of Rtfsm1 in X & the InitS of Rtfsm2 in X ) by A7, A8; :: thesis: X = the InitS of (the_reduction_of tfsm)
( X is Subset of the carrier of tfsm & the InitS of (the_reduction_of tfsm) is Subset of the carrier of tfsm ) by A6, TARSKI:def 3;
then ( X = the InitS of (the_reduction_of tfsm) or X misses the InitS of (the_reduction_of tfsm) ) by A6, EQREL_1:def 4;
hence X = the InitS of (the_reduction_of tfsm) by A7, A5, XBOOLE_0:3; :: thesis: verum