let IAlph, OAlph be non empty set ; :: thesis:
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis:
let Rtfsm1, Rtfsm2 be non empty reduced Mealy-FSM of IAlph,OAlph; :: thesis:
set rtfsm1 = Rtfsm1;
set rtfsm2 = Rtfsm2;
assume A1: ( tfsm = Rtfsm1 -Mealy_union Rtfsm2 & the carrier of Rtfsm1 misses the carrier of Rtfsm2 & Rtfsm1,Rtfsm2 -are_equivalent ) ; :: thesis:
set RUN = the_reduction_of tfsm;
set SRUN = the carrier of (the_reduction_of tfsm);
set Stfsm = the carrier of tfsm;
set Srtfsm1 = the carrier of Rtfsm1;
set Srtfsm2 = the carrier of Rtfsm2;
A2: the carrier of tfsm = the carrier of Rtfsm1 \/ the carrier of Rtfsm2 by A1, Def24;
reconsider IS1 = the InitS of Rtfsm1 as Element of the carrier of tfsm by A1, Def24;
reconsider IS2 = the InitS of Rtfsm2 as Element of the carrier of tfsm by A2, XBOOLE_0:def 3;
A3: the carrier of (the_reduction_of tfsm) = final_states_partition tfsm by Def18;
A4: final_states_partition tfsm is final by Def15;

let w be FinSequence of IAlph; :: thesis:
the InitS of Rtfsm1,w -response = the InitS of Rtfsm2,w -response by A1, Def9;
hence IS1,w -response = the InitS of Rtfsm2,w -response by A1, Th72
.= IS2,w -response by A1, Th74 ;
:: thesis:

end;

then IS1,IS2 -are_equivalent by Def10;
then consider X being Element of the carrier of (the_reduction_of tfsm) such that
A5: ( IS1 in X & IS2 in X ) by A3, A4, Def14;
take X ; :: thesis:
thus ( the InitS of Rtfsm1 in X & the InitS of Rtfsm2 in X ) by A5; :: thesis:
the InitS of tfsm = the InitS of Rtfsm1 by A1, Def24;
then A6: the InitS of Rtfsm1 in the InitS of (the_reduction_of tfsm) by Def18;
A7: X is Subset of the carrier of tfsm by A3, TARSKI:def 3;
the InitS of (the_reduction_of tfsm) is Subset of the carrier of tfsm by A3, TARSKI:def 3;
then ( X = the InitS of (the_reduction_of tfsm) or X misses the InitS of (the_reduction_of tfsm) ) by A3, A7, EQREL_1:def 6;
hence X = the InitS of (the_reduction_of tfsm) by A5, A6, XBOOLE_0:3; :: thesis: